An independence of the MIN principle from the PHP principle

技术摘要：MIN 原理与 PHP 原理的独立性

问题陈述
本文探讨了命题证明复杂性与有界算术中的一个核心主题：理解证明系统的相对强度并确立证明长度的下界。具体而言，作者在相对化有界算术的框架内，研究了**极小化原理（MIN）与鸽巢原理（PHP）**之间的逻辑独立性。

极小化原理 $MIN(\triangleleft)$ 断言：有限区间 $[0, \dots, n)$ 上的任何严格线性序 $\triangleleft$ 都具有最小元。已知该原理可在理论 $T^2_2(\triangleleft)$ 中得证，但在较弱的片段 $T^1_2(\triangleleft)$ 中不可证。鸽巢原理 $PHP$指出：不存在从大小为$n+1$的集合到大小为$n$的集合的单射映射。尽管$PHP$即使在$T_2(\alpha)$等强理论中也不可证，但其在较弱扩展中相对于$MIN$ 的地位尚不明确。

核心问题在于：理论 $T^1_2(\triangleleft)$ 若增加所有针对 $\Delta^b_1(\triangleleft)$ 公式的鸽巢原理实例（记为 $PHP(\Delta^b_1(\triangleleft))$），是否足以证明 $MIN(\triangleleft)$？本文旨在证明该扩展是不足够的，从而确立 $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft))$ 无法证明 $MIN(\triangleleft)$。

方法论
证明采用了一种类似于力迫法（forcing）的模型论构造，其结构表现为在真算术的可数非标准模型 $M$ 上，由三方参与的一场博弈。目标是通过对子结构 $I \subset M$ 进行扩张，定义一个满足特定性质但违反其他性质的二元关系 $\triangleleft$。

1. 博弈框架：
   该构造被视为在可数多步中由三名玩家参与的博弈 $G_O$：

   • $P_{MIN}$： 旨在构造一个在 $[0, \dots, n)$ 上没有最小元的严格线性序，从而证伪 $MIN(\triangleleft)$。
   • $P_{IND}$： 旨在确保生成的结构满足多项式归纳（$\Sigma^b_1(\triangleleft)$-归纳），从而保持理论 $T^1_2(\triangleleft)$。
   • $P_{PHP}$： 旨在确保结构满足所有针对 $\Delta^b_1(\triangleleft)$ 公式的鸽巢原理实例。

   博弈按回合进行，玩家扩展部分序条件 $o \in O$（即有限个不同数字的序列）。最终关系 $\triangleleft$ 即为这些条件的并集。

2. 制胜策略：

   • $P_{MIN}$ 策略： 利用外部可数队列，确保每个元素最终都被插入，且每个元素都有一个更小的前驱，从而保证存在一个没有最小元的全序。
   • $P_{IND}$ 策略： 依赖于 Paris 和 Wilkie 的经典结果（由 Riis 推广），确保对于任何 $\Sigma^b_1$ 公式，如果存在见证者，则能找到一种“稳定”条件，从而保证最小数原理成立。
   • $P_{PHP}$ 策略（核心贡献）： 这是技术难度最大的部分。玩家必须确保对于任何 $\Delta^b_1(\triangleleft)$ 公式 $\phi$，由 $\phi$ 定义的关系都不是从较大集合 $p$ 到较小集合 $h$ 的单射。

3. 组合分析（“数组”方法）：
   为了证明 $P_{PHP}$ 拥有制胜策略，作者引入了$(o, p, h)$-PHP-数组的概念。这些是可定义的条件族，代表了 $\Delta^b_1$ 公式的预言机计算的可能结果。

   • 证明通过将这些数组扩展为均匀树（类似于预言机查询的决策树），确立了此类数组大小的下界。
   • 证明了力迫偏序中任何两两不相容条件集合大小的上界。
   • 通过比较这些界限，作者推导出：若 $p > h$ 则产生矛盾；有效数组的存在意味着 $p \le h$。因此，若 $p > h$，玩家 $P_{PHP}$ 总能迫使单射性被破坏（要么发现碰撞，要么发现缺失值），从而确保 PHP 原理成立。

主要贡献与结果

• 主要定理： 本文证明了 $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft)) \nvdash \forall n MIN(\triangleleft)_n$。
  • 该结果将 $T^2_2(\triangleleft)$（其可证明 $MIN$）的强度与通过鸽巢原理扩展$T^1_2$ 后的理论区分开来。
  • 这意味着在相对化设定下，理论 $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft))$ 与 $T^2_2(\triangleleft)$ 在强度上是不可比的：前者无法证明 $MIN$，而后者无法证明普通 PHP。
• 组合技术： 本文发展了一种涉及PHP-数组和MIN-树的精细组合方法。该技术允许在力迫构造中对条件大小进行精确计数，改进了以往的下界论证，提供了确切的大小估计。
• 其他分离结果： 该方法被应用于展示进一步的独立性结果：
  • 可以构造 $T^1_2(\alpha) + PHP(\Delta^b_1(\alpha))$ 的模型，使其不满足对偶弱鸽巢原理（dWPHP）。
  • 可以构造不满足**锦标赛原理（TOUR）**的模型。
  • 该构造可被修改，以生成其中排序 $\triangleleft$ 在特定子集上是稠密线性序的模型。

意义与主张
本文声称提供了一条理解有界算术中开放问题的新途径，例如相邻理论 $T^i_2$ 与 $T^{i+1}_2$ 的分离，以及 $R(\log)$ 问题。通过表明向 $T^1_2$ 添加鸽巢原理并不能推导出极小化原理，该工作突显了组合原理在加强弱算术理论方面的局限性。

作者指出，虽然已知弱鸽巢原理（WPHP）不足以证明像 MIN 这样的强原理（见文献 [12] 中的结果），但本文将这一理解扩展到了限制在 $\Delta^b_1$ 公式上的强鸽巢原理。其意义在于证明：即使是强 PHP，当限制在多项式时间可计算的图上时，也无法弥合与 $T^2_2$ 在极小化方面的强度差距。

本文最后提出了一个开放问题：相同的组合方法能否将 $T^1_2(\triangleleft) + PHP'(\Delta^b_1(\triangleleft))$（一种允许多值函数的变体）与 $MIN(\triangleleft)$ 分离开来。作者对此表示不确定，指出在行元素不一定不相容的数组中确立下界存在困难。