Janis Bailitis: Bachelor's Thesis
Löb's Theorem in Coq
Advisors: Yannick Forster and Dominik Kirst
Summary
Löb's Theorem for Peano arithmetic (PA) states that, when proving a sentence, we can assume a sentence expressing internal provability of it. This result was shown by Martin Löb in 1955, solving a problem posed by Henkin in 1952, and yields Gödel's Second Incompleteness Theorem as a corollary. In its general form, it concerns sufficiently strong formal systems of first-order logic, assuming provability being expressed by a particular formula. To derive the result in an abstract way, it suffices to show that provability obeys a fixed set of axioms. We define a formula expressing provability in PA, usually a process requiring much formal detail, by employing a variant of Church's Thesis, stating that any function on natural numbers can be represented by a formula in PA, enabling us to abstract over many technical details, and investigate which of Löb's axioms already hold in this setting. To derive one of the axioms, we show Gödel's Diagonal Lemma, from which we derive both Tarski's Indefinability Theorem and Gödel's First Incompleteness Theorem as by-products.
References
Resources
A memo on the current state is available here.
Legal notice, Privacy policy
