标准图灵模型中统一认证的局限性——语义不变量与可接受方法
Limits of Uniform Certification in the Standard Turing Model -- Semantic Invariants and Admissible Methods
浏览论文内容
中文总结 AI 辅助
研究标准图灵模型中统一证明生成方法的结构局限，将可接受方法形式化为生成器-验证器对，通过赖斯定理揭示对非平凡语义不变量认证的约束，应用此框架于相关语义不变量，表明标准模型中不存在统一可接受方法认证它们。
中文摘要 AI 辅助
本文不探讨P与NP的数学真值，而是识别标准图灵模型中统一证明生成方法的结构局限性。该观察是模型理论的，关乎语义不变量与句法验证的交互，而非复杂性陈述的可证性。我们将可接受方法形式化为生成器-验证器对，为每个程序生成有限证书以确立语义属性。可接受性迫使生成器-验证器组合在被认证的不变量方面表现一致。在标准模型中，这种统一语义认证隐含地为属性诱导出一个决策过程。赖斯定理表明，对于非平凡语义不变量，这种隐含行为无法实现，揭示了形式认证的结构约束。理解这一点需要元计算视角：障碍源于认证诱导的计算行为，而非属性的复杂性理论状态。我们将此框架应用于与P对NP的形式认证及密码学硬度假设（特别是单向函数）自然相关的两个语义不变量。两者都受同一局限性：在标准模型中，不存在能认证它们的统一可接受方法。文中提供了完整的Coq形式化，捕捉了可接受方法的外延结构以及结果背后的语义-句法交互。
英文摘要
This work introduces a general obstructional framework, the "Double Bind," exposing intrinsic structural limitations of formal verification across computational complexity, mathematical physics and broader theoretical domains. Structurally, it operates as a nested case-switch mechanism: its two primary branches (horns) never activate simultaneously, nor are both guaranteed to trigger, while the first contains a nested switch where exactly one specific case is activated. We demonstrate how the expectation of a formally verifiable proof regarding SAT solver complexity (e.g., via Coq) conflicts with the fundamental limits of computation. While this suggests the logical undecidability of the P vs NP problem, the Double Bind framework resolves the apparent paradox. This obstruction encompasses all standard complexity barriers, such as relativization, natural proofs, and algebrization, while fundamentally blocking a vast class of potential future proof strategies not covered by traditional limitations. To establish its universality, we derive a second formulation via a prefix-closure topology on Deterministic Turing Machine programs and Kolmogorov complexity. This leads to the "Principle of General Non-Measurability," proving that such computational double binds stem from a deep, invariant geometric structure. We show that this framework governs a wide class of foundational limits, analyzing its implications across Geometric Complexity Theory (GCT), the certification of the Langlands program, cryptography, and the theoretical boundaries of quantum supremacy. Finally, we expose a hidden, correlated assumption within the theory of one-way functions. Given the subtle architecture of the framework, the introductory sections provide an essential narrative disambiguation to explicitly separate it from conventional misapplications of Rice's theorem.
