关于经典逻辑博弈语义的两个注记：技术总结

本文是 Thierry Coquand 为纪念 Stefano Berardi 64 岁生日而撰写的论文，旨在阐述 Berardi 关于经典逻辑博弈语义（Game Semantics）的两个未发表的重要见解。文章回顾了 Berardi 与 Coquand 在 30 年前关于经典逻辑博弈语义的合作背景，并深入探讨了两个核心问题：无限交互序列的超限扩展，以及基于连续性的实现性语义（Realizability Semantics）在验证假公式时的局限性。

1. 研究背景与问题定义

1.1 经典逻辑的博弈语义

文章首先回顾了基于无限命题演算的经典逻辑博弈语义。该语义将公式视为两个玩家（$\exists$loise 代表存在量词，$\forall$belard 代表全称量词）之间的完美信息博弈。

• 直觉主义有效性：对应于 $\exists$loise 拥有必胜策略（无回溯）。
• 经典有效性：引入了**回溯（Backtracking）机制。$\exists$loise 被允许改变之前的选择，从而从环境（$\forall$belard）中“学习”。这种机制对应于证明论中的Cut-elimination（切消）**过程。
• 交互序列：博弈过程被形式化为交互序列（Interaction Sequence），由指针结构 $\phi$ 定义，记录当前移动是对之前哪一步的回应。

1.2 核心问题

尽管基于博弈的语义成功解释了经典逻辑的 Cut-elimination 和终止性，但 Berardi 指出了两个关键的理论边界：

1. 无限交互的语义：如果博弈不终止（即存在无限交互序列），如何从几何/结构上定义“观点（View）”并扩展至超限（Transfinite）阶段？
2. 实现性语义的充分性：在修改后的实现性（Modified Realizability）中，如果 $\exists$loise 拥有针对所有“连续”对手的必胜策略，是否意味着该公式在实现性语义下为真？Berardi 指出这一条件可能不足以排除假公式。

2. 方法论与理论框架

2.1 交互序列与观点（View）

文章定义了交互序列 $(V, \phi)$，其中 $V(n)$ 是阶段 $n$ 的“观点”集合，$\phi(n)$ 指向之前的移动。

• 线段（Segment）：$S(k) = [\phi(k), k]$。
• 确定性线段：若 $k$ 不在 $\phi$ 的像中，则 $S(k)$ 为确定性线段。
• 嵌套结构：确定性线段形成嵌套结构（Nest structure），即任意两个确定性线段要么不相交，要么一个完全包含另一个。

2.2 连续性假设

在涉及函数（如可数选择公理）的博弈中，对手 $\forall$belard 被假设为连续的，即其决策仅依赖于函数 $f$ 的有限部分信息。这一假设是实现性解释中证明终止性的关键。

3. 主要贡献与结果

3.1 第一个注记：无限交互序列的超限扩展

Berardi 对 Coquand 等人关于无限交互序列的古典证明进行了精炼。

• 定理 1：存在唯一的序列 $n_k < n_{k+1}$，使得 $n_k + 1 = \phi(n_{k+1})$，且这些线段 $S(n_k)$ 构成了 $[0, \omega[$ 的一个划分。
• 技术意义：
  • 该序列 $n_k$ 可被视为阶段 $\omega$ 的“观点” $V(\omega)$。
  • 序列中所有 $n_k$ 具有相同的奇偶性，这意味着如果存在无限辩论，可以明确归责于某一位玩家（即该玩家导致了无限循环）。
  • 超限扩展：基于此唯一序列，可以定义 $\phi(\omega) = n_k$，从而将交互序列扩展至超限阶段（$\omega + 1, \dots$）。这为理解非终止博弈的语义结构提供了严格的几何基础。

3.2 第二个注记：连续性策略无法排除假公式

这是本文最具颠覆性的发现。Berardi 指出，即使 $\exists$loise 拥有针对所有连续对手的必胜策略，该公式在经典逻辑中仍可能是假的。

• 反例公式：
  $$(\ast) \quad \bigvee_f \bigwedge_x \bigvee_y (f(x) = 0 \land f(y) \neq 0)$$
  该公式断言“存在一个函数 $f$，使得对于任意 $x$，存在 $y$ 满足 $f(x)=0$ 且 $f(y) \neq 0$"。在标准模型中，若取 $f$ 为常值函数 $1$，则$f(x)=0$ 永远不成立，故公式为假。

• 博弈过程分析：

  • $\exists$loise 的策略 ($A_1$)：$\exists$loise 初始选择 $f_0 = \lambda n. 1$。若 $\forall$belard 给出 $x_0$，$\exists$loise 回溯并修改函数为 $f_1$（令 $f_1(0)=0$）。若 $\forall$belard 给出 $x_1$，若 $x_1 < 1$ 则获胜，否则继续回溯修改 $f_2$（令 $f_2(1)=0$），以此类推。
  • 结果：只要 $\forall$belard 是连续的（即每次只查询有限个值），$\exists$loise 最终会找到一个 $n$ 使得 $x_n < n$，从而获胜。
  • 矛盾：尽管 $A_1$ 对所有连续对手必胜，但公式 $(\ast)$ 本身是假的。

• 无限辩论与 Cut-elimination 的失效：
  当 $A_1$ 与针对 $(\ast)$ 否定的策略 $B_1$ 对弈时，会产生一个无限辩论。

  • $A_1$ 不断修改函数 $f_n$ 以覆盖 $\forall$belard 的查询。
  • $B_1$ 不断选择新的 $x$ 值来挑战 $A_1$。
  • 这种无限交互对应于无法进行 Cut-elimination（切消），表明基于连续性的论证不足以作为实现性语义的充分条件。

• 哲学类比：
  文章将此现象与 Sergei Soloviev 关于 Ackermann 函数的研究进行类比。如果两个玩家在计算资源上存在不对称（一方更强），强者可以诱导弱者相信一个错误的命题。

4. 结论与意义

1. 理论深化：Berardi 的第一个注记将博弈语义从有限阶段推广到了超限阶段，通过唯一性序列明确了无限辩论的责任归属，丰富了经典逻辑博弈语义的数学结构。
2. 语义局限性：第二个注记揭示了“针对连续对手的必胜策略”这一条件在构造性实现性语义中的不充分性。它表明，仅凭连续性论证无法保证公式的真值，必须考虑更深层的交互结构（如 Cut-elimination 的终止性）。
3. 对实现性语义的影响：这一发现解释了为什么某些系统（如带有可数选择的经典 HA$\omega$）可以成功赋予修改后的实现性解释，而包含类似结构的假公式（如公式 $(\ast)$）则不能。这为理解经典逻辑计算内容的边界提供了新的视角。
4. 方法论启示：文章强调了在分析经典逻辑的证明和语义时，必须超越简单的“对手策略”视角，深入考察交互序列的几何结构和回溯机制的深层逻辑含义。

综上所述，本文通过两个精妙的注记，不仅致敬了 Stefano Berardi 的学术思想，也推动了经典逻辑博弈语义和实现性理论的发展，指出了当前基于连续性的语义解释的边界，并提出了向超限交互和更复杂结构分析发展的方向。