Advisors: Dominik Kirst and Moritz Weber
The goal of this thesis is to formalise Peano Arithmetic in the proof assistant Coq. Once achieved, further topics like incompleteness, models of PA, Tennenbaums theorem or self-verifying theories can be explored.
Using the undecidability of diophantine equations as a starting point, I establish undecidability of validity for Peano Arithmetic.
Tennenbaum's theorem is a result in the model-theory of Peano arithmetic, stating that no recursive non-standard model exists. In my master thesis I look at classical proof and reconsider it from the perspective of a constructive logic which includes Markov's principle and a version of Church's thesis.