Uniform Interpolation of Basic Tense Logic

기술 요약: 기본 시제 논리의 균등 보간(Uniform Interpolation)

문제 정의
본 논문은 기본 시제 논리(basic tense logic, 또는 두 방향 양상 논리 또는 역방향 양상 연산자를 포함한 양상 논리라고도 함)로 표기되는 $K_t$의 균등 보간 성질을 확립하는 미해결 문제를 다룬다. $K_t$에 대한 크레이그 보간(Craig interpolation) 성질은 증명론적 및 의미론적 방법을 통해 잘 확립되어 있으나, 균등 보간 성질—즉, 임의의 공식 $\phi$와 변수 $p$에 대하여, $\exists p.\phi$가 $p$에 독립적이며 모든 $p$-free 공식들과의 증명 가능성 관계를 보존하는 "균등 보간자" $\exists p.\phi$의 존재를 요구하는 성질—은 완전히 입증되지 않은 상태였다. 저자는 Visser(1996)가 층위적 비동형성(layered bisimulations)을 사용하여 기본 양상 논리 $K$의 균등 보간에 대한 의미론적 논거를 제공했으나, 이 결과가 역방향 양상 연산자가 포함된 시제 확장으로 확장되지 않았음을 지적한다.

방법론
본 논문은 V서의 층위적(또는 유계된) 비동형성에 기반한 모델 이론적 논거를 시제 논리 맥락으로 확장하는 의미론적 접근 방식을 채택한다. 방법론은 다음 단계들을 통해 진행된다:

1. 정의 및 프레임워크: 저자는 기본 시제 논리의 구문론과 의미론을 정의하며, 표준 힐베르트 체계 $H(K_t)$와 전방($\square$) 및 후방($\blacksquare$) 양상 연산자를 포함하는 크립키 의미론을 도입한다. 층위적 비동형성의 개념은 시제 논리에 맞게 조정되며, 양상 깊이 $n$에 의해 인덱스화된 전방($Forth$, $Back$) 및 후방($Forth^{-1}$, $Back^{-1}$) 전이 조건을 포함한다.
2. 비동형성 확장 성질: 정규 시제 논리 $\Lambda_{\mathcal{F}}$(프레임 클래스 $\mathcal{F}$와 연관된)가 균등 보간 성질을 갖기 위한 충분 조건을 공식화한다. 비동형성 확장 성질이라 명명된 이 조건은, 공유된 변수 집합 위에서 깊이 $n$까지 비동형인 임의의 두 점유 모델 $(M_1, w_1)$과 $(M_2, w_2)$가 존재할 때, 각각의 변수 집합에 대한 비동형성을 통해 두 모델을 연결하는 중간 모델 $(N, x)$가 $\mathcal{F}$ 내에 존재할 것을 요구한다.
3. 중간 모델의 구성: 핵심적인 기술적 기여는 모든 프레임의 클래스($\mathcal{F}_{all}$)가 비동형성 확장 성질을 가진다는 것을 증명하는 것이다. 저자는 두 입력 모델의 이산 합집합을 취하고 모든 상태에 연결된 새로운 "보편적" 상태 $T$를 추가함으로써 중간 모델 $N$을 구성한다. $N$에서의 관계는 원래 모델들의 상태와 "층위" 인덱스를 포함하는 곱 공간 위에서 정의되며, 이는 확장 성질을 만족시키기 위해 필요한 비동형 단계들을 효과적으로 시뮬레이션한다.
4. 전이 결과: 저자는 다음과 같은 다양한 확장에 따른 균등 보간 성질의 보존을 조사한다:
   • 거울 이미지(Mirror Images): 만약 논리 $\Lambda$가 거울 이미지 연산($\square$와 $\blacksquare$를 교체)에 대해 불변이라면, 해당 성질은 거울 이미지 공리로의 확장에 따라 전이된다.
   • 상수 공리(Constant Axioms): 성질은 상수 공식(명제 변수가 없는 공식)을 추가할 때 보존된다.
   • Boxdot 번역(Boxdot Translation): 성질은 boxdot 번역을 통해 해당 논리의 반사적 대응물로 전이됨이 보여진다.
5. 반례 구성: 성질의 한계를 보여주기 위해, 본 논문은 $S4$의 시제 확장( $S4_t$로 표기)을 분석한다. 특정 모델 구성(명제 $r$에 대해 교대하는 진릿값을 가진 무한 경로)과 층위적 비동형성 논거를 사용하여, 저자는 $S4_t$가 균등 보간 성질을 결여하고 있음을 증명한다.

주요 기여 및 결과

• 주요 정리: 본 논문은 최소 기본 시제 논리 $K_t$가 균등 보간 성질을 가짐을 확립한다. 이는 모든 프레임의 클래스가 비동형성 확장 성질을 만족함을 증명함으로써 달성된다.
• 의미론적 특징화: $K_t$에서의 균등 보간자는 **비동형성 양화사(bisimulation quantifier)**와 일치함이 입증된다. 구체적으로, 상태에서 $\exists p.\phi$가 성립한다는 것은 $\phi$가 성립하는 (즉, $p$가 다르게 해석되는) 비동형 모델이 존재한다는 것과 동치이다.
• 하위 논리로의 확장: 균등 보간 성질은 상수 공리(예: 첫 번째/마지막 순간의 존재)에 의해 정의되는 것을 포함하여 $K_t$의 다양한 확장들에 대해 성립함이 보여진다.
• $S4_t$에서의 실패: 본 논문은 $S4$의 시제 확장($S4_t$)이 균등 보간 성질을 가지지 않음을 증명한다. 이는 $S4$에 대한 Ghilardi와 Zawadowski의 초기 연구 결과를 시제 설정으로 확장하여, 반사성과 추이성 공식의 추가가 균등 보간 성질을 깨뜨린다는 것을 보여준다.
• 전이 메커니즘: 저자는 거울 이미지, 상수 확장, 그리고 boxdot 번역을 통한 균등 보간 성질의 전이에 대한 공식적인 증명을 제공하며, 이를 통해 $K_t \oplus T_\square$ 및 (특정 조건 하의) $K_t \oplus 4_\square$와 같은 논리들의 결과를 도출할 수 있게 한다.

의의
본 논문은 기본 시제 논리에 관한 문헌의 중요한 공백을 해결한다고 주장한다. V서의 의미론적 논거를 두 방향 양상 설정으로 확장함으로써, 저자는 $K_t$가 균등 보간 성질을 향유한다는 점을 확인하였는데, 이는 철학, 컴퓨터 과학, 형식 의미론에서 이 논리가 널리 사용됨에도 불구하고 이전에는 알려지지 않았던 결과이다. 이 연구는 균등한 린던 보간(Lyndon interpolation)을 갖는 논리(예: $K_t$)와 그렇지 않은 논리(예: $S4_t$) 사이의 경계를 명확히 하며, 시제 논리에서의 보간을 분석하기 위한 견고한 의미론적 프레임워크(층위적 비동형성)를 제공한다. 나아가, 본 논문은 $K_t$에서의 균등 보간자가 의미론적으로 비동형성 양화사의 시간적 버전으로 이해될 수 있음을 시사하며, 이는 해당 논리의 표현력에 대한 더 깊은 개념적 이해를 제공한다. 또한, 이 결과들은 균등 린던 보간에 대한 향후 조사와 멀티모달 및 하이브리드 시제 논리에 대한 이러한 기법의 적용을 위한 토대를 마련한다.