Advisor: Dominik Kirst
Gödel published his groundbreaking first incompleteness theorem in 1931, stating that a large class of formal logics admits independent sentences which are neither provable nor refutable. This result, in conjunction with his second incompleteness theorem, established the impossibility of resolving Hilbert's program, which proposed a possible path towards a single formal system unifying all of mathematics. Gödel's incompleteness result was strengthened further by Rosser in 1936 regarding the conditions imposed on the formal systems.
Computability theory, which also originated in the 1930s, was quickly applied to formal logics by Turing, Kleene, and others to yield incompleteness results similar in strength to Gödel's original theorem, but weaker than Rosser's strengthening. These proofs have become folklore in computer science. Kleene later found a stronger proof of incompleteness using computability theory, yielding an incompleteness result as strong as Rosser's, which is, however, much lesser-known than the folklore proof.
In this thesis, we work in constructive type theory to reformulate Kleene's incompleteness results abstractly in the setting of synthetic computability theory, assuming a form of Church's thesis which internalises the fact that all functions in such a setting are computable. This extremely succinct reformulation showcases the simplicity of the computational argument while staying formally entirely precise, a combination hard to achieve in typical textbook presentations. As an application, we instantiate the abstract result to first-order logic to derive essential incompleteness of Robinson arithmetic.
This thesis is accompanied by a Coq mechanisation including all mentioned results and based on existing libraries of undecidability proofs and first-order logic.
As a part of my bachelor's thesis, I: