2025-11-11T11:28:09.453044

A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic

d'Aragona
I deal with two approaches to proof-theoretic semantics: one based on argument structures and justifications, which I call reducibility semantics, and one based on consequence among (sets of) formulas over atomic bases, called base semantics. The latter splits in turn into a standard reading, and a variant of it put forward by Sandqvist. I prove some results which, when suitable conditions are met, permit one to shift from one approach to the other, and I draw some of the consequences of these results relative to the issue of completeness of (recursive) logical systems with respect to proof-theoretic notions of validity. This will lead me to focus on a notion of base-completeness, which I will discuss with reference to known completeness results for intuitionistic logic. The general interest of the proposed approach stems from the fact that reducibility semantics can be understood as a labelling of base semantics with proof-objects typed on (sets of) formulas for which a base semantics consequence relation holds, and which witness this very fact. Vice versa, base semantics can be understood as a type-abstraction of a reducibility semantics consequence relation obtained by removing the witness of the fact that this relation holds, and by just focusing on the input and output type of the relevant proof-object.
academic

3種類の単調証明論的意味論の比較と直観主義論理の基-不完全性

基本情報

  • 論文ID: 2501.03297
  • タイトル: A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
  • 著者: Antonio Piccolomini d'Aragona (エーベルハルト・カール大学テュービンゲン)
  • 分類: math.LO cs.LO
  • 発表時期: 2025年1月 (arXiv プレプリント)
  • 論文リンク: https://arxiv.org/abs/2501.03297

要旨

本論文は、証明論的意味論の2つのアプローチを研究している。1つは論証構造と証明の可約性意味論に基づくもの、もう1つは原子基上の公式（集合）間の帰結関係に基づく基意味論である。後者は標準的解釈とSandqvistによって提案された変種に分かれている。著者は、適切な条件下で一方の方法から他方の方法への変換を可能にする結果を証明し、これらの結果が再帰的論理体系の証明論的妥当性概念に対する完全性問題に及ぼす影響を分析している。論文は基-完全性概念に焦点を当て、直観主義論理の既知の完全性結果と組み合わせて分析している。

研究背景と動機

問題背景

証明論的意味論(PTS)は構成的意味論の枠組みであり、その中核概念はモデル論における真値ではなく、証明である。この分野には3つの主要な単調証明論的意味論アプローチが存在する：

  1. 可約性意味論(Reducibility semantics)：Prawitzの業績に基づき、論証構造と可約性を使用
  2. 標準基意味論(Standard base semantics)：原子規則集上の公式帰結関係に基づく
  3. Sandqvist基意味論：標準基意味論の変種で、選言に対して除去式ではなく導入式を採用

研究動機

  1. 理論的統一性：3つの方法間の関係、特にそれらが等価である条件を理解する
  2. 完全性問題：異なる証明論的意味論下での直観主義論理(IL)の完全性と不完全性を探究する
  3. 構成的精神：Prawitzの「証拠」方法から基意味論の「証拠除去」方法への移行が構成的内容を失うかどうかを分析する

既存の限界

  • 3つの方法間の関係は体系的な比較が不足している
  • 基-完全性概念はまだ十分に研究されていない
  • 異なる枠組みにおける直観主義論理の振る舞いの差異は説明が必要である

核心的貢献

  1. 等価性結果：可約性意味論と標準基意味論の完全な等価性を証明（定理1-2）
  2. 条件付き等価性：可約性意味論とSandqvist基意味論間の条件付き等価関係を確立（定理4）
  3. 基-非可比性：Prawitz方法とSandqvist方法がモデルレベルで非可比であることを証明（定理10-12）
  4. 基-完全性理論：基-完全性概念を発展させ、直観主義論理に対するその矛盾性を証明（定理18-19）
  5. コンパクト導出原理：証明論的意味論におけるコンパクト導出原理の役割を導入・分析

方法の詳細

タスク定義

本論文の中核的タスクは、3つの証明論的意味論方法を比較し、それらが論理体系の完全性に及ぼす影響を分析することである。具体的には以下を含む：

  • 異なる意味論方法間の変換条件の確立
  • 基-完全性概念の一貫性の分析
  • 直観主義論理の不完全性現象の研究

理論的枠組み

言語と原子基

言語Lは以下のように定義される：

X ::= p, q, r, s, t, ... | ⊥ | X ∧ X | X ∨ X | X → X

原子規則は階層的に帰納的に定義される：

  • 階層0：任意の原子は原子規則である
  • 階層1：A₁...Aₙ/A の形式の規則。ここで全ての公式は原子である
  • 階層κ+1：ℜ₁A₁...ℜₙAₙ/A の形式の規則

基意味論

標準基意味論 (Γ |=_{B,n} A)：

  1. Γ = ∅の場合：
    • A ∈ ATOM_L ⟹ ⊢_B A
    • A = B ∧ C ⟹ |={B,n} B かつ |={B,n} C
    • A = B ∨ C ⟹ |={B,n} B または |={B,n} C
    • A = B → C ⟹ B |=_{B,n} C
  2. Γ ≠ ∅ ⟹ ∀C ⊇ₙ B (|={C,n} Γ ⟹ |={C,n} A)

Sandqvist基意味論の相違点は選言節にある：

  • A = B ∨ C ⟹ ∀C ⊇ₙ B ∀D ∈ ATOM_L (B |=ˢ_{C,n} D かつ C |=ˢ_{C,n} D ⟹ |=ˢ_{C,n} D)

可約性意味論

論証構造 ⟨T, ⟨f, h, g⟩⟩に基づく。ここで：

  • Tは有限根木で、ノードは公式でラベル付けされている
  • f, h, gは解決関数である

n-妥当性 (⟨D, J⟩がB上でn-妥当)：

  • Dが閉じている場合：結論が原子ならばDERB内の閉じた構造に可約化；そうでなければ正規形に可約化
  • Dが開いている場合：全てのσ, J⁺ ⊇ J, C ⊇ₙ Bに対して、仮定がC上で妥当ならばDσはC上で妥当

技術的革新点

  1. 等価性証明技術：帰納法と受容可能性節を通じて異なる意味論間の等価性を確立
  2. 条件付き等価性枠組み：「大域的可比性」概念を導入して点対点等価でない場合を処理
  3. 基-非可比性分析：完全性/不完全性の差異を利用してモデルクラスの分岐を証明
  4. コンパクト導出原理：無限原子基の処理を有限断片の分析に変換

実験設定

理論検証方法

本論文は主に数学的証明方法を採用し、以下の戦略を通じて理論結果を検証している：

  1. 帰納的証明：公式の複雑性と導出長に対する構造帰納法
  2. 反例構築：具体的な原子基（例えば規則R）を使用して非等価性を示す
  3. 既知結果の応用：Sandqvistの完全性定理とPiecha等の不完全性結果を利用

重要な例

原子基{R}：

    A
  [B]   [C]
   D     D
   -------
      D

ある A, B, C ∈ ATOM_L と各 D ∈ ATOM_L に対して。

この基は以下を満たす：A |=ˢ_,2 B ∨ C だが、A ⊭^α_,2 B ∨ C かつ A ⊭_,2 B ∨ C。

実験結果

主要定理結果

等価性結果

定理1-2：Γ |={B,n} A ⟺ Γ |=^α{B,n} A かつ Γ |=ₙ A ⟺ Γ |=^α_n A

これは可約性意味論と標準基意味論の完全な等価性を確立する。

条件付き等価性

定理4：もし ∀Γ ∀A ∀C ⊇ₙ B (Γ |=ˢ_{C,n} A ⟹ Γ |=^α_{C,n} A) ならば、 ∀Γ ∀A ∀C ⊇ₙ B (Γ |=^α_{C,n} A ⟹ Γ |=ˢ_{C,n} A)

基-非可比性

定理10：n = 2の場合、推論3の前件と後件の両方が失効する。

これはPrawitz方法とSandqvist方法が2階原子基上で非可比であることを意味する。

基-完全性の矛盾性

定理18：IL基-完全 ⊩ₙ ⟺ ⊩ₙ がコンパクト導出原理を享受かつ IL完全 ⊩ₙ

推論11-13：ILはいかなる証明論的意味論下でも基-完全ではない。

重要な推論

  1. 変換の十分条件：定理13は2つの意味論が等価である十分条件を与える
  2. 不完全性の伝播：等価性結果により、不完全性結果は異なる枠組み間で伝播可能
  3. コンパクト性の制限：基-完全性は「局所的」コンパクト性を要求し、これはある意味論の性質と矛盾する

関連研究

歴史的発展

  1. Prawitz (1965-1973)：論証構造に基づく証明論的意味論を確立
  2. Schroeder-Heister (2006)：標準基意味論を発展
  3. Sandqvist (2015)：除去式選言処理の変種を提案
  4. Piecha等 (2015-2019)：直観主義論理の不完全性を証明

本論文の貢献の位置付け

  • 統一性：3つの主要方法を初めて体系的に比較
  • 深い分析：等価性を確立するだけでなく、非等価性の条件と理由を分析
  • 理論的拡張：基-完全性概念を導入し、その矛盾性を明らかにする

結論と考察

主要な結論

  1. 構造的等価性：可約性意味論と標準基意味論は与えられた制限下で構造的に同一であり、「証拠」の存在または欠如は構成的精神に影響しない
  2. 条件付き統一：Prawitz方法とSandqvist方法は大域的レベルで比較可能だが、モデルレベルでは分岐する
  3. 基-完全性のパラドックス：基-完全性は直観主義論理に対して矛盾した概念であり、これは証明論的意味論の深層構造特性を明らかにする
  4. コンパクト性の役割：コンパクト導出原理は証明論的意味論において重要な役割を果たし、その失効は完全性問題をもたらす

限界

  1. 有限性仮定：結果は主に有限公式集に適用され、無限の場合への拡張には追加の作業が必要
  2. 階層的制限：ある結果は特定の階層の原子基に限定されるが、著者はこの制限を除去できることを示している
  3. 構成性の程度：等価性は証明されたが、「構成性の程度」の正確な特性化はまだ深い検討が必要

今後の方向

  1. より自由な基序：より一般的な原子基序構造下での類似結果を研究する
  2. 非単調拡張：分析を非単調証明論的意味論に拡張する
  3. 応用研究：これらの理論結果を具体的な論理体系設計への応用を探究する

深い評価

利点

  1. 理論的深さ：証明論的意味論分野の重要な理論的統一を提供し、長年存在していた空白を埋める
  2. 技術的厳密性：証明技術は精巧であり、特に条件付き等価性と基-非可比性を扱う方法は優れている
  3. 洞察の深さ：基-完全性の矛盾性の発見は証明論的意味論の本質的特性を明らかにする
  4. 記述の明確性：複雑な技術内容が適切に組織され、概念説明が明確である

不足点

  1. 実用性の制限：主に理論結果であり、実際の論理体系設計への直接的指導は限定的
  2. 例の不足：重要な反例はあるが、より多くの具体的応用場面の分析が欠けている
  3. 哲学的考察：構成的意味論の哲学的含意についての議論はより深くあり得る

影響力

  1. 理論的貢献：証明論的意味論に重要な統一枠組みを提供し、この分野の後続研究に影響を与える
  2. 方法論的価値：確立された比較方法論は他の論理意味論分野にも参考価値がある
  3. 基礎研究：明らかにされた基-完全性のパラドックスは証明論的意味論の基礎概念の再検討を促す可能性がある

適用場面

  1. 理論論理学：異なる証明論的意味論方法の研究に理論的基礎を提供
  2. 論理体系設計：適切な意味論枠組みの選択に判断基準を提供
  3. 構成的数学：構成的推論の意味論的基礎の理解にツールを提供

参考文献

論文は当該分野の中核文献を引用しており、以下を含む：

  • Prawitzの開拓的業績 18-21
  • Schroeder-Heisterの基意味論理論 24-26
  • Sandqvistの完全性結果 22
  • Piecha等の不完全性研究 15-17
  • Martin-Löfの型理論 9

これらの引用は、著者が分野の発展経路を深く理解し、関連研究を包括的に把握していることを十分に示している。

総合評価：これは証明論的意味論という専門分野において重要な貢献をした高品質の理論論理学論文である。技術性は高いが、構成的論理の意味論的基礎の理解に重要な価値を持つ。論文の理論的統一作業と基-完全性のパラドックスの発見は長期的な影響を及ぼす可能性がある。