Four intuitionistic modal connectives

기술 요약: 네 가지 직관주의 양상 연결사

문제 제기
본 논문은 직관주의 양상 논리(IMLs)의 기초적인 의미론과 공리계화를 다룬다. 전통적으로 IML은 양상 연결사를 관계 구조 $(W, \leq, R, V)$ 내에서 해석하며, 여기서 $\leq$는 전순서(preorder)이고 $R$은 이항 관계이다. 두 가지 주요 학파 사이에는 가능성 연산자에 관한 핵심적인 긴장이 존재한다.

1. 피셔 서비(Fischer Servi)의 접근법: 가능성($\diamond_{FS}$)을 $s \models \diamond_{FS} A$ 이면 $sRt$이고$t \models A$인$t$가 존재한다로 정의한다. 이 접근법은 일반적으로 상속 성질(Heredity Property, $\leq$에 대한 단조성)을 만족시키기 위해 모델의 클래스를 "전방 및 후방 합류적(forward and backward confluent)" 프레임으로 제한해야 한다.
2. 위제세케라(Wijesekera)의 접근법: 가능성($\diamond_{W}$)을 $s \models \diamond_{W} A$ 이면 모든 $t \geq s$에 대하여 $tRu$이고$u \models A$인$u$가 존재한다로 정의한다. 이 접근법은 상속 성질을 유지하기 위해 합류성을 엄격하게 요구하지 않는다.

저자들은 논의를 합류적 모델(피셔 서비가 하는 방식)로 제한하는 것이 여러 가지 직관주의 1차 논리 중 특정 변형에 특권을 부여하는 임의적인 선택이라고 주장한다. 또한, IML을 1차 논리로의 표준 번역이 합류적 모델에만 국한될 경우 의도된 의미론을 포착하지 못하는 경우가 많다는 점을 지적한다. 따라서 본 논문은 모든 프레임의 범위를 사전에 제한하지 않고 네 가지 뚜xt렷한 양상 연결사를 통합하는 체계를 구축함으로써, 직관주의 양상의 전체 지형을 탐구하고자 한다.

방법론
저자들은 관계 의미론, 대응 이론, 대수적 증명 체계, 그리고 모델 이론적 기법을 엄격하게 결합하여 사용한다:

1. 구문론 및 의미론:

   • 표준 직관주의 연결사($\to, \top, \bot, \lor, \land$)와 그 쌍대 함축/공함축($\leftarrow$)을 포함하는 언어를 도입한다.
   • 네 가지 양상 연산자를 다음과 같이 정의한다:
     • $\Diamond$ (Přenosil 스타일의 가능성): $s \models \Diamond A$ 이면 $\exists t \leq s, \exists u (tRu \land u \models A)$이다.
     • $\Box$ (Fischer Servi 스타일의 필연성): $s \models \Box A$ 이면 $\forall t \geq s, \forall u (tRu \to u \models A)$이다.
     • $\Diamond$ (Wijesekera 스타일의 가능성): $s \models \Diamond A$ 이면 $\forall t \geq s, \exists u (tRu \land u \models A)$이다.
     • $\blacksquare$ (쌍대 필연성): $s \models \blacksquare A$ 이면 $\exists t \leq s, \forall u (tRu \to u \models A)$이다.
   • 의미론은 (합류성 제한이 없는) 모든 프레임의 클래스 위에서 정의되며, 이 정의들에 대해 상속 성질이 모든 공식에 대해 성립함이 증명된다.

2. 대응 이론:

   • 기초적인 프레임 클래스(예: 직렬, 반사적, 대칭, 추이적, 합류적)의 양상 정의 가능성을 조사한다.
   • 부호화된 공식(signed formulas)과 추론 규칙을 사용하여 프레임 속성을 특징짓는다.
   • 특정 프레임 클래스에 대한 양상 정의 가능성 문제의 결정 불가능성을 증명하기 위해 모델 이론의 "상대화 성질(Relativization Property)"을 활용한다.

3. 공리계 및 완전성:

   • 유니폼 대입(uniform substitution)과 특정 추론 규칙(쌍대 함축 및 양상 간의 상호작용을 포함하는 규칙)에 대해 닫혀 있는 부호화된 공식 세트(양의 공식과 음의 공식)를 사용하는 힐베르트 스타일 시스템을 제시한다.
   • 네 가지 양상과 쌍대 함축 사이의 복잡한 상호작용을 처리하기 위해 "균형 잡힌 클립(balanced clips)"(소원 필터, 소원 아이디얼, 보조 공식으로 구성된 삼조항)을 사용하여 **정준 모델(Canonical Model)**을 구축한다. 이 구성은 필수적이다.
   • 최소 논리와 특정 프레임 클래스(반사적, 직렬, 전방/하향 합류적)에 대응하는 확장 논리에 대한 완전성 정리를 증명한다.

4. 결정 가능성:

   • 결정 가능성을 증명하기 위해, 최소 IML을 고전 1차 논리의 **단항 2-변수 가드ed 파편(Monadic Two-Variable Guarded Fragment)**에 임베딩한다.
   • 직관주의 공식을 가드된 1차 공식으로 매핑하는 번역 함수를 정의하여, 가드된 파편의 알려진 결정 가능성을 활용한다.

주요 기여 및 결과

• 통합 프레임워크: 본 논문은 네 가지 뚜렷한 양상 연결사($\Diamond, \Box, \Diamond, \blacksquare$)를 단일 직관주의 프레임워크에 성공적으로 통합하였으며, 이들이 모든 프레임 클래스 위에서 상호 정의 가능하지 않음을 입증하였다.
• 제거 가능성 분석: 전방 및 하향 합류적 프레임($C_{fd}$) 위에서는 네 가지 연결사가 모두 제거 가능(상호 정의 가능)함을 보여준다. 그러나 더 넓은 클래스(예: $C_{bdu}$) 위에서는 이들이 서로 구별됨을 보인다.
• 대응 결과:
  • 전방 합류적($C_f$) 및 하향 합류적($C_d$) 프레임 클래스는 양적으로 정의 가능하다.
  • 반사적($C_{ref}$), 대칭($C_{sym}$), 추이적($C_{tra}$), 유클리드($C_{Euc}$), 결정적($C_{det}$) 프레임 클래스는 모든 프레임 클래스(또는 $C_{fbdu}$와 같은 특정 하위 클래스)에 대해 양상적으로 정의 가능하지 않다.
  • 후방 합류적($C_b$) 및 상향 합류적($C_u$) 프레임은 $C_{fd}$에 대해 양상적으로 정의 가능하지 않다.
• 공리계: 최소 논리($L_{min}$)와 반사성, 직렬성, 합류성 속성에 대응하는 그 확장 논리들을 위한 완전한 공리계를 제공한다. 최소 논리는 모든 프레임의 논리임이 밝혀졌다.
• 결정 가능성: 최소 직관주의 양상 논리($L_{min}$)와 여러 확장 논리(반사적, 직렬, 합류적)의 멤버십 문제가 결정 가능함을 증립하였다. 이는 문제를 단항 2-변수 가드된 파편의 충족 가능성 문제로 환원함으로써 달성되었다.
• 정의 가능성의 결정 불가능성: 기초적인 프레임 클래스가 양상적, 양적 또는 음적으로 정의 가능한지 여부를 결정하는 결정 문제가 결정 불가능함을 증명한다.

의의 및 주장
저자들은 합류적 모델로의 임의적인 제한을 피함으로써 IML에 대해 더 자연스럽고 덜 제한적인 기초를 제공한다고 주장한다. 쌍대 함축과 네 가지 양상 연결사를 도입함으로써, 직관주의 양상의 전체 범위를 포착하는 대칭적이고 포괄적인 언어를 제공한다.

저자들은 최소 논리의 결정 가능성은 확립되었으나, 이 문제의 복잡도 클래스는 여전히 미해결 과제로 남아 있다고 겸허히 언급한다. 또한, 완전성 증명에 특정 추론 규칙($R8+$ 및 $R8-$)이 사용되었으나, 이 규칙들이 유한한 공리 집합으로 대체될 수 있는지 여부는 현재 알려지지 않았다고 강조한다. 아울러 대칭 및 추이적 프레임에 대응하는 논리의 유한 공리화 가능성과, 이 특정 설정에 여과(filtration) 기법을 적용할 수 있는지에 대한 열린 질문을 던진다.

본 연구는 전통적인 피셔 서비와 위제세케라의 이분법을 넘어, 서로 다른 직관주의 양상 의미론과 그에 대응하는 프레임 속성 사이의 상호작용을 이해하기 위한 기초적인 단계 역할을 한다.