A Computability Proof of Gödel's First Incompleteness Theorem

“Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e. there are statements of the language of F which can neither be proved nor disproved in F.”

Gödel’s 1931 paper containing the proof of his first incompleteness theorem is difficult. It is 26 pages long, contains 46 preliminary definitions and several important propositions which are presented in a highly formal way (Nagel & Newman, 2001). Gödel’s proof had to be this long, because it was formulated before the establishment of the general theory of computability (Turing, 1936; Church, 1936) and so the general concept of a formal system had indeed yet to be formulated (Franzen, 2005).

Gödel hence instead proved his incompleteness theorem for a formal system of his own making, P, and argued that it contained properties shared by a wide class of systems. Utilizing Turing and Church’s invention of computability, with the help of the late, great Torkel Franzén (2005) we can devise the sketch for a computability proof of Gödel’s incompleteness theorem that is equally as strong as Gödel’s version, but much easier to deduce. Continue reading