Inferentialist Game Semantics (Extended Abstract)

기술 요약: 추론주의적 게임 의미론 (Inferentialist Game Semantics)

문제 제기
본 논문은 논리학의 두 가지 서로 다른 내포적 의미론인 **게임 의미론(Game Semantics)**과 증명론적 의미론(Proof-Theoretic Semantics, P-tS) 사이의 관계를 다룬다.

• 게임 의미론(특히 Hyland-Ong 게임)은 논리적 타당성을 제안자(Proponent)와 반대자(Opponent) 사이의 역동적인 상호작용으로 해석하며, 여기서 증명은 승리 전략에 대응한다.
• 증명론적 의미론(특히 Sandqvist가 발전시킨 Base-Extension Semantics, B-eS)은 원자적 규칙들의 "기저(bases)"에서의 증명 가능성을 통해 의미를 해석하며, 논리적 타당성을 모델론적 진리가 아닌 선(先)논리적 파생 개념에 근거하여 정립한다.

두 프레임워크 모두 내포적 의미 설명을 제공하지만, 게임의 개념을 P-tS의 원형으로부터 재구성할 수 있는지는 미해결 과제였다. 즉, 게임을 외부에서 부과된 모델이 아니라 본질적으로 증명론적인 실체로 볼 수 있는가? 저자들은 직관주의 명제 논리(IPL)에 대해 B-eS와 Hyland-Ong 게임 의미론 사이의 완전 추상적 상관관계를 확립하는 것을 목표로 한다.

방법론
저자들은 두 프레임워크 사이의 간극을 메우기 위해 구성적 번역 전략을 채택한다.

1. 사전 구축 (Dictionary Construction): 이들은 Sandqvist의 B-eS의 원형과 Hyland-Ong 게임의 구성 요소 사이의 정밀한 대응 관계를 정의한다.
   • **기저(base)**의 원자적 규칙들은 아레나(arena)(루트 트리의 포레스트)에 대응한다.
   • 가정으로부터의 **논증(argument)**은 플레이(play)(움직임의 순서)에 대응한다.
   • **증명(proof)**은 **승리 전략(winning strategy)**에 대응한다.
2. 형식적 정의:
   • 원자적 아레나(Atomic Arenas): 원자를 나타내는 노드들로 이루어진 트리의 포레스트로 정의된다. 루트 노드는 제안자(P)의 주장이며, 자식 노드는 반대자(O)의 도전이다.
   • 움직임과 플레이 (Moves and Plays): 움직임은 질문(정당화 요구)과 답변(양보)으로 분류된다. 플레이는 정당화, 교대, 초기 가정의 처리에 관한 특정 구조적 제약을 만족하는 유한한 순서이다.
   • 전략 (Strategies): 전략은 반대자의 움직임으로 끝나는 플레이를 제안자의 움직임 시퀀스로 매핑하는 함수이다. 전략이 "승리"한다는 것은 모든 극대 플레이(maximal play)에서 초기 질문에 대한 제안자의 답변을 보장함을 의미한다.
3. 선언(Disjunction) 처리: 핵심적인 방법론적 단계는 선언($\lor$)의 처리를 포함한다. 저자들은 단순히 "하나의 선언항에서 승리하는" 방식의 나이브한 접근법을 거부한다. 대신, Sandqvist의 이차적 절을 채택한다: 선언은 만약 임의의 원자적 목표 $p$와 아레나의 확장(extension)에 대하여, $p$가 두 선언항 모두로부터 유도 가능하다면, 그 선언 또한 $p$로부터 유도 가능할 때 지지된다. 이는 게임 이론적으로, 조기 결정을 피하는 (연속 전달 스타일(continuation-passing style)의 읽기) 전략, 즉 두 선언항 모두에 대한 연속(continuation)을 제공하는 전략으로 해석된다.
4. 예시: 이 프레임워크는 4x4 스도쿠 퍼즐을 사용하여 설명된다. 스도쿠는 규칙들이 트리를 정의하는 아레나로서 공식화되며, 이는 논리적 귀결에 대한 즉각적인 참조 없이 플레이어 대 환경의 역동성을 보여준다.

주요 결과
본 논문은 다음의 정리와 따름정리를 확립한다.

• 데이터 구조의 동형성 (Lemma 13): 기저(규칙의 집합)와 아레나(트리의 포레스트) 사이에는 상호 역번역이 존재하며, 이는 두 구조가 데이터 구조로서 동형임을 증명한다.
• 적절성 (Corollary 16): 임의의 원자 집합 $S$와 원자 $p$에 대하여, $S$가 기저 $B$에서 유도 가능하다면($S \vdash_B p$), 이는 곧 $S$로부터 $p$에 대한 제안자의 승리 전략이 아레나 $B$에 대응하는 아레나에서 존재함($S \triangleright_{Arena(B)} p$)과 동치이다. 이는 게임 이론적 해석이 기저에서의 유도 가능성에 대해 건전하고 완전함을 입증한다.
• 게임-확장 의미론 (Game-Extension Semantics, G-eS): Sandqvist의 절에서 "기저에서의 유도 가능성"을 "아레나에서의 승리 전략의 존재성"으로 대체함으로써, 저자들은 IPL을 위한 새로운 의미론을 정의한다.
• 주요 논리적 결과 (Corollary 20): 저자들은 직관주의 명제 논리(구체적으로 자연 연역 체계 NJ)가 이 새로운 게임-확장 의미론에 대해 건전하고 완전함을 증명한다. 즉, $\Gamma \vdash_{NJ} \phi$인 것은 $\Gamma \Vdash' \phi$ (게임 의미론에서의 타당성)인 것과 동치이다.

의의 및 주장
본 논문은 IPL에 대해 B-eS와 Hyland-Ong 게임 의미론 사이의 완전 추상적 상관관계를 달성했다고 주장한다. 주요 의의는 다음과 같다:

1. P-tS로부터의 게임 재구성: 저자들은 게임 의미론의 개념이 증명론적 의미론의 원형으로부터 재구성될 수 있음을 보여준다. 이는 게임이 단순히 외부적인 모델이 아니라, 논리의 증명론적 성격에 내재된 것으로 볼 수 있음을 시사한다.
2. 타당성의 조작적 읽기: 타당성을 승리 전략과 연결함으로써, 이 의미론은 조작적 읽기를 획득한다. 아레나에서의 타당성은 정적인 속성이 아니라, 목표 지향적 탐색을 통해 계산 가능한 "실행 가능한" 것이다.
3. 선언의 계산적 내용: 본 논문은 B-eS의 기술적으로 동기 부여된 선언 절이 게임 설정에서 직접적인 계산적 내용을 갖는다고 주장한다. 이는 어떤 선언항이 결국 해결되더라도 탐색을 지속하는 방법을 아는 전략을 나타내며, 효과적으로 직관주의 틀 내에서 백트래킹(backtracking) 메커니즘을 내부화한다.
4. 추후 연구를 위한 토대: 이 작업은 아레나에 대한 제약(예: 수축 제한)을 통한 부분 구조 논리 탐구, 또는 정당화 규칙이나 동시적 게임의 수정을 통한 고전적 추론 조사 등, 일차 및 고차 논리로 의미론을 확장하기 위한 토대를 제공한다.

저자들은 완전한 대응(full-and-faithful correspondence, 즉 서로 다른 유도 과정을 서로 다른 전략에 매핑하는 것)을 위해서는 유도와 전략의 동일성을 정의하는 추가적인 작업이 필요하다는 점을 언급하며, 이를 향후 연구 과제로 남겨두는 겸허한 어조를 유지한다.