Support is Search

1. 문제 제기 (Problem)

• 배경: 산드퀴스트의 기반 확장 의미론은 논리 상수의 의미를 모델 이론적 진리 조건이 아닌, 추론적 행동 (증명 이론적 의미론) 으로 정의합니다. 여기서 '지지 (support)' 관계 ($\Vdash_B \varphi$) 는 주어진 기반 (atomic base) $B$와 그 확장들에 대해 정의되며, 전역적 유효성 (모든 기반에서의 지지) 은 직관적 논리의 유효성과 일치함이 증명되었습니다.
• 국소적 질문의 부재: 기존 연구는 "어떤 공식이 전역적으로 유효한가?"라는 전역적 질문에 집중했습니다. 반면, 이 논문은 **"주어진 고정된 기반 $B$에서 $\Vdash_B \varphi$가 무엇을 의미하는가?"**라는 국소적 질문을 다룹니다.
• 현존하는 난제:
  • 기존 의미론의 정의는 베이스 확장 ($C \supseteq B$) 과 원자 (atom) 에 대한 보편 양화 (universal quantification) 를 포함합니다. 이를 실재론적 (realist) 으로 읽으면, 완결된 무한 집합을 전제하게 되어 반실재론적 (anti-realist) 인 의미론의 기초와 모순됩니다.
  • 또한, 지지 관계는 단순히 기반을 공리 집합으로 변환한 후의 추론 ($B^* \vdash \varphi$) 과 동치이지 않습니다 (예: 분배 법칙의 실패).
  • 따라서 지지 관계의 계산적 내용 (computational content) 과 국소적 의미를 명확히 규명할 필요가 있었습니다.

2. 방법론 (Methodology)

이 논문은 직관적 논리 공식을 2 차원 계승 하에로프 (Second-Order Hereditary Harrop) 논리 프로그래밍 목표로 인코딩하여, 의미론적 지지 관계를 논리 프로그램 실행 (증명 탐색) 과 연결합니다.

• 계산적 표현 (Rules-as-Clauses):
  • 고차원 원자 시스템 (Higher-level Atomic Systems) 을 논리 프로그래밍의 절 (clauses) 로 해석합니다.
  • 특히, 논리 프로그래밍의 **계속 전달 스타일 (Continuation-Passing Style, CPS)**을 의미론적 정의에 적용합니다. 예를 들어, 논리합 ($\lor$) 의 정의는 두 가지 지지 ($\varphi \Vdash_C p$ 및 $\psi \Vdash_C p$) 를 '연속체 (continuation)'로 받아들이는 CPS 패턴으로 재해석됩니다.
• 인코딩 정의 ($\llbracket \varphi \rrbracket$):
  • 각 논리식 $\varphi$를 논리 프로그래밍 목표 $\llbracket \varphi \rrbracket$로 매핑합니다.
  • 주요 인코딩 규칙:
    • $\llbracket \bot \rrbracket = \forall X (X)$
    • $\llbracket \varphi \to \psi \rrbracket = \llbracket \varphi \rrbracket \supset \llbracket \psi \rrbracket$
    • $\llbracket \varphi \land \psi \rrbracket = \forall X ((\llbracket \varphi \rrbracket \supset \llbracket \psi \rrbracket \supset X) \supset X)$
    • $\llbracket \varphi \lor \psi \rrbracket = \forall X ((\llbracket \varphi \rrbracket \supset X) \supset (\llbracket \psi \rrbracket \supset X) \supset X)$
  • 여기서 $\forall X$는 원자 변수에 대한 2 차 양자이며, 이는 논리 프로그래밍의 고유 변수 (eigenvariable) 규칙에 따라 처리됩니다.
• 운영적 의미론 (Operational Semantics):
  • 논리 프로그램 $B$와 목표 $\llbracket \varphi \rrbracket$에 대한 증명 탐색 관계 ($B \vdash_O \llbracket \varphi \rrbracket$) 를 정의합니다.
  • 이 과정은 'Fact', 'Backchain', 'Augment', 'Generic' 등의 규칙을 통해 이루어지며, 여기서 보편 양자는 완결된 도메인을 순회하는 것이 아니라, **새로운 원자 (fresh atom)**를 도입하는 고유 변수 규칙으로 처리됩니다.

3. 주요 기여 (Key Contributions)

1. 메타이론적 약속의 재해석 (Meta-theoretic Commitments):
   • 의미론적 절에 포함된 보편 양자 ($\forall C \supseteq B, \forall p$) 가 완결된 무한 집합을 가정하는 실재론적 전제가 아님을 보였습니다. 대신, 이는 증명 탐색 프레임워크 내부의 **구성적 해석 (constructive interpretation)**으로, 고유 변수 규칙에 의해 통제됩니다. 이는 의미론의 반실재론적 기초를 내부적으로 정합성 있게 만듭니다.
2. 계산적 내용 (Computational Content):
   • 지지 관계가 단순히 원칙적으로 검증 가능한 것이 아니라, 실제로 **검색 가능 (searchable)**함을 보였습니다. $\Vdash_B \varphi$가 성립할 때, 이를 만족시키는 균일한 유도 (uniform derivation) 를 찾는 구체적인 논리 프로그래밍 절차가 존재합니다.
3. 국소적 건전성과 완전성 (Local Soundness and Completeness):
   • 산드퀴스트의 전역적 정리 ($\forall B, \Vdash_B \varphi \iff \varphi$ is valid) 를 보완하여, 임의의 고정된 기반 $B$에 대해 다음 동치 관계를 증명했습니다:
     $$\Vdash_B \varphi \iff B \vdash_O \llbracket \varphi \rrbracket$$
   • 이는 주어진 기반에서의 지지 관계를 정확히 특징짓는 국소적 대응 관계를 확립합니다.

4. 주요 결과 (Results)

• 주요 정리 (Theorem 4.6): 임의의 기반 $B$와 공식 $\varphi$에 대해, $\Vdash_B \varphi$가 성립할 필요충분조건은 논리 프로그램 $B$가 목표 $\llbracket \varphi \rrbracket$를 증명하는 것 ($B \vdash_O \llbracket \varphi \rrbracket$) 입니다.
• 증명 전략:
  • 건전성 (Soundness): 지지 관계의 정의 (Fig 1) 를 통해 유도된 구조적 귀납법을 사용하여, 지지 관계가 논리 프로그래밍의 운영적 규칙을 만족함을 보였습니다.
  • 완전성 (Completeness): 논리 프로그래밍의 증명 ($B \vdash_O \llbracket \varphi \rrbracket$) 이 지지 관계 ($\Vdash_B \varphi$) 를 함의함을 보였습니다. 특히, 논리합 ($\lor$) 의 경우 CPS 인코딩이 어떻게 베이스 확장에 대한 보편 양화를 증명 탐색의 'Augment' 및 'Backchain' 단계로 변환하는지를 상세히 증명했습니다.
• 고차원 규칙의 중요성: 직관적 논리를 얻기 위해 고차원 원자 시스템 (higher-level atomic rules) 이 필수적임을 재확인했습니다. 1 차원 규칙만 사용하면 고전 논리가 도출되는데, 이는 논리 프로그래밍 관점에서 가설적 목표 (hypothetical goals) 가 없는 호른 절 (Horn clauses) 만을 사용하는 것과 동일하며, CPS 인코딩이 불가능해지기 때문입니다.

5. 의의 및 향후 과제 (Significance and Future Work)

• 철학적 의의: 이 결과는 기반 확장 의미론이 단순히 반실재론적 이상을 가진 것이 아니라, 실행 (execution) 단계에서도 완전히 구성적이고 계산적으로 투명함을 입증했습니다. 의미론의 보편 양자는 '완결된 전체'가 아닌 '증명 과정에서의 새로운 자원 도입'으로 해석됨으로써, 의미론의 철학적 일관성을 회복시켰습니다.
• 실용적 의의: 이 대응 관계는 기반 확장 의미론을 모델링 작업에 구현할 수 있는 길을 열었습니다. 논리 프로그래밍 엔진을 사용하여 논리식의 지지 여부를 직접 계산할 수 있게 되었습니다.
• 한계 및 향후 연구:
  • 고전 논리: 고전 논리의 경우 고차원 규칙이 부재하여 CPS 인코딩이 실패하므로, 고전 논리에 대한 계산적으로 투명한 증명 기반 의미론은 여전히 미해결 문제입니다.
  • 일반화: 다른 논리 체계 (예: 선형 논리, 모달 논리 등) 에 대해 동일한 패턴 (소거 행동을 보편 양화로 인코딩) 이 적용 가능한지, 그리고 이에 적합한 논리 프로그래밍 언어와 균일 증명 (uniform proof) 개념을 어떻게 정의할지에 대한 체계적인 연구가 향후 과제로 남았습니다.

결론적으로, 이 논문은 "지지 (Support) 는 검색 (Search) 이다"라는 명제를 통해, 추상적인 의미론적 개념을 구체적인 계산 과정으로 환원시킴으로써 증명 이론적 의미론의 기초를 강화하고 실용적 구현의 토대를 마련했습니다.