기술 요약: 명제 동적 논리(PDL)는 크레이그 보간법을 가진다

1. 문제 제기

본 논문은 명제 동적 논리(Propositional Dynamic Logic, PDL)가 크레이그 보간 성질(Craig Interpolation Property, CIP)을 갖는지에 대한 오랜 미해결 문제를 다룬다. CIP는 타당한 함축 $\phi \to \psi$에 대하여, $\phi \to \theta$와 $\theta \to \psi$가 타당하며, $\theta$가 $\phi$와 $\psi$에 공통으로 포함된 명제 기호 및 원자적 프로그램만을 포함하는 보간자(interpolant) $\theta$가 존재함을 의미한다.

PDL은 결정 가능성(decidability)과 완전성(completeness) 결과가 확립된 잘 알려진 양상 논리임에도 불구하고, 그 보간 성질의 상태는 수십 년 동안 불분명한 상태로 남아 있었다. 문헌에는 PDL의 보간법을 증명하려 했던 세 가지 이전 시도가 기록되어 있다:

1. Leivant (1981): 증명을 주장했으나, Kracht (1999)에 의해 잘못된 이유로 반박되었다. 다만, Leivant의 증명에는 여전히 실질적인 간극이 남아 있다.
2. Borzechowski (1988): 증명을 주장한 석사 학위 논문(Diplomarbeit)으로, 거의 주목받지 못했으며 일부로부터 검증 불가능하다는 평가를 받았다.
3. Kowalski (2002): 증명을 주장했으나 반박되었으며, 2004년에 공식적으로 철회되었다.

어려움은 PDL이 (반복 연산자 $*$로 인해) 양상 고정점 논리(modal fixpoint logic)라는 점에서 발생한다. 보간법은 순환 증명 체계(cyclic proof systems)를 사용하는 전체 $\mu$-calculus 및 그 교대 없는 파편(alternation-free fragment)에 대해서는 확립되었지만, PDL의 구체적인 제약 조건은 보간자를 특징짓는 고정점 방정식의 해가 $\mu$-calculus의 전체 표현력을 요구하는 것이 아니라, PDL 자체 내에서 표현될 수 있도록 보장하는 것을 어렵게 만든다.

2. 방법론

저자들은 순환 타블로(cyclic tableau) 체계와 마에하라(Maehara)의 증명론적 방법의 변형을 기반으로 한 구성적 증명을 제공한다.

2.1. PDL를 위한 순환 타블로 체계

저자들은 분할 시퀀트(split sequents, 쌍을 이루는 공식 집합)를 작동하는 PDL를 위한 새로운 타블로 체계를 정의한다. 주요 특징은 다음과 같다:

• 국소적 vs 양상적 추론: 시스템은 국소적 추론(단일 상태 내에서의 명제 추론 및 프로그램 전개)과 양상적 추론(크립키 모델 내에서의 상태 간 이동)을 구분한다.
• 전개 메커니즘: 각 프로그램 생성자에 대한 표준 축약 규칙 대신, 시스템은 "로딩(loading)" 메커니즘을 사용한다. $[\alpha]\psi$ 형태의 공식(여기서 $\alpha$는 비원자적임)은 "테스트 프로파일(test profiles)"에 기초하여 유한한 시퀀트 집합으로 전개된다. 이 집합 $\text{unfold}_\square(\alpha, \psi)$는 특정 테스트가 성공하거나 실패하는 모든 가능한 실행 경로의 논리합을 나타낸다.
• 반복 처리: $[\alpha^*]\psi$와 같은 공식의 무한한 국소 전개를 방지하기 위해, 시스템은 전개 과정 중에 재생된 공식의 출현을 제거한다. 이는 $[\alpha^*]\psi$가 최대 고정점(greatest fixpoint)이라는 관찰에 기초한다.
• 순환 증명(Cyclic Proofs): 시스템은 "반복(repeats)"(조상 노드와 동일한 레이블을 가진 노드)을 허용한다.
  • 로드된 경로 반복(Loaded-path repeats): 조상(동반자)으로부터 현재 노드까지의 경로가 전적으로 로드된 노드로 구성된 반복이다. 이는 공식을 만족하는 루프를 나타내는 "성공적인" 리프로 취급된다.
  • 자유 반복(Free repeats): 경로에 언로드된(unloaded) 노드가 포함된 반복이다. 이는 잠재적 반례 모델을 나타내는 "실패한" 리프로 취급된다.
• 종료(Termination): 시스템은 모든 자유 반복과 로드된 경로 반복이 리프(leaf)가 되도록 강제하고, 피셔-래드너 폐쇄(Fischer-Ladner closure)를 활용하여 공식 집합을 제한함으로써 유한성을 보장한다.

2.2. 준타블로(Quasi-tableaux)와 고정점 방정식을 통한 보간

저자들은 순환 환경에 마에하라의 방법을 적응시켜 보간자를 구성한다:

• 클러스터(Clusters): 타블로는 반복에서 동반자로 향하는 역방향 에지를 가진 그래프로 간주된다. 이 그래프의 강결합 컴포넌트(SCC)를 "클러스터"라고 부른다.
• 준타블로(Quasi-tableaux): 적절한 클러스터(단일 원소가 아닌 SCC)에 대해, 저자들은 "준타블로"를 정의한다. 이 구조는 보간자를 특징짓는 방정식 체계를 설정하는 데 사용된다.
• 사전 보간자(Pre-interpolants): 이 방법은 리프에서 루트로 향하는 귀납법을 통해 준타블로 내 노드들에 대한 사전 보간자를 정의한다.
  • 탈출 노드(Exit nodes) (클러스터의 일부가 아닌 리프): 사전 보간자는 해당 탈출 노드의 보간자(귀납에 의해 존재한다고 가정됨)이다.
  • 반복 리프(Repeat leaves): 사전 보간자는 내부 명제 변수 $q_x$이다.
  • 동伴자 노드(Companion nodes): 사전 보간자는 리프에서 루트로의 귀납을 통해 정의된다. 구체적으로, 만약 동반자 $x$가 사전 보간자 $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$를 가진 자식 $y$를 가진다면, $x$의 사전 보간자는 $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$로 정의된다.
• PDL에서의 해결: 이 핵심적인 통찰은 이러한 구성이 고정점 방정식의 해가 PDL 언어 내에 머물도록 보장한다는 것이다. $\iota_x$의 정의에서 반복 연산자 $*$를 사용하는 것은 PDL 내에서 방정식 $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$를 효과적으로 해결한다.
• 최종 보간자: 클러스터 루트의 보간자는 분할 시퀀트의 좌변의 논리합인 해당 영역 공식(region formulas)으로 루트의 내부 변수들을 치환함으로써 얻어진다.

3. 주요 기여 및 결과

• PDL에 대한 CIP 증명: 본 논문은 PDL가 크레이그 보간 성질을 가짐을 입증한다.
• 베스 정의 가능성(Beth Definability): 결론으로서, 본 논문은 (추론 정리의 존재 하에 CIP가 베스 정의 가능성을 함축하므로) PDL가 베스 정의 가능성을 가짐을 증명한다.
• 구성적 알고리즘: 증명은 구성적이다. 저자들은 닫힌 타블로로부터 보간자를 계산하는 명확한 알고리즘을 제공한다.
• 형식적 검증: 저자들은 증명을 대화형 정리 증명기인 Lean 4에서 부분적으로 정형화하였다. 논문 작성 시점에서 건전성(Soundness) 및 완전성(Completeness) 정리와 여러 지원 정리들이 검증되었다.
• 구현: 타블로 체계와 보간자 구성을 위한 Haskell 구현체가 제공되며, 웹 인터페이스를 통해 이용 가능하다.

4. 의의 및 주장

본 논문은 PDL의 보간 성질 상태에 관한 문헌의 난제를 해결하며, 이전 시도들의 간극을 극복한 최초의 검증된 증명을 제공한다고 주장한다.

• 역사적 문제의 해결: 저자들은 Borzechowski (1988)의 핵심 아이디어를 기반으로 하되, 순환 증명과 PDL 언어 내에서의 보간자 구성을 엄격하게 정형화함으로써 PDL의 보간 성질에 관한 역사적 문제를 명시적으로 다룬다.
• 방법론적 참신함: 저자들은 마에하라의 방법이 비순환 증명에는 표준적이지만, 순환 증명(고정점 논리)에 적용하려면 고정점 방정식을 풀어야 한다는 점을 강조한다. 저자들은 PDL의 경우 이러한 해가 PDL 자체의 반복 연산자를 사용하여 표현될 수 있음을 보여주며, 이는 그러한 해가 전체 $\mu$-calculus를 요구할 수 있는 다른 파편들과 구별되는 비자명한 결과이다.
• 미해결 과제: 저자들은 자신의 방법이 테스트 프로그램($\tau?$)의 존재에 의존한다는 점을 겸허히 언급한다. 따라서, 입력이 테스트가 없는 경우에도 보간자가 테스트를 포함하는 결과를 생성하므로, 테스트가 없는 PDL 파편이 보간성을 갖는지 여부는 여전히 미해결 과제로 남아 있다. 또한, 이들의 방법을 다른 PDL 변형(예: 역(converse) 또는 교집합(intersection)이 있는 경우)으로 확장하는 것과 클린 대수(Kleene Algebra with Tests, KAT)에 미치는 영향에 대해서도 열린 결말로 남겨두었다.

요약하자면, 본 논문은 새로운 순환 타블로 체계와 특화된 고정점 해결 기술을 사용하여 PDL에 대한 크레이그 보간법의 결정적이고 구성적인 증명을 제공하며, Haskell 구현체와 Lean을 통한 부분적 형식 검증으로 이를 뒷받침한다.