Gödel’s Incompleteness Theorems
In this second article, we will take up the topics presented in the previous publication and focus on the actual proof of Gödel's Incompleteness Theorems—one of the most important mathematical achievements of the 20th century.
Recap: Recursion and Gödelization
In the previous article, we introduced the concepts of recursion and Gödelization. The former is of fundamental importance to the later Theory of Computation, which did not yet exist as an independent discipline in 1931, because it allows certain mechanical and effective operations to be described formally.
Primitive recursive functions are closely related to the finitistic procedures employed by Hilbert’s school. However, they should not simply be identified with the entirety of Hilbertian finitism, whose exact scope is a more complex historical and philosophical question. Hilbert’s Program sought to prove the consistency of Arithmetic and other mathematical theories by relying exclusively on elementary and secure methods.
The second concept, Gödelization, is the key to Gödel’s argument, since it is the tool that makes it possible to construct a numerical reflection of the formal system under study. Symbols, formulas, and proofs come to be represented by natural numbers.
The combination of these two tools will make it possible to translate certain metamathematical statements—statements about formulas and proofs—into arithmetic relations expressible within the system itself.
Incompleteness Theorems and Metamathematics
The Incompleteness Theorems do not arise merely from constructing a self-referential sentence. Their proof depends on the formal system’s ability to represent, by means of arithmetic formulas, properties such as “being a formula,” “being a correct proof,” or “being a provable formula.”
Gödel thus enables an arithmetic theory to speak indirectly about its own expressions. Metamathematics, which in Hilbert’s Program studied formal systems from the outside, becomes partially represented within Arithmetic itself.
Formal System
The formal system from which Gödel begins, which he calls \(P\), is based on the theory of types of Russell and Whitehead’s Principia Mathematica, enriched with axioms and resources sufficient to develop the Arithmetic of the natural numbers.
It is not simply the unmodified Principia Mathematica. Gödel defines a specific system that combines a hierarchy of types with arithmetic axioms similar to Peano’s. Within it, the natural numbers, their fundamental operations, and the arithmetic relations required for the proof can be represented.
This is very important, since the Incompleteness Theorems apply to formalized systems containing sufficient resources to express an elementary part of Arithmetic. As we have seen since Frege, the foundation of numbers is a far more complex matter than it may initially appear.
The proof is not restricted to the system \(P\). It extends to any theory satisfying certain conditions: it must be effectively axiomatized, capable of representing the relevant primitive recursive relations, and contain a sufficient amount of elementary Arithmetic.
This includes, among other systems, Peano Arithmetic and stronger theories such as Zermelo–Fraenkel Set Theory, which can interpret Arithmetic within its own language.
Recursive Properties
Gödel numbers designate symbols, formulas, and sequences of formulas. We will use expressions such as \(r(x_{1},x_{2},\ldots,x_{n})\) to denote the arithmetic relations among these numbers that reflect syntactic properties of the formal system.
Thus, for example, a number \(x\) designates a variable of the formal system of type \(n\)—where “type” has the meaning given in Russell’s Theory of Types—when there exists a prime number \(p\), greater than \(13\), such that \(x=p^{n}\):
$$\operatorname{Var}_{n}(x)\leftrightarrow\exists p\left[p>13\land\operatorname{Primo}(p)\land x=p^{n}\right]$$
This property is defined arithmetically. To verify it, one need only examine a finite number of possible divisors and determine whether \(x\) is a power of a prime greater than \(13\). Its metamathematical interpretation is: “\(x\) is the Gödel number corresponding to a variable of type \(n\).”
For example:
$$17=17^{1}$$
Therefore:
$$\operatorname{Var}_{1}(17)$$
The number \(17\) can thus be interpreted as the code of an individual variable, or a variable of the first type.
Gödelizing Sequences
Gödelization allows us not only to create an arithmetic reflection of each symbol and each formula, but also to represent general properties of sequences of formulas. This enables us to define relations such as “\(x\) is the Gödel number of a proof whose final formula has Gödel number \(y\)” or “\(z\) is the result of substituting a certain numeral for the variable \(x\) in a formula.”
These quoted statements are metamathematical interpretations. The relations themselves are defined by means of arithmetic properties of numbers.
We will denote by:
$$\operatorname{Prf}_{P}(x,y)$$
the relation “\(x\) is the Gödel number of a valid proof in \(P\) whose final formula has Gödel number \(y\).”
This relation is primitive recursive in Gödel’s system. Given a particular number \(x\), we can determine in a finite number of steps whether it encodes a sequence of formulas, whether each formula is an axiom or follows by an allowed rule, and whether the last formula has code \(y\).
Factoring \(x\) is not enough: after recovering the encoded sequence, it is necessary to verify the correctness of each of its steps. But this entire procedure can be carried out effectively.
Some recursive definitions represent concatenation operations. For example, a function \(\operatorname{Neg}(x)\) may return the Gödel number of the formula obtained by placing the symbol \(\neg\) before the formula encoded by \(x\).
Metamathematics
In summary, Gödelization allows us to transform formulas and sequences of formulas into numbers, while recursion allows us to define decidable arithmetic relations and operations among those numbers that can be interpreted as syntactic relations and operations.
The proof of the Incompleteness Theorems depends on numerous relations of this kind. Many of them are complex and technically tedious, so we will not develop them here. The example involving variables and the proof relation is sufficient to understand the general procedure.
For any formula \(A\), we will use \(\ulcorner A\urcorner\) to denote its Gödel number externally. The numeral representing that number within the system will be:
$$\overline{\ulcorner A\urcorner}$$
This numeral is an expression of the arithmetic language formed using the symbol \(0\) and repeated application of the successor function:
$$s(s(s(\ldots s(0)\ldots)))$$
It is important to distinguish the Gödel number, which is a natural number considered from the metamathematical perspective, from the numeral by which that number is represented within the system.
First Incompleteness Theorem
The proof of the First Incompleteness Theorem involves constructing a sentence that, under its metamathematical interpretation, asserts its own unprovability.
It is neither a meaningless formula nor a paradox resembling Russell’s Paradox. It is a well-formed arithmetic sentence that states a certain property of natural numbers and that, thanks to Gödelization, can also be interpreted as a statement about its own provability.
Consistency and Completeness
To understand Gödel’s original formulation, we must distinguish between consistency and \(\omega\)-consistency.
A system \(P\) is consistent when there is no sentence \(A\) such that both \(A\) and \(\neg A\) are provable.
\(\omega\)-consistency requires more. There cannot be a formula \(A(x)\) such that the system proves each of the following individually:
$$A(0),\quad A(1),\quad A(2),\quad\ldots$$
for every specific numeral and, at the same time, proves:
$$\neg\forall x\,A(x)$$
Equivalently, it cannot prove \(\exists x\,B(x)\) while proving \(\neg B(n)\) for every specific numeral \(n\).
Every \(\omega\)-consistent system is consistent, but a consistent system need not be \(\omega\)-consistent.
As for completeness, a system is syntactically complete when, for every closed sentence \(A\) formulable in it, it can prove either \(A\) or \(\neg A\).
An inconsistent system proves every sentence and is therefore complete in this trivial sense. The relevant property is thus the completeness of a consistent system.
Recursion and Proof
Before presenting the First Theorem, Gödel proves a fundamental result, known as Proposition V of his paper: every recursive relation can be represented by a formula of the system \(P\).
This means that, given a recursive relation \(R(x_{1},\ldots,x_{n})\), there exists a formula \(\mathcal{R}(x_{1},\ldots,x_{n})\) such that, for every specific combination of natural numbers:
- if \(R(n_{1},\ldots,n_{n})\) is true, the system proves \(\mathcal{R}(\overline{n_{1}},\ldots,\overline{n_{n}})\);
- if \(R(n_{1},\ldots,n_{n})\) is false, the system proves \(\neg\mathcal{R}(\overline{n_{1}},\ldots,\overline{n_{n}})\).
Thus, the arithmetic relation \(\operatorname{Prf}_{P}(x,y)\) can be represented within \(P\) by a formula expressing that one number encodes a proof of the formula encoded by another number.
From this relation, we define the provability predicate:
$$\operatorname{Prov}_{P}(y)\equiv\exists x\,\operatorname{Prf}_{P}(x,y)$$
\(\operatorname{Prov}_{P}(y)\) means that there exists some number encoding a proof in \(P\) of the formula whose Gödel number is \(y\).
Checking whether a particular number encodes a particular proof is a decidable procedure. Determining whether some proof exists among an unlimited number of possible sequences is not, in general, a decidable problem.
Statement of the First Theorem
In its original formulation, the First Incompleteness Theorem states that, if the system \(P\) is \(\omega\)-consistent, there exists a sentence \(G\) such that neither \(G\) nor \(\neg G\) is provable in \(P\).
The result extends to other formalized systems whose axioms are effectively recognizable and that possess sufficient resources to represent elementary Arithmetic.
The modern formulation is stronger: every consistent, effectively axiomatized system expressive enough to develop an elementary part of Arithmetic is incomplete. This improvement is due to J. Barkley Rosser, who in 1936 eliminated the need to assume \(\omega\)-consistency.
Self-Reference
The construction of the sentence \(G\) relies on a diagonalization procedure. Suppose that a formula \(A(x)\) contains a single free numerical variable \(x\). Substitution allows us to introduce into it the numeral corresponding to the Gödel number of another formula.
It is not enough, however, to write \(A(\ulcorner A\urcorner)\) directly. The Gödel number is a metamathematical object, whereas the formula must contain its numeral. Moreover, we need to construct a formula that receives precisely its own code.
The procedure is now captured by the Diagonal Lemma: for any formula \(A(x)\) with one free variable, there exists a sentence \(G\) such that the system proves:
$$G\leftrightarrow A\left(\overline{\ulcorner G\urcorner}\right)$$
The sentence \(G\) is a fixed point of the property expressed by \(A\): it asserts of itself what \(A\) asserts of the Gödel number it receives as an argument.
Expressing Provability
We now apply the Diagonal Lemma to the property:
$$A(x)\equiv\neg\operatorname{Prov}_{P}(x)$$
This formula asserts that the expression whose Gödel number is \(x\) is not provable in \(P\).
The Diagonal Lemma therefore guarantees the existence of a sentence \(G\) for which \(P\) proves:
$$G\leftrightarrow\neg\operatorname{Prov}_{P}\left(\overline{\ulcorner G\urcorner}\right)$$
Under its metamathematical interpretation, \(G\) asserts:
“The sentence \(G\) is not provable in \(P\).”
This is not a literal translation of its arithmetic symbols, but the interpretation they acquire through the representation of the provability relation.
Epimenides and the Incompleteness Theorems
Throughout this series, we have examined some of the most famous paradoxes. Probably the most recognizable is the Epimenides Paradox, commonly paraphrased by the sentence “this sentence is false.”
Gödel’s construction bears a superficial resemblance to it, since both expressions seem to speak about themselves. But there is a fundamental difference. The liar sentence asserts its own falsehood and leads to a semantic contradiction. Gödel’s sentence asserts its own unprovability within a specific formal system.
The sentence \(G\) does not say “I am false,” but rather “there is no sequence of formulas in \(P\) that constitutes a proof of me.”
No paradox therefore arises. The coherent possibility is that \(G\) is true with respect to the natural numbers and yet is not provable in \(P\).
The Proof
Suppose first that \(P\) proves \(G\). Then there exists a specific proof of \(G\), whose Gödel number we may denote by \(n\):
$$\operatorname{Prf}_{P}\left(\overline{n},\overline{\ulcorner G\urcorner}\right)$$
Since the proof relation is correctly represented within the system, \(P\) can prove that \(n\) encodes a proof of \(G\). Therefore, it can prove:
$$\operatorname{Prov}_{P}\left(\overline{\ulcorner G\urcorner}\right)$$
But \(G\) asserts precisely the opposite:
$$\neg\operatorname{Prov}_{P}\left(\overline{\ulcorner G\urcorner}\right)$$
If \(P\) proved \(G\), it would prove both the existence and the nonexistence of a proof of \(G\). The system would be inconsistent.
Therefore, if \(P\) is consistent:
$$P\nvdash G$$
Now consider the possibility that \(P\) proves \(\neg G\). From the equivalence constructed by diagonalization, this is equivalent to proving:
$$\operatorname{Prov}_{P}\left(\overline{\ulcorner G\urcorner}\right)$$
That is:
$$\exists x\,\operatorname{Prf}_{P}\left(x,\overline{\ulcorner G\urcorner}\right)$$
However, by the consistency of \(P\), we know from the metamathematical perspective that no specific natural number encodes a proof of \(G\). For each numeral \(\overline{n}\), the system can verify:
$$\neg\operatorname{Prf}_{P}\left(\overline{n},\overline{\ulcorner G\urcorner}\right)$$
The system would be proving that none of the specific numerals represents a proof of \(G\), while at the same time asserting that some number does represent a proof of \(G\). This is precisely a form of \(\omega\)-inconsistency.
Therefore, if \(P\) is \(\omega\)-consistent:
$$P\nvdash\neg G$$
We conclude that, under the original condition of \(\omega\)-consistency, neither \(G\) nor its negation is provable in \(P\).
Consequences
Gödel’s original proof uses two different assumptions. Ordinary consistency is sufficient to show that \(G\) is not provable. The stronger condition of \(\omega\)-consistency additionally allows us to conclude that \(\neg G\) is not provable either.
Rosser would later modify the construction of the self-referential sentence to show that ordinary consistency alone is sufficient to obtain an undecidable sentence.
The modern conclusion of the First Theorem can be expressed as follows: every consistent, effectively axiomatized formal system sufficiently powerful to represent elementary Arithmetic contains sentences that it can neither prove nor refute.
The word undecidable is used here relative to a particular theory: neither the sentence nor its negation is a theorem of the system. It does not necessarily mean that no stronger theory can settle it or that the human mind is incapable of understanding it.
If \(P\) is consistent, the sentence \(G\) is true in the standard interpretation of the natural numbers. It asserts that there is no proof of \(G\) in \(P\), and the metamathematical argument has established precisely that no such proof exists.
Second Incompleteness Theorem
The Second Incompleteness Theorem builds on the preceding result, but it is not merely a repetition of it. A sufficient portion of the metamathematical argument used to construct \(G\) must be formalized within the system itself.
The system can represent its provability relation and express, by means of an arithmetic sentence, that no proof of a contradiction exists.
Statement of the Second Theorem
Let \(P\) be a consistent, effectively axiomatized system sufficiently powerful to represent elementary Arithmetic. The Second Incompleteness Theorem states that \(P\) cannot prove its own consistency, as expressed by the usual arithmetical formulation.
We can represent the consistency of \(P\) by the sentence:
$$\operatorname{Con}(P)\equiv\neg\operatorname{Prov}_{P}\left(\overline{\ulcorner 0=1\urcorner}\right)$$
This expression states that there is no number encoding a proof in \(P\) of the contradiction \(0=1\).
The theorem states:
$$P\nvdash\operatorname{Con}(P)$$
provided that \(P\) is in fact consistent and satisfies the technical conditions required to represent its provability predicate correctly.
Proof of the Second Theorem
The argument used to show that \(G\) is unprovable can be partially formalized within the system itself. \(P\) can prove that, if there is no proof of a contradiction, then there is no proof of \(G\):
$$P\vdash\operatorname{Con}(P)\rightarrow G$$
The intuition is as follows: if \(G\) were provable, then the statement that \(G\) is provable would also be provable; but \(G\) asserts that it is not. A contradiction could therefore be obtained from a proof of \(G\).
Now suppose that \(P\) could prove its own consistency:
$$P\vdash\operatorname{Con}(P)$$
Since the system also proves \(\operatorname{Con}(P)\rightarrow G\), by modus ponens we would obtain:
$$P\vdash G$$
But the First Theorem establishes that, if \(P\) is consistent, \(G\) cannot be provable. Therefore, a consistent system cannot prove its own consistency.
Conclusion of the Second Theorem
The theorem does not state that proving the consistency of a system is impossible. It prevents a sufficiently powerful system from proving its own consistency through its usual arithmetical formulation, assuming that the system is in fact consistent.
A stronger theory \(P^{+}\) may prove the consistency of a weaker theory \(P\). But if \(P^{+}\) satisfies the conditions of the Incompleteness Theorems, it will be unable to prove its own consistency:
$$P^{+}\nvdash\operatorname{Con}(P^{+})$$
We can successively construct stronger and stronger theories by adding consistency principles, but each new system will raise a new question about the legitimacy of its own axioms.
This does not lead to a contradiction or show that all mathematical justification is impossible. It shows that, under the conditions of the theorem, there can be no final internal justification of the entire system using the same resources that the system is intended to legitimize.
Conclusion of the Incompleteness Theorems
The publication of the Incompleteness Theorems left no one indifferent, although views about their consequences varied from one author to another. John von Neumann quickly understood that the results imposed a decisive limitation on Hilbert’s Program.
Gödel himself was initially less conclusive. His theorems did not by themselves show that no revised form of the formalist program could survive. Hilbert’s original requirement was to provide a finitistic proof of the consistency of Arithmetic. The Second Theorem established that a proof of the consistency of Arithmetic could not be fully formalized within the theory itself, assuming that the theory was consistent.
The decisive question was therefore whether the finitistic methods accepted by Hilbert could be represented within the arithmetic system under study. If so, the expected finitistic proof would be ruled out by the Second Theorem. This is the interpretation that ultimately prevailed with respect to the original program.
A few years later, Gerhard Gentzen presented a proof of the consistency of Peano Arithmetic. His proof used transfinite induction up to the ordinal \(\varepsilon_{0}\), a principle exceeding the strict finitistic methods Hilbert had hoped to employ.
Gentzen’s result does not contradict the Second Theorem: the proof relies on resources that cannot be fully formalized within the Peano Arithmetic whose consistency it seeks to establish.
Hilbert’s original program could not be completed on the terms originally envisaged. Proof Theory did not, however, disappear. It developed into a field devoted to comparing the strength of formal systems, studying which principles are required to prove their consistency, and analyzing the different forms of mathematical reasoning.
Philosophical Consequences of the Incompleteness Theorems
As for the philosophical impact of these theorems, Gödel himself had a deep interest in philosophy, and much of his writing addresses this subject. The issue is so vast that we will not develop it here. We will simply leave the reader with a reflection by Gödel himself, written several decades after the publication of the Incompleteness Theorems.
– My theorems only show that the mechanization of mathematics, that is, the elimination of the mind and of abstract entities, is impossible if one wishes to have a satisfactory foundation and system of mathematics. I have not proved that there are mathematical questions undecidable for the human mind, but only that there is no machine (or blind formalism) capable of deciding every number-theoretical question (even of a very special kind). Likewise, it does not follow from my theorems that there are no convincing consistency proofs for the usual mathematical formalisms, although such proofs must use modes of reasoning not contained in those formalisms.
What is practically certain is that, for the classical formalisms, there are no conclusive combinatorial consistency proofs (such as those Hilbert hoped to provide), that is, no consistency proofs using only concepts referring to finite combinations of symbols and making no reference to any infinite totality of such symbols. –
– Kurt Gödel. Letter to Leon Rappaport (1962).
The Incompleteness Theorems do not prove that the human mind is superior to every machine or that there are truths no human being can know. Nor do they state that all mathematical theories are incomplete. They apply to effectively axiomatized, consistent systems sufficiently powerful to represent Arithmetic.
Their fundamental lesson is more precise: no formal system with these characteristics can simultaneously possess consistency, completeness, and the ability to prove its own consistency using its own resources.
Formalization allows proofs to be transformed into mathematical objects and subjected to exact analysis. Yet that very analysis reveals that every sufficiently expressive system encounters limits it cannot overcome from within.
Recommended Reading
– Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.
– Gödel, K. (2006). Collected Works. Edited by Jesús Mosterín.
– Nagel, E. and Newman, J. R. (1958). Gödel’s Proof.
– Smullyan, R. M. (1992). Gödel’s Incompleteness Theorems.
