DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911474673254400 |
|---|---|
| author | Bryce, Aaron Gore', Rajeev |
| author_facet | Bryce, Aaron Gore', Rajeev |
| contents | Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of
mathematics. We provide here a modified version of the proof, based on Gödel's reformulation, and including additional
details and minor corrections which are necessary to definitively prove the well-foundedness of the cut-elimination argument in
a constructive environment. All results have been verified using the Coq theorem prover.
NOTE TO READERS 26 February 2026: this is a draft which we had intended to submit to the Journal of Automated Reasoning with no particular time-line in our minds as the work was completed as part of Aaron's honours project at ANU in 2023. For that reason, we have used the Springer style files. We are putting it on arxiv as there appears to be some interest in this work as indicated by a post to
https://proofassistants.stackexchange.com/questions/6462/how-far-is-gentzens-consistency-proof-of-peano-arithmetic-from-being-formalized
in early February 2026. The Coq code is available here: https://github.com/aarondroidbryce/Gentzen/tree/master |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_00487 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments Bryce, Aaron Gore', Rajeev Logic in Computer Science Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on Gödel's reformulation, and including additional details and minor corrections which are necessary to definitively prove the well-foundedness of the cut-elimination argument in a constructive environment. All results have been verified using the Coq theorem prover. NOTE TO READERS 26 February 2026: this is a draft which we had intended to submit to the Journal of Automated Reasoning with no particular time-line in our minds as the work was completed as part of Aaron's honours project at ANU in 2023. For that reason, we have used the Springer style files. We are putting it on arxiv as there appears to be some interest in this work as indicated by a post to https://proofassistants.stackexchange.com/questions/6462/how-far-is-gentzens-consistency-proof-of-peano-arithmetic-from-being-formalized in early February 2026. The Coq code is available here: https://github.com/aarondroidbryce/Gentzen/tree/master |
| title | DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.00487 |