From Phase Semantics to Base-extension Semantics (and back)

문제점
선형 논리(Linear Logic, LL)는 다양한 의미론적 프레임워크를 필요로 하는 자원 민감적 귀결 개념을 지니고 있으며, 여기에는 위상 세만틱스(phase semantics)와 같은 대수적 모델부터 기저 확장 세만틱스(base-extension semantics, B-eS)와 같은 증명론적 접근 방식에 이르기까지 다양한 방식이 포함된다. 위상 세만틱스는 위상 공간(직교 관계를 가진 가환 모노이드) 위에서 공식을 해석하고, B-eS는 추론 규칙(기저)에 대한 귀납적 지지 관계를 통해 타당성을 정의하지만, 이 두 가지 서로 다른 프레임워크 사이의 관계는 공식적으로 확립되지 않았다. 구체적으로, 이 세만틱스들이 서로 다른 형식화(대수적 vs 추론적)에도 불구하고, 선형 귀결의 동일한 근본적 증명 행위를 포착하는지 여부는 불분명했다. 특히, 지수적 양태(! 및 ?)와 관련하여 그러했다.

방법론
본 논문은 두 영역 사이의 양방향 사상(bidirectional maps)을 체계적으로 구축함으로써 고전 선형 논리에 대한 위상 세만틱스와 B-eS 사이의 동치성을 확립한다:

1. 위상에서 기저로(Phase to Base): 위상 공간 $P$가 주어지면, 저자들은 $P$의 사실(fact) 집합에 대응하는 원자(atom)를 갖는 기저 $P_B$를 구성한다. $P_B$의 추론 규칙은 귀류법(reductio ad absurdum) 및 구조적 행위를 포함하여 위상 공간의 직교성 및 폐쇄성을 반영하도록 정의된다.
2. 기저에서 위상으로(Base to Phase): 기저 $B$가 주어지면, 저자들은 $B$의 원자들에 대한 공식의 멀티셋으로 구성된 모노이드를 갖는 위상 공간 $B_P$를 구성한다. 고정 부분집합 $\bot$은 모순을 지지하는($\Gamma \Vdash_B \bot$) 멀티셋들의 집합으로 정의된다.
3. 모피즘과 동형성(Morphisms and Isomorphism): 저자들은 기저와 위상 공간 사이의 구조 보존 사상(morphism)을 정의한다. 저자들은 두 방향의 사상의 합성이 항등 사상(또는 기저 설정에서의 "상호 지지(intersupport)"까지의 항등 사상)을 생성함을 보여줌으로써, 두 구조가 동형임을 증명한다.
4. 지수적 양태로의 확장(Extension to Exponentials): 중요한 방법론적 단계는 고전 선형 논리의 맥락에서 이전에 공식화되지 않았던, B-eS 내에서의 지수적 양태(! 및 ?)에 대한 세만틱 절(semantic clauses)을 정의하는 것이다. 이 절들은 지수적 성질(약화 및 축약)을 모사하기 위해 기저 내의 "구조적 원자(structural atoms)"를 활용한다.

주요 기여

• 동치성 증명: 본 논문의 주요 기여는 고전 선형 논리에 대해 위상 세만틱스와 기저 확장 세만틱스가 동치임을 엄밀하게 증명한 것이다. 이는 위상 공간을 기저로, 또는 그 반대로 변환할 수 있으며, 결과적으로 생성된 구조들이 동형임을 보여줌으로써 달성된다.
• 새로운 세만틱 절: 본 논문은 고전 선형 논리에서 지수적 양태(!와 ?)를 위한 최초의 공식적인 B-eS 절을 도입한다. 이 절들은 지수적 성질에 내재된 자원 관리 측면(약화 및 축약)을 처리하기 위해 구조적 원자의 개념에 의존한다.
• 대응 관계의 공식화: 본 연구는 위상 공간의 대수적 구조와 기저의 추론적 구조 사이의 관계를 공식화하며, 타당성 및 지지 관계를 보존하는 특정 모피즘을 정의한다.

결과

• 정리 25 및 29: 본 논문은 위상에서 기저로, 그리고 다시 위상으로 가는 사상의 합성이 위상 공간에 대한 항등 사상을 생성함을 증명한다. 마찬가지로, 기저에서 위상으로, 그리고 다시 기저로 가는 사상의 합성은 상호 지지(intersupport, 기저 내에서의 논리적 동치)까지의 항등 사상이 된다.
• 건전성 및 완전성: 본 논문은 선형 논리가 지수적 양태를 위한 새로 정의된 B-eS 절에 대해 건전하고 완전하다고 단언한다. 이러한 성질에 대한 증명은 부록 A에 제공되며, 구조적 원자와 지지 관계 사이의 상호작용에 의존한다.
• 보조정리 16: 위상 공간으로부터 유도된 기저에서, 원자가 구조적(structural)일 필요충분조건은 그것이 지수적 공식($! \alpha$)의 해석에 대응하는 것임을 입증한다. 이는 지수적 양태의 위상 세만틱스 내 대수적 정의와 B-eS 내 구조적 원자의 추론적 정의 사이의 간극을 메운다.

의의
본 논문은 이 동치성을 확립하는 것이 다음과 같은 여러 목적을 수행한다고 주장한다:

1. 정확성 검증: 증명에 대한 귀납(B-eS)을 통해 공식화된 세만틱스와 위상 공간에 대해 공식화된 세만틱스가 정확히 동일한 추론을 표현함을 보여줌으로써 두 프레임워크를 검증한다.
2. 결과의 전이: 한 설정(예: 위상 세만틱스에서의 결정 가능성 또는 컷 소거성 증명)에서 얻은 결과를 다른 설정(B-eS)으로 재구성하여 전달할 수 있게 한다.
3. 통합: 비교적 최근의 기저 확장 세만틱스를 선형 논리의 확립된 세만틱스 이론 내에 배치하여, 다른 표준 프레임워크와의 체계적인 비교를 가능하게 한다.
4. 범주론적 잠재력: 저자들은 정의된 모피즘이 기저와 위상 공간을 범주로 볼 수 있음을 시사하며, 이는 더 추상적인 범주론적 증명 세만틱스로의 연결을 가능하게 하는 보다 추상적인 범주론적 해석의 문을 연다.

본 논문은 동치성은 확립되었으나, 제안된 고전적 B-eS의 지수적 양태 절과 기존의 직관주의적 버전 사이에 미묘한 차이가 남아 있어 추가 조사가 필요함을 겸허히 언급하며 마무리한다. 또한, 두 세만틱스의 고전적 버전과 직관주의적 버전 사이의 구조적 유사성을 고려할 때, 유사한 동치성 결과가 직관주의 선형 논리에 대해서도 성립할 가능성이 높음을 시사한다.