Analytic Cut in Epistemic Logics with Distributed Knowledge

기술 요약: 분산 지식을 포함한 인식 논리에서의 분석적 컷(Analytic Cut)

문제 제기
다중 에이전트 인식 논리에서 분산 지식(distributed knowledge)은 그룹의 모든 구성원의 개별 지식을 외부 관찰자가 결합할 수 있을 때 그룹이 보유하게 되는 지식을 나타낸다. 의미론적으로 이는 그룹 내 에이전트들의 접근 가능성 관계(accessibility relations)를 교집합함으로써 모델링된다. K45 및 KD45와 같은 표준 양상 논리는 컷 프리(cut-free) 시퀀트 계산법을 허용하지만, 분산 지식 연산자($D_G$)의 도입은 증명론적 분석을 복잡하게 만든다. 이전 연구들은 기초 양상 논리인 K45와 KD45에 대해 컷 프리 계산법을 확립했으나, 컷 제거(cut elimination)가 S5에서 실패하며, 본 논문이 입증하듯 K45D, KD45D, S5D(K45, KD45, S5의 분산 지식 확장형)에서도 실패함을 보여준다. 구체적으로, 표준 시퀀트 계산법 $G(S5D)$와 그에 대응하는 K45D 및 KD45D의 계산법은 컷 제거를 허용하지 않는다. 본 논문은 이러한 시스템들을 위한 견고한 증명론적 프레임워크를 구축하는 문제를 다루며, 특히 분석적 컷 성질(analytic cut property, 컷 공식이 결론의 부분 공식으로 제한되는 경우)이 회복될 수 있는지 조사한다.

방법론
저자들은 Takano(2018)가 양상 논리 S5를 위해 개발한 전략을 응용한 세만틱(semantic) 접근법을 채택한다. 방법론은 다음 단계로 진행된다:

1. 시스템 정의: 본 논문은 힐베르트 체계 $H(K45D)$, $H(KD45D)$, $H(S5D)$와 그에 대응하는 겐첸 스타일(Gentzen-style) 시퀀트 계산법 $G(K45D)$, $G(KD45D)$, $G(S5D)$를 정의한다. 이 계산법들은 그룹 포함 관계와 에이전트 간의 상호작용을 다루는 특정 규칙을 포함하여 명제 기반 $LK_0$를 확장한다.
2. 컷 제거의 실패: 저자들은 비제한적 컷(unrestricted cut)을 사용할 때 세 시스템 모두에서 컷 제거가 실패함을 반례(구체적으로 $\Rightarrow D_{\{a\}}\neg D_{\{a\}}p, D_{\{a,b\}}p$ 시퀀트)를 통해 입증한다.
3. 부분 밸류에이션을 통한 세만틱 완전성: 분석적 컷 계산법 $G_a(\Lambda)$에 대해 분석적 컷 성질을 확립하기 위해, 저자들은 $\Xi$-부분 밸류에이션($\Xi$-partial valuations) 개념을 활용한다. 쌍 $(\Gamma, \Delta)$는 $\Xi$-부분 밸류에이션이다. 이는 분석적 컷 계산법 $G_a(\Lambda)$에서 유도되지 않으며, 부분 공식 집합 $\Xi$로부터의 공식들만을 포함하고, 특정 폐쇄 성질을 만족하는 것이다.
4. 정준 모델(Canonical Model) 구축: 이러한 부분 밸류에이션을 사용하여 저자들은 의사 모델(pseudo-models) $M^\Lambda_\Xi$를 구축한다. 이 모델들에서 상태(states)는 $\Xi$-부분 밸류에이션이며, 접근 가능성 관계 $R_G$는 밸류에이션 내의 $D_H$ 공식 분포에 기초하여 정의된다.
   • K45D 및 KD45D의 경우, 관계는 이행성(transitivity)과 유클리드 성질(Euclidean property)을 보장하도록 정의된다(KD45D의 경우 서열성(seriality) 포함).
   • S5D의 경우, 관계는 반사성(reflexivity), 대칭성(symmetry), 이행성을 보장하도록 정의된다.
5. 완전성 및 보간법: 저자들은 시퀀트가 의사 프레임(pseudo-frames) 클래스에서 타당하다면 분석적 컷 계산법에서 유도 가능하다는 것을 증명한다. 이 세만틱 완전성 결과는 분석적 컷 성질을 함의한다. 나아가, 저자들은 마에하라(Maehara)의 방법을 적용하여 크레이그 보간 정리(Craig interpolation theorem)를 도출하며, 이를 통해 보간물(interpolants)이 명제 변수와 에이전트 집합 모두를 준수하도록 보장한다.
6. 전역 양상(Global Modality)으로의 확장: 전역 양상 $A$(공집합 그룹의 분산 지식 $D_\emptyset$와 동일)를 포함하도록 프레임워크를 확장한다. 저자들은 의사 모델 구축에 동치 관계 $\sim_A$를 포함하도록 수정하며, 확장된 시스템 $G(K45DA)$, $G(KD45DA)$, $G(S5DA)$에 대해 분석적 컷 성질과 보간 결과가 유지됨을 증명한다.

주요 기여 및 결과

• 컷 제거의 실패: 본 논문은 $G(K45D)$, $G(KD45D)$, $G(S5D)$ 시퀀트 계산법에서 컷 제거가 실패함을 공식적으로 확립하며, 이는 $G(S5)$에서 알려진 실패를 분산 지식 맥락으로 확장한 것이다.
• 분석적 컷 성질: 주요 기여는 세 시스템 모두가 분석적 컷 성질을 만족한다는 것을 증명하는 것이다. 컷 공식을 결론의 부분 공식 집합으로 제한함으로써, 저자들은 구조적 분석에 충분한 형태의 컷 제거를 회복한다.
• 크레이그 보간 정리: 분석적 컷 성질의 결과로서, 본 논문은 K45D, KD45D, S5D에 대한 크레이그 보간 정리를 증명한다. 결정적으로, 보간물은 명제 변수와 관련된 조건뿐만 아니라 관련된 에이전트 집합에 대해서도 조건을 만족하며, 이는 분산 지식 논리에서 비교적 새로운 결과로 언급된다.
• 전역 양상 통합: 공집합 그룹(여기서 $D_\emptyset$를 전역 양상 $A$로 해석)을 허용하는 것이 분석적 컷 성질과 보간 결과를 보존함을 보여준다. 이는 의사 모델을 개별 관계의 교집합이 그룹 관계와 일치하는 표준 모델로 변환하는 "트리 언래블링(tree unraveling)" 기법을 통해 달성된다.
• 증명론적 vs 모델론적: 본 논문은 [34]의 모델론적 보간 증명과 달리, [26]의 방법론을 따라 시퀀트 계산법을 통한 증명론적 도출을 제공한다는 점에서 차별화된다.

의의
본 논문은 이러한 결과들이 분산 지식을 가진 논리가 기초 양상 논리의 "좋은" 확장임을 시사한다고 주장한다. 이는 일부 기초 양상 논의 확장이 크레이그 보간 정리를 만족하지 못하는 것과 달리, 본 연구의 시스템들(K45D, KD4D, S5D)은 증명론적 접근을 통해 이를 성공적으로 만족한다는 점에 의해 뒷받침된다. 본 연구는 분석적 컷과 세만틱 완전성 논증을 활용하여 표준 컷 제거의 한계를 극복함으로써, 분산 지식을 위한 기초적인 증명론적 프레임워크를 제공한다. 저자들은 연산자의 그룹 매개변수화로 인해 Takano의 구문론적 전략 방식의 분석적 컷 성질에 대한 구문론적 증명은 여전히 미해결 과제로 남아 있으나, 여기서 사용된 세만틱 전략이 추가적인 논리적 조사를 위한 필요한 성질들을 성공적으로 확립했음을 명시한다.