Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Aaron Bryce, Rajeev Gore'

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ö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

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

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ö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
Paper Structure (21 sections, 17 theorems, 1 figure)

This paper contains 21 sections, 17 theorems, 1 figure.

Table of Contents

  1. Introduction
  2. A Crisis of Foundations
  3. Incompleteness and Consistency
  4. Finiteness and Formalisation
  5. Components of Gentzen's Proof
  6. Hilbert Calculus for Peano Arithmetic
  7. Finitely Representable Ordinals
  8. The PA$_\omega$ Sequent Calculus
  9. Derivations in PA$_\omega$
  10. Law of the Excluded Middle with a Bound
  11. Connecting PA$_\omega$ and PA
  12. Gentzen's Proof Process
  13. Inverting Deductive Rules
  14. Gödel's Method
  15. Cut Elimination
  16. ...and 6 more sections

Key Result

Theorem 1

For any Hilbert calculus $L$, if $L$ contains Robinson Arithmetic and is consistent, then $L$ can not prove $Cons_{L}$godel.

Theorems & Definitions (59)

  • Theorem 1: Gödel's Second Incompleteness Theorem
  • Corollary 2
  • Corollary 3
  • Example 1: Relationship between the different logics in Gentzens proof
  • Definition 1: First-order logic axioms
  • Definition 2: Arithmetic axioms
  • Definition 3: The axiom schema for induction
  • Definition 4: Deductive rules of Peano Arithmetic
  • Definition 5: Standard Representation of the Ordinal Numbers
  • Definition 6: Ordinals as Nested Lists
  • ...and 49 more