Left: Kurt Gödel (ca 1925). Right: Alan Turing (ca 1935).

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

Jørgen Veisdal
Nov 27 · 12 min read

“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.


First, let us sketch an outline of what Gödel showed in his first incompleteness proof, courtesy of Ernest Nagel and James R. Newman’s wonderful book Gödel’s Proof:

Steps of Gödel's proof (Nagel & Newman, 2001)
In his proof, Gödel showed the following:
i) How to construct a formula G of Peano arithmetic (PA) that represents the statement: "The formula G is not demonstrable using the rules of Peano arithmetic"ii) That G is demonstrable if and only if its formal negation not-G is demonstrableiii) That although G is not formally demonstrable, it nevertheless is a true arithmetic statementiv) That since G is both true and formally undecidable within Peano arithmetic, Peano arithmetic must be incompletev) How to construct a formula A of Peano arithmetic that represents the statement "Peano arithmetic is consistent" and that the formula A ⊃ G is formally demonstrable inside Peano arithmeticvi) Finally, that the formula A is not demonstrable in Peano arithmetic

In order to construct the sketch for a computability proof which shows the same, we must first define a few necessary concepts. The following section is based on the chapter “Computability, Formal Systems, and Incompleteness” in Franzén (2005).

Numerical strings

Most of us are familiar with the term ‘string’ from computer science, a term traditionally used to describe any finite sequence of symbols. Numerical strings, in turn, may be used to describe strings used in mathematics to denote natural numbers (nonnegative integers) such as “0”, “13” or “125 239”. An alternative way of representing such natural numbers as strings is in binary notation, such that the three numbers above instead are expressed in the base-2 numeral system which uses only two symbols: “0”, “1101”, “11110100100110111”.

The set of numerical strings has two properties that are relevant to our investigation of Gödel’s incompleteness theorem (Franzen, 2005). They are:

  1. There must exist a mechanical procedure for generating numerical strings such as in the binary case, e.g first writing down the single digit strings 0 and 1, then the two-digits strings {00, 01, 10, 11}, then the three-digit strings {000, 001, 010, 100, 011, 110, 101, 111}, then the four-digit strings and so on.
  2. There must exist an algorithm that can decide whether or not, given any string of symbols, whether or not it will ever appear in a computable enumeration of the set. That is, there must exist a mechanism for determining whether or not a symbol appears in a numerical string.

Enumerability and Decidability

Sets of numerical strings have two properties that are of particular relevance to computability and incompleteness. They are enumerability and decidability:

A set E of strings is computably enumerable if it is possible to program a computer to compute and print out the members of E
A set E of strings is computably decidable if it is possible to program a computer to decide, given any string s of symbols, whether or not is in E.

To ask the questions of whether a set of strings is computably enumerable and/or decidable only makes sense if the set can be given a formal mathematical definition. That is, informally, it only makes sense if we know the rules that generated the members of the set. As such, the “set of all sentences in English” cannot be deemed either enumerable or decidable, as we cannot express formally how English sentences were and are generated by human beings in a sufficiently systematic way.

So, in order to progress, let us go about generating the sets of strings we are interested in for our purposes of proving the incompleteness of formal systems.

Gödel Numbering

Look down at your keyboard. Observe that the keys are arranged in a certain order, and so that every sentence you type can be represented by a numerical string of digits representing which key you pushed in which order. The length of the string corresponds to the length of what ever sentence you type.

From this outset, it should be trivial to observe that the property required above for generating numerical strings (enumerability) can be modified so as to generate all possible strings (Franzen, 2005). A Gödel numbering, introduced in his 1931 paper, is a way of representing arbitrary strings, not just numerical ones, by numbers. Formally,

A Gödel numbering is a function that assigns each symbol and a well-formed formula of some formal language a unique natural number called its Gödel number.

It is worth noting that this Gödel numbering is only one of an infinite ways of representing arbitrary strings (of symbols, letters, numbers etc) by numbers (Franzen, 2005). Also worth noting about the Gödel numbering in particular is that it satisfies two conditions:

  • Given any string, we can mechanically compute its Gödel number by generating strings and counting them until we find the string whose Gödel number we are looking for;
  • Given a number, vice versa, we can decide whether it is the Gödel number of a string we have generated, and if so, which one;

Examples of Gödel’s original encoding of symbols, letters and integers to Gödel numbers is included below in modern notation:

Odd Gödel numbers from 1–13, and their associated symbols, in modern notation

From his construction of Gödel numbering, we know that:

A set of strings is computably enumerable or decidable if and only if the set of Gödel numbers of strings in the set is computably enumerable or decidable.

That is, we can only tell whether a set of strings (representing e.g. words in a sentence) can be mechanically computed (are enumerable) and/or can be determined whether or not they belong to a given set (are decidable) if and only if, the set of Gödel numbers associated with the strings in the set are themselves enumerable (can be mechanically computed) and/or decidable (can be determined whether or not they belong to a given set).

Let us pause here and reiterate. Every sentence represented by symbols (such as letters), is representable by a unique string of (very large) numbers. The sets of strings representing every sentence in the English (or any other) language can only be mechanically computed, printed out and checked to belong to a given set if its corresponding Gödel numbers can also be mechanically computed, printed out and checked to belong to a given set.

We may in other words use Gödel numbers associated with sets of strings (such as sentences) to determine whether any sentence is computably enumerable and/or decidable. This is important.

Undecidable sets

Given that some sets of strings are decidable, it stands to reason that other sets of strings are not. To find them, let us first assert fundamental two properties of computably decidable sets (sets which can be computationally determined to either belong, or not belong to a set such as e.g. formal system) (Franzén, 2005):

  • Every computably decidable set is computably enumerable
  • A set E is computably decidable if and only if both E and its complement are computably enumerable

The first property can easily be derived from the definition of computable enumerability (if a set of strings is computably decidable, it is possible for a computer to determine whether or not it belongs to a given set, but for a computer to be able to do so, the members of the set it is comparing the string to must also hold the property that they can be produced mechanically by a computer).

The second property regards the complement of a set E, that is, all the strings which are not in set E. First, notice that if E is decidable, so is the complement of E (we can construct a set F of all the strings that are shown to not belong to E). As such, if the set E can be constructed by a mechanical process (is computably enumerable), so too must its complement.

Alan Turing and Alonzo Church in 1936 both independently proved that a general solution to the Entscheidungsproblem, what is now known as the undecidability theorem, is impossible, namely that

Undecidability Theorem (Turing, 1936; Church, 1936)
There are computably enumerable sets which are not computably decidable.

That is, there are strings of symbols which may be generated by a computer, but which we cannot determine whether or not belongs to a given set.

Formal systems

In mathematics, a formal system such as the Peano arithmetic (PA) Gödel’s paper is based around is based on a formal language, a set of inference rules and a set of axioms. Overall, the subset of the language which comprises its sentences is assumed to be decidable. The subset of the sentences, in turn, which comprises the axioms and its inference rules need to be defined in such a way that the formal system satisfies the following basic property of formal systems, namely that (Franzén, 2005):

The set of theorems of a formal system is computably enumerable

That is, the theorems which can be devised by a system of axioms and inference rules expressed by sentences in a formal language must also be mechanically computable by a computer. As such, by choosing the right axioms and inference rules, we can construct a formal system S which is decidable, and so show that the set of proofs in the system are also decidable. The property in other words implies that it is always possible to search for a proof of a given sentence of a formal system in a mechanical way, and that if such a proof exists, it will eventually be found and the computation will halt (be finite).

The First Incompleteness Theorem

“Corresponding to any given axiomatization of number theory, one can explicitly construct a Diophantine equation which as no solutions, but such that this fact cannot be proved within the given axiomatization”

The above (stronger) version of Gödel’s first incompleteness theorem can be derived from Matiyasevich’s theorem (sometimes referred to as the Matiyasevich-Robinson-David-Putnam theorem), which states that

Every computably enumerable set is Diophantine

That is, the set of strings which it is possible to program a computer to compute and print out the members of is expressible as a polynomial equation with integer coefficients and a finite number of unknowns which take integer values. Stated differently, Matiyasevich proved that (Franzén, 2005):

There is no algorithm that given any Diophantine equation will decide whether or not the equation has a solution

When announced in 1970, the result settled Hilbert’s Tenth Problem which asked for a general algorithm which for any Diophantine equation (a polynomial equation with integer coefficients and a finite number of unknowns) can decide whether the equation has a solution with all unknowns taking integer values.

That is, the proof showed that there cannot exist an algorithm that given any Diophantine equation D(x₁, x₂, … xᵢ) = 0 will decide whether or not the equation has a solution. The set of Diophantine equations is in other words undecidable (ref. Turing and Church’s undecidability theorem).

Implied by the proof, via our second stated property of undecidable sets above (“A set is computably decidable if and only if both and its complement are computably enumerable”) is that its negation, “the Diophantine equation D(x₁, x₂, …. xᵢ) = 0 has at least one solution” is also undecidable. This because, if not, given a formal system S, we could decide whether or not a given Diophantine equation D(x₁, x₂, …. xᵢ) = 0 has a solution by systematically searching for a proof in S of either the statement “the Diophantine equation D(x₁, x₂, …. xᵢ) = 0 has at least one solution” or its negation, and in this way construct the set of all Diophantine equations with solutions. The algorithm conducting this search would violate Matiyasevich’s result that such an algorithm cannot exist.

Gödel’s First Incompleteness Theorem

Suppose S is a formal system that contains enough arithmetic to be able to prove all true statements of the form (Franzén, 2005)

D(x₁, x₂, …. xᵢ) = 0 has no solution

If S is consistent, every such theorem of S is true. That is, if there are no statements A such that both A and not-A are provable in S, then every such theorem of S is true. The set of all equations for which it is provable in S that they have no solution is a computably enumerable subset of the equations that do not have a solution (Franzén, 2005).

However, since the latter is not computably enumerable (i.e. the subset of equations D which can be proven not to have solutions cannot be computed by a mechanical process), it follows that there are infinitely many equations D(x₁, x₂, …. xᵢ) = 0 which have no solution, but which we cannot prove have no solutions (the remainder of the set of equations D that have no solutions must exist).

As such, our formal system S must be incomplete, since it is not sufficiently strong to prove all theorems derivable from its axioms and inference rules.


Gödel’s 1931 paper which includes his first incompleteness result is entitled Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (“On Formally Undecidable Propositions of Principia Mathematica and Related Systems”). Although occupying dozens of pages (26 to be exact), Gödel’s paper is based on a remarkably simple idea, namely that (Sigmund, 2017):

"In any formal system, mathematical statements are simply strings of symbols. Gödel found a systematic way of turning any such string into a unique integer. The given string of symbols determined its integer uniquely, and vice versa - given a large integer, if it represented a string of symbols, then that string was uniquely determined."

As Whitehead and Russell’s momentous Principia Mathematica and indeed, any complete formal system, including its proofs, must be constructed systematically, Gödel noticed that one could essentially represent any formal system as integers.

"Thus for any theorem there was a theorem-number that could be defined in terms of addition, multiplication, and other mathematical operations. Therefore, provability of a string in a formal system corresponded to a purely mathematical property of a very large number, and this property could be talked about using the notation of Principia Mathematica."

Just as one might assert of a number N that it has properties such as being a square, the square root, a cube or a prime number, and use such properties to construct proofs for various conjectures, one can also assert of a number N that it is a theorem number (i.e. that it represents strings of letters, symbols and integers which show that stated assumptions logically guarantee a conclusion to a proposed conjecture).

"Gödel's coup de grâce was the construction of a special mathematical proposition G that asserted that a certain string having Gödel number g is unprovable - meaning that it cannot be formally derived from the system of axioms of Principia Mathematica. And astonishingly, Gödel managed to arrange things so that the integer g was precisely the Gödel number of the statement G ("somewhat fortuitously", as he slyly noted)."- Excerpt, "Exact Thinking in Demented Times" by Karl Sigmund (2017)

Those interested in further investigating the nature of Gödel’s incompleteness results are encouraged to obtain the book Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse by Torkel Franzén (2005) and the book Computability: Turing, Gödel, Church and Beyond, edited by Copeland, Pose and Shagrir (2015).

This essay is part of a series of stories on math-related topics, published in Cantor’s Paradise, a weekly Medium publication. Thank you for reading!

Cantor’s Paradise

Medium’s #1 Math Publication!

Jørgen Veisdal

Written by

Editor-in-Chief at Cantor’s Paradise. Research fellow at the Norwegian University of Science and Technology.

Cantor’s Paradise

Medium’s #1 Math Publication!

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade