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

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

基本信息

  • 论文ID: 2501.03297
  • 标题: A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
  • 作者: Antonio Piccolomini d'Aragona (Eberhard Karls Universität Tübingen)
  • 分类: math.LO cs.LO
  • 发表时间: 2025年1月 (arXiv预印本)
  • 论文链接: https://arxiv.org/abs/2501.03297

摘要

本文研究了两种证明论语义学方法：一种基于论证结构和证明的可还原性语义，另一种基于原子基上公式（集合）间后承关系的基语义。后者又分为标准解读和Sandqvist提出的变体。作者证明了在适当条件下允许从一种方法转换到另一种方法的结果，并分析了这些结果对递归逻辑系统相对于证明论有效性概念的完全性问题的影响。文章重点讨论了基完全性概念，并结合已知的直觉主义逻辑完全性结果进行分析。

研究背景与动机

问题背景

证明论语义学(PTS)是一个构造性语义学框架，其核心概念不是模型论中的真值，而是证明。该领域存在三种主要的单调证明论语义方法：

  1. 可还原性语义(Reducibility semantics)：基于Prawitz的工作，使用论证结构和还原
  2. 标准基语义(Standard base semantics)：基于原子规则集上的公式后承关系
  3. Sandqvist基语义：标准基语义的变体，对析取采用消去式而非引入式处理

研究动机

  1. 理论统一性：理解三种方法之间的关系，特别是它们在什么条件下等价
  2. 完全性问题：探讨直觉主义逻辑(IL)在不同证明论语义下的完全性和不完全性
  3. 构造性精神：分析从Prawitz的"见证"方法到基语义的"去见证"方法是否丢失了构造性内容

现有局限性

  • 三种方法之间的关系缺乏系统性比较
  • 基完全性概念尚未得到充分研究
  • 直觉主义逻辑在不同框架下的表现存在差异需要解释

核心贡献

  1. 等价性结果：证明了可还原性语义与标准基语义的完全等价性（定理1-2）
  2. 条件等价性：建立了可还原性语义与Sandqvist基语义之间的条件等价关系（定理4）
  3. 基不可比性：证明了Prawitz方法与Sandqvist方法在模型层面不可比（定理10-12）
  4. 基完全性理论：发展了基完全性概念并证明其对直觉主义逻辑的不一致性（定理18-19）
  5. 紧致导出原理：引入并分析了紧致导出原理在证明论语义中的作用

方法详解

任务定义

本文的核心任务是比较三种证明论语义方法，并分析它们对逻辑系统完全性的影响。具体包括：

  • 建立不同语义方法之间的转换条件
  • 分析基完全性概念的一致性
  • 研究直觉主义逻辑的不完全性现象

理论框架

语言和原子基

语言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. 不完全性传递：等价性结果使得不完全性结果可在不同框架间传递
  3. 紧致性限制：基完全性要求"局部"紧致性，这与某些语义的性质冲突

相关工作

历史发展

  1. Prawitz (1965-1973)：建立了基于论证结构的证明论语义
  2. Schroeder-Heister (2006)：发展了标准基语义
  3. Sandqvist (2015)：提出了消去式析取处理的变体
  4. Piecha等 (2015-2019)：证明了直觉主义逻辑的不完全性结果

本文贡献定位

  • 统一性：首次系统比较三种主要方法
  • 深度分析：不仅建立等价性，还分析了不等价的条件和原因
  • 理论扩展：引入基完全性概念并揭示其矛盾性

结论与讨论

主要结论

  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

这些引用充分体现了作者对领域发展脉络的深入理解和对相关工作的全面掌握。

总体评价：这是一篇高质量的理论逻辑学论文，在证明论语义学这一专门领域做出了重要贡献。虽然技术性较强，但对理解构造性逻辑的语义基础具有重要价值。论文的理论统一工作和基完全性悖论的发现都可能产生长远影响。