DRAFT：一种使用序数赋值经形式验证构造性证明皮亚诺算术一致性的方法
计算机科学中的逻辑
2026-03-03 v1
摘要
Gentzen 于1936年对皮亚诺算术一致性的证明是数学基础领域的重要成果。我们在此提供该证明的修订版本，基于Gödel的改进版本，并包括额外的细节和微小的纠正，这些都是为在构造性环境中确切证明cut消除论证良-founded性所必需的。所有结果均已使用Coq定理证明器进行验证。给读者的说明2026年2月26日：这是一份草稿，最初计划提交给Journal of Automated Reasoning，但当时并无特定时间表，因为该工作是在2023年阿瑟顿的项目中完成的。因此，我们使用了Springer样式文件。我们将其放在arxiv上，因为似乎有人对这项工作感兴趣，如下所述：https://proofassistants.stackexchange.com/questions/6462/how-far-is-gentzens-consistency-proof-of-peano-arithmetic-from-being-formalized 于2026年2月初。Coq代码可在此处获取：https://github.com/aarondroidbryce/Gentzen/tree/master
关键词
引用
@article{arxiv.2603.00487,
title = {DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments},
author = {Aaron Bryce and Rajeev Gore'},
journal= {arXiv preprint arXiv:2603.00487},
year = {2026}
}
备注
current draft as at 28 February 2026