Uniform Lyndon Interpolation via Non-wellfounded Proofs

기술 요약: 비정형적(Non-wellfounded) 증명을 통한 균등 린던 보간법(Uniform Lyndon Interpolation)

문제 정의
비정형적 증명 이론은 다양한 논리(증명 논리 포함)에 대해 크레이그 보간법(Craig interpolation), 린던 보간법(Lyndon interpolation), 그리고 균등 보간법(uniform interpolation)을 확립하는 데 성공적으로 사용되어 왔다. 그러나 이러한 속성들의 결합, 즉 **균등 린den 보간 성질(Uniform Lyndon Interpolation Property, ULIP)**은 이 연구 이전에는 비정형적 방법을 사용하여 다루어진 바 없다. 본 논문은 참인 산술(true arithmetic) 하에서의 페아노 산술의 증명 술어를 대응시키는 증명 논리 GLS(S라고도 함)에 초점을 맞춘다. GLS가 균등 보간 및 크레이그 보간을 가진다는 것은 알려져 있었으나, GLS가 균등 린던 보간(또는 비균등 린던 보간)을 허용하는지는 미해결 과제로 남아 있었다. 정형적(wellfounded) 증명 체계에서의 주요 장애물은 모달 규칙에서의 "대각선 공식(diagonal formula)"으로, 이는 린던 보간법의 요구 사항인 변수의 극성(polarity)을 보존하지 못한다는 점이다.

방법론
저자들은 정형적 증명의 한계를 극복하기 위해 **비정형적 시퀀트 계산법(non-wellfounded sequent calculi)**과 **국소적 진행 증명 이론(local progress proof theory)**을 활용한다. 이 방법론은 세 가지 핵심적인 기술적 구성 요소에 의존한다:

1. 국소적 진행 시퀀트 계산법: 저자들은 국소적 진행 시스템인 $G_{\infty}^{GLS}$ 계산법을 사용한다. 표준적인 정형적 계산법과 달리, 이 시스템의 증명은 무한한 가지를 포함할 수 있는 트리 형태이지만, 모든 무한한 가지는 반드시 무수히 많은 "진행 노드"(구체적으로는 모달 규칙 $\square K4_{sat}$의 적용)를 포함해야 한다. 이 시스템은 정형적 계산법 $G_{GLS}$에서 발견되는 대각선 공식을 제거함으로써, 증명 탐색 과정 전반에서 변수의 극성을 보존한다.
2. 보간 템플릿(Interpolation Templates): 보간자를 구성하기 위해, 저자들은 특정 집합의 포화 규칙(saturation rules)에 의해 생성된 순환적 전증명(cyclic preproofs, 백엣지(back-edge)를 가진 증명)인 "보간 템플릿"을 정의한다. 이 템플릿들은 공식을 포화 상태에 도달할 때까지 분해하는 규칙들을 적용하여 구축된다. 템플릿은 순환 증명의 반복 노드(repeat nodes)에 대응하는 유계 변수(bound variables)를 포함하는 의사 공식(pseudoformulas)인 "전보간자(preinterpolants)"로 주석이 달린다.
3. 린던 방정식 체계(Lyndon Equational Systems): 전보간자를 유효한 공식으로 해결하기 위해, 저자들은 **린던 고정점(Lyndon fixpoints)**과 린던 방정식 체계의 개념을 도입한다. 방정식 체계는 미지 변수를 양의 어휘(positive vocabulary)와 음의 어휘(negative vocabulary, 특정 극성을 가진 변수들의 집합)에 의해 제약된 공식들에 연결하는 방정식들로 구성된다. 저자들은 "단순(simple)"하고 "양의 모달화된(positive modalized)" 린던 방정식 체계가 GLS에서 가해 가능하다는 것을 증로한다. 이러한 가해성은 전보간자의 유계 변수를 극성을 준수하는 실제 공식으로 치환할 수 있게 한다.

주요 기여
본 논문은 세 가지 뚜렷한 기여를 한다:

1. 대안적 컷 제거(Alternative Cut Elimination): 정형적 계산법에서 비정형적 계산법 $G_{\infty}^{GLS}$로 증명을 번역하고 $G_{\infty}^{GLS}$에서 컷 규칙의 국소적 허용 가능성을 확립함으로써, $G_{GLS}$에 대한 새로운 컷 제거 증명을 제공한다.
2. 새로운 이론적 개념: 린던 고정점과 린던 방정식 체계를 도입한다. 이 개념들은 비정형적 증명을 통해 구축된 균등 보간자가 린던 보간법에서 요구되는 극성 제약을 준수함을 입증하는 데 필수적이다.
3. GLS의 ULIP 증명: GLS가 균등 린던 보간 성질을 가진다는 최초의 증명을 제시한다.

결과
중심 결과는 GLS가 균등 린던 보간 성질을 가진다는 정리 4.16이다. 증명 과정은 다음과 같다:

• 주어진 시퀀트에 대한 보간 템플릿을 구축한다.
• 템플릿의 반복 노드에 양의 모달화된 린던 방정식 체계를 연관시킨다.
• 솔루션 시퀀스를 얻기 위해 이 체계를 GLS에서 해결한다(정리 4.7에 의해 보장됨).
• 이 솔루션을 루트 노드의 전보간자에 대입하여 균등 린던 보간자 $\iota_T$를 생성한다.
• 보조정리 4.14와 4.15를 통해 $\iota_T$가 ULIP의 조건(지정된 양의 및 음의 어휘만을 포함하며, 호환 가능한 어휘를 가진 임의의 공식 $\psi$에 대해 보간자로 작용함)을 만족함을 검증한다.

또한, 저자들은 $G_{\infty}^{GLS}$로의 번역을 통해 $G_{GLS}$에서 컷 규칙이 제거 가능하며, $G_{\infty}^{GLS}$에서 컷 규칙이 국소적으로 허용 가능하다는 것을 확립한다.

의의 및 범위
본 논문은 비정형적 방법을 사용하여 증명 논리에 대한 균등 린던 보간에 관한 문헌의 공백을 메웠다고 주장한다. 저자들은 자신들의 방법론이 비정형적 시퀀트 계산법이 존재하는 경우 다른 증명 논리에도 적용 가능하다는 점을 언급한다. 저자들은 단항 해석 논리(unary interpretability logics), 이중 모달 증명 논리(bimodal provability logics), 그리고 직관주의 증명 논리(intuitionistic provability logics)에 적용하는 것을 포함한 향와 방향을 명시적으로 식별하였다. 또한, 단순 린던 고정점이 존재하지 않는 논리(예: 해석 논리 IL)에서도 양의 모달화된 린던 방정식 체계가 여전히 해결 가능한지 조사할 것을 제안한다. 이 연구는 모든 모달 논리에 대해 ULIP를 해결한다고 주장하는 것이 아니라, GLS에 대한 비정형적 접근법의 타당성을 입증하고 확장 가능한 프레임워크를 제시하는 것이다.