What Gödel showed was that any system of axioms capable of describing arithmetic, such as Peano’s axioms or Principia Mathematica, will always contain a well-formed statement that cannot be decided, making the system incomplete. This means that within these systems there exists a well-formed statement without free variables p such that neither p nor not p can be proved from the axioms. Not only this, but he gave an example of such a statement, and showed that this fact implies that these systems are incapable of proving their own consistency, and thus any proof of their consistency must rely on systems more complex than arithmetic, whose own consistency may be in doubt.
Gödel’s proof was written to a small group of specialists in a niche field of mathematics using completely novel methods of argument. It contains some difficult language. Here, before going into the details of the proof, we will go through some requisite definitions and concepts.
There are two types of logic necessary for our discussion, propositional logic and predicate logic. These are also known as zero-order and first-order logic, respectively. We will go through a formalization of them to familiarize ourselves with the symbols.
Propositional logic deals with statements, or propositions, and their combinations in arguments. Its utility is in the generalization of the forms of valid arguments. The relevant ideas and the symbols for them are as follows:
| And | ∧ |
| Or | ∨ |
| Not | ¬ |
| Implies | ⇒ |
| Ordering | “(” and “)” |
Some of these, however, are redundant. In the stead of p ∧ q, we can write ¬(¬p ∨ ¬q) (DeMorgan’s Laws). And for p ⇒ q we can write ¬p ∨ q (Material Implication). Thus we see that we can write any statement in propositional logic using only ¬, ∨, and the parentheses*. This simplification will become important when we go through Gödel’s proof.
Predicate logic extends propositional logic and enables us to talk not only about statements, but variables. It consists of what are called quantifiers, which allow for the quantification of variables. The relevant concepts and symbols for them are
| There Exists | ∃ |
| For All | ∀ |
We call ∃ the existential quantifier and ∀ the universal quantifier.
And yet again we are able to do away with a certain term. Instead of writing ∃ x(p) (there exists an x such that p is true), we can write ¬(x ∀ ¬p) (it is not the case that for all x, p is false). Thus we can make any statement in predicate logic using only the universal quantifier and the symbols from propositional logic.
An important fact about predicate logic is that every variable must be paired with a quantifier in order for the statement to be considered true or false. Consider the statement “x is prime”. Is that statement true or false? The correct answer is no; it is not true or false. We can, however, assign a truth value to the statements “∃ x (x is prime)” and “x ∀ (x is prime)” (these statements being true and false, respectively). When a variable is quantified it is called bound. When it is not bound it is called free. And when there exists a free variable in a statement we know the statement cannot be assigned a truth value, and thus cannot be proved nor disproved.
Thus, the elimination of the existential quantifier allows us to test whether a statement can be assigned a truth value with greater ease, as we need only test whether every variable is paired with the universal quantifier. This will be useful in Gödel’s proof, as we will need to make many very specific statements about the exact structure of strings (which we recall are the formal representations of statements).
Primitive recursive is a fancy term for a fairly basic idea. If a formula is primitive recursive all that is meant is that we can assign a finite bound to how long it will take to evaluate it. By formula we mean either what is commonly called a function, like x2 or x!, something that takes an input and transforms it in some way, or a statement, in which case an evaluation would yield true or false (upon binding all variables, that is).
Examples of primitive recursive formulae include x!, as we know this will take at most x steps to evaluate, and x < y, as we know this will take at most y steps to very its truth or falsity*. In reality these will take far longer, as evaluating x!, for example, requires x steps of multiplication, which will in turn take many steps of addition, which will in turn take many steps of the successor function, but all of these are primitive recursive operations, and successive iterations of finite operations will always be finite. All common arithmetic formulae, such as addition, multiplication, exponentiation, factorials, equality, etc. are primitive recursive.
For an example of a formula that is not primitive recursive think of just about any unsolved problem in number theory. The Collatz Conjecture, for example, considers the function
\[ f(n) = \begin{cases} 3n+1 & \text{if $n$ is odd} \\ n/2 & \text{if $n$ is even} \\ \end{cases} \]and claims that continuously applying the function to any positive integer will always result, eventually, in getting a 1. The problem is that there doesn’t seem to be any way to assign a bound to the “eventually” part. Even though every number we’ve tried goes 1, we have no idea how to calculate how long it might take as a function of the number with which we start.
The importance of primitive recursive formulae is that if an arithmetic formula is primitive recursive it can be expressed within an axiomatic system for arithmetic of equivalent or greater power than Peano arithmetic, such as Principia Mathematica or Zermelo-Fraenkel. This means that if a formula can be shown to be primitive recursive we can be sure that there exists a formalization of that formula (that is, a string of symbols representing the formula) within our system. This is absolutely crucial to Gödel’s work, as a large portion of his proof is dedicated to showing that certain arithmetic relations can be expressed in the system of Principia Mathematica.
We will now prove the Incompleteness of arithmetic.
We will start by going through the details of the formal system in which we are working, which we will call P. P is Principia Mathematica augmented by the Peano axioms. Including the Peano axioms is actually redundant, but they are useful in simplifying things. The basic symbols we will use are “¬” (not), “∨” (or), “∀” (for all), “0”, “s” (successor), “(”, and “)”.
In addition to these, we will need an infinite amount of symbols to represent variables. Recall that Principia Mathematica advanced Ramified Type Theory, in which there are terms of first type, which are numbers*, terms of second type, which are sets of numbers, terms of third type, which are sets of sets of numbers, and so on. Thus, we will have variables of different types, which we will indicate with a subscript. So x1, y1, z1 ... will be variables that stand for numbers, x2, y2, z2 ... will be variables that stand for sets, x3, y3, z3 ... will be sets of sets, and so on.
Thus, our basic symbols are
$$ \neg, \vee, \forall, 0, s, (, ) $$ $$ x_1, y_1, z_1, \ldots $$ $$ x_2, y_2, z_2, \ldots $$ $$ \vdots $$We now define our axioms.
I - Axioms from Peano Arithmetic
Note that =, ∧, and ⇒ are abbreviations only; the actual axioms do not contain them. We have discussed before the substitutions for ∧ and ⇒, but the way to write equality is a little more complicated.
x1 = y1 can be expressed in our system as x2∀(¬(x2(x1)) ∨ x2(y1)). To see why, note that ¬(x2(x1)) ∨ x2(y1) is the same as x2(x1) ⇒ x2(y1), so we can rewrite x2∀(¬(x2(x1)) ∨ x2(y1)) as x2∀(x2(x1) ⇒ x2(y1)). In plain English, this statement is saying that, for all x2 (which we recall represents a set), if x1 ∈ x2, then y1 ∈ x2. Or in other words, for every set, if x1 is in it, then y1 is in it. This is what equality means. If, for every single set, x1 being in it implies that y1 is in it, x1 and y1 must be the same thing.
II - Axioms from Propositional Logic
Where any formulae may be substituted for p, q, and r.
III - Axioms from Predicate Logic
Where a may be any formula, v any variable, b any variable of the same type as v which does not contain a variable bound in a where v is free (more will be said on this later), and c any formula in which v is bound.
IV - Axiom of Comprehension
Where v and u may be substituted for a variable of type n and n + 1, respectively, and a may be any formula in which u is bound. This axiom establishes that sets are defined by rules, sometimes called intensions.
V - Axiom of Extensionality
Or any version of this formula where the type of all variables are increased by the same amount (called a type-lift). This axiom defines set equality for every type of set.
We now define the relation immediate consequence of. A formula c is an immediate consequence of a if a is the formula v ∀ c, where v is any given variable. It is the immediate consequence of a and b if a is the formula b ⇒ c. It is a fact of great import that all statements within any proof are produced from previous statements using only these logical steps. Thus, the set of provable formulae is the set that contains the axioms and is closed with respect to immediate consequence of. This fact will prove of great use, as we will later need to describe relations that define provability.
This next step is the key to the proof. What we will do is assign each formula and proof (sequence of formulae) a number, which we will call the Gödel number*. We will do this in such a way that if the proof a is a proof of the formula b, then the Gödel number for a will have a certain arithmetic relation with the Gödel number for b. And because this relation is arithmetic, it can be described within our system P. This will enable P to, in a sense, talk about itself. As things turn out, self-reference can never be banished from math.
We will begin by defining a function Γ : {Strings in P} → N which will take strings in P and yield their Gödel number. We will define this function in terms of the basic symbols to start, and use that definition to allow statements and proofs into the domain of Γ.
| Γ(0) = 1 | Γ(s) = 3 | Γ(¬) = 5 | Γ(∨) = 7 |
| Γ(∀) = 9 | Γ(() = 11 | Γ()) = 13 |
Further, Γ will assign to each variable a number. To variables of first type, x1, y1, z1, and so on, it will assign primes greater than 13. So
| Γ(x1) = 17 | Γ(y1) = 19 | Γ(z1) = 23 ... |
For variables of greater type we will do the same, but raise the primes to powers equal to the type. So in general
| Γ(xn) = 17n | Γ(yn) = 19n | Γ(zn) = 23n ... |
Now we will use this numbering to assign numbers to formulae. Every formula can be thought of as a sequence of symbols, and as such may be represented by a sequence of Gödel numbers. For example, the statement
which states the existence of the empty set (we'll call this formula e), would be given the sequence
We can use such sequences to produce a unique number for every formula by taking the first prime to the power of the first number in the sequence, the second prime to power of the second number in the sequence, and so on. Thus, the Gödel number for e, the above formula, would be
Which is approximately 2.4 · 10743. These numbers get very large very quickly, and as such we will not calculate any of them explicitly. This assignment is used because it gives every formula a unique number* that has convenient arithmetic properties.
Now that we have a unique number for every formula we can get a unique number for every proof by simply repeating the process described above. A proof can be thought of as a sequence of formulae, so if a proof a consisted of formulae that gave the sequence of Gödel numbers a1, ..., an the Gödel number for the proof would be
\[ \Gamma(a)=\prod_{k = 1}^{n} p_k^{a_{k}} \]Where pk is the kth prime. This assignment makes Γ injective. If we restrict the codomain of Γ to Gödel numbers, we get a bijective function Γ : {Strings in P} → {Gödel Numbers}, which allows us to formulate Γ-1, which gives the statement for a given Gödel number.
We can now use the Γ function to allow P to talk about itself. For example, if we consider our statement e = ¬x2 ∀ ¬(x1 ∀ ¬(x2(x1))) and wish to say of it that its first symbol is “¬”, we could say that 25 divides Γ(e), but 26 does not. This gives an arithmetic interpretation of a statement about a statement of P.
To show that something about P may be said within P it is sufficient to show that the arithmetic relation corresponding to that something is primitive recursive. In our example, this would mean that in order to be sure that P can say that “¬” is the first symbol in a statement we would show that “25 divides x, while 26 does not” is a primitive recursive relation. Fortunately it is, and this is easily shown, but more complicated and esoteric relations are not so readily shown. Our goal will be to show that P is capable of saying “x is a proof of y”, and to do so we will show that the arithmetic relation corresponding to this statement is primitive recursive.
It can easily be shown that addition, multiplication, exponentiation, less than, and equality are primitive recursive, so we will start from these and build up a series of 45 formulae, each employing previous ones, of which the final will be an arithmetic relation between two numbers x and y such that, if satisfied, Γ-1(x) will be a proof of Γ-1(y).
For each formula (in gold) we will indicate a bound (in pink) on the number of steps necessary to evaluate the formula in order to ensure it is primitive recursive. Where a bound is not indicated the formula is an explicit function, as in [4], [9], [10]*.
Thus far the formulae have been purely arithmetic with no relation to describing Gödel numbers. From here on out the arithmetic formulae will be designed to operate on Gödel numbers and will correspond to some description of the statements those Gödel numbers represent. As such, the corresponding description the arithmetic formulae represent will be given in place of arithmetic descriptions. The arithmetic descriptions will however, as above, be given explicitly. The reader is encouraged to go through the arithmetic definition to verify its correspondence with the stated interpretation. The [n]’s are useful references for this.
We will pause for a moment and summarize some of the things we have found. We now have arithmetic formulae for finding any term within a string [6], for joining two strings together [8], for assessing whether a string is a variable and of what type ([12] and [11] respectively), and for placing various logical operations on strings [13, 14, 15], among other things.
While these formulae have been a sort of hodge-podge of concepts, our next four formulae will be dedicated to producing an arithmetic formula for the concept “x is a formula”. To do this we recognize that all formulae can be built with only four concepts - set membership, negation, disjunction, and generalization. So we will define in [20] an arithmetic formula that tests whether a string is of the form xn+1(xn), which we recall denotes xn ∈ xn+1. Then in [21] we will give a formula that tests whether the string is a negation, disjunction, or generalization. In [22] we will test whether the string is a series of formulae*, which we will use in [23] to isolate the last formula, which we will know must be a formula.
We now have a way to take the Gödel number for a string and determine whether that string is a formula using the arithmetic formula defined above.
In the next eight formulae we will develop the ability to talk about free and bound variables in formulae. Recall that a variable is bound if it is quantified, which in our case means that it is quantified with the universal quantifier. If it is not bound it is free. The importance of this is that the only formulae that can be assigned a truth value are those in which every variable is bound. In [31] we will have an arithmetic formula that corresponds to the notion of replacing all free variables with something else.
We now have an arithmetic formula that allows us to take the Gödel numbers for a formula, a variable, and a string and get a new number, which will be the Gödel number for that same formula, except that everywhere where the variable was free in the formula it is replaced with the string. This will become very important as it will allow us to make every variable in a formula quantified, which we recall is necessary for assigning a truth value to a statement.
We will now define two formulae that will help us define the axioms arithmetically. In [32] we will actually define four formulae in one go, which will use our previously defined formulae for negation, disjunction, and generalization [13, 14, 15] to make formulae representing implication, conjunction, logical equivalence, and the existential qualifier. These will help in defining the axioms. In [33] we will define a formula that represents type-lifting, where the type of every variable in a formula is raised by the same amount. The only use of this will be to define the Axiom of Extensionality in [41].
Now that we have these formulae we will be able to define arithmetic formulae that assess whether a number is the Gödel number for an axiom. This will be accomplished in [42].
The axioms from Peano arithmetic are statements that only make use of our basic symbols* and as such have Gödel numbers of their own. So we will define α1, α2, and α3 to be the Gödel numbers for axioms I - 1, 2, and 3 respectively.
The axioms of propositional logic and predicate logic and the axiom of comprehension are not written using our basic symbols, but rather are general forms of statements involving formulae and variables. So instead of seeing, as in [34], whether or not the Gödel number for a formula equals the Gödel number of an axiom, we will have to determine whether the formula is of a certain form. In [35] we will give an explicit definition of such a test for axiom II - 1, but won’t do so for axioms II - 2, 3, and 4, as it will be easy to see how they are constructed given the formula in [35]. In [36] we will test whether a formula comes from the axioms for propositional logic.
For the axioms of propositional logic we only needed to check that the things we were substituting were formulae. Predicate logic allows us to talk about variables, and as such we will need to develop formulae that allow us to test for certain constraints on variables.
The first axiom for predicate logic is v ∀ a ⇒ a Sub(v, b). In this a can be any formula, v any variable, and b any variable of the same type as v that does not contain a variable bound in a where v is free. It makes sense why b must be the same type as v, but what does the second qualification mean?
Recall that a term of first type is something of the form 0, ss...s0, x1, or ss...sx1. So consider the case when v is a variable of first type, a is the statement “∃y1(v = y1)” and b is the variable of first type “sy1”. Upon substituting v for b, as this axiom suggests we can do, we get “∃y1(sy1 = y1)”, which is plainly false. The reason for this is that b contains a variable, y1, that is bound in a, and upon substitution with v the quantification of y1 in a applies to the thing being substituted, which it shouldn’t. So in [37] we will develop a formula that tests for this condition.
Once this is done, we will develop formulae for the axioms of predicate logic in [38] and [39].
We now have means to test whether a formula is derived from the axioms of predicate logic. We will now develop the same for the axiom of comprehension.
The axiom of extensionality is, like the axioms for Peano Arithmetic, written in terms of our basic symbols, and so has a Gödel number, but this axiom applies to any type-lift of itself, which is when the type of every variable is raised by the same amount. Thus, we define α4 to be the Gödel number for the axiom of extensionality at the lowest type (see its definition above), and will test whether a formula is a type-lift of this formula (or this formula itself), in [41].
We now have a means to test whether a formula is derived from an axiom. Recall that valid proofs are those sequences of statements that include the axioms and are closed with respect to the relation immediate consequence of. In [43] we will develop a means to test whether a formula is an immediate consequence of two other formulae, then in [44] we will test whether a string is closed with respect to this relation (making it a proof). In a proof of this nature what is proved is the last formula it comprises, so in [45] we will finally be able to test if x is a proof of y by testing whether y is the last formula that constitutes the proof x.
In xDem y we have a primitive recursive arithmetic formula between x and y that, if satisfied, means that Γ-1(x) is a proof of Γ-1(y). What this means is that there is a statement within our system P that can say whether or not two other strings constitute a valid proof within P. In the next section we will use this to create an undecidable statement.
We will now construct a statement that is undecidable within P.
Consider the statement
This is a statement claiming that there does not exist an x1 such that Γ-1(x1) is a proof of Γ-1(y1) (see [45]), or in other words, that Γ-1(y1) is not provable.
We now consider the statement
Which states that y1Sub(19, y1) is not provable*. We recall (see [31]) that y1Sub(19, y1) represents going into Γ-1(y1) and wherever Γ-1(19) (see Gödel Numbering) is free substituting y1. It is important to note that y1 is being treated as a Gödel number in its first appearance and a “normal” number in the second. That is, we are interested in the statement y1 represents in one instance, but only its numerical value in the other. Why we would want to do this may not be clear as of yet, but already we see the interplay between the arithmetic and the interpretation of the arithmetic.
As of now p cannot be assigned a truth value, as it has a free variable, y1, but p is nonetheless well-formed, and as such has a Gödel number, which we will call n, so that Γ(p) = n.
We now consider the statement
Which states that nSub(19, n) is not provable. In this case there are no free variables, and as such r should have a truth value. To determine what this truth value is, we must examine nSub(19, n) more closely.
The statement nSub(19, n) represents going into Γ-1(n), and wherever Γ-1(19) is free, substituting n. So what is Γ-1(n)? We defined n such that Γ(p) = n, so Γ-1(n) = p. Thus, we will go into p = ¬∃x1 (x1Dem [y1 Sub(19, y1)]) and wherever Γ-1(19) is free replace it with n. We know Γ-1(19) = y1, so going into ¬∃x1 (x1 Dem [y1 Sub(19, y1 )]) and replacing free instances of y1 with n we get ¬∃x1(x1Dem [nSub(19, n)]) as the meaning of nSub(19, n). But recall that r = ¬∃x1(x1Dem [nSub(19, n)]), so we can say that
Or in other words, r says that r is not provable.
This is a truly remarkable statement. We have uncovered a way to form a statement in P that says of itself that it is not provable in P. We now look to see if this is indeed the case. Is it provable? And if not, is its negation provable?
If r is provable, then there exists a proof of it, so we can prove that ∃x1(x1Dem r). But that is in fact the negation of r, so if r is provable, then so is ¬r. If P is consistent then this cannot be the case.
If ¬r is provable, then ∃x1(x1Dem r) is provable (this being the negation of r), which would mean yet again that there exists a proof of r. So if ¬r is provable then r is provable. Again, this cannot be the case if P is consistent.
We can thus conclude that if P is consistent then neither r nor ¬r is provable, meaning P is incomplete. This concludes the proof of Gödel’s first incompleteness theorem.
We have shown that if P is consistent then it is incomplete. More specifically, we have shown that consistency implies r, as r is the statement that r cannot be proven, which is indeed the case if P is consistent. We can represent this relation succinctly as
Where C is the statement claiming the consistency of P.
We then come to another remarkable conclusion. Because r follows from the consistency of P, if there exists a proof of the consistency of P within P then r would be provable. But we have shown above that there cannot exist a proof of r, so likewise there cannot exist a proof of the consistency of P within P. So not only is P incomplete, but it is incapable of proving its own consistency. This is Gödel’s Second Incompleteness Theorem.
This fact contrasts arithmetic systems such as propositional and predicate logic, both of which are capable of an internal proof of consistency. The consistency of P can, however, be proven by auxiliary means, and indeed Gentzen proved its consistency using transfinite induction in 1936, but any such proof will necessarily rely on assumptions that go beyond those of arithmetic, so if the consistency of arithmetic is in doubt, a system capable of proving its consistency must share similar doubts.