机械化哥德尔不完备定理与可证性逻辑
Mechanizing Gödel's Incompleteness Theorems and Provability Logic
发表机构东北大学 · 神户大学
查看机构详情
- Tohoku University（东北大学）
- Kobe University（神户大学）
机构由 AI 辅助整理，请以论文原文为准。
首次发表
浏览论文内容
中文总结 AI 辅助
该研究在Lean 4中形式化验证了哥德尔不完备定理及可证性逻辑GL的Solovay完备性，为数学基础提供机器证明。
中文摘要 AI 辅助
我们在Lean 4定理证明器中机械化证明了哥德尔第一和第二不完备定理、\u000bGL的Solovay算术完备性定理及相关结果。
英文摘要
We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.
