Marc Hermes: Master’s Thesis

The goal of this thesis is to formalize Peano Arithmetic in the proof assistant Coq. Once achieved, further topics like incompleteness, models of PA, Tennenbaum's theorem or self-verifying theories can be explored.

Thesis: Modeling Peano Arithmetic in Constructive Type Theory

Advisors:Dominik Kirst and Moritz Weber

Abstract

Gödel's first incompleteness theorem entails that the first-order theory
of Peano arithmetic (PA) and its consistent extensions admit a wealth of
independent statements. By the completeness theorem then, PA cannot be
categorical, meaning it does not posses a unique model up to isomorphism.
A theorem by Stanley Tennenbaum however tells us that if we restrict our
attention to computable models, first-order PA is categorical with regards
to this class of models.
In this thesis we develop the first-order theory of PA inside of a constructive
type theory to revisit and study Tennenbaum's theorem in this constructive setting.
This approach allows for a synthetic viewpoint of computability and we can
furthermore consistently assume Church's thesis, making it possible to farther
abstract from many details in computability arguments. As an additional result,
we establish the undecidability of PA via a reduction to the solvability of
Diophantine equations. Both parts have been verified in the Coq proof-assistant.

Thesis and Coq Code

My Thesis can be found here.
The Coq code for the undecidability of PA has been integrated into the Coq library of undecidability proofs.
The development on Tennenbaum's theorem can be explored here

Github

Memos and Talks

Memo on the Undecidability of PA
Memo on Tennenbaum's Theorem
Slides of the first talk I gave (also available with no animations)
Slides of the second talk
Slides of the final talk

Legal notice, Privacy policy