Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

기술 요약: 자동화된 증명론적 의미론을 향하여: 3차원 K3 및 LP에 대한 추론-행위 의미론

문제 제기
논리적 추론의 자동화(예: resolution, 정리 증명기, 그리고 Rocq 및 Lean과 같은 대화형 보조 도구)는 잘 확립되어 있으나, 이러한 추론을 위한 증명론적 의미론(P-tS)의 자동 제공은 여전히 미해결 과제로 남아 있다. MUltlog와 같은 시스템들은 모델론적 진릿값으로부터 임의의 다가 논리(finitely-valued logics)를 위한 시퀀트 계산법, 타블로, 그리고 자연 연역 체계를 자동으로 생성할 수 있지만, 해당 체계 내의 연결사들에 대한 증명론적 의미 명세를 생성하는 역방향의 능력은 결여되어 있다. 증명론적 타당성(proof-theoretic validity)이나 기저 확장 의미론(base-extension semantics)과 같은 기존의 P-tS 접근 방식들은 계산법에 의존적인 경우가 많아, 서로 다른 논리(예: 고전 논리 대 직관주의 논리) 간의 연결사 의미를 비교하는 것을 방해한다. 본 논문은 연결사의 최소 추론 행위를 통해 연결사의 의미를 모델링하는 추론-행위 의미론(I-bS) 접근 방식을 MUltlog 프레임워크에 통합하여, 다가 논리를 위한 P-tS 생성을 자동화하는 것을 목표로 한다.

방법론
본 논문은 기존에 2차원 시퀀트 계산법으로 제한되었던 I-bS 프레임워크를 n차원 시퀀트 계산법으로 확장한다. 방법론은 다음 단계로 진행된다:

1. 형식적 장치: 저자는 $n$-차원 시퀀트를 공식들의 멀티셋(multisets)의 $n$-튜플로 정의한다. 이를 모델론적 진릿값에 의존하지 않고 해석하기 위해, 저자들은 다측면적(multilateralist) 해석을 채택한다. 3차원 시퀀트(특히 강한 클레이니 논리 K3 및 역설의 논리 LP를 위한)의 경우, 이는 세 가지 화행(speech acts)을 포함한다: 단언(assertion, 차원 1), 판단의 유보(suspension of judgement, 차원 2), 그리고 부정(denial, 차원 3).
2. 최소 유도 관계: 특정 논리의 구조적 특징으로부터 연결사의 의미를 격리하기 위해, 저자는 항등식($Id_3$)과 제한된 컷 규칙($Cut_2$)으로 구성된 최소 유도 관계를 정의한다. 이는 표준 계산법에서 발견되는 완전한 구조적 규칙(예: 수축 및 약화)의 "혼란스러운" 효과를 피하기 위함이다.
3. 정의 가능성 및 추론 행위: 벨냅(Belnap) 스타일의 정의를 따라, 연결사는 기저 계산법을 보수적으로 확장하고 대응하는 대상과 유일하게 상호 유도 가능할 때 정의된다. 핵심 지표는 연결사의 정의 증명 과정 중 수평적 위치(차원)와 규칙 적용을 추적하는 함수인 추론 행위($ib$)이다.
4. 의미 확장: 서로 다른 차원(예: 2D 고전 논리 대 3D 파라콘시스턴트 논리) 간의 연결사를 비교하기 위해, 본 논문은 의미 확장을 도입한다. $m$-차원 연결사가 $n$-차원 연결사의 의미를 확장한다는 것은($m > n$), 전자의 $n$-차원 파편 내에서 후자의 추론 행위가 보수적으로 보존됨을 의미한다.

주요 기여 및 결과
본 논문은 MUltlog에 의해 생성된 3차원 시퀀트 계산법을 활용하여 두 가지 3가 논리인 K3와 LP에 이 확장된 프레임워크를 적용한다.

• K3/LP를 위한 의미 절(Semantic Clauses): 저자는 최소 $\{Id_3, Cut_2\}$ 관계에 대하여 곱적(multiplicative) 버전과 가법적(additive) 버전 모두에 대한 K3 연결사의 유일성과 보수성을 증명한다. 저자는 각 연결사 버전(예: 곱적 결합 $\otimes$ 대 가법적 결합 $\sqcap$)에 대한 별개의 의미 절을 도출하며, 표준 K3 계산법이 구조적 규칙들로 인해 의미론적으로 구별되는 연결사들을 혼동시키고 있음을 입증한다.
• K3와 LP 의미의 동일성: 핵심 결과는 K3와 LP의 연결사들이 동일한 의미를 갖는다는 것이다. K3(차원 3을 지정)와 LP(차원 2와 3을 지정)는 지정된 값에서 서로 다르지만, 그들의 수직적 유도 성질과 연산 규칙은 동일하다. 결과적으로, 그들의 정의 증명에서의 추론 행위는 동일하며, 동일한 의미 절을 산출한다.
• 고전 논리의 의미 확장: 본 논문은 K3 및 LP의 3차원 연결사가 LK(2차원)의 고전적 대응물들의 의미 확장임을 보여준다. 3차원 의미 절을 1차원과 3차원으로 투영(2차원을 제거)함으로써, 도출된 규칙들은 고전적 LK 연결사의 의미 절과 구문론적으로 동일하다. 이는 K3/LP 연결사들이 고전적 의미를 변경하지 않으면서 보수적으로 확장함을 확인시켜 준다.
• 구조적 규칙 처리: 분석 결과, 최소 추론 행위를 유지하기 위해서는 문맥 제한(예: 시퀀트 구성 요소 내의 공식 수 제한)이 필요하다는 것이 밝혀졌다. 이러한 제한이 없다면, 표준 구조적 규칙(예: 수축)은 추론 행위를 변화시켜 실질적으로 연결사의 의미를 변경하게 된다.

의의 및 주장
본 논문은 I-bS를 2차원보다 높은 차원으로 확장하는 첫 번째 기초 사례 연구를 제공한다고 주장한다. 주요 의의는 다음과 같다:

1. 교차 계산법 비교: 서로 다른 차원의 논리 간에 연결사 의미를 비교할 수 있는 메커니즘을 확립하였으며, 이는 서로 다른 구조적 성질을 가진 논리들을 비교하는 데 어려움을 겪었던 기존의 P-tS 문헌의 공백을 메운다.
2. 논리적 다원주의의 검증: K3와 LP가 동일한 연결사 의미를 공유한다는 발견은, 서로 다른 지정된 값이나 타당성 조건을 가짐에도 불구하고 서로 다른 논리가 동일한 연결사 의미를 공유할 수 있다는 증명론적 관점의 논리적 다원주의를 뒷받침한다.
3. 자동화를 향한 경로: 3차원 계산법을 I-bS에 성공적으로 매핑함으로써, 본 논문은 I-bS를 MUltlog에 통합하기 위한 토대를 마련한다. 궁극적인 목표는 임의의 다가 논리에 대한 의미 절 생성을 자동화하는 것이다. 저자는 현재의 작업이 수동적인 사례 연구임을 인정하며, 임의의 $n$-차원 계산법에 대한 필요한 정의 가능성 증명을 생성하는 것이 계산적 도전 과제로 남아 있음을 언급하면서도, 이론적 프레임워크는 이제 갖추어졌다고 밝히고 있다.