The proof theory and semantics of second-order (intuitionistic) tense logic

기술 요약: 2차 (직관주의적) 시제 논리의 증명론 및 의미론

문제 및 동기
본 논문은 고전적 및 직관주의적 토대 모두에 대한 2차 시제 논리의 기초적 발전을 다룬다. 2차 논리는 수학 및 계산 논리의 표준적인 도구이지만, 그 메탈로지컬(metalogical) 기초, 특히 증명론과 의미론은 상당한 난제를 제기해 왔다. 직관주의 양상 논리에서의 구체적인 어려움은, 고전 논리에서처럼 박스($\Box$)를 통해 다이아몬드($\Diamond$)를 정의할 수 없기 때문에 적절한 다이아몬드 양상에 대한 공리화에 대한 합의가 부족하다는 점이다. 다양한 제안들(예: CK, IK)이 존재하지만, 이들은 종종 임의적인 공리 선택을 포함한다.

저자들은 2차 양화(second-order quantification)를 사용하는 통일된 접근 방식을 제안한다. 핵심적인 관찰은 2차 직관주의 논리에서 양의 연결사(positive connectives)가 음의 파편(negative fragment)으로부터 정의될 수 있다는 것이다. 구체적으로, 본 논문은 전방(forward) 및 후방(backward) 양상(시제 논리)이 모두 포함되어 있다면, 박스($\Box$)와 역박스($\blacksquare$)만을 사용하여 다이아몬드 양상(및 그 관련 이론)을 복구할 수 있음을 입증한다. 이는 $\Diamond A$를 $\forall X(\Box(A \to \blacksquare X) \to X)$로 정의할 수 있게 하여, 임의적인 공리화를 피하게 해준다.

방법론
저자들은 세 가지 병렬적인 2차 시제 논리 정의를 개발한다:

1. 공리적(Axiomatic): $Kt2$(고전적)와$IKt2$(직관주의적) 시스템이 정의된다. 이들은 정규 양상과 시제 쌍을 위한 인접(adjunction) 공리를 포함하는 2차 명제 논리를 확장한다. 결정적으로, 이들은 비예측적(impredicative) 정의를 허용하는 완전한 포괄 공리(comprehension axiom)를 포함한다.
2. 의미론적(Semantic): 저자들은 직관주의의 경우를 위한 (이)관계적 의미론(birelational semantics)과 고전적 경우를 위한 관계적 의미론을 도입한다. 이러한 구조들은 부분 순서(직관주의를 위함)와 접근 가능성 관계를 포함한다. 중심적인 특징은 집합의 도메인이 모든 공식의 연장(extensions)을 포함하여 포괄 공리를 모델링하도록 하는 "포괄성(comprehensiveness)" 요구이다. 또한 저자들은 "술어 구조(predicate structures)"(세계가 고전적 양상 모델인 경우)를 정의하고 이것이 이관계적 구조와 동치임을 보인다.
3. 증명론적(Proof-Theoretic): 레이블된 서구트 계산법($\ell Kt2$ 및 $\ell IKt2$)이 제안된다. 이 시스템들은 세계 레이블과 관계 원자(relational atoms)를 사용하여 의미론을 내재화한다. 직관주의의 경우, 증명 탐색 논증을 용이하게 하기 위해 중간 다중 후건(multi-succedent) 계산법($m\ell IKt2$)이 도입되며, 이것이 단일 후건 버전 위에 보존적(conservative)임이 입증된다.

핵심 기술 전략은 이 세 가지 정의가 일치함을 증명하는 것이다. 이는 공리적 증명 가능성, 의미론적 타당성, 그리고 증명론적 유도 가능성을 연결하는 "그랜드 투어(grand tours)"로 시각화된다. 완전성 증명은 비예측성을 극복하기 위해 슐테(Schütte)의 준-값(semi-valuations) 개념과 프라우츠(Prawitz)의 가능값(possible values) 개념을 응용한 증명 탐색 논증에 의존한다.

주요 기여 및 결과

• 2차 양화를 통한 다이아몬드의 정의: 본 논문은 시제 양상이 존재할 때, 다이아몬드 양상이 2차 직관주의 논리에서 $\Diamond A \iff \forall X(\Box(A \to \blacksquare X) \to X)$로 정의될 수 있음을 확립한다. 이는 임의적인 공리 선택 없이 Fischer Servi와 Simpson의 $IK$, 그리고 Ewald의 $IKt$의 이론을 복구한다.
• 건전성 및 완전성:
  • 직관주의: $IKt2$ 시스템이 포괄적인 이관계적 의미론에 대해 건전하고 완전함이 입증되었다 (주요 정리 3.3).
  • 고전적: $Kt2$ 시스템이 포괄적인 관계적 의미론에 대해 건전하고 완전함이 입증되었다 (주요 정리 3.14).
• 컷-제거성(Cut-Admissibility): 본 논문은 레이블된 서구트 계산법 $\ell Kt2$ 및 $\ell IKt2$에 대한 컷-제거성을 확립한다 (주요 정리 4.2). 이는 실패한 증명 탐색으로부터 반례 모델을 구성하는 증명 탐색 논증을 통해 달성된다.
  • 고전적 경우, 이 논증은 관계적 반례 모델을 추출하기 위해 슐테의 준-값과 프라우츠의 가능값을 응용한다.
  • 직관주의적 경우, 크립키 모델의 부분 순서를 다루기 위해 (가지(branch)가 아닌) 증명 탐색 *트리(tree)*를 구성해야 하므로 더 복잡하며, 궁극적으로 술어 모델 반례를 산출한다.
• 레이블된 증명의 공리적 건전성: 본 논문은 레이블된 증명에서 공리적 증명으로의 번역을 제공하여(정리 7.1), 동치 관계의 순환을 완성한다. 이는 레이블된 폴리트리(polytree) 서구트를 시제 공식으로 해석하고 각 추론 규칙이 공리적 시스템에서 허용 가능한 규칙에 대응함을 보여주는 과정을 포함한다.
• 고전적-직관주의적 관계: 본 논문은 괴델-젠첸 번역과 유사하게, 부정 번역(negative translation)을 통해 고전적 2차 시제 논리($Kt2$)를 직관주의 시스템($IKt2$)으로 임베딩할 수 있음을 확립한다 (정리 8.2).

의의
본 논문은 2차 시제 논리에 대한 견고하고 통일된 기초를 제공한다고 주장한다. 공리적, 의미론적, 증명론적 정의가 일치함을 보여줌으로써 선택된 최소 공리화를 검증한다. 이 연구는 임의적인 공리 없이 직관주의 설정에서 양의 양상을 정의하는 특정한 과제를 해결하며, 2차 양화의 표현력을 활용한다.

방법론은 고전적 및 직관주의적 환경 모두에 적용 가능하도록 제시되는데, 직관주의의 경우 비예측성과 크립키 모델의 구조를 다루기 위한 새로운 기술적 적응이 필요하다. 결과는 2차 시제 논리에 대한 완전한 증명론적 설명(컷-제거성을 포함한)을 제공한다는 점에서 중요하다. 이는 이전에 결여되었거나 (재귀적으로 열거 불가능한) 전체 의미론에 국한되었던 영역이다. 본 논문은 관련 연구에서 언급된 바와 같이, 지식 표현 및 인공지능 분야에서 2차 양상 논리를 채택하는 데 필요한 이론적 도구에 대한 기여를 목표로 한다.