GÖDEL'S INCOMPLETENESS THEOREMS

The axiomatic method is at the heart of mathematics. The work of mathematicians is to derive the consequences of axioms. According to Euclid, axioms are evidently true, and deduction from them is a powerful method of learning new truths. The rise of non-Euclidean geometry disrupted the carefree connection between truth and proof and led many modern thinkers to adopt the formalistic attitude that the mathematician's sole endeavor is to work out the consequences of axioms, taking no professional interest in inquiring what, if anything, the axioms are true of.

In 1931 Kurt Gödel proved a deep theorem that showed that deduction from axioms cannot be all there is to mathematical understanding. Gödel showed that, for whatever system of truths of number theory we choose to regard as axiomatic, there will be statements of basic arithmetic that we can recognize as true even though they are not consequences of the axioms. That there are truths not derivable from our axioms is hardly surprising; nobody ever promised us omniscience. What is surprising is that there are arithmetical statements we can recognize as true even though they are not derivable, so that no system of axioms we can write down fully captures our arithmetical understanding. Moreover this situation holds not only for systems of axioms we are capable of producing today but also for whatever systems we may devise in the future.

Gödel's true, unprovable sentence is obtained by using strings of numbers to encode strings of symbols, thereby reducing statements about language to statements about numbers. Under such a coding Gödel's sentence says that the system of axioms is consistent. Of course if we accept the axioms, we regard the axioms as true, so we certainly regard them as consistent. But even though adopting the axioms means accepting their consistency, the statement that the axioms are consistent cannot be proved from the axioms. We could adopt the thesis that the axioms are consistent as a new axiom. This would give us a new, larger system of axioms that can prove the consistency of the old system but not the consistency of the new system. We can continue the process of adding consistency statements repeatedly, but however far we go we shall never catch up with Gödel. No consistent system that includes basic arithmetic can prove its own consistency.

Gödel's result has important corollaries, notably, Church's theorem (1936) that there is no algorithm for testing whether a sentence is logically valid and Tarski's theorem (1935) that the set of true sentences of a language cannot be defined within the language itself.

The Language of Arithmetic

Gödel's results apply to the language of arithmetic, which is an artificial language for formalizing reasoning about the natural numbers, and to other languages into which the language of arithmetic can be translated. To state his results we need to specify the language exactly. As numerals, the language uses "0" and expressions obtained from "0" by repeatedly prefixing "S," which stands for the successor function. The numeral for 3 is "SSS0," which we abbreviate "3." The language also contains function signs "+" "×" and "E," for addition, multiplication, and exponentiation, so that the terms of the language make up the smallest class that contains the numeral "0" and the variables v ₀, v ₁, v ₂, v ₃, …, and that contains S τ, (τ+ρ), (τ×ρ), and (τEρ) whenever it contains τ and ρ. In the exposition here we shall sometimes use other letters as variables in place of the official v _i s, so as to reduce the proliferation of subscripts. Including "E" as a primitive operation is not strictly necessary, as we shall see below, but it enables us to get off to a fast start.

A term without variables is closed. Rules that we learned in elementary school enable us to calculate the numerical value of each closed term. A term with n variables represents an n -ary function, calculable by a grade-school algorithm.

The atomic formulas take the form τ = ρ or τ ≤ ρ, where τ and ρ are terms, and the formulas constitute the smallest class containing the atomic formulas and containing ∼ ϕ, (ϕ ∨ ψ), and (∃v _i )ϕ, whenever it contains ϕ and ψ. An occurrence within a formula of the variable v _i is bound if it occurs within some subformula that begins with (∃v _i ), and it is free otherwise. A formula without free variables is a sentence ; it is sentences that are either true or false. The symbols for conjunction ("∧"), the conditional ("→"), the biconditional ("↔"), universal quantification ("(∀v _i )"), and the less-than relation ("<") are treated as defined.

Where v _i does not occur within the term τ, we use (∃v _i ≤τ)ϕ and (∀v _i ≤τ)ϕ to abbreviate (∃v _i )(v _i ≤τ ∧ ϕ) and (∀v _i )(v _i ≤τ → ϕ). These are bounded quantifiers, and a formula with no quantifiers that are not bounded is a bounded formula. For example 'v ₀ is prime' is formalized by the bounded formula '(SS0≤v ₀ ∧ (∀v ₁≤v ₀)(∀v ₂≤v ₀)(v ₀ = (v ₁ x v ₂) → (v ₁ = S0 ∨ v ₂ = S0)))'. A set or relation is said to be bounded if it is the extension of a bounded formula.

We can test whether an atomic sentence is true by grade-school algorithms; "true," that is, in the standard model consisting of the natural numbers 0,1,2,3, … Any bounded sentence is demonstrably equivalent to a truth-functional combination of atomic sentences, since bounded quantifiers can be cashed out as long but finite disjunctions and conjunctions. Thus we have an algorithm for determining the truth value of a bounded sentence. It follows that every bounded set or relation is decidable; that is, there is an algorithm for testing membership in the set or relation. If S is the extension of the bounded formula σ(x ₀), we can test whether n ∈ S by asking whether σ(ṉ ) is true.

The Σ formulas are obtained by prefixing a block of existential quantifiers to a bounded formula, and their extensions are recursively enumerable sets and relations. Any recursively enumerable set is the extension of a formula obtained by prefixing a single existential quantifier to a bounded formula, since (∃x ₁)(∃x ₂)…(∃x_n )ϕ is equivalent to (∃x ₀)(∃x ₁≤x ₀)(∃x ₁≤x ₀)…(∃x_n ≤x ₀)ϕ. (The same goes for recursively enumerable relations; in the future we shall let this go without comment.) The union and intersection of recursively enumerable sets are recursively enumerable, since ((∃y )ϕ(x,y ) ∨ (∃z )ψ(x,z )) and ((∃y )ϕ(x,y ) ∧ (∃z )ψ(x,z )) are, respectively, logically equivalent to (∃y )(∃z )(ϕ(x,y ) ∨ (ψ(x,z )) and (∃y )(∃z )(ϕ(x,y ) ∧ (ψ(x,z )) (assuming bound variables have been chosen so as to avoid conflicts). If χ(x,y,z ) is bounded and τ is a term, {x : (∃y ≤τ)(∀∃z )χ(x,y,z )} and {x :(∀y ≤τ)(∃z )χ(x,y,z )} are both recursively enumerable since they are the extensions of (∃z )(∃y ≤τ)χ(x,y,z ) and (∃w )(∀y ≤τ)(∃z ≤w )χ(x,y,z ), respectively. If a Σ sentence is true, we can show it is true by providing an appropriate witness.

Σ Formulas and Decidability

A set of numbers is effectively enumerable if there is a mechanical procedure for listing the set, so that every member of the set turns up on the list eventually and nothing appears on the list that is not in the set. Every recursively enumerable set is effectively enumerable. To see this, we introduce the pairing function. Pair (x,y ) = ½(x ² + 2xy + y ² + 3x + y ) is a one-one correspondence between ℕ × ℕ and ℕ (where ℕ is the set of natural numbers). Define the functions 1st and 2nd so that Pair (1st(z ),2nd(z )) = z. Given a recursively enumerable function S = {x ₀: (∃x ₁)σ(x ₀,x ₁)}, with σ bounded, we can list S by the following algorithm: At stage n, test whether the sentence σ(1st(n ), 2nd(n ) ) is true; if it is, add 1st(n ) to the list.

Every set that is known to be effectively enumerable is recursively enumerable. This striking fact, together with a large body of evidence obtained by examining idealized models of computation and examining structural properties of effectively enumerable and recursively enumerable sets, has led to the general acceptance of the Church-Turing thesis : A set of natural numbers is effectively enumerable if and only if it is recursively enumerable.

A set of natural numbers is decidable if and only if there is an algorithm for testing membership in the set. A set can be effectively enumerable without being decidable, since, if we have a procedure for listing an infinite set, there will be no stage at which, from the fact that a given number has not yet turned up on the list, we can conclude that the number will never appear on the list. On the other hand if a set and its complement are both effectively enumerable then the set is decidable, and conversely. Defining a set to be recursive if it and its complement are both recursively enumerable, the Church-Turing thesis tells us that a set is decidable if and only if it is recursive.

An unary partial function is a set of ordered pairs ƒ with the property that, whenever <i,j > and <i,k > are both in ƒ, we have j = k. If <i,j > ∈ ƒ, for some j, we say that i is in the domain of ƒ, and we write ƒ(i ) = j. (Partial functions of more than one variable are defined similarly.) ƒ is said to be calculable if there is an algorithm that, for given input i, gives the output ƒ(i ) if i is in the domain of ƒ, and yields no output at all if i is outside the domain of ƒ. A unary partial function is calculable if and only if, qua binary relation, it is effectively enumerable. It follows according to the Church-Turing thesis that ƒ is calculable if and only if it is recursively enumerable. If so, ƒ is said to be a partial recursive function. (The notation is confusing—a collection of ordered pairs can be a partial recursive function without being a recursive relation—but entrenched.) A total recursive function —a partial recursive function whose domain is all of ℕ—will be a recursive relation, since if ƒ is {<i,j >: (∃x )θ(i,j,x )}, with θ bounded, the complement of ƒ is {<i,j >:(∃x )(∃y )(∼ y = j ∧ θ(i,y,x ))}.

Arithmetization of Metamathematics

The set-theoretic paradoxes, particularly Russell's paradox, had on David Hilbert much the same effect that Zeno's paradoxes had on Aristotle. Both thinkers came to realize that the idea of the infinite held great intellectual peril with the risk of contradiction at every turn. Unlike Aristotle, however, Hilbert was unwilling to banish the actual infinite from mathematical reasoning. Instead he proposed to develop the theory of infinite sets in such a way that we could be assured that no contradiction would ensue, by treating mathematical proofs as the objects of mathematical study, in the same way that earlier mathematicians had treated curves, planes, and numbers as objects of mathematical study. A mathematical proof is, after all, a finite object, even if the sentences that appear in the proof talk about infinite objects, and Hilbert proposed that a new science of metamathematics could show by finite means that set theory was free of contradiction, by showing that there is no finite path that leads from the axioms to "∼ 0=0."

The great breakthrough in metamathematics was Gödel's proof, which showed that it was not necessary to go outside set theory or even outside arithmetic to carry out metamathematical investigations. By assigning numerical codes to formulas and finite strings of formulas, and by reducing properties of proofs to properties of their code numbers, it was possible to develop proof theory as a branch of number theory. This technique led to a great flowering of metamathematics even though as we shall see, it derailed Hilbert's plan.

The arithmetization of metamathematics proceeded in two stages. In the first stage numerical codes are assigned to simple symbols more-or-less arbitrarily, so that a formula, which is a string of simple symbols, can be coded as a sequence of numbers. Second we devise a method for encoding a finite sequence of numbers as a single number. This enables us to encode a formula as a single number. In this way a proof, which is a sequence of formulas, is encoded as a sequence of numbers, which is, in turn, coded as a single number.

We attack the second stage first. We already know how to use the function Pair to code a pair of natural numbers by a single number. We can encode a finite set of natural numbers by a single number by setting the code number of the finite set F, Code (F ), equal to Σ_{i ∈F} (2Ei ) Code provides a one-one correspondence between the set of finite sets of natural numbers and ℕ. The number n is the image under Code of the set of places in the binary decimal expansion of n in which "1"s appear. Finally, we encode the finite sequence <k ₀,k ₁, … ,k _m> as the number Code ({Pair (0,k ₀), Pair (1,k ₁), … , Pair (m,k _m )}). Here we shall use an expression like "<3,2,1>" ambiguously to denote a sequence of length three and to denote the code number for that sequence, which is 448.

The relation that holds between k and n if k is an element of the set coded by n is defined by a bounded formula; abusing notation, we write "k ∈ n " to represent the statement that (∃i < (2 Ek ))(∃j < n )n = (i + ((2 E k ) + (j × (2 E(Sk ))))). The set of all code numbers of finite sequences is the extension of a bounded formula, as are the concatenation operation and the partial function that takes i and n to the i th member of the sequence coded by n (provided n codes a sequence of i or more elements). The simplicity of this technique for encoding a finite sequence of numbers by a single number is the motive for including exponentiation as a primitive operation.

The details of the assignment of numerical codes to terms and formulas are highly arbitrary. A motive for the particular choices here is to avoid fretting over parentheses. With each term τ, we associate a number ^┌τ^┐, as follows: The numeral "0" is assigned <0,0>, and the variable x _i is assigned <1,i >. ^┌S τ^┐ is <2,^┌τ^┐>, and ^┌(τ+ρ)^┐, ^┌(τ×ρ)^┐, and ^┌(τEρz )^┐ are <3,^┌τ^┐,^┌ρ^┐>, <4,^┌τ^┐,^┌ρ^┐>, and <5,^┌τ^┐,^┌ρ^┐>, respectively.

A number x is a the code of a term just in case it is an element of a finite set s with the following property: For any element y of s, either y = <0,0>; or y = <1,i >, for some i ≤ y ; or y = <2,z >, for some z in s ; or y is equal to one of <3,z,w >, <4,z,w>, and <5,z,w>, for some z and w in s. s represents a finite tree, with each node labeled by the code of a term, so that when a node is labeled by a complex term, nodes beneath it are labeled by the term's constituents and so that each leaf of the tree is labeled either by the code of "0" or by the code for a variable. This characterization is naturally written out as a Σ formula, showing that the set of (code numbers of) terms is recursively enumerable.

The set of terms is, in fact, recursive. To see this, we note that, if x is not a term, then the attempt to construct a labeled tree with x at its trunk winds up with at least one branch that does not terminate in either ^┌0^┐ or a variable. More precisely, x does not encode a term if and only if there is a sequence <x ₀,x ₁,…,x_n > of numbers ≤ x with the following properties:

x ₀ = x.

If x_i has the form <2,y >, then i < n and x _{i +1} = y.

If x_i has one of the forms <3,y,z >, <4,y,z >, or <5,y,z >, then i < n and either x_{i +1} = y or x_{i +1} = z.

If i < n, x_i has one of the forms <2,y >, <3,y,z >, <4,y,z >, or <5,y,z >.

x_n does not have either of the forms <0,0> or <1,k >.

This can readily be written out as a Σ formula, showing that the complement of the set of terms is recursively enumerable.

The function Z that takes a number n to the code number for the numeral n can be described by a recursive definition:
Z (0) = <0,0> = 5.
Z (m +1) = <2,Z (m )> = 8 + (2E(Pair (1,Z (m )))).
We can convert this recursive definition into an explicit definition, using a quite general technique that Gödel obtained by refining an idea from Gottlob Frege's Begriffschrift. Z (n ) = k if and only if there is a sequence <x ₀,x ₁,…,x_n > with the following features:

x ₀ = <0,0>.

For m < n, x _{m +1} = <2,x_m >.

x_n = k.

This characterization shows that Z is a total recursive function.

The function that associates a code ^┌ϕ^┐ with each formula ϕ is again highly arbitrary. For τ and ρ terms, we let <6,^┌τ^┐,^┌ρ^┐> and <7,^┌τ^┐,^┌ρ^┐> be the codes of τ = ρ and τ ≤ ρ. For ϕ and ψ formulas, we let <8,^┌ϕ^┐> be ^┌∼ ϕ^┐, <9,^┌ϕ^┐,^┌ψ^┐> be ^┌(ϕ ∨ ψ)^┐, and <10,i,^┌ϕ^┐> be ^┌(∃v _i )ψ^┐. The proof that the set of codes of formulas is recursive is just like the corresponding argument for terms.

It is straightforward if somewhat laborious to verify, just by writing down an appropriate formula, that, for example, the arithmetical operations corresponding to forming the disjunction and the conjunction of two formulas, to prefixing a quantifier to a formula, and to substituting a given term for free occurrences of a variable in a formula are partial recursive functions. Also, for example, that the set of terms in which the variable v ₁₇ appears and the set of formulas in which v ₁₂₃ appears free are recursive sets.

Proofs and Computations

Euclid's Elements deduces highly sophisticated geometric theorems as consequences of simple, intuitively obvious axioms. Aristotle, the father of logic, investigated the methods by which consequences are derived from axioms, identifying simple patterns of valid reasoning like the following so-called syllogism : "All men are animals. No stone is an animal. Therefore, no stone is a man." The methods of reasoning Euclid actually employed were far more sophisticated than the mere production of chains of syllogisms, however, and the ancients were generally content to take it as obvious that Euclid's deductions were legitimate, without demanding a detailed survey of deductive methods.

Meticulous nineteenth-century investigations revealed the surprising fact that, despite having been accepted by generations of scholars as the exemplar of deductive rigor, Euclid's proofs were often invalid. In proving a theorem he sometimes imported information from the accompanying diagram that was not justified by either the hypotheses of the theorem or the axioms. These investigations led to a search for fully precise methods of deduction in which one could have complete confidence. This search culminated in the widespread acceptance of a system of precise rules for the first-order predicate calculus—the logic governing the operators "∨," "∼," (∃v _i ), and "="—within which the deductions of classical mathematics can be formalized with scrupulous rigor.

With these rules in hand, we can capture the notion of logical consequence precisely, by pressing it from below and from above. It is clear that, if a sentence ϕ is a logical consequence of a theory (set of sentences) Γ, then it cannot be possible to choose a domain of discourse and semantic values for the nonlogical terms so as to make the members of Γ all true and ϕ false. Thus a necessary condition for a ϕ to be a logical consequence of Γ is that ϕ be true in every model of Γ. It is also clear, from examining the rules (for whichever of the standard textbook systems is convenient), that if ϕ derivable from Γ, ϕ is a logical consequence of Γ; this gives us a sufficient condition for logical consequence. Gödel's 1930 Completeness Theorem shows that these two conditions meet, so that if ϕ is true in every model of Γ then ϕ is derivable from Γ.

The Completeness Theorem applies equally well to any of many different logical calculi for first-order predicate logic. W. V. Quine developed a particularly convenient system the following two properties: The (codes of the) axioms of logic form a recursive set; and each logical consequence of a theory Γ can be found at the end of a sequence of sentences, each member of which is either an axiom of logic, an element of Γ, or obtained from earlier members of the sequence by modus ponens, the rule that permits the deduction of ψ from ϕ and (ϕ → ψ). (Such a sequence is a proof of the sentence from Γ.) Quine's axioms will not be written out here.

If Γ is recursive, the set of pairs <s, ^┌ϕ^┐> such that s is a proof of ϕ from Γ is a recursive relation, represented by a Σ formula we shall abbreviate "s B_Γ ^┌ϕ^┐." (In terminology introduced below, "B_Γ" "binumerates" the relation.) We write "Bew _Γ;(^┌ϕ^┐ )" to abbreviate "(∃s )s B_Γ^┌ϕ^┐." Since "Bew _Γ," is Σ, the set of logical consequences of Γ is recursively enumerable.

William Craig noted a converse result: If the set of consequences of the theory Γ is recursively enumerable then Γ has the same consequences as some recursive set to axioms; Γ is, as they say, recursively axiomatizable. To see this, note that there is a bounded formula ψ(x,y ) such that the consequences of Γ constitute the set of sentences whose code numbers satisfy (∃y )ψ(x,y ). Let Γ_Craig be the set of all sentences of the form (m = m ∧ θ), for which the pair <^┌θ^┐,m satisfies ψ(x,y ). Then Γ_Craig is recursive (bounded, in fact), and Γ_Craig and Γ are logically equivalent.

We would now like to see how any numerical computation by algorithm can be simulated by a logical deduction from basic arithmetical axioms. Q_E, a variant of Robinson's arithmetic, is the conjunction of the following nine statements:

(∀x )(x = 0 ↔ ∼ (∃y )x = Sy ).

(∀x )(∀y )(Sx = Sy → x = y )

(∀x )(x + 0) = x.

(∀x )(∀y )(x + Sy ) = S (x + y ).

(∀x )(x × 0) = 0.

(∀x )(∀y )(x × Sy ) = ((x × y ) + x )

(∀x )(x E 0) = S0.

(∀x )(∀y )(x E Sy ) = ((x E y ) × x )

(∀x )(∀y )(x ≤ y ↔ (∃z )(x + z ) = y ).

Q, which we shall talk about later on, is obtained from Q_E by deleting the two clauses involving exponentiation.

A straightforward induction on the complexity of terms shows that, for every closed term τ, there is a number m such that the sentence τ = m is a theorem of Q_E. Another induction shows that every bounded sentence is decidable (either provable or refutable) in Q_E. Since every true bounded sentence is provable in Q_E, it follows that every true Σ sentence is provable in Q_E, since we can prove an existential sentence by providing a witness. If S is a recursively enumerable set, it is the extension of some Σ formula σ. Because every true Σ sentence is provable in Q_E and (because Q_E is true) no false Σ sentence is provable, we have (where "├" is provability):

For any n, n ∈ S if and only if Q_E ├ σ(n ).

We shall say that σ enumerates S in Q_E. (The same observation holds for recursively enumerable relations.)

We shall say a formula ϕ binumerates a set S in Q_E if and only if, for each n, we have:

n ∈ S if and only if Q_E ├ ϕ(n ).

n ∉ S if and only if Q_E ├ ∼ ϕ(n ).

If S is recursive then there is a bounded formula χ(x,y ) such that (∃y )χ(x,y ) enumerates S in Q_E, and there is a bounded formula θ(x,y ) such that (∃y )θ(x,y ) enumerates the complement of S in Q_E. To show that S is binumerable in Q_E, we need to show that S is enumerable by a formula whose negation enumerates the complement of S. Developing an idea of J. Barclay Rosser, Tarski, Mostowski, and Robinson showed that the following Σ formula does the job:
(∃y )(χ(x,y ) ∧ ∼ (∃z < y )θ(x,z )).
Clearly if ϕ binumerates S in Q_E, it binumerates S in any consistent theory that entails Q_E.

A formula ψ(x,y ) functionally represents a total function ƒ in a theory if and only if, for each k, the following sentence is a consequence of the theory:
(∀y )(ψ(k,y ) ↔ y = ƒ(k) ).
If ƒ is a total recursive function, we know that there is a formula ϕ(x,y ) that binumerates ƒ in Q_E. Tarski, Mostowski, and Robinson showed that the following formula functionally represents ƒ in Q_E (and hence in any theory that entails Q_E):
(ϕ(x,y ) ∧ (∀z < y )∼ ϕ(x,z )).

The First Incompleteness Theorem

We are now ready to see how to construct, for any recursively axiomatizable, true theory that includes Q_E, a true sentence that is not a consequence of the theory. The key to the construction is to see how to produce sentences that can talk about themselves so that we can construct a sentence that asserts its own unprovability. Such a sentence cannot be provable since if it were provable it would be a false consequence of the axioms. So the sentence must be true. To carry out this plan we use the following result, one of the masterpieces of modern mathematics:

gÖdel's self-reference lemma

For any formula ψ(y ), one can construct a sentence ϕ such that Q_E ├ (ϕ ↔ ψ(^┌ ϕ^┐ )).

The hard part, the part that requires true genius, is to figure out what sentence to write down. The easy part is to verify that the sentence works. Here we shall only attempt the easy part.

Define a function ƒ as follows: If m is the code of a formula χ(x,y ) with only "x " and "y " free, let ƒ (m ) be the code of the formula
(∃x )(∃y )((x = m ∧ χ(x,y )) ∧ ψ(y )).
Otherwise, ƒ(m ) = 0.

This definition can easily be written as a Σ formula, showing that ƒ is a total recursive function. Consequently, there is a formula θ(x,y ) that functionally represents ƒ in Q_E. Let m be ^┌(θ(x,y )^┐, and ϕ be the following sentence:
(∃x )(∃y )((x = m ∧ θ(x,y )) ∧ ψ(y )).
Then ^┌ϕ^┐ = ƒ(m ), and so the following sentences are consequences of Q_E:

(∀y )(θ(m,y ) ↔ y = ^┌ ϕ^┐ ).

((∃x )(∃y )((x = m ∧ θ(x,y )) ∧ ψ(y )) ↔ ψ(^┌ϕ^┐ )).

(ϕ ↔ ψ(^┌ϕ^┐ )).

Let Γ be a consistent, recursive set of sentences that entails Q_E. Using the Self-reference Lemma, we can find a sentence γ so that (Γ ↔ ∼Bew _γ^┌γ^┐ ) is a consequence of Q_E; γ is called the Gödel sentence for Γ. If γ were a consequence of Γ, ∼ Bew _Γ(^┌γ^┐ ) would be a consequence of Γ, and also Bew _Γ(^┌γ^┐) would be a true Σ sentence, hence a consequence of Q_E, hence a consequence of Γ. This contradicts the consistency of Γ. So γ is unprovable, so that Bew _Γ(^┌γ^┐ ) is false, and γ is true. Thus γ is our example of a true, unprovable sentences.

If Γ is true then Γ does not prove ∼γ because ∼γ is false, so that γ is undecidable in Γ. Let us say that a theory Δ is ω-inconsistent if there is a formula χ(x ) such that (∃x )χ(x ) is a consequence of Δ, and yet, for each n, ∼ χ(n ) is a consequence of Δ. Every ω-consistent theory is consistent, so if Δ is a recursive, ω-consistent theory that entails Q_E, the Gödel sentence γ for Δ is a true sentence not provable in Δ. Hence, for each m, the sentence ∼ m B _Δ ^┌γ^┐ is true, hence provable in Q_E, hence provable in Δ. It follows by ω-consistency that Bew _Δ ^┌γ^┐ is not a consequence of Δ, and so ∼γ is not a consequence of Δ. Thus the assumption of ω-consistency, rather than truth, is enough to ensure that γ is undecidable in Δ. Because γ is unprovable in Δ, Δ ∪ {∼γ} is consistent, although ω-inconsistent. So consistency does not imply ω-consistency.

Gödel used γ to show that every ω-consistent, recursively axiomatizable theory that entails Q_E is incomplete, that is, that there are sentences that the theory cannot decide; this is the First Incompleteness Theorem. Rosser went a step farther, showing that the assumption of ω-consistency can be weakened to consistency. Rather than examine Rosser's proof, we shall derive his conclusion from a stronger result, one due, in essentials, to Tarski, Mostowski, and Robinson:

recursive inseparability theorem

There is no recursive set that includes the consequences of Q_E and excludes all the sentences refutable in Q_E.

Suppose C were such a recursive set, and take a formula μ(x ) that binumerates C in Q_E. The Self-reference Lemma gives a sentence ν such that (ν ↔ ∼ μ(^┌ν^┐ )) is a consequence of Q_E. We derive a contradiction by examining two cases:

Case 1

ν ∈ C. Then Q_E ├ μ(^┌ν^┐ ), and so Q_E ├ ∼ ν. Thus υ is a sentence refutable in Q_E, and so it is excluded from C. Contradiction.

Case 2

υ ∉ C. Then Q_E ├ ∼ μ(^┌ν^┐ ), and so Q_E ├ ν. Thus υ is a consequence of Q_E, and so an element of C. Contradiction.

Corollary

No consistent theory that entails Q_E has a recursive set of consequences.

This follows from the fact that, if a consistent theory entails Q_E, it excludes the sentences refutable in Q_E.

Corollary (Rosser's Theorem)

No consistent, recursively axiomatized theory that entails Q_E is complete.

If Γ is consistent, recursively axiomatized, and complete, then the complement of Γ is recursively enumerable, since it is the union of the set of non-sentences with the set of sentences whose negations are provable in Γ.

Corollary

No theory consistent with Q_E has a recursive set of consequences.

If Δ were such a theory then the set of sentences ψ such that (Q_E → ψ) is a consequence of Δ would be a consistent, recursive set of sentences, closed under consequence, that included Q_E.

Corollary (Church's Theorem)

The set of logically valid sentences in not recursive.

The valid sentences are the consequences of the empty theory, which is consistent with Q_E.

Mathematical Induction

Q_E is a weak axiom system. It cannot prove the associative law of addition or multiplication, nor can it prove the commutative law of addition or multiplication. The system is weak because it leaves out the essential feature of the natural number system, the principle of mathematical induction, according to which any collection of natural numbers that includes 0 and is closed under the successor operation has to include all the natural numbers. Modulo Q_E, the principle is equivalent to the thesis that the natural numbers are well-founded, that is, that any nonempty collection of natural numbers has a least element.

Richard Dedekind showed that the system one gets from Q_E by adding the principle of mathematical induction completely characterizes the natural numbers. The system is categorical, that is, there is an isomorphism—a one-one correspondence that preserves mathematical structure—between any two models of the system. Thus if 𝔄 and 𝔅 are models of Q_E plus the principle of induction, let ƒ be the smallest class that includes the pair <0^𝔄, 0^𝔅> and includes <S^𝔄(x ), S^𝔅(y )> whenever it contains <x,y >. It is easy to verify, using induction several times, that ƒ is an isomorphism. It follows that the system is complete, since if it left ϕ undecided, it would have a model 𝔄 in which ϕ is true and a model 𝔅 in which ϕ is false; but then 𝔄 and 𝔅 could not be isomorphic.

Peano Arithmetic (PA), is the system used to formalize the principle of induction into a precise system of axioms. Its axioms are Q_E together with all instances of the induction axiom schema :
((R (0) ∧ (∀x )(R (x ) →R (Sx )))→(∀x )R (x )).
An induction axiom is a sentence of the language of arithmetic obtained from the schema by substituting a formula of the language of arithmetic for "R," then prefixing universal quantifiers to bind all the variables other than "x " that appear free in the substituted formula.

In view of Dedekind's categoricity theorem, it is surprising to realize that PA is incomplete. But incomplete it must be, since it is a true, recursively axiomatized theory that entails Q_E. The explanation is that the induction axiom schema does not fully capture the principle of mathematical induction. It tries to assure us that every nonempty collection has a least element, but only succeeds in telling us that every nonempty collection that is the extension of a predicate (with parameters) of the language of arithmetic has a least element.

Let γ be the Gödel sentence for PA. We know that γ isn't a consequence of PA, so that, by the Completeness Theorem, there is a model 𝔄 in which all the axioms of PA + ∼ γ are true. In 𝔄 there is an element g that satisfies "x B_PA ^┌γ^┐." For each n, "∼n B_PA ^┌γ^┐." is a theorem of PA, so g must be different from the referents of all the numerals 0, 1, 2, …. Instead, g is one of the nonstandard numbers that lie above all the standard numbers in the relation 𝔄 assigns to "≤."

It is worth emphasizing because there has been some confusion on this score that the existence of nonstandard models of PA does not depend on the First Incompleteness Theorem. Their existence follows from the Compactness Theorem, according to which an infinite set of sentences has a model if every finite subset does, which Gödel derived from the Completeness Theorem. Let Γ be a consistent theory that entails Q_E. Add a new constant "c " to the language, and let Γ^c be the union of Γ with the set of sentences "∼ c = n," for n natural number. Any finite subset of Γ^c has a model, obtained by taking a model of Γ and letting"c " denote a sufficiently large standard number. The Compactness Theorem gives us a model of Γ^c , which means we have a nonstandard model of Γ. This construction works even if we take Γ to be true arithmetic, the set of sentences true in the standard model, even though true arithmetic is complete. Because it is complete, the First Incompleteness Theorem tells us that true arithmetic is not recursively axiomatizable.

The Second Incompleteness Theorem

The proof of the First Incompleteness Theorem showed that, if Γ, a recursively axiomatized theory that entails Q_E, is consistent, then the Gödel sentence γ for Γ is unprovable in Γ. Using "Con (Γ)" as an abbreviation for
"∼ Bew _Γ(^┌ ∼ 0=0 ^┐ ),"
we can formalize this result in a sentence of the language of arithmetic:
(Con (Γ) → ∼ Bew _Γ(^┌ γ^┐ )).
If we were able to prove this conditional in Γ, we could conclude that, if Con (Γ) were provable in Γ, ∼ Bew _Γ;(^┌ γ^┐ ) would be provable in Γ. Since we already know that ∼ Bew _Γ(^┌γ^┐ ) is only provable in Γ if Γ is inconsistent, we could conclude that Con (Γ) is only provable in Γ if Γ is inconsistent.

Can we prove the conditional in Γ? We certainly cannot do so if we take Γ to be Q_E, for we can scarcely prove any significant generalizations in Q_E. We can, however, prove the conditional if we take Γ to be PA. This is hardly surprising, since nearly all our reasoning about natural numbers can be formalized in PA. The details are, nonetheless, burdensome; so we only present a faint sketch here.

Let Γ be a recursively axiomatized theory that entails PA. M. H. Löb singled out the following three principles as central to Gödel's proof that, if Γ is consistent, it does not prove Con (Γ):

1. If Γ ├ ϕ, then Γ ├ Bew _Γ(^┌ϕ^┐ ).
2. Γ ├ (Bew _Γ(^┌ϕ^┐ ) → Bew _Γ(^┌Bew Γ(^┌ϕ^┐ )^┐ )).
3. Γ ├ (Bew _Γ(^┌(ϕ → Ψ)^┐ ) → (Bew _Γ(^┌ϕ^┐ )→ Bew _Γ(^┌Ψ^┐ )).

We have already seen why (L1) has to hold. If ϕ is a consequence of Γ, Bew _Γ(^┌ϕ^┐ ) is a true Σ sentence, hence provable in Q_E, hence provable in Γ. (L2) is obtained, laboriously, by formalizing the proof of (L1). In fact, Γ proves (θ → Bew _Γ(^┌θ^┐ )), for each Σ sentence θ. (L3) is easy. If we have proofs of (ϕ → ψ) and ϕ, we get a proof of ψ by concatenating the two proofs and tacking ψ on the end.

Given the Löb conditions, the proof of the Second Incompleteness Theorem, according to which, if Γ is a consistent, recursively axiomatized theory that entails PA, then Γ does not prove its own consistency, is straightforward. Let γ be the Gödel sentence for Γ. Because of the way γ was constructed, we have:

Γ ├ (γ → ∼ Bew _Γ(^┌γ^┐ )),

which is logically equivalent to:

Γ ├ (γ → (Bew _Γ(^┌γ^┐ ) → ∼ 0=0)).

One application of (L1) and two applications of (L3) give us this:

Γ ├ (Bew _Γ(^┌γ^┐ ) → (Bew _Γ(^┌Bew _Γ(^┌γ^┐ )^┐ ) → Bew _Γ(^┌∼_0=0^┐ ))).

(L2) gives us this:

Γ ├ (Bew _Γ(^┌γ^┐ ) → Bew _Γ(^┌Bew _Γ(^┌γ^┐)^┐ )),

and these two results together give us:

Γ ├ (Bew _Γ(^┌γ^┐ ) → Bew _Γ(^┌∼ _0=0^┐ )).

By contraposition,

Γ ├ (∼ Bew _Γ ^┌∼_0=0^┐ ) → ∼ Bew _Γ (^┌γ^┐ )),

that is,

Γ ├ (Con (Γ) → ∼ Bew _Γ (^┌γ^┐) )

Now assume

Γ ├ Con (Γ).

Then

Γ ├ ∼ Bew _Γ (^┌γ^┐ ).

By the way γ was constructed,

Γ ├ γ.

Hence, by (L1),

Γ ├ Bew _Γ (^┌γ^┐ ),

and so Γ is inconsistent.

In accepting PA, we recognize that the axioms of PA are all true. If the axioms are all true then the theory is certainly consistent, and if the theory is consistent its Gödel sentence is true. So we have good reason to accept the Gödel sentence for PA, even though it is not a consequence of PA. If in this argument we replace PA with our total arithmetical theory—the (admittedly, vaguely defined) totality of arithmetical sentences we are willing to accept as true—we seem to get the curious result that, assuming that our total theory is recursively enumerable, we accept the Gödel sentence for our total theory even though it is not a consequence of the theory. But this contradicts the characterization of our total theory.

J. R. Lucas (1961) and Roger Penrose (1989) took this puzzling situation as reason to believe that the cognitive processes of the human mind cannot be simulated by any purely mechanical device, and that this conclusion undermines the prospects for a naturalistic conception of mind, according to which the human mind is a product of the orderly operation of the laws of nature, not in principle any more mysterious or less constrained by physical law than a player piano or a personal computer. Adherents to the computational theory of mind hold that the operations of the mind are usefully understood on the model of a sophisticated electronic computer, and even naturalists who are not advocates of the computational model will be inclined to say that the facts that the human body is produced by natural selection rather than conscious design and that its central processing unit is carbon-based rather than silicon-based will not affect its capabilities in any fundamental way, so that, accordingly to a naturalistic conception, the cognitive activities of a human being can, in principle, be simulated by a purely mechanical device.

The connection between mechanism and recursive enumerability is given by a variant of the Church-Turing Thesis, supported by similar evidence, that declares that the set of numbers accepted by a mechanical input-output device is invariably recursively enumerable. This includes nondeterministic machines, whose operation is to some extent a matter of random chance, so that the set S is accepted by the machine just in case, for any n, n is in S if and only if there is some possible computation of the machine on input n that yields a positive outcome, as well as deterministic machines for which the course of a computation is uniquely determined by its input.

The argument that our total arithmetical theory is not recursively enumerable proceeds by reductio ad absurdum. If the theory were recursively enumerable, it would be recursively axiomatizable, so it would have a Gödel sentence. But we can see that the Gödel sentence is true, even though it is not part of the total theory.

The Lucas-Penrose argument is vulnerable to two criticisms. First, for naturalism to be correct, there has to exist a recursive axiomatization of our total theory. In order to construct the Gödel sentence, we have to be able to specify a recursive axiomatization by writing down a formula that binumerates it. However it is perfectly possible for a recursive axiomatization to exist without our being able to specify it.

Second, even if we were able to specify a recursive axiomatization, perhaps by analyzing a futuristic brain scan, it is hard to see how we could be justified in being completely confident that our total theory is consistent. If we decide to be strict about what arithmetical sentences we are willing to count as "accepted," so that we only regard a sentence as part of our total theory if we arrive at it by unimpeachably lucid reasoning, we shall increase our confidence that our total theory is consistent, but raising the bar this way will also heighten the hurdle that the Gödel sentence has to pass in order to count as "accepted." There are different standards we might use for when we are willing to count a sentence as proven, and each standard has a different Gödel sentence, but however high we set the standard the Gödel sentence corresponding to that standard cannot pass it, on pain of inconsistency.

The Logic of Provabilty

If we explicitly embrace a theory Γ, so that we are willing consciously to acknowledge that the axioms of Γ are all statements we regard as true then we surely ought to regard Γ as consistent. Yet (assuming that Γ implies PA and is recursively axiomatizable and consistent) the statement that Γ is consistent is not provable in Γ. Thus the arithmetical statements that we commit ourselves to in embracing Γ go beyond what Γ itself entails.

The disparity between what consciously accepting Γ commits us to and what Γ entails is even wider than the Second Incompleteness Theorem indicates. Accepting Γ means acknowledging that all the consequences of Γ are true. For a given sentence ϕ, we may not know whether ϕ is a consequence of Γ—there is after all no algorithm to tell us—but at least we accept that, if ϕ is a consequence of Γ, ϕ is true. Consciously accepting Γ commits us to the conditionals Bew _Γ(^┌ϕ^┐ ) → ϕ), but they are not in general consequences of Γ. In fact such a conditional is a consequence of Γ only if its consequent is a consequence of Γ.

Löb's Theorem. Let Γ be a recursively axiomatized theory that entails PA. If Bew _Γ(^┌ϕ^┐ ) → ϕ) is a consequence of Γ, so is ϕ.

We can regard the Second Incompleteness Theorem as the special case of Löb's Theorem in which ϕ is taken to be the sentence "∼ 0=0." Conversely we can derive Löb's Theorem from the Second Incompleteness Theorem. The argument, which is due to Saul Kripke, utilizes the observation that, for any ψ and θ, Γ ├ (ψ → θ) if and only if Γ ∪ {ψ} ├ θ, and the fact that this observation is provable in PA.

Suppose that ϕ is not a consequence of Γ. Then Γ ∪ {∼ ϕ} is consistent, which implies, by the Second Incompleteness Theorem, that Con (Γ ∪ {∼ ϕ}) is not a consequence of Γ ∪ {∼ ϕ}. Thus we have:

Γ ∪ {∼ ϕ} ⊬ ∼ Bew _{Γ ∪ {∼ϕ}}(^┌∼0=0^┐ )

Γ ∪ {∼ ϕ} ⊬ ∼ Bew _Γ(^┌(∼ ϕ → ∼0=0^┐ )

Γ ∪ {∼ ϕ} ⊬ ∼ Bew _Γ(^┌ϕ^┐ )

Γ ⊬ (∼ ϕ → ∼ Bew _Γ(^┌ϕ^┐ ))

Γ ⊬ Bew _Γ(^┌ϕ^┐ ) → ϕ)

Conditionals of the form Bew _Γ(^┌ϕ^┐ ) → ϕ) are called reflection principles. We cannot obtain them by working within Γ. We get them from the outside by reflecting on the fact that Γ is a theory we accept.

We can describe the logic of provability precisely by utilizing the methods of modal logic. Modal sentential calculus has, in addition to formulas built up from atomic formulas by the familiar connectives "∨" and "∼," a new connective "□." "□ϕ," usually read "It is necessary that ϕ," is here understood to mean, "It is provable in Γ that ϕ," where Γ is a consistent, recursively axiomatizable theory that implies PA. An interpretation of the modal sentential calculus is a function i that associates an arithmetical sentence with each modal formula, subject to the conditions that i (ϕ ∨ ψ) be equal to (i (ϕ) ∨ i(ψ)), i (∼ϕ) be equal to ∼ i (ϕ), and i (□ϕ) be equal to Bew _Γ^┌i (ϕ)^┐. A modal formula ϕ is always provable if, for each interpretation i, i (ϕ) is provable in Γ. ϕ is always true if, for each ϕ, i (ϕ) is true.

(L1) tells us, if i (P ) is provable, i (□P ) is provable, so that the set of always-provable formulas is closed under necessitation, the rule of modal logic that infers □θ from θ. (L2) tells us that (□P → □ □ P ) is always true, and the formalization of (L2) tells us that it is always provable. (L3) tells us that (□(P → Q) → (□P → □Q )) is always true; it is easily seen to be always provable as well. Löb's Theorem tells us that whenever i (□P → P) is a theorem, i (P ) is a theorem. Formalizing his proof, we see that the formula (□(□P →P ) → □P ) is always provable and always true.

Robert Solovay deployed an ingenious application of the Self-referential Lemma within the possible-world semantics for modal logic to show that, provided Γ does not prove any false Σ sentences, a formula is always provable if and only if it is derivable by modus ponens and necessitation from sentential-calculus tautologies (formulas that are assigned the value "true" by every function assigning truth-values to formulas that respects the meanings of "∨" and "∼") and instances of the following schemata:

(□(ϕ → ψ) → (□ϕ → □ψ)) (□(□ϕ → ϕ) → □ϕ)

Assuming Γ is true, a formula is always true if and only if it is derivable by modus ponens from always-provable formulas and instances of the reflection principle (□ϕ → ϕ).

Beyond the Language of Arithmetic

Gödel's results apply not only to the language of arithmetic but to any language into which the language of arithmetic can be translated. Thus any recursively axiomatized, consistent theory into which one can translate Q_E is incomplete. The appropriate notion of translation was made precise by Tarski, Mostowski, and Robinson. An interpretation (what they call a "relative interpretation") of an arithmetical theory Γ into a language 𝓛 is obtained by doing the following: First, having rewritten all the sentences in Γ so that the "+" sign only appears in the canonical form "(v _i + v _j ) = v _k ," pick a formula "A (x,y,z )" of 𝓛 and replace "(v _i + v _j) = v _k," by "A (v _i ,v_j,v_k )," changing bound variables to avoid conflicts. Do the same thing for the other function signs and "0" and pick a formula L (x,y ) to replace "≤." Next pick a formula "N (x )" of 𝓛 to represent the members of the domain of 𝓛 that are to play the role of natural numbers, and restrict the quantifiers, writing "(∃v _i )(N (v _i ∧ …") in place of (∃v _i ). Finally add an axiom ensuring that "A (x,y,z )" represents a function on the set of things that satisfy "N (x )," writing " (∀x )(N (x ) → (∀y )(N(y ) → (∃z )(N (z ) ∧ (∀w )(N (w ) → (A (x,y,w ) ↔ w = z ))))." Do the same thing for the other function signs and "0." If the theory thus obtained is a consequence of the theory Δ of 𝓛, Δ is said to interpret Γ.