不正确/不完整证明的证明论分析
Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
浏览论文内容
中文总结 AI 辅助
本文基于希尔伯特epsilon演算，形式化分析不正确或不完整证明的语义修复机制，提出通过语义投影和最弱前置条件修正推导，并证明扩展的第一epsilon定理具有虚假容忍性。
中文摘要 AI 辅助
我们研究了不正确/不完整证明的证明论结构，即包含语法错误或不完整推理步骤、但仍保持部分语义有效性的推导。基于希尔伯特的epsilon演算，我们形式化了此类推导如何通过语义投影和最弱前置条件进行修正，从而得到有效的Herbrand析取。我们表明，epsilon演算为分析证明中虚假容忍性以及识别不正确证明可被语义修复的条件提供了自然框架。该方法将希尔伯特纲领扩展到正确性之外，朝向一种错误与恢复的逻辑。此外，我们证明了扩展的第一epsilon定理是虚假容忍的。
英文摘要
We investigate the proof-theoretic structure of incorrect/incomplete proofs, that is, derivations containing syntactic errors or incomplete inferential steps that nonetheless preserve partial semantic validity. Building on Hilbert's epsilon calculus, we formalize how such derivations can be corrected through semantic projection and weakest preconditions, leading to valid Herbrand disjunctions. We show that the epsilon calculus provides a natural framework for analyzing tolerance of falsity in proofs and for identifying conditions under which an incorrect proof can be semantically repaired. This approach extends Hilbert's program beyond correctness, toward a logic of error and recovery. Moreover we show that the extended first epsilon theorem is false-tolerant.
发表机构
- Technische Universität Wien（维也纳工业大学）
机构由 AI 辅助整理，请以论文原文为准。
