Gödel's Incompleteness Theorems

Updated Print Article Share Article
views updated

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 0, v 1, v 2, v 3, , 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 0 is prime' is formalized by the bounded formula '(SS0v 0 (v 1v 0)(v 2v 0)(v 0 = (v 1 x v 2) (v 1 = S0 v 2 = 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 0), we can test whether n S by asking whether σ(ṉ ) 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 1)(x 2)(xn )ϕ is equivalent to (x 0)(x 1x 0)(x 1x 0)(xn x 0)ϕ. (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 2 + 2xy + y 2 + 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 0: (x 1)σ(x 0,x 1)}, 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 confusinga collection of ordered pairs can be a partial recursive function without being a recursive relationbut 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 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 0,k 1, ,k m> as the number Code ({Pair (0,k 0), Pair (1,k 1), , 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 0,x 1,,xn > of numbers x with the following properties:

x 0 = x.

If xi has the form <2,y >, then i < n and x i +1 = y.

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

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

xn 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 0,x 1,,xn > with the following features:

x 0 = <0,0>.

For m < n, x m +1 = <2,xm >.

xn = 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 17 appears and the set of formulas in which v 123 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 calculusthe 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. QE, 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 QE 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 QE. Another induction shows that every bounded sentence is decidable (either provable or refutable) in QE. Since every true bounded sentence is provable in QE, it follows that every true Σ sentence is provable in QE, 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 QE and (because QE is true) no false Σ sentence is provable, we have (where "" is provability):

For any n, n S if and only if QE σ(n ).

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

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

n S if and only if QE ϕ(n ).

n S if and only if QE ϕ(n ).

If S is recursive then there is a bounded formula χ(x,y ) such that (y )χ(x,y ) enumerates S in QE, and there is a bounded formula θ(x,y ) such that (y )θ(x,y ) enumerates the complement of S in QE. To show that S is binumerable in QE, 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 QE, it binumerates S in any consistent theory that entails QE.

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 QE. Tarski, Mostowski, and Robinson showed that the following formula functionally represents ƒ in QE (and hence in any theory that entails QE):
(ϕ(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 QE, 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 QE (ϕ ψ( ϕ )).

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 QE. 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 QE:

(y )(θ(m,y ) y = ϕ ).

((x )(y )((x = m θ(x,y )) ψ(y )) ψ(ϕ )).

(ϕ ψ(ϕ )).

Let Γ be a consistent, recursive set of sentences that entails QE. Using the Self-reference Lemma, we can find a sentence γ so that (Γ Bew γγ ) is a consequence of QE; γ 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 QE, 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 QE, 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 QE, 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 QE 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 QE and excludes all the sentences refutable in QE.

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

Case 1

ν C. Then QE μ(ν ), and so QE ν. Thus υ is a sentence refutable in QE, and so it is excluded from C. Contradiction.

Case 2

υ C. Then QE μ(ν ), and so QE ν. Thus υ is a consequence of QE, and so an element of C. Contradiction.

Corollary

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

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

Corollary (Rosser's Theorem)

No consistent, recursively axiomatized theory that entails QE 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 QE has a recursive set of consequences.

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

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

Mathematical Induction

QE 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 QE, 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 QE by adding the principle of mathematical induction completely characterizes the natural numbers. The system is categorical, that is, there is an isomorphisma one-one correspondence that preserves mathematical structurebetween any two models of the system. Thus if 𝔄 and 𝔅 are models of QE 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 QE 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 QE. 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 BPA γ." For each n, "n BPA γ." 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 QE. 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 QE, 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 QE, for we can scarcely prove any significant generalizations in QE. 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 QE, 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 theorythe (admittedly, vaguely defined) totality of arithmetical sentences we are willing to accept as truewe 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 usbut 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 QE 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 ,vj,vk )," 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 Γ.

We can translate the language of arithmetic into the language of set theory, identifying a number with the set of its predecessors, so that 0 corresponds to , 1 corresponds to {}, 2 corresponds to {, {}}, and so on, and defining set-theoretic analogues of "+," "×," "E," "S," and "" accordingly. The axioms of set theory, in any of its normal versions, interpret PA. We can arithmetize proofs in set theory just as we artimeticized proofs in PA, proving the Second Incompleteness Theorem for set theory. The axioms of set theory, if consistent, cannot prove their own consistency.

This result devastates the Hilbert program. Hilbert wanted to prove the consistency of set theory in a finitistic theory much weaker than set theory, and it turns out that proving the consistency of set theory requires a theory even stronger than set theory.

The standard way to prove that there is no algorithm for testing whether a given sentence is a consequence of a theory Γthat is, for showing that Γ is undecidable is to interpret an arithmetical theory strong enough to prove the First Incompleteness Theorem into Γ. As far as what we have looked at so far, we would need to take our arithmetical theory to be QE, but we can actually do much better. We can define exponentiation in terms of "0," "S," "+," and "×," and we can prove the First Incompleteness Theorem in the dialect of the language of arithmetic without "E," with Q in place of QE. In trying to prove undecidablity results, this improvement (which is due to Gödel) is an enormous practical advantage.

Let us define β(u,v,w ) to be the remainder obtained on dividing u by (v ×w ) + 1. β can be defined by a bounded formula in the language of arithmetic. For x > 0, we have (x Ey ) = z if and only if the following formula is satisfied:
(u )(v )((β(u,v,0) = 1 (w < y )β(u,v,Sw ) = (β(u,v,w ) × x )) β(u,v,y ) = z ).
The right-to-left direction of this characterization is obvious. What is hard is to verify the left-to-right direction by finding an appropriate u and v. We make use of the Chinese Remainder Theorem, which says that, given p 0, p 1, , p n relatively prime (that is, no two of the pi s have a common divisor other than 1), and given a sequence a 0, a 1, , an, with each ai < pi, we can find a number b such that ai is the remainder on dividing b by pi, for each i. A proof of the theorem can be found in any number-theory textbook or in George Boolos's The Logic of Provability (1993).

Given x,y, and z with (x Ey ) = z, let v = z !, the product of the positive integers z. If s < t z, then (s ×v ) + 1 and (t ×v ) + 1 are relatively prime, since if p were a prime that divided both of them, p would divide (t - s ) × v, and so, since (t - s ) is one of the factors of v, p would divide v. But this enables us to conclude that the remainder on dividing (t ×v ) + 1 by p is one, contrary to our assumption that p divides (t ×v ) + 1. Use the Chinese Remainder Theorem to find u so that, for each t y, x Et is the remainder on dividing u by (t ×v ) + 1.

Now that we have our Σ definition of exponentiationΣ, that is, in the restricted languagewe can apply our standard tricks for pulling quantifiers to the fronts of formulas to convert a Σ formula of the language with exponentiation to a Σ formula of the language without exponentiation. With this emendation, all the proofs go through.

The use of interpretations originates with Beltrami's proof of the consistency of non-Euclidean geometry. By interpreting non-Euclidean geometry (Euclid's axioms with the axiom of parallels replaced by its negation) into Euclidean geometry, Beltrami showed that if the latter is consistent then so is the the former. Beltrami's strategy was exploited by Alex Wilkie and Samuel Buss to obtain a dramatic strengthening of the Second Incompleteness Theorem, applying it to theories that merely contain Q rather than PA. The details are complicated, but the idea is to interpret into Q a theory that, while weaker than PA (the induction axiom schema being restricted), is just strong enough to provide the Löb conditions (L1)-(L3). The interpretation leaves the arithmetical symbols unchanged but restricts the domain of quantification to an initial segment, replacing "(x )" by "(x )(J (x ) ," for artfully chosen "J (x );" call the sentence thus obtained from ϕ "ϕJ ."

Where Γ is a recursively axiomatized theory that includes Q, let Γ-J be the set of sentences ϕ for which Γ entails ϕJ . Suppose that Γ entails Con(Γ). Con(Γ) entails Con(Γ)J , so that Con(Γ) is in Γ-J . The argument Beltrami used tells us that if Γ is consistent then Γ-J is too. This proof can be formalized in Γ-J , so that Γ-J entails Con(Γ-J ). Because (L1)-(L3) yield the Second Incompleteness Theorem for Γ-J , Γ-J must be inconsistent. Consequently Γ is inconsistent.

Truth

There is a bounded formula of the language of arithmetic that defines the set of prime numbers, and there is a Σ formula that defines the set of consequences of PA. Tarski proved that there is no formula of the language of arithmetic that defines the set of codes of true sentences. The difficult part of his argument was to say precisely what would be required for a formula to define truth; the easy part is to show that there is no such formula.

A proposed definition of truth is a formula of the form (Tr (x ) τ(x )), where τ(x ) is a formula of the language of arithmetic. A proposed definition is materially adequate, Tarski tells us, if and only if it lets us derive all sentences of the form:
(T)      Tr (ϕ) ϕ.
To see that there is no materially adequate definition, apply the Self-reference Lemma to find a sentence λ so that (λ τ(λ )) is a consequence of Q. The argument here is a formalization of the paradox posed by Eubulides, who asked whether a man who says "I am lying" speaks truthfully.

We can define the set of true sentences of the language of arithmetic within, say, the language of set theory, but we cannot define it within the language of arithmetic. This negative result obtains for any language into which we can translate the language of arithmetic.

The question of what moral, if any, these formal results have for the notion of truth as applied to natural languages is deeply troubling. Tarski showed that there is no formula of the language of arithmetic that means (or even has the same extension as) "true sentence of the language of arithmetic." Manifestly there is a phrase of English that means "true sentence of English," and Tarski and Eubulides' reasoning would appear to apply to that phrase just as to the formal language. Is there in spite of this a coherent way to talk about the truth of an English sentence?

Bibliography

Aristotle. Prior Analytics. In Complete Works of Aristotle, edited by Jonathan Barnes. Princeton, NJ: Princeton University Press, 1995.

Beltrami, Eugenio. "Saggio di Interpretazione della Geometria Noneuclidea." Giornale di Matematiche 6 (1868): 284312.

Boolos, George S. The Logic of Provability. Cambridge, U.K.: Cambridge University Press, 1993.

Buss, Samuel R. "First-Order Proof Theory of Arithmetic." In Handbook of Proof Theory, edited by Samuel R. Buss, 79147. Amsterdam-Elsevier, 1998.

Church, Alonzo. "A Note on the Entscheidungsproblem." Journal of Symbolic Logic 1 (1936): 4041, with a correction on pp. 101102. Reprinted in 110115. The Undecidable, edited by Martin Davis/Hewlett, NY: Raven Press, 1965.

Craig, William. "On Axiomatizability Within a System." Journal of Symbolic Logic 18 (1953): 3032.

Davis, Martin. The Undecidable. Hewlett, NY: Raven Press, 1965.

Dedekind, Richard. Was sind und was sollen die Zahlen? Brunswick: Vieweg, 1888. Reprinted in Dedekind, Essays on the Theory of Numbers. New York: Dover, 1963, 29115.

Euclid. Elements. 2 vols. Translated by Thomas L. Heath. 2nd ed. New York: Dover, 1956.

Frege, Gottlob. Begriffschrift. Halle: L. Nebert, 1879. Reprinted in From Frege to Gödel, edited by Jean van Heijenoort. 182. Cambridge, MA: Harvard University Press, 1967.

Gödel, Kurt. "Die Vollständigkeit der Axiome der logischen Funktionenkalküls." Monatschefte für Mathematik un Physik 37 (1930): 349360. Reprinted in From Frege to Gödel, edited by Jean van Heijenoort (1967), 583591. Also reprinted in Gödel, Collected Works, vol. I, 144195. New York: Oxford University Press, 1986.

Gödel, Kurt. "Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I." Monatshefte für Mathematik und Physik 38 (1931): 173198. Reprinted in The Undecidable, edited by Martin Davis, 438. Hewlett, NY: Raven Press, 1965. Also reprinted in From Frege to Gödel, edited by Jean van Heijenoort (1967), 596628. Also reprinted in Gödel, Collected Works, vol. I, 102123. New York: Oxford University Press, 1986.

Hájek, Petr, and Pavel Pudlák. Metamathematics of First-Order Arithmetic. New York: Springer, 1993.

Hilbert, David. "Über dan Undendliche." Mathematische Annalen 95 (1926): 161190. Reprinted in From Frege to Gödel, edited by Jean van Heijenoort. 367392. Cambridge, MA: Harvard University Press, 1967.

Löb, M. H. "Solution to a Problem of Leon Henkin." Journal of Symbolic Logic 20 (1955): 115118.

Lucas, J. R. "Minds, Machines, and Gödel." Philosophy 36 (1961): 120124.

Penrose, Roger. The Emperor's New Mind. New York: Oxford University Press, 1989.

Quine, Willard van Orman. Mathematical Logic. 2nd ed. Cambridge, MA: Harvard University Press, 1951.

Rosser, John Barclay. "Extensions of Some Theorems of Gödel and Church." Journal of Symbolic Logic 1 (1936): 8791. Reprinted in The Undecidable, edited by Martin Davis, 231235. Hewlett, NY: Raven Press, 1965.

Smorynski, Craig. "The Incompleteness Theorems." In Handbook of Mathematical Logic, edited by Jon Barwise, 821865. New York: North-Holland, 1977.

Smullyan, Raymond M. Gödel's Incompleteness Theorems. New York: Oxford University Press, 1992.

Solovay, Robert M. "Provability Interpretations of Modal Logic." Israel Journal of Mathematics 25 (1976): 287304.

Tarski, Alfred. "Der Wahrheitsbegriff in den formalisierten Sprachen." Studia Philosophica 1 (1935): 261405. Reprinted in Tarski, Logic, Semantics, Metamathematics, 2nd ed., 152278. Indianapolis: Hackett, 1983.

Tarski, Alfred, Andrzej Mostowski, and Raphael M. Robinson. Undecidable Theories. Amsterdam: North-Holland, 1953.

Turing, Alan Mathison. "On Computable Numbers, with an Application to the Entscheidungsproblem." Proceedings of the London Mathematical Society, 2nd series, 42 (1937): 230265, with a correction at vol. 43 (1938): 544546. Reprinted in The Undecidable, edited by Martin Davis, 115154. Hewlett, NY: Raven Press, 1965.

Van Heijenoort, Jean. From Frege to Gödel. Cambridge, MA: Harvard University Press, 1967.

Wilkie, Alex J., and Jeff B. Paris. "On the Scheme of Induction for Bounded Arithmetic Formulas." Annals of Pure and Applied Logic 35 (1987): 261302.

Vann McGee (2005)