Formally Verifying Peano Arithmetic

This work is concerned with implementing Gentzen’s consistency proof in the Coq theorem prover. In Chapter 1, we summarize the basic philosophical, historical, and mathematical background behind this theorem. This includes the philosophical motivation for attempting to prove the consistency of Peano arithmetic, which traces itself from the first attempted axiomatizations of mathematics to the maturation of Hilbert’s program. We introduce many of the basic concepts in mathematical logic along the way: first-order logic (FOL), Peano arithmetic (PA), primitive recursive arithmetic (PRA), Gödel's 2nd Incompleteness theorem, and the ordinals below ε0. In Chapter 2, we give a detailed exposition of one version of Gentzen’s proof. Gentzen himself gave many similar proofs of the consistency of PA, as did several others after him; we describe the version given in Mendelson [20]. In comparison to the latter, our formulation fills in many erstwhile omitted details that we feel the reader deserves to see spelled out. We also have made other minor rearrangements, but altogether have found little to improve on that classic work of exposition. Chapter 3 is a detailed walkthrough of our present 5000-line implementation, with each section corresponding to the 11 sections of our code. There were three main conceptual challenges to implementing the chapter 2 proof: properly defining the ordinals below ε0 and proving their basic properties, defining PAω’s proof trees in a streamlined way, and defining the proof tree transformation operations discussed in section 2.4. We have successfully addressed these problems, as discussed in sections 3.2, 3.8, and 3.9 respectively. Our implementation is still incomplete as of this writing, but we substantiate our claim that the remaining work is largely routine. In our concluding chapter, we consider the likely future directions of this work, and discuss its place in the current literature.