Operational Evidence and Incompleteness: A Minkowski Radar Model

技术摘要：操作性证据与不完备性：一个闵可夫斯基雷达模型

问题陈述
本文探讨了计算理论与操作物理学交集领域的一个基础性问题：一个有效理论是否能对关于“有限测量记录不存在”的断言做出确定性的判定？具体而言，作者研究了一个形式系统能否在不存在有限验证记录的情况下，判定一个物理配置是否满足严格的距离界限（例如，$1 < d < 2$）。其核心矛盾在于：尽管每一个具有固定精度的测量协议都会终止（产生一个有限记录），但“在所有精度下都不存在成功记录”这一命题本身可能是不可判定的。

方法论
作者构建了一个“闵可夫斯基雷达模型”，旨在将标准的计算障碍操作化。其方法论如下：

1. 雷达设置： 在闵可夫斯基时空中（设 $c=1$）放置一个单一的惯性观测者（$P$）和一个静止反射器。观测者在固有时间 $\tau_-$ 发射光脉冲，脉冲经目标反射后在 $\tau_+$ 返回。距离 $d$ 由往返时间定义：$d = (\tau_+ - \tau_-)/2$。
2. 计算编码： 根据图灵机 $\Phi_e(0)$ 的停机行为，为给定的问题索引 $e$ 编码距离 $d_e$。
   • 如果 $\Phi_e(0)$ 在第 $h_e$ 步停机，则距离设定为 $d_e = 1 + 2^{-h_e}$。
   • 如果 $\Phi_e(0)$ 永不停机，则距离设定为 $d_e = 1$。
   • 因此，$1 \leq d_e \leq 1.5$。条件 $1 < d_e < 2$ 成立当且仅当 $\Phi_e(0)$ 停机。
3. 逼近协议： 定义了一个一致可计算的有理数逼近族 $q(e, k)$。通过模拟 $\Phi_e$ 至第 $k$ 步，协议生成一个区间 $J_{e,k} = [q(e, k) - 2^{-k}, q(e, k) + 2^{-k}]$。
   • 如果机器停机，足够大的 $k$ 会产生一个完全位于 $(1, 2)$ 内部的区间，从而证明该距离界限。
   • 如果机器永不停机，每一个区间 $J_{e,k}$ 都包含 1，从而无法证明严格界限 $1 < d_e < 2$。
4. 证书系统： 定义一个“有限证书”为记录 $(e, k, L, H)$，其中计算出的区间 $[L, H]$ 是 $(1, 2)$ 的有效子区间。论文证明了存在此类证书的索引 $e$ 的集合是递归可枚举（RE）的。

核心贡献

• RE-完备性的操作实现： 本文证明了对于严格界限 $1 < d_e < 2$ 的有限雷达验证记录的存在性是 RE-完备的。这直接将抽象的停机问题映射到了涉及基于时钟距离标准的物理测量场景中。
• 缺失陈述的形式化： 作者将“缺失陈述”（即断言不存在验证记录）形式化为 $\Pi^0_1$ 句子。论文证明，虽然记录的存在性是 RE 的，但 true 缺失陈述的集合对应于停机集的补集，而该补集不是 RE 的。
• 雷达模型的不可判定性定理： 本文建立了一个结论：对于任何对这些雷达缺失陈述及其否定形式均满足可靠性（sound）的有效理论 $T$，都存在无穷多个真实的缺失陈述（即机器永不停机的情况），而 $T$ 无法证明这些陈述。此外，由于可靠性，$T$ 也无法反驳它们。

结果

• 终止与可判定性： 在固定的精度 $k$ 下，每一个具体的测量协议都会终止并产生结果。然而，关于特定 $e$ 是否存在验证记录的“全局”问题是不可判定的。
• 缺失的可判定性： 如果理论 $T$ 是可靠的，它无法判定无穷多个关于“不存在有限测量记录能证实该界限”的真实陈述的真假值。这是因为停机集的补集不是递归可枚举的。
• 距离的有理性： 所有构建的距离 $d_e$ 均为有理数。然而，一个能够从索引 $e$ 中恢复 $d_e$ 精确有理值的算法将解决停机问题，而这是不可能实现的。

意义与主张
本文声称提供了一个“标准计算障碍的简单雷达实现”。其意义在于弥合了抽象计算理论与操作物理学之间的鸿沟：

• 它澄清了“终止测量程序”与“在所有精度下实现成功细分”之间的区别。
• 它断言，不完备性并非源于测量精度的物理限制，而是源于验证“记录之不存在”的逻辑结构。
• 作者明确指出，这是一个数学模型；关于如何准备此类物理配置或如何校准测量以提供所需的包围（enclosures）的问题，属于开放性问题。其结论严格限于该模型内的“认证极限”：即使每一个单独的尝试都会终止，没有任何可靠的有效理论能解决所有“不存在验证记录”的实例。