标准图灵模型中统一认证的局限性——语义不变量与可容许方法

本文不讨论P与NP的数学真理性。相反，它识别了标准图灵模型中统一证明生成方法的结构性局限。该观察是模型论的：它关注语义不变量与句法验证之间的相互作用，而非复杂性断言的证明性。我们将可容许方法形式化为一个生成器-验证器对，它为每个程序生成一个建立语义属性的有限证书。可容许性迫使生成器-验证器组合相对于被认证的不变量统一行为。在标准模型中，这种统一的语义认证隐式地诱导了该属性的决策过程。Rice定理表明，对于非平凡的语义不变量，这种隐式行为无法实现，揭示了形式认证的结构性约束。理解这一点需要元计算视角：障碍源于认证所诱导的计算行为，而非属性的复杂性理论状态。我们将此框架应用于两个与P vs. NP的形式认证和密码学硬度假设（特别是一维函数）自然相关的语义不变量。两者都受到相同的限制：在标准模型中，没有统一的可容许方法可以认证它们。我们提供了完整的Coq形式化，捕获了可容许方法的外延结构以及支撑该结果的语义-句法相互作用。