A Proof-theoretic Semantics for Intuitionistic Linear Logic

문제점
증명론적 의미론(P-tS)은 진리보다는 증명의 개념을 통해 논리적 표현에 의미를 부여하는 것을 목표로 한다. Sandqvist가 직관주의 명제 논리(IPL)를 위한 기저-확장 의미론(B-eS)을 성공적으로 구축하고, Gheorghiu, Gu, Pym이 이를 직관주의 선형 논리의 곱셈적 파편(IMLL)으로 확장했으나, 완전한 직관주의 선형 논리(ILL)를 위한 P-tS는 여전히 미지의 영역으로 남아 있었다. 주요 과제는 ILL의 부수적 성격에 있으며, 이는 일반적인 약화(weakening)와 축약(contraction)을 금지하고, 가법적 연결사(additive connectives) 및 지수적 양태(exponential modality, !)를 포함한다는 점이다. 기존의 접근 방식들은 이러한 특징들이 B-eS 프레임워크 내에서 상호작용하는 방식을 다루는 데 어려움을 겪고 있다. 구체적으로, 자원 민감한 ILL의 성격을 존중하면서도, 엄격한 도출을 요구하는 모달 연산자인 "방글(!)" 연결사의 추론적 내용을 정확하게 포착하는 지지 관계(support relation)를 정의하는 것은 상당한 난제를 제시한다. 더욱이, 표준적인 ILL 자연 연역 체계는 종종 문맥 공유(가법성) 및 전제의 변수 개수와 관련된 임시적인 부가 조건(side conditions)에 의존하는데, 이는 B-eS에서 원자적 규칙에 요구되는 비스키마적(non-schematic) 구조 내에서 정식화하기 어렵다.

방법론
본 논문은 두 가지 주요 기술적 장애물, 즉 스키마적 문맥 메타변수를 사용하지 않는 자연 연역 규칙의 정식화와 가법성 및 양태를 처리하는 지지 관계의 정의를 해결함으로써 ILL를 위한 새로운 기저-확장 의미론을 제안한다.

1. 자연 연역의 재구성: 저자는 "가법적 박스"(additive boxes, {...}로 표기)와 "양태적 박스"(modal boxes, J...K로 표기)를 사용하여 자연 연역 체계인 NILL의 새로운 구문을 도입한다.

   • 가법적 박스: 이들은 공유된 문맥을 구분하며, 이를 통해 시스템이 임의의 문맥 메타변수에 의존하지 않고도 가법적 연결사(예: & 및 ⊕)와 가변적인 전제를 가진 규칙(예: ⊤I 및 0E)을 표현할 수 있게 한다. 이를 통해 가법적 박스 내부의 도출이 동일한 열린 가정들의 멀티셋을 공유하도록 하는 가법성의 체계적인 처리가 가능해진다.
   • 양태적 박스: 이는 승격 규칙(Prom)을 특징짓기 위해 사용된다. 이 규칙은 결론이 오직 양태적 박스만을 포함하는 규칙들로부터 도출된 가정들로 구성된 문맥으로부터 따라온다는 것을 요구하도록 재정의된다. 이는 ! 연결사를 규칙의 구조적 정의에서 명시적으로 참조하지 않고도 지수적 양태의 엄격한 도출 요구사항을 포착한다.
   • 저자는 이 새로운 체계가 표준적인 서열 스타일(sequent-style) NILL와 동등함을 증명한다 (정리 2.7).

2. 원자적 도출 가능성 및 지지 관계:

   • 원자적 규칙: 의미론은 원자적 규칙을 세 개의 요소(가법적 박스의 멀티셋, 단일 가법적 박스, 그리고 하나의 원자)로 구성된 삼중쌍으로 정의한다. 이는 재구성된 자연 연역 규칙의 구조를 반영한다.
   • 기저 확장: 기저 $B$는 이러한 원자적 규칙들의 집합이다. 도출 관계 $\vdash_B$는 문맥의 곱셈적 분할과 박스 구조를 통한 가법적 공유를 처리하며 귀납적으로 정의된다.
   • 지지 관계 ($\Vdash_B^L$): 핵심적인 의미론적 정의는 지지 관계를 ILL로 확장한다. 결정적으로, 지수적 양태 !ϕ에 대한 절은 단순히 구조적 규칙으로서가 아니라, 기저 확장에 걸친 $\phi$의 타당성에 대한 조건으로 정의된다. 구체적으로, $\V_B^L !\phi$는 임의의 확장 $C$에 대하여, 만약 $\phi$가 $C$의 "정리"라면(즉, 모든 $D \supseteq C$에 대해 $\Vdash_D^\emptyset \phi$ 이면), 해당 자원을 사용할 수 있다는 것을 의미한다.
   • 양태 처리: 본 논문은 기저 내의 "지속적 원자(persistent atoms)" 개념을 도입하며, 이는 !ϕ 형태의 공식들에 대응한다. 이 원자들은 $\phi$를 지원하는 $\phi$와 $\phi$를 지원하는 !Γ 사이의 관계를 허용함으로써, 표준적인 가정과 축약이나 약화가 가능한 가정을 구분하는 역할을 수행한다.

주요 기여

• ILL를 위한 완전한 B-eS: 본 논문은 가법적 연결사와 지수적 양태를 포함한 완전한 직관주의 선법 논리(ILL)를 다루는 최초의 기저-확장 의미론을 제시한다.
• 가법성의 체계적 처리: 가법적 박스를 도입함으로써, 저자는 임의의 부가 조건이나 명시적인 문맥 메타변수 없이도 자연 연역의 문맥 공유 및 가변 전제 규칙을 처리하는 방법을 제공한다. 이는 추론 형상(inference figures)에 대한 더 깔끔하고 균일한 표현을 제공한다.
• 양태적 박스 특성화: 양태적 박스를 사용한 승격 규칙의 재정의는 특정 연결사 구문과는 독립적인 지수적 양태의 구조적 특징을 제공하여, 이를 B-eS 프레임워크에 통합하는 것을 용이하게 한다.
• !의 추론적 설명: 본 논문은 ! 연결사의 추론적 내용에 대한 상세한 논의를 제공한다. 저자는 의미론이 !를 기저 확장 전반에 걸친 기본 공식의 타당성에 대한 조건으로 취급함으로써, !의 양태적 성격을 포착하고, 결과적으로 "필연화(necessitation)" 측면을 효과적으로 내재화한다고 주장한다.
• 건전성 및 완전성: 저자는 제안된 의미론이 NILL 자연 연역 체계에 대해 건전하고 완전함을 증명한다. 완전성 증명은 원자적 규칙이 NILL의 추론 규칙을 모방하는 "시뮬레이션 기저" $N$을 구성하고, 평탄화 사상(flattening map)을 통해 ILL 공식을 원자로 변환하는 과정을 포함한다.

결과

• 정리 2.7: 표준적인 서열 스타일 도출 가능성($\vdash$)과 새로운 박스 기반 도출 가능성($\vdash^*$) 사이의 동등성을 확립한다.
• 정리 5.1 (건전성): 만약 어떤 서열이 NILL에서 증명 가능하다면, 그것은 제안된 의미론에서 유효하다 ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$)는 것을 증명한다.
• 정리 6.1 (완전성): 만약 어떤 서열이 의미론에서 유효하다면, 그것은 NILL에서 증명 가능하다 ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$)는 것을 증명한다.
• 정리 4.15: !를 가진 가설을 처리하기 위해 사용된 특정 (Inf) 절이 더 일반적인 (Gen-Inf) 절과 동등함을 입증하여, 양태적 가설의 특수한 처리를 검증한다.
• 따름정리 4.11 & 4.12: !와 지지 관계 사이의 상호작용에 관한 구조적 성질을 확립하며, $\phi$가 유효하면 !ϕ도 유효하고, !Γ가 !ϕ를 지원한다면 ϕ도 지원함을 보여준다.

의의
본 논문은 B-eS 접근 방식을 IPL 및 IMLL에서 완전한 ILL로 확장함으로써 P-tS의 중요한 공백을 메웠다고 주장한다. 저자는 Gheorghiu, Gu, Pym이 곱셈적 파편을 성공적으로 다루었지만, 가법적 요소와 지수적 양태의 추가는 상당한 새로운 기제(machinery)를 요구했다고 언급한다. 이 연구는 양태에 대한 본질적인 증명론적 접근 방식을 통해 의의를 가지며, "방글" 연결사를 단순한 구조적 규칙이 아니라 기저-확장 프레임워크 내에서 공식들의 타당성에 대한 조건으로 이해하는 방법을 제시한다. 저자는 승격 규칙과 가법성을 처리하기 위한 해결책이 "다소 복잡하다(convoluted)"는 점을 겸허히 인정하면서도, 추론 형상의 깔끔하고 체계적인 표현을 달성하기 위해 필수적이었다고 밝힌다. 또한, 본 논문은 Sandqvist의 IPL 의미론을 이 ILL 프레임워크로 직접 매핑하는 작업의 어려움을 강조하며, 두 체계 사이의 매핑 일반화 문제를 향후 연구를 위한 열린 과제로 남겨두었다. 이 연구는 P-tS에서의 현재 양태 처리 방식이 이제 막 다뤄지기 시작한 깊은 형이상학적 또는 구조적 통찰력을 필요로 할 수 있음을 시사한다.