Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA

基本信息

• 论文ID: 2507.11643
• 标题: Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA
• 作者: Vladimir Kanovei, Vassily Lyubetsky
• 分类: math.LO (数理逻辑)
• 发表时间: October 13, 2025
• 论文链接: https://arxiv.org/abs/2507.11643

摘要

本文证明了理论Z⁻、ZF⁻、ZFC⁻（上标减号表示缺少幂集公理）与PA₂、PA₂⁻（上标减号表示缺少可数选择公理模式）之间的等一致性。所使用的方法包括通过良基树在PA₂⁻中解释无幂集的集合论，以及在所述无幂集集合论中使用哥德尔可构造性。

研究背景与动机

核心问题

本文旨在解决一个基础数学逻辑问题：证明几个重要数学理论系统之间的等一致性关系。具体来说，要建立以下理论之间的等一致性：

• 无幂集公理的集合论系统：Z⁻、ZF⁻、ZFC⁻
• 二阶算术系统：PA₂、PA₂⁻

问题重要性

1. 基础数学理论的关系：这些理论都是现代数学的重要基础，理解它们之间的逻辑关系对数学基础研究具有根本意义
2. 一致性问题的核心地位：在数学逻辑中，理论的一致性是最基本的性质，等一致性关系揭示了不同理论系统的相对强度
3. 历史意义：该结果自1960年代末就已知晓，但缺乏完整的自包含证明

现有方法局限性

作者指出，虽然该定理自至少1960年代末就已为人所知，但显然从未发表过自包含且相对完整的证明。这正是本文的主要动机——提供这样一个完整的证明。

核心贡献

1. 提供完整证明：首次给出定理1.1（主要等一致性结果）的自包含、完整证明
2. 构建中间理论TMC：引入了一个中间理论TMC，它扩展了Z⁻并包含三个额外公理
3. 建立解释关系：通过良基树结构在PA₂⁻中解释TMC，在PA₂中解释ZFC⁻
4. 应用哥德尔可构造性：在TMC框架下发展可构造性理论，建立ZFC⁻在TMC中的解释
5. 提供具体模型：给出了满足ZFC⁻的具体集合或类L*的构造

方法详解

任务定义

证明以下理论的等一致性：

• 输入理论：PA₂⁻、PA₂、Z⁻、ZFC⁻、ZF⁻
• 输出：建立这些理论之间的相互解释关系
• 约束条件：证明必须是自包含的，不依赖于未发表的结果

核心架构

第一部分：树结构解释

1. 定义结构V：在PA₂⁻中定义结构V = ⟨WFT; ∼=, ∼∈⟩，其中：
   • WFT是所有良基树T ⊆ ω<ω的集合
   • ∼=是树之间的双模拟等价关系
   • ∼∈是基于∼=定义的成员关系
2. 建立解释：
   • 定理5.2证明V在PA₂⁻下满足TMC
   • V在PA₂下满足ZFC⁻

第二部分：可构造性方法

1. 中间理论TMC：包含三个关键公理
   • 传递超集公理（TrSups）：每个集合都有传递超集
   • Mostowski坍缩公理（MostColl）：每个良基关系都允许传递模型
   • 可数性公理（Countability）：所有集合都是至多可数的
2. 可构造层次：在TMC中发展Gödel可构造层次：

   L₀[u] = ω ∪ {u}
   Lₐ₊₁[u] = Def Lₐ[u]
   Lλ[u] = ⋃ₐ<λ Lₐ[u]
   L[u] = ⋃ₐ∈Ord Lₐ[u]
   

技术创新点

关键定理8.6

在条件F(u,Ω,K)下，集合K满足ZFC⁻，其中F(u,Ω,K)定义了两种情况：

• 情况A：Ω = Ord，K = Lu，且ω₁^Lu不存在
• 情况B：Ω = ω₁^Lu存在，K = L_Ωu

主要技术定理1.2

L* = {
  L,                    如果ω₁^L不存在
  L_Ω = ⋃ₐ<Ω Lₐ,      如果ω₁^L = Ω存在
}

该集合或类满足ZFC⁻。

实验设置

理论框架验证

本文是纯理论数学工作，不涉及传统意义上的实验。验证方法包括：

1. 逻辑推理验证：每个定理都通过严格的数学证明来验证
2. 一致性检查：确保各个理论系统内部的一致性
3. 解释关系验证：验证建立的解释关系确实保持理论的公理和推理规则

对比方法

• Simpson的方法：作者比较了与Simpson 30, VII.4中相关解释的异同
• 早期方法：回顾了17中定义的早期解释方法
• 其他模型：在第13节中讨论了三种其他的ZFC⁻模型

主要结果

核心定理

定理1.1：理论PA₂⁻、PA₂、Z⁻、ZFC⁻、ZF⁻是等一致的。

关键中间结果

定理5.2（解释定理）

PA₂⁻/PA₂框架下，结构V是良定义的，且V分别满足TMC/ZFC⁻。

定理1.3（可构造性结果）

在TMC下：

1. L ∩ P(ω)满足PA₂
2. L本身满足分离公理

推论12.1

在PA₂⁻下，L ∩ P(ω)满足PA₂，这提供了PA₂在PA₂⁻中的解释。

相关工作

历史发展

• 1960年代末：该结果首次被发现（如24中所述）
• Kreisel 24：早期相关工作
• Simpson 30：在ATR₀^set理论框架下的相关结果
• Marek系列工作：26, 27中的相关技术

本文与相关工作的关系

1. 完整性：首次提供完全自包含的证明
2. 方法统一：将树解释方法与可构造性方法有机结合
3. 技术改进：在TMC框架下简化了某些技术细节

结论与讨论

主要结论

1. 成功建立了五个重要数学理论之间的等一致性关系
2. 提供了完整的、自包含的证明方法
3. 展示了树解释和可构造性方法的有效结合

局限性

1. 开放问题：作者提出是否存在避免大量使用集合论概念的PA₂在PA₂⁻中的解释方法
2. 技术复杂性：证明涉及多个复杂的技术步骤，理解门槛较高
3. 应用范围：主要是基础理论结果，直接应用有限

未来方向

问题15.1

关于公理TrSups是否真的独立于TMC的其余公理。

问题15.2

寻找定理14.3在PA₂⁻中的纯分析证明，不显式或隐式涉及V或类似的派生集合论结构。

应用前景

作者期望该方法可用于加强Cohen的集合论强制方法在ZFC⁻和PA₂理论中的最新应用。

深度评价

优点

1. 理论完整性：填补了该领域长期存在的证明空白
2. 方法创新：巧妙结合了树解释和可构造性两种经典方法
3. 技术深度：展现了深厚的数理逻辑技术功底
4. 写作清晰：尽管技术复杂，但组织结构清晰，便于理解

不足

1. 技术门槛高：需要深厚的数理逻辑背景才能完全理解
2. 实用性有限：主要是理论贡献，直接应用场景有限
3. 某些证明细节：部分证明（如定理1.3(II)）只给出了概要

影响力

1. 基础理论贡献：为数学基础研究提供了重要的理论工具
2. 方法论价值：展示的技术方法可应用于其他相关问题
3. 教学价值：可作为高级数理逻辑课程的重要参考

适用场景

1. 数学基础研究：为研究不同数学理论系统关系提供工具
2. 逻辑学研究：为模型论和证明论研究提供技术支持
3. 计算机科学基础：为类型理论和程序语言语义学提供理论基础

参考文献

论文包含35篇参考文献，涵盖了从经典的Gödel、Kleene工作到近期的集合论强制方法研究，体现了该领域的历史发展脉络和最新进展。

总体评价：这是一篇高质量的数理逻辑理论论文，成功解决了一个长期存在的重要问题。虽然技术门槛较高，但其理论贡献和方法论价值使其成为该领域的重要文献。