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
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
Memos and Talks