Advisors: Yannick Forster and Dominik Kirst
Löb's theorem for Peano arithmetic (PA) states that, when proving a sentence, one can assume a sentence expressing provability of it. This result was shown by Löb in 1955, solving a problem posed by Henkin in 1952. In its general form, it concerns sufficiently strong formal systems of first-order arithmetic, assuming provability being expressed by a particular formula, which is called provability predicate. To derive the result in an abstract way, it suffices to show that the provability predicate obeys a set of axioms called Hilbert-Bernays-Löb derivability conditions.
Even for a fixed formal system, there are many different provability predicates of varying strengths, and not all qualify for Löb's theorem. Following Feferman's notions of extensionality and intensionality, we distinguish external provability predicates that characterise theorems of PA, and internal ones that, in addition, allow proving PA's deduction rules as object-level implications. To define an external provability predicate abstractly, we employ Church's thesis (CT) for arithmetic, which states that any function in a constructive setting can be represented by a formula in PA. Löb's Theorem requires internal provability, and we explain why one cannot define this - unlike external provability - abstractly using CT. To demonstrate that such an abstract perspective is nevertheless useful, we show Gödel's diagonal lemma using CT, from which we derive both Tarski's theorem as well as Gödel's first incompleteness theorem.
To define a candidate for an internal provability predicate - usually a tedious task - we extend the signature of PA by functions simplifying such a definition. We mechanise a large part of the correctness proof for this candidate, leaving one derivability condition called internal necessitation as further work. Based on an already fully mechanised internal provability predicate from Paulson's proof of Gödel's incompleteness theorems, we mechanise a proof of Löb's theorem.
All key results presented in this thesis are mechanised in the Coq proof assistant, based on existing libraries for first-order logic and synthetic computability. A small part is mechanised in Isabelle/HOL on top of Paulson's development. Not only do these tools assure error-free reasoning, proof assistants are also extremely helpful in organising large proofs, and they help to make informal arguments rigorous.