Marc Hermes: Master’s Thesis

Saarland University Computer Science

Formalisation of PA in Coq

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.

Undecidability of PA

Using the undecidability of diophantine equations as a starting point, I establish undecidability of validity for Peano Arithmetic.

Tennenbaum's Theorem in Constructive Type Theory

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.

Legal notice, Privacy policy