DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments

TL;DR

This paper presents a formally verified constructive proof of the consistency of Peano Arithmetic, based on Gentzen's original proof and formalized in Coq, ensuring rigorous correctness and detailed formalization.

Contribution

It provides the first fully formalized, constructive proof of Peano Arithmetic's consistency using ordinal assignments in Coq, improving on previous non-verified or non-constructive approaches.

Findings

Verified the well-foundedness of the cut-elimination argument

Formalized Gentzen's consistency proof in Coq

Enhanced the rigor of proof verification in foundational mathematics

Abstract

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\"{o}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