Gödel's Incompleteness Theorems

First published Mon Nov 11, 2013; substantive revision Tue Jan 20, 2015

Gödel's two incompleteness theorems are among the most important results in modern logic, and have deep implications for various issues. They concern the limits of provability in formal axiomatic theories. The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F. According to the second incompleteness theorem, such a formal system cannot prove that the system itself is consistent (assuming it is indeed consistent). These results have had a great impact on the philosophy of mathematics and logic. There have been attempts to apply the results also in other areas of philosophy such as the philosophy of mind, but these attempted applications are more controversial. The present entry surveys the two incompleteness theorems and various issues surrounding them. (See also the entry on Kurt Gödel for a discussion of the incompleteness theorems that contextualizes them within a broader discussion of his mathematical and philosophical work.)

1. Introduction

1.1 Outline

Gödel's incompleteness theorems are among the most important results in modern logic. These discoveries revolutionized the understanding of mathematics and logic, and had dramatic implications for the philosophy of mathematics. There have also been attempts to apply them in other fields of philosophy, but the legitimacy of many such applications is much more controversial.

In order to understand Gödel's theorems, one must first explain the key concepts essential to it, such as “formal system”, “consistency”, and “completeness”. Roughly, a formal system is a system of axioms equipped with rules of inference, which allow one to generate new theorems. The set of axioms is required to be finite or at least decidable, i.e., there must be an algorithm (an effective method) which enables one to mechanically decide whether a given statement is an axiom or not. If this condition is satisfied, the theory is called “recursively axiomatizable”, or, simply, “axiomatizable”. The rules of inference (of a formal system) are also effective operations, such that it can always be mechanically decided whether one has a legitimate application of a rule of inference at hand. Consequently, it is also possible to decide for any given finite sequence of formulas, whether it constitutes a genuine derivation, or a proof, in the system—given the axioms and the rules of inference of the system.

A formal system is complete if for every statement of the language of the system, either the statement or its negation can be derived (i.e., proved) in the system. A formal system is consistent if there is no statement such that the statement itself and its negation are both derivable in the system. Only consistent systems are of any interest in this context, for it is an elementary fact of logic that in an inconsistent formal system every statement is derivable, and consequently, such a system is trivially complete.

Gödel established two different though related incompleteness theorems, usually called the first incompleteness theorem and the second incompleteness theorem. “Gödel's theorem” is sometimes used to refer to the conjunction of these two, but may refer to either—usually the first—separately. Accommodating an improvement due to J. Barkley Rosser in 1936, the first theorem can be stated, roughly, as follows:

First incompleteness theorem
Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.

Gödel's theorem does not merely claim that such statements exist: the method of Gödel's proof explicitly produces a particular sentence that is neither provable nor refutable in F; the “undecidable” statement can be found mechanically from a specification of F. The sentence in question is a relatively simple statement of number theory, a purely universal arithmetical sentence.

A common misunderstanding is to interpret Gödel's first theorem as showing that there are truths that cannot be proved. This is, however, incorrect, for the incompleteness theorem does not deal with provability in any absolute sense, but only concerns derivability in some particular formal system or another. For any statement A unprovable in a particular formal system F, there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC; see the section on the axioms of ZFC in the entry on set theory), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel's first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today's “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.

Gödel's second incompleteness theorem concerns the limits of consistency proofs. A rough statement is:

Second incompleteness theorem
For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.

In the case of the second theorem, F must contain a little bit more arithmetic than in the case of the first theorem, which holds under very weak conditions. It is important to note that this result, like the first incompleteness theorem, is a theorem about formal provability, or derivability (which is always relative to some formal system; in this case, to F itself). It does not say anything about whether, for a particular theory T satisfying the conditions of the theorem, the statement “T is consistent” can be proved in the sense of being shown to be true by a conclusive argument, or by a proof generally acceptable for mathematicians. For many theories, this is perfectly possible.

1.2 Some Formalized Theories

The existence of incomplete theories is hardly surprising. Take any theory, even a complete one (see below for examples), and drop some axiom; unless the axiom is redundant, the resulting system is incomplete. The incompleteness theorems, however, deal with a much more radical kind of incompleteness phenomenon. Unlike the above sort of trivially incomplete theories, which can be easily completed, there is no way of completing the relevant theories; all their extensions, inasmuch as they are still formal systems and hence axiomatizable, are also incomplete. They remain, so to speak, eternally incomplete and can never be completed. They are “essentially incomplete”.

In the first and loose statements of the incompleteness theorems given above, the vague requirement that “a certain amount of elementary arithmetic can be carried out” occurred. It is time to make this more precise.

1.2.1 Arithmetical Theories

The weakest standard system of arithmetic that is usually considered in connection with incompleteness and undecidability is so-called Robinson arithmetic (due to Raphael M. Robinson; see Tarski, Mostowski and Robinson 1953), standardly denoted as Q. As axioms, it has the following seven assumptions:

  • ¬(0 = x′)
  • x′ = y′ → x = y
  • ¬(x = 0) → ∃y(x = y′)
  • x + 0 = x
  • x + y′ = (x + y)′
  • x × 0 = 0
  • x × y′ = (x × y) + x

The intended interpretation of “ x′ ” is the successor function, and obviously, of + and ×, the addition and the multiplication functions, respectively. “0” is the only constant and denotes the number zero.

Adding to these elementary axioms the axiom scheme of induction:

(IND)
φ(0) ∧ ∀x[φ(x) → φ(x′)] → ∀xφ(x),

results in (first order) Peano Arithmetic (PA). Note that unlike Q, PA contains infinitely many axioms, because all (infinitely many) instances of the induction scheme, one corresponding to every formula φ(x) (with at least one free variable) of the language, are taken as axioms. But it is a routine mechanical task to check whether a given sentence is an instance of this scheme. PA is generally taken as the standard first-order system of arithmetic.

Another natural and much-studied arithmetical system, which lies between Q and PA in strength, is Primitive Recursive Arithmetic (PRA). It contains not just the above axioms of Q governing successor, addition and multiplication, but also defining axioms for all primitive recursive functions (see the entry on recursive functions), and the application of the induction scheme is restricted to quantifier-free formulas (i.e., φ(x) is not allowed to contain any (unbounded) quantifiers).

However, essentially the same system is obtained if one takes just the axioms of Q and the induction scheme restricted to, roughly, purely existential formulas (in technical terms, Σ01-formulas; see below) (this was first showed by Parsons 1970). Moreover, Σ01-induction can be shown (Paris and Kirby 1978) to be equivalent to the induction scheme restricted to (roughly) purely universal formulas (Π01-formulas). PRA can also be formulated as a “logic-free” equational calculus. PRA, or something equivalent to it, is sufficient for developing the theory of syntax for formalized theories. It is often taken as the unproblematic background theory in which various other systems, whose legitimacy may be more controversial, are studied.

A much stronger system than PA, important in the foundations of mathematics, which will be mentioned now and then below, is second-order arithmetic PA2 (also often denoted by Z2). It is more than sufficient for developing all ordinary analysis and algebra. Its language is a two-sorted first-order language (see then entry on second-order and higher-order logic), i.e., it contains two sorts of variables, number variables x1,x2, … (or x, y, z, …) and set variables X1, X2, … (or X, Y, Z, …) and as axioms, in addition to the basic axioms of PA, all instances of the comprehension scheme:

  • ∃X∀x[Xx ↔ φ(x)]

where φ(x) can be any formula of the language of PA2 in which X doesn't occur free.

PA2 is a very strong theory. Via the method of interpretations (see below), one can show that it is proof-theoretically as strong as the Zermelo-Fraenkel set theory ZFC without the power-set axiom, call it ZFC–Pow (whereas the standard, first-order PA is similarly proof-theoretically equivalent to ZFC without the axiom of infinity, ZFC–Inf). (cf. the section on the axioms of ZFC in the entry on set theory)

Obviously, it is assumed that our formal systems are also equipped with a system of rules of inferences (and possibly some logical axioms), usually some standard system of classical logic (though the incompleteness theorems do not essentially presuppose classical logic, but also apply to systems with, e.g., intuitionistic logic). The above standard systems all come with classical logic. The standard notation F ⊢ A is used to express (in the meta-level) that A is derivable in F, that is, that there is a proof of A in F, or, in other words, that A is a theorem of F. Accordingly, F ⊬ A means that A is not derivable in F.

To summarize: when it is said, in the context of the incompleteness theorems, that “a certain amount of elementary arithmetic can be carried out” in a system, this usually means that it contains PRA or at least Q. For the first incompleteness theorem, Q is sufficient; for the standard proofs of the second theorem, something like PRA, at a minimum, is needed. There is a version of the second incompleteness theorem for Q (see Bezboruah & Shepherdson 1976) but there has been some debate on whether the relevant statement in Q can really be taken to express consistency, Q being so weak (see Kreisel 1958; Bezboruah & Shepherdson 1976; Pudlák 1996; Franks 2009).

1.2.2 Theories not Formulated in the Language of Arithmetic

Of course, there are many important and interesting theories in mathematics which are not even formulated in the language of arithmetic. However, the applicability of the incompleteness theorems can be dramatically extended outside the language of first-order arithmetic and its extensions, when it is noted that all that is needed is that weak theories such as Q, or PRA, can be interpreted in the system in question. Most importantly, this involves various systems of set theory. For example, the incompleteness theorems hold for ZFC–Inf (i.e., ZFC without the axiom of infinity) and all its extensions, however strong (as long as they are axiomatizable.)

Roughly, a theory T1 is interpretable in another theory T2 if the primitive concepts and the range of the variables of T1 are definable in T2 so that it is possible to translate every theorem of T1 into a theorem of T2. One should not misunderstand such interpretations as providing anything like intuitive synonymity. Two theories may have radically different intended subject matter and yet, as formal systems, one may be interpretable in another. (As an illustration: a simple theory of ancestors may be, taken as a formal system, interpreted in arithmetic; obviously this does not mean that grandmothers and such are really numbers.) What is significant is that interpretability preserves certain elementary formal properties of theories, most importantly, consistency: if T1 is interpretable in T2 and T2 is consistent, T1 is also consistent. And any system in which Q can be interpreted is guaranteed to be essentially incomplete. For any such theory in which Q is interpretable, the incompleteness could be proved also directly; for example, in various theories of set theory, one can code formulas and derivations (instead of numbers) by sets, “Gödel sets”, and proceed then as usual (see, e.g., Fitting 2007). However, for most purposes, it is just much simpler to establish the interpretability of Q in the theory at issue.

In sum, when it is said that “a certain amount of elementary arithmetic can be carried out within a system”, what is meant is either that the system is an axiomatizable extension of Q, or that Q can be interpreted in it. (In the case of (the standard proofs of) the second incompleteness theorem, substitute PRA for Q).

1.2.3 Some Exceptions: Complete Theories

On the other hand, not all theories of arithmetic are incomplete. The theory of only addition of natural numbers but without multiplication (often called “Presburger arithmetic”), for example, is complete (and decidable) (Presburger 1929), as is the theory of multiplication of the positive integers (Skolem 1930). These theories are, though, very weak. But in any case, at least a theory which deals with both addition and multiplication is needed. More interestingly, the natural first-order theory of arithmetic of real numbers (with both addition and multiplication), the so-called theory of real closed fields (RCF), is both complete and decidable, as was shown by Tarski (1948); he also demonstrated that the first-order theory of Euclidean geometry is complete and decidable. Thus, one should keep in mind that there are some non-trivial and interesting theories to which Gödel's theorems do not apply.

1.3 The Relevance of the Church-Turing Thesis

Gödel originally only established the incompleteness of a particular though very comprehensive formalized theory P, a variant of Russell's type-theoretical system PM (for Principia Mathematica, see the sections on Paradoxes and Russell's Type Theories in the entries on type theory and Principia Mathematica), and all extension of P with the same language, whose set of axioms is primitive recursive. He also suggested, though did not demonstrate, that the proof could be adapted to apply also to the standard axiom systems of set theory such as ZFC. Though it turns out that Gödel in fact already had a very general result, it was, at the time, unclear just how general this really was (see also Section 5).

What was still missing was an analysis of the intuitive notion of decidability, needed in the characterization of the notion of an arbitrary formal system. Recall that the set of axioms and the proof relation of a formalized system are required to be decidable. Mathematicians and logicians have implicitly used the intuitive notion of a decision method since antiquity, and as long as one asked for a positive solution, it was sufficient that one presented a concrete method that intuitively striked everyone as a mechanical method. For the general limitative results, such as the general incompleteness theorems, or the undecidability results (see 4.2), however, a precise mathematical explication of the notion would be needed. Instead of decidable sets or properties, one often considers effective or computable functions or operations, but in fact these are just two sides of the same coin—talk of one can be easily transcribed to talk of another.

Gödel (1934), Alonzo Church (1936a, b) and Alan Turing (1936–7) came up independently with different proposals for an exact mathematical definition of computable functions, and consequently, of decidable sets (of numbers). These proposals, though, all turned out to be equivalent. Turing's careful conceptual analysis which used fictional and abstract computing machines (nowadays conventionally called “Turing machines”; see the entry on Turing machines) was particularly important, as Gödel himself emphasized (see, e.g., Gödel 1963). The equation of the intuitive notion and some of these mathematical explications is often called “The Church-Turing-thesis”. The label “recursive function” has, for historical reasons, been dominant in the logical literature. Consequently, decidable sets are often called “recursive sets”. (See the entries on computability, recursive functions and the Church-Turing thesis.)

For a proper understanding of the incompleteness and undecidability results, it is vital to understand the difference between the two key notions regarding sets. First, there may be a mechanical method which decides whether any given number belongs to the set at issue or not (in which case the set is called “decidable” or “recursive”), and, second, there may be a mechanical method which generates or lists the elements of the set, number by number. In the latter case, the set is called “recursively enumerable” (r.e.), that is to say, it can be effectively generated, or it is “semi-decidable.” It is a fundamental result of the theory of computability (or “the theory of recursive functions”) that there are semi-decidable sets, sets which can be effectively generated (i.e., are recursively enumerable), but are not decidable (i.e., not recursive). In fact, this is, in the very abstract level, the essence of the first incompleteness theorem. However, if both a set and its complement are recursively enumerable, the set is recursive, i.e., decidable.

2. The First Incompleteness Theorem

In this section, the main lines of the proof of the first incompleteness theorem are sketched. A reader interested in more details can consult the Supplements (Gödel Numbering and The Diagonalization Lemma).

2.1 Preliminaries

The formal term (“numeral”) canonically denoting the natural number n is abbreviated as n. In the standard language of arithmetic used here, the number n is denoted by the term 0′…′, where the successor symbol ‘ ′ ’ is iterated n times. That is, numerals which name 1, 2, 3, … are 0′, 0′′, 0′′′, … and are abbreviated by 1, 2, 3, …

In his original proof, Gödel used his specific notion of ω-consistency, and for some purposes, it is still convenient to follow Gödel's original approach. A formalized theory F is ω-consistent if it is not the case that for some formula A(x), both F ⊢ ¬A(n) for all n, and F ⊢ ∃xA(x). Naturally this implies normal consistency, and follows from the assumption that the natural numbers satisfy the axioms of F.

Actually, a simple special case of ω-consistency suffices here; namely, the assumption is only needed with respect to what logicians call Σ01-formulas; these are, roughly, the purely existential formulas; more exactly, formulas of the form ∃x1∃x2…∃xnA, where A does not contain any unbounded quantifiers (A may contain bounded universal quantifiers ∀x < t and bounded existential quantifiers ∃x < t). This restricted ω-consistency is called 1-consistency.

ω-consistency and 1-consistency are purely syntactic notions. If the use of the notions of truth and falsity is allowed, the assumption of 1-consistency can be expressed intuitively simply as the requirement that the formal system in question does not prove any false Σ01-sentences (i.e., the system is sound at least in the case of such sentences). From now on, it is assumed that the formalized systems under consideration contain Q and are assumed to be at least 1-consistent, unless otherwise stated.

2.2 Representability

Gödel's proof also requires the notion of representability of sets and relations in a formal system F. More precisely, two related notion are needed.

A set S of natural numbers is strongly representable in F if there is a formula A(x) of the language of F with one free variable x such that for every natural number n:

  • n ∈ S ⇒ F ⊢ A(n);
  • n ∉ S ⇒ F ⊢ ¬A(n),

A set S of natural numbers is weakly representable in F if there is a formula A(x) of the language of F such that for every natural number n:

  • n ∈ S ⇔ F ⊢ A(n).

It is obvious how all these notions are generalized to many-place relations. There are also related notions of representability for functions. As the incompleteness results in particular teach us, there are sets which are only weakly but not strongly representable (the key example being the set of statements provable in the system).

[Warning: Here the terminology in the literature varies a lot: “strongly represent” is sometimes called, e.g., “represent”, “numeralwise express”, “bi-numerate”, “define” or “strongly define”; “weakly represent” is in turn also expressed, e.g., by “represent”, “define”, “weakly define”, or “numerate”. One should be careful here and focus on the relevant definitions, and not let the words mislead.]

In the case of both kinds of representability (weak and strong), there is always a simple existential Σ01-formula, which (weakly or strongly) represents the set in question, and usually such a formula is used to represent S.

Though these notions are relative to the formal system, it has turned out that strong and weak representability are extremely stable. Quite independently of the particular formal system chosen, exactly the decidable, or recursive, sets (relations) are strongly representable, and exactly the semi-decidable, or recursively enumerable sets (relations) are weakly representable. This holds for all formalized systems which contain Robinson arithmetic Q, from Robinson arithmetic itself to the strongest axioms systems of set theory like ZFC and beyond (as long as they are (recursively) axiomatizable). Instead of using the notion of “representability”, Gödel took a different approach by speaking of sets being “decidable in a formal system F” (“entscheidungsdefinit”). If the proofs of F are systematically generated, it will be eventually determined, for any given number n, whether it belongs to S or not—given that S is strongly representable in F.

In sum, we have:

The Representability Theorem
In any consistent formal system which contains Q:
  1. A set (or relation) is strongly representable if and only if it is recursive;
  2. A set (or relation) is weakly representable if and only if it is recursively enumerable.

Both notions of representability—strong and weak—must be clearly distinguished from mere definability (in the standard sense of the word). A set S is definable in the language of arithmetic if there is a formula A(x) in the language such that A(n) is true in the standard structure of natural numbers (the intended interpretation) if and only if n ∈ S. There are many sets which can be defined in the language of arithmetic but not (even weakly) represented in any F, such as the set of consistent formulas, the set of sentences unprovable in the system F, or the set of Diophantine equations with no solutions (see below).

2.3 Arithmetization of the Formal Language

The next essential step of Gödel's proof is to take the language of a formal system, which is always precisely defined (this is part of being a formal system), and fix a correspondence of a certain kind between the expressions of that language and the system of natural numbers—a coding, “arithmetization”, or “Gödel numbering”, of the language. There are many possible ways of accomplishing this, and the details do not really matter (for some more details of one quite standard approach, see the supplementary document Gödel Numbering). The essential point is that the chosen mapping is effective: it is always possible to pass, purely mechanically, from an expression to its code number, and from a number to the corresponding expression. Today, when most of us are familiar with computers and the fact that so many things can be coded by zeros and ones, the possibility of such an arithmetization is hardly surprising.

Roughly, one proceeds as follows: First, the primitive symbols of the language are paired with distinct natural numbers, “symbol numbers”. A little number theory then suffices to code sequences of numbers by single numbers. Consequently, well-formed formulas, as sequences of primitive symbols, are each assigned a unique number. Finally derivations, or proofs, of the system, being sequences of formulas, are arithmetized, and are also assigned specific numbers. Such a code, the “Gödel number” of a formula A, is denoted as ⌈A⌉, and similarly for derivations.

In this way, syntactical properties, relations and operations are reflected in arithmetic: for example, neg(x) is the arithmetical function that sends the Gödel number of a formula to the Gödel number of its negation; in other words, neg(⌈A⌉) = (⌈¬A⌉); similarly, impl(x, y) is the function which maps the Gödel numbers of a pair of formulas to the Gödel number of the implication of the formulas: impl(⌈A⌉,⌈B⌉) = ⌈A → B⌉; and so on. There is an arithmetical formula, call it Fmla(x), which is true of n iff n is a Gödel number of a well-formed formula of the system. There is also an arithmetical formula M(x, y, z) which is true exactly if one has a valid application of the rule of inference modus ponens for some formulas A and B with x = ⌈A⌉, y = ⌈A → B⌉ and z = ⌈B⌉; etc. In this way, all the syntactic properties and operations can be simulated at the level of numbers, and moreover they are strongly representable in all theories which contain Q.

As it is decidable (by the definition of formal systems) whether a given sequence of formulas constitutes a proof of a given sentence, according to the rules of the chosen formal system F, the binary relation “x is (the Gödel number of) a proof of the formula (with the Gödel number) y” can be strongly represented in all systems containing Q, and thus in F in particular. Let us denote the formula which strongly represents this relation in F itself as PrfF(x, y). The property of being provable in F can then be defined as ∃xPrfF(x, y). Let us abbreviate this formalized provability predicate as ProvF(x). It follows that the latter is weakly representable (though, it turns out, not strongly):

  • F ⊢ A ⇒ F ⊢ ProvF(⌈A⌉).

It is always possible to choose the provability predicate ProvF(x) to be a Σ01-formula.

2.4 Diagonalization, or, “Self-reference”

The next and perhaps somewhat surprising ingredient of Gödel's proof is the following important lemma (we still assume that F is a formal system which contains Q):

The Diagonalization Lemma
Let A(x) be an arbitrary formula of the language of F with only one free variable. Then a sentence D can be mechanically constructed such that
F ⊢ D ↔ A(⌈D⌉).
(For a sketch of the proof; see Supplement: The Diagonalization Lemma)

In the literature, this lemma is sometimes also called “the self-referential lemma” or “the fixed point lemma”. It has many important applications beyond the incompleteness theorems.

It is often said that given a property denoted by A(x), the sentence D is a self-referential sentence which “says of itself” that it has the property A. Such figures of speech may be heuristically useful, but they are also easily misleading and suggest too much. For example, note that the lemma only provides a (provable) material equivalence between D and A(⌈D⌉) (which states that both sides must have the same truth-value) and does not claim any sort of sameness of meaning. In particular, D and A(⌈D⌉) are by no means identical—and neither are ⌈D⌉ and ⌈A(⌈D⌉)⌉.

2.5 The First Incompleteness Theorem—Proof Completed

To complete the proof, the Diagonalization Lemma is applied to the negated provability predicate ¬ProvF(x): this gives a sentence GF such that

(G)
F ⊢ GF ↔ ¬ProvF(⌈GF⌉).

Thus, it can be shown, even inside F, that GF is true if and only if it is not provable in F.

It is not difficult to show that GF is neither provable nor disprovable in F, if F only is 1-consistent.

For the first half, assume that GF were provable. Then, by the weak representability of provability-in-F by ProvF(x), F would also prove ProvF(⌈GF⌉). However, because F in fact also proves the equivalence (G), i.e, F ⊢ GF ↔ ¬ProvF(⌈GF⌉), F would then prove ¬GF too. But this would mean that F is inconsistent. In sum, if F is consistent, then GF is not provable in F. For this first half, the assumption of the simple consistency of F suffices.

For the second half, it has to be assumed that F is 1-consistent (if ProvF(⌈GF⌉) has been chosen such that it is a Σ01-sentence; otherwise, the more general assumption of ω-consistency is needed).

Assume that F ⊢ ¬GF. Then F cannot prove GF, for otherwise F would be simply inconsistent. Hence no natural number n is the Gödel number of a proof of GF, and because the proof relation is strongly representable, for all n, F ⊢ ¬PrfF(n, ⌈GF⌉). If also F ⊢ ∃xPrfF(x, ⌈GF⌉), F is not 1-consistent, against the assumption. Therefore F does not prove ∃xPrfF(x, ⌈GF⌉), in other words, by the definition of ProvF(x), F does not prove ProvF(⌈GF⌉). By the key equivalence (G), F also does not prove ¬GF.

Gödel's First Incompleteness Theorem
Assume F is a formalized system which contains Robinson arithmetic Q. Then a sentence GF of the language of F can be mechanically constructed from F such that:
  1. If F is consistent, then F ⊬ GF.
  2. If F is 1-consistent, then F ⊬ ¬GF

Such an independent, or “undecidable” (that is, neither provable nor refutable in F) statement GF in F is often called “the Gödel sentence” of F.

In fact, in favourable circumstances, it can be shown that GF is true, provided that F is indeed consistent. This is the case if, for example, the provability predicate ProvF(x) has been chosen as a Σ01-formula: The Gödel sentence is then provably equivalent to the universal formula ∀x¬PrfF(x, ⌈GF⌉). Such formulas can be proved false whenever they in fact are false: if false, there would be a number n such that F ⊢ PrfF(n, ⌈GF⌉) (this holds already in Q). This, however, would contradict the incompleteness theorem. Therefore, GF cannot be false, and must be true. For this reason, the Gödel sentence is often called “true but unprovable”.

One should not get confused here: “Gödel's theorem” is the general incompleteness result of Gödel which concerns a large class of formal systems, while the “Gödel sentence” is the constructed, formally undecidable sentence which varies from one formal system to another. This is why it is important to include the subscript F in GF. Furthermore, one should not confuse the two different senses of “undecidable” in this context. On the one hand, a particular sentence, like the Gödel sentence, may be undecidable in the sense of being independent, i.e., neither provable not refutable in a chosen system. On the other hand, a theory may be undecidable (see below) in the sense that there does not exist a decision method for determining of an arbitrary given sentence of the language whether or not it is derivable in the theory (so this latter sense of “undecidable” concerns, so to speak, an infinite class of statements).

In informal explanations of the first incompleteness theorem, it is often said that the Gödel sentence GF “says of itself that it is not provable”. Such imprecise statements, however, should be taken at least with a grain of salt. There are a number of reasons to conclude that, at least in general, Gödel sentences do not really say anything substantial about themselves (Milne 2007 is a careful analysis of such issues); for example, as was previously noted in the case of the Diagonalization Lemma, one is usually operating here with mere material equivalences.

Rosser's Improvement—From ω-consistency to Consistency

In 1936, J. Barkley Rosser made an important improvement that allows one to get rid of the somewhat clumsy assumption of ω-consistency in the proof of Gödel's first theorem. For this purpose, Rosser introduced a new, somewhat artificial “provability predicate” Prov*(x) which was constructed, informally, as follows:

There exists y such that y is the Gödel number of a proof of the formula with Gödel number x, AND there does not exist z smaller than y such that z is the Gödel number of a proof the negation of the formula with Gödel number x.

More formally:

  • Prov*(x) =def ∃y[PrfF(y, x) ∧ ∀z < y(¬PrfF(z, neg(x)))],

where PrfF(y, x) is the more standard proof relation discussed earlier.

As it happens, if the formal system F under consideration is indeed consistent, Rosser's provability predicate is co-extensional with the ordinary provability predicate. Applying the Diagonalization Lemma to the negation of Rosser's provability predicate Prov*(x) gives:

Rosser's modification of the first theorem (Rosser 1936)
Let F be consistent formalized system which contains Q. Then there is a sentence RF of the language of F such that neither RF nor ¬RF is provable in F.

2.6 Incompleteness and Non-standard Models

It is illuminating to reflect on the first incompleteness theorem also from the model theoretic perspective—though the theorem itself does not in any way require this. Namely, it is possible to conclude that any theory F satisfying the conditions of the theorem must possess, in addition to the intended interpretation or “standard model” (in the case of arithmetical theories, the structure of natural numbers), non-intended interpretations or “non-standard models”—that no such theory can rule out the latter and fix uniquely the intended interpretation. Namely, if there are independent statements such as GF, F must have both models which satisfy GF and models which rather satisfy ¬GF. As ¬GF is equivalent to ∃xPrfF(x, ⌈GF⌉), the latter models must possess entities which satisfy the formula PrfF(x, ⌈GF⌉). And yet we know (because PrfF(x, y) strongly represents the proof relation) that for any numeral n, F can prove ¬PrfF(n, ⌈GF⌉). Therefore, no natural number n can witness the formula. It follows that any such non-standard model must contain, in addition to natural numbers (denotations of the numerals n), “infinite” non-natural numbers after the natural numbers.

The study of non-standard models did not start with Gödel's results—Skolem, in particular, was already aware of them earlier in a different context (he had discovered that first-order theories of set theory have unnaturally small, namely, countable models, in Skolem 1922; cf. the entry on Skolem's paradox)—but the first incompleteness theorem elucidates the existence of non-standard models in the context of arithmetic, while the nonstandard models elucidate the first incompleteness theorem. Non-standard models have since then become a rich research area in mathematical logic (see, e.g., Boolos & Jeffrey 1989: Ch. 17; Kaye 1991).

3. The Second Incompleteness Theorem

3.1 Preliminaries

Informally, the reasoning leading to the second incompleteness theorem is relatively simple. Given the arithmetized provability predicate, it is also easy to present an arithmetized consistency statement: pick some manifestly inconsistent formula (in arithmetical theories, a standard choice is (0 = 1)); let us denote it by ⊥; (the arithmetized counterpart of) the consistency of the system can then be defined as ¬ProvF(⌈⊥⌉). Let us abbreviate this formula by Cons(F). The proof of the first part of the first incompleteness theorem (i.e., the case (i) above) can then presumably be formalized inside F (in practice this would certainly be intricate). This gives:

  • F ⊢ Cons(F) → GF,

where GF is the Gödel sentence for F provided by the first theorem. If Cons(F) were provable in F, so would be GF, by simple logic. This would contradict Gödel's first theorem. Consequently, Cons(F) cannot be provable in F either.

Gödel's second incompleteness theorem
Assume F is a consistent formalized system which contains elementary arithmetic. Then F ⊬ Cons(F).

There is a question of philosophical importance that should be mentioned here: As it stands, Gödel's second incompleteness theorem only establishes the unprovability of one sentence, Cons(F). But does this sentence really express that F is consistent? (Compare this with the remark above that GF does not, strictly speaking, express its own unprovability.) Furthermore, might there not be other sentences which are provable and also express the consistency of F?

Giving a rigorous proof of the second theorem in a more general form that covers all such sentences, however, has turned out to be very complicated. The basic reason for this is that, unlike in the first theorem, not just any, merely extensionally adequate provability predicate works for the formalization of the consistency claim. The manner of presentation makes all the difference. For example, Rosser's provability predicate mentioned above would not do; one can prove the “consistency” of F in F, if consistency is expressed in terms of Rosser's provability predicate. One must thus add some further conditions for the provability predicate in order for the proof of the second incompleteness theorem to go through. Following Feferman (1960), it is customary to say that whereas the first theorem and its relatives are extensional results, the second theorem is intensional: it must be possible to think that Cons(F) in some sense expresses the consistency of F—that it really means that F is consistent.

3.2 Derivability Conditions

The proof of the second incompleteness theorem requires that the provability predicate in F satisfies a number of conditions which are used in the details of the proof. There are several different sets of conditions that will do.

The first detailed proof of the second incompleteness theorem appeared in (Hilbert & Bernays 1939) (mainly written by Bernays), though only for one specific theory, PA. It uses a rather awkward set of conditions for the provability predicate. These were more technical lemmas for the needs of a particular proof and not any sort of analysis of “natural” provability predicates. A much more elegant, now standard list of “derivability conditions” was presented by Löb (1955)—though their intended use was somewhat different (see below).

Löb's Derivability Conditions
(D1)
F ⊢ A ⇒ F ⊢ ProvF(⌈A⌉).
(D2)
F ⊢ ProvF(⌈A⌉) → ProvF(⌈ProvF(⌈A⌉)⌉).
(D3)
F ⊢ ProvF(⌈A⌉) ∧ ProvF(⌈A → B⌉) → ProvF(⌈B⌉).

(D1) is simply a restatement of the requirement from the proof of the first theorem that provability is weakly representable. Roughly put, (D2) requires that the whole demonstration of (D1), for the candidate provability predicate ProvF, can itself be formalized inside F. Finally, (D3) requires that the provability predicate is closed under Modus Ponens.

If the arithmetized provability predicate indeed satisfies these conditions, the second theorem can be proved. Let GF once again be the Gödel sentence for F given by the first theorem. It is not too difficult to show, using the derivability conditions, that:

  • F ⊢ GF ↔ Cons(F).

This immediately yields the unprovability of Cons(F), given the first incompleteness theorem.

Furthermore, Jeroslow (1973) demonstrated, with an ingenious trick, that it is in fact possible to establish the second theorem without (D3). However, in some other cases (e.g., when proving Löb's theorem; see below), and in Provability Logic, all three conditions are still needed.

3.3 Feferman's Alternative Approach to the Second Theorem

Under the assumption that a provability predicate for a theory satisfies the derivability conditions (or, by Jeroslow's trick, at least D1 and D2) it is relatively easy to prove the relevant case of the second incompleteness theorem. However, in practise one has to establish whether a proposed arithmetized provability predicate really satisfies the conditions case by case, and typically this is long and tedious.

This drawback, among other things (see Feferman 1997), led Solomon Feferman in the late 1950s to look for an alternative line of attack to the second theorem (see Feferman 1960). Feferman approaches the issue in two steps: First, he isolates the formulas ProvFOL(x) which arithmetize some standard notion of derivability in first-order logic in order to allow us to fix one chosen formula for provability in logic. How the set of non-logical axioms of the system at issue are presented is left open at this stage. Secondly, Feferman looks for a suitable constraint for presenting the axioms. Among the formulas of the language of arithmetic, he isolates what he calls PR- and RE-formulas; the former correspond to the canonical primitive recursive (PR) definitions in arithmetic, and the latter to existential generalizations of the former. Every recursively enumerable (RE) set can be defined by a formula of the latter sort; these are just the Σ01-formulas. These two classes are easy to discriminate purely by their syntactical form. (In fact, by the MRDP Theorem (see below), one could—instead of RE-formulas—focus on even simpler class of existentially quantified Diophantine equations.)

We have above noted the important fact that in all arithmetical theories F containing Q, a set is strongly representable in F if and only if it is recursive, and a set is recursively enumerable if and only if it is weakly representable. Furthermore, one can always take the formula weakly or strongly representing the set to be a RE-formula (i.e., Σ01-formula; and, by MRDP Theorem, even an existentially quantified Diophantine equation). It is then natural to require that the set of non-logical axioms of the system at issue is represented by such a formula. If the arithmetized definition of the set of Gödel numbers of axioms reflects how the axioms, if infinite, are inductively defined, the resulting formula will be Σ01. (For theories which are axiomatizable with finitely many axioms, there is a unique representation of the axioms in the form of a list, and consequently, a unique consistency statement relative to ProvFOL(x).) In contrast to determining whether the derivability conditions are satisfied, it is a relatively routine task to determine that a given formula which formalizes the axioms is indeed of the required form (Σ01).

Now the version of the second incompleteness theorem presented in Feferman 1960 is:

A variant of second incompleteness theorem (Feferman 1960)
Let F be a consistent extension of PA, and let AxF(x) be a Σ01-formula which weakly represents the axioms of F, and Cons(F) be a consistency statement constructed from AxF(x) and ProvFOL(x). Then Cons(F) is not provable in F.

For still different approaches to the second incompleteness theorem, see Feferman 1982, 1989a; Visser 2011. For some philosophical complications concerning the second theorem, see Detlefsen 1979, 1986, 1990, 2001; Auerbach 1985, 1992; Roeper 2003; Franks 2009 (see also section on incompleteness in the entry on Hilbert's program).

4. Results Related to the Incompleteness Theorems

4.1 Tarski's Theorem on the Undefinability of Truth

Gödel first arrived at the incompleteness results (see Section 5 below) by noting that truth (of the language of a system) must be undefinable in the system, a result conventionally credited to Tarski (there are certain real virtues in Tarski's way of presenting the issue; see Gómez Torrente 2004). Let us now view the result in the context of Tarski's approach to truth.

Tarski clearly distinguished the object language, i.e., the language the truth of whose sentences is at stake, and the metalanguage in which the former is discussed. He also required (see the entry on Tarski's truth definitions) that any satisfactory definition of truth True(x) for the object language should satisfy his “Convention T”, that is, it should have as its consequence all equivalences (“T-equivalences”) of the form

(T)
True(⌈A⌉) ↔ B,

where ⌈A⌉ is a name of a sentence of the object language, and B its translation in the metalanguage. If the metalanguage is identical with the object language, or is an extension of the object language, B is simply A itself, and the T-equivalences are of the form:

  • True(⌈A⌉) ↔ A.

What the undefinability theorem shows is that the object language and the metalanguage cannot coincide, but must be distinct.

Tarski's Undefinability Theorem
Let F be a consistent formalized system that contains a sufficient amount of arithmetic. Then there is no formula Tr(x) in the language of F such that for every sentence A of the language of F:

F ⊢ Tr(⌈A⌉) ↔ A.

The idea of the proof: If there were such a formula of the language of F, an easy application of the Diagonalization Lemma to its negation would result in the paradoxical sentence L (for “Liar”; see the Liar paradox)), such that:

F ⊢ ¬Tr(⌈L⌉) ↔ L,

which, together with the T-equivalences, which were assumed to be derivable, would quickly give an explicit contradiction, thus contradicting the assumption that F is consistent.

Similarly, it can be proved that the set of true sentences of F is not definable in the intended interpretation of F—in the now standard sense of “definability” (see above).

4.2 The Undecidability Results

The tools used in proving Gödel's theorems also provide various important undecidability results. A theory is called decidable if the set of its theorems (sentences derivable in it) is decidable, that is (by the Church-Turing thesis) recursive. Otherwise, the theory is undecidable. Informally, being decidable means that there is a mechanical procedure which enables one to decide whether an arbitrary given sentence (of the language of the theory) is a theorem or not.

If a theory is complete, it is decidable (proof sketch: given a sentence A, systematically generate the theorems of the theory; by completeness, eventually either A or ¬A will be produced in a finite time). The converse, though, does not always hold: there are incomplete theories which are decidable. Nevertheless, incompleteness at least opens the possibility of undecidability. Moreover, all theories which contain Robinson arithmetic Q (either directly, or Q can be interpreted in them) are both incomplete and undecidable. Thus, for a very wide class of theories, incompleteness and undecidability go hand in hand.

One elegant and simple way of demonstrating the undecidability of extensions of Q goes, roughly, as follows: Let F be any consistent theory that contains Q. Assume then that the set of its theorems is decidable, that is (by the Church-Turing thesis), recursive. It would then follow that the set (of the Gödel numbers) of the theorems of F is strongly representable in F itself. Recall that this means that there is some formula B(x) of the language of F such that not only F ⊢ B(⌈A⌉) whenever F ⊢ A (which even weak representability guarantees), but also that F ⊢ ¬B(⌈A⌉) whenever F ⊬ A. However, the technique used in the proof of the first incompleteness theorem also shows that there are always sentences for which the latter does not hold: it is possible to construct a Gödel sentence GB relative to B(x) for F such that:

(D)
F ⊢ GB ↔ ¬B(⌈GB⌉).

As before, it follows that F ⊬ GB. It has been assumed that B(x) strongly represents the set of theorems, so this entails F ⊢ ¬B(⌈GB⌉), and therefore, by (D), F ⊢ GB, a contradiction. Therefore, F must be undecidable.

A theory F is called essentially undecidable if every consistent extension of it in the language of F is undecidable. The above proof sketch in fact establishes that Q is essentially undecidable. (There are some very weak theories that are undecidable but not essentially undecidable.)

Recall that Q has only finitely many axioms and let AQ stand for the single sentence consisting of the conjunction of the axioms of Q. Then for any sentence B of the language of arithmetic,

  • Q ⊢ B if and only if it is a theorem of first-order logic that AQ → B.

But then a decision procedure for first-order logic would provide a decision method for Q. The latter, however, is impossible, as it has already been shown. Therefore, it can be concluded:

Church's Theorem
First-order predicate logic is undecidable.

(This undecidability result was first established by Church 1936a, b; the method of deriving it via the undecidability of Q is due to Tarski, Mostowski and Robinson 1953.)

Subsequently, a number of theories and problems from different areas of mathematics have been shown to be undedicable (see, e.g., Davis 1977; Murawski 1999: Ch 3).

4.3 Reflection Principles and Löb's Theorem

Heuristically, one may view the Gödel sentence GF as expressing its own unprovability—saying “I am not provable”—though, as was already emphasized, such claims should be taken with a grain of salt. Leon Henkin put forward the question whether the sentence expressing its own provability (“I am provable”) is true or false, and provable or not (Henkin 1952). Georg Kreisel soon pointed out that this depends vitally on how provability is expressed; with different choices, one gets opposite answers (Kreisel 1953).

The paper of Martin Hugo Löb (1955), augmented by comments of a referee, brought substantial advances on various fronts. First, it introduces the now standard Löb derivability conditions discussed previously in the context of the second incompleteness theorem. Second, it contains Löb's solution of Henkin's problem about sentences “expressing their own provability”. Third, it contains a generalization now called “Löb's Theorem”, but which Löb actually credits to the anonymous referee (who happened to be none other than Henkin himself; the whole story is told in Smoryński 1991.)

In order to understand Löb's theorem properly it is useful to first consider the so-called “reflection principles”. Above, the focus has been on expressing, inside a formal system, that the system is consistent, i.e., on Cons(F). But naturally the theory should not merely be consistent but also sound, i.e., prove only true sentences. How should the soundness of a system, i.e., the claim that everything derivable in the system is true, be expressed? If one wants to express this in the language of the system itself, it cannot be done by a single statement saying this, because there is, by the undefinability of truth, no suitable truth predicate available in the language. Various restricted and unrestricted soundness claims can, however, be expressed in the form of a scheme, the so-called Reflection Principles:

(Ref)
ProvF(⌈A⌉) → A.

By taking A to be ⊥, and noting that ⊥ is refutable in F, it is easy to see that Reflection Principle entails the consistency statement Cons(F), i.e., ¬ProvF(⌈⊥⌉); hence it cannot be generally provable in the system.

The scheme can also be restricted. Equivalent to the assumption of 1-consistency, or Σ01-soundness, for example, is the Reflection Principle restricted to Σ01-sentences (i.e., the sentence A in the scheme is required to be a Σ01-sentence.) Or, it can be restricted to the universal Π01-sentences; and so forth.

Exactly which instances of the reflection scheme are actually provable in the system? Löb's Theorem gives a precise answer to this question (assuming that ProvF(x) satisfies the derivability conditions):

Löb's Theorem
Let A be any sentence of the language of F. Then: F ⊢ ProvF(⌈A⌉) → A if, and only if, F ⊢ A.

Hence, the instances of soundness (reflection principle) provable in a system are exactly the ones which concern sentences which are themselves provable in the system. As a consequence, this also settles Henkin's original problem: assuming that the arithmetized provability predicate is again “normal” (i.e., satisfies Löb's derivability conditions), all sentences “asserting their own provability” are provable.

Actually, Löb's theorem can be proved quite quickly as a consequence of the second incompleteness theorem. Kreisel has also noted that, in the opposite direction, the second incompleteness theorem can also be easily derived as a consequence of Löb's theorem.

4.4 Hilbert's Tenth Problem and the MRDP Theorem

The tenth on Hilbert's famous list of important open problem in mathematics from 1900 asks for a decision method for the so-called Diophantine equations. Despite the unfamiliar term “Diophantine,” what is at issue here is truly elementary. Consider any equation with one or more variables and with integer coefficients, which involves only addition and multiplication, such as x2 + y2 = 2, or 3x2 + 5y2 + 2xy = 0. If real-number solutions are sought, one usually speaks simply about an “equation”. However, in number theory, typically a solution is sought consisting only of integers. That makes a great difference. The former of the above equations has infinitely many solutions among real numbers, but only four among integers. The equation x2 + y2 = 3 also has infinitely many real solutions but no integer solutions. When the focus is on the integer solutions, one talks about “Diophantine equations” (after the ancient number theorist Diophantus of Alexandria).

For a positive solution of Hilbert's tenth problem, it would have sufficed to present a particular concrete method which would have intuitively been a “mechanical” decision method. However, Turing's pioneering analysis of the notion of decision method brought into focus the possibility of a negative solution. Beginning in the early 1950s, Julia Robinson and Martin Davis worked on this problem, later joined by Hilary Putnam. As a result of their collaboration, the first important result in this direction was achieved. Call an equation “an exponential Diophantine equation” if it involves also exponentiation, as well as addition and multiplication (that is, one can have both constants and variables as exponents); naturally, the focus is still in the integer solutions. Davis, Putnam, and Robinson (1961), showed that the problem of solvability of exponential Diophantine equations is undecidable. In 1970, Yuri Matiyasevich added the final missing piece, and demonstrated that the problem of the solvability of Diophantine equations is undecidable. Hence the overall result is often called MRDP Theorem (for an exposition, see, e.g., Davis 1973; Matiyasevich 1993).

The essential technical achievement was that all semi-decidable (recursively enumerable) sets can be given a Diophantine representation, i.e., they can be represented by a simple formula of the form ∃x1…∃xn(s = t), where (s = t) is a Diophantine equation. More exactly, for any given recursively enumerable set S, there is a Diophantine equation (s(y, x1, … , xn) = t(y, x1, … , xn)) such that n ∈ S if and only if ∃x1…∃xn(s(n, x1, … , xn) = t(n, x1, … , xn)).

As there are semi-decidable (recursively enumerable) sets which are not decidable (recursive), the general conclusion follows immediately:

MRDP Theorem
There is no general method for deciding whether or not a given Diophantine equation has a solution.

This also provides an elegant variant of the incompleteness theorems dealing with Diophantine equations:

Corollary
For any 1-consistent axiomatizable formal system F there are Diophantine equations which have no solutions but cannot be proved in F to have no solutions.

(The question of avoiding the requirement of 1-consistency here is tricky; see Dyson, Jones and Shepherson 1982.)

4.5 Concrete Cases of Unprovable Statements

The undecidable sentences provided by Gödel's proofs are (if written out) extremely complicated formulas with no intuitive significance, construed only for the purposes of the incompleteness proofs. The question then arises whether there are any simple and natural mathematical statements which are likewise undecidable in chosen basic theories, e.g., in PA. There are now various specific statements with clear mathematical content which are known to be undecidable in some standard theories (though, just how natural even these are has been disputed; see Feferman 1989b). Some well known, natural examples are listed below, beginning with some quite natural mathematical statements which are independent of PA, and proceeding to more and more powerful theories. Sometimes such results are called variants of Gödel's theorem, or their proofs of independence alternative proofs of Gödel's theorem, but this is misleading: interesting as they may be, they don't have the generality of Gödel's theorems proper, but only provide statements independent of a particular theory.

It is often stated that before the celebrated Paris-Harrington theorem (see below), no such natural independent mathematical statements were known. This is not, however, strictly speaking, correct. Already much earlier, around 1935, Gerhard Gentzen (see the entry on the development of proof theory) had provided such a statement. It is very natural to generalize the idea of induction from the domain of natural numbers to the domain of ordinal numbers. In set theory, such generalizations are called principles of transfinite induction. Though some constructivists may be sceptical about the legitimacy of full set theory, there are limited and more concrete cases of transfinite induction (only dealing with some well-defined classes of countable ordinals) that are perfectly acceptable even from the constructivist or intuitionist viewpoint. One important case is the principle of transfinite induction up to the ordinal called ε0. Gentzen showed that the consistency of PA can be proved if this transfinite induction principle is assumed. Therefore, because of the second incompleteness theorem, the principle itself cannot be provable in PA (Gentzen 1936).

Ramsey's theorem is a result in infinitary combinatorics, established by Frank Ramsey (1930), and deals with possibilities of “colouring” for certain graphs. Jeff Paris and Leo Harrington formulated a finitary variant of Ramsey's theorem, and showed that it is not provable in PA (Paris & Harrington 1977). This provides a quite natural statement of finite combinatorics which is independent of PA. Perhaps an even cleaner example is Goodstein's theorem, due to Reuben Goodstein (1944), which is purely number theoretic in nature. First one defines a certain natural class of sequences of natural numbers, now called “Goodstein sequences”. The theorem states that every Goodstein sequence eventually terminates at 0. Goodstein's theorem is certainly a natural mathematical statement, for it was formulated and proved (obviously by proof methods that go beyond PA) by Goodstein long before (that is, in 1944) it was shown, in 1982, that the theorem is not provable in PA (Kirby & Paris 1982).

Moving now to stronger theories beyond PA, one can mention, for example, Kruskal's Theorem. This is a theorem which concerns certain orderings of finite trees (Kruskal 1960). Harvey Friedman showed that this theorem is unprovable even in subsystems of second-order arithmetic much stronger than PA (see Simpson 1985). In particular, it is not provable in any theory which is predicatively justified (under a widely accepted explication of “predicative”, cf. the section on predicativism in the entry on the philosophy of mathematics).

There are some concrete examples of mathematical statements undecided even in stronger theories which come from the so-called descriptive set theory. This field of mathematics is related to topology and was initiated by the French semi-intuitionists (Lebesgue, Baire, Borel; see the section on descriptive set theory, etc., in the entry on intuitionism in the philosophy of mathematics). It studies sets which possess relatively simple definitions (in contradistinction to the ideas of arbitrary sets and various higher power-sets, which the semi-intuitionists rejected as meaningless) called projective or analytic sets. Classically these were defined as the sets that can be built up from a countable intersection of open sets by taking continuous images and complements finitely many times; they coincide with the sets which are definable in the language of PA2. In particular, the so-called Borel sets can be simply defined both by a formula of the form ∃XA(x) and by a formula of the form ∀XB(x), where A and B do not contain any set variables (in logician's terminology, Borel sets are the Δ11 sets). A Borel function is defined analogously (see, e.g., Martin 1977).

Harvey Friedman has established the following theorem: roughly, if S is a Borel set, then there exists a Borel function f such that the graph of f is either included in or disjoint from S. Friedman showed that this simple-sounding theorem is not provable even in full second-order arithmetic PA2, but proving it necessarily requires the full power of ZFC (see Simpson 1999: 23).

Further, it was a traditional question of descriptive set theory (a question which can be formulated in the language of second order arithmetic) whether all projective sets (see above) are Lebesque measurable. This remained an open problem for many decades, and for a good reason: it turned out that the statement is independent even of the full ZFC set theory (see Solovay 1970). Only by postulating the existence of some extremely large cardinals (so-called Woodin cardinals) can the hypothesis that all projective sets are Lebesque measurable be proved (this was achieved as a consequence of their work on so-called projective determinacy by Woodin, Martin and Steel; see Woodin 1988; Martin & Steel 1988, 1989).

Sometimes Paul Cohen's celebrated result that the Continuum Hypothesis (CH) is independent of ZFC (Cohen 1963, 1964; see the entry on independence and large cardinals). However, this case is very different. In all the above independence results the relevant statements are still theorems of mathematics, taken as shown to be true (the last case, which requires large cardinal axioms that go beyond ZFC, is more controversial; still, at least many set-theoreticians find such axioms plausible). And with the first incompleteness theorem itself, the truth of the unprovable statement easily follows, given that the assumption of the consistency of the system is indeed correct. However, in the case of Cohen's result, there is absolutely no indication whether CH should be considered true, false, or perhaps lacking a truth-value.

5. The History and Early Reception of the Incompleteness Theorems

Gödel's results were certainly surprising, but some sort of incompleteness phenomenon was not totally unexpected. The possibility of incompleteness in the context of set theory was discussed by Bernays and Tarski already in 1928, and von Neumann, in contrast to the dominant spirit in Hilbert's program, had considered it possible that logic and mathematics were not decidable. Gödel himself had mentioned the possibility of an undecidable problem concerning real numbers in his thesis in 1929 (see Dawson 1985). Hilbert (1928), on the other hand, had assumed that Peano Arithmetic and other standard theories were complete. Apparently Gödel was also impressed by Brouwer, who in his lecture in Vienna in 1928 had suggested that mathematics is inexhaustible and cannot be completely formalized (see Wang 1987, 84; and the section on Brouwer's view of the formalist program in the entry on the development of intuitionistic logic).

Be that as it may, it seems that Gödel actually arrived at the first exact observations about incompleteness via a different route, during his attempts to contribute to Hilbert's program, and not to undermine it (see Dawson 1997: Ch. IV). Namely, in 1930, Gödel made an effort to advance Hilbert's program by attempting to prove the consistency of analysis (or, second-order arithmetic) with the resources of arithmetic, and thus reduce the consistency of the former to the consistency of the latter. In his attempted proof, he needed the notion of truth. Gödel soon faced various paradoxes (such as the Liar paradox), and had to conclude that arithmetical truth cannot be defined in arithmetic. Hence, Gödel first arrived at a version of the undefinability of truth theorem, usually associated with Tarski (cf. Murawski 1998). This also easily yields a weak version of the incompleteness result: the set of sentences provable in arithmetic can be defined in the language of arithmetic, but the set of true arithmetical sentences cannot; therefore the two cannot coincide. Moreover, under the assumption that all provable sentences are true, it follows that there must be true sentences which are not provable. This approach, though, does not exhibit any particular such sentence.

However, the intellectual environment of Gödel was that of the Vienna Circle with its radically anti-metaphysical attitude. In particular, even the notion of truth was considered as suspicious or even nonsensical at the time, at least by some logical positivists (e.g., Neurath, Hempel). Therefore, Gödel worked hard to eliminate any appeal to the notion of truth and attempted to do without it. He therefore introduced the notion of ω-consistency, which can be defined rigorously and purely syntactically. This led to the incompleteness theorems in the form that they are now known.

As to the Diagonalization Lemma, actually Gödel himself originally demonstrated only a special case of it, that is, only for the provability predicate. The general lemma was apparently first discovered by Carnap 1934 (see Gödel 1934, 1935). Still more general versions, for formulas with free variables, were presented in Ehrenfeucht & Feferman 1960 and Montague 1962 (see Smoryński 1981).

The reception of Gödel's results was mixed. Some important figures in the field of logic and the foundations of mathematics quite quickly assimilated the results and understood their relevance, but there was also quite a lot of misunderstanding and resistance (for detailed accounts of the reception, see Dawson 1985; Mancosu 1999).

Gödel revealed his results to Carnap in Vienna on 26 August 1930, and announced his result (the first theorem) in a casual discussion remark in the famous Königsberg Conference on September 7, 1930. John von Neumann, who was in the audience and was at the time working in the context of Hilbert's program, immediately understood the great importance of the result. On 20 November he wrote a letter to Gödel on a “remarkable” corollary of Gödel's result he had discovered: the unprovability of consistency (the second theorem). Meanwhile Gödel himself, however, had found the same idea and had already sent the final version of his article, which now contained also a statement of the second incompleteness theorem, for publication. The article was published in January 1931 (Gödel 1931; helpful introductions to Gödel's original paper are Kleene 1986 and Zach 2005). The word quickly started to spread of these results which apparently had great importance for the foundations of mathematics—though views on what really was the moral varied. Paul Bernays, perhaps the most important collaborator of Hilbert, showed great interest in the results, though he first had difficulties in understanding them properly. His active correspondence with Gödel also shows that Gödel was already at the time fully aware of the undefinability of truth.

As Gödel's original approach focused on his specific though very comprehensive system P and its (primitive recursive) extensions, some doubted the generality of Gödel's results. Alonzo Church, for example, in a letter to Gödel in July 1932, suggested that Gödel's results would not apply to his system of λ-conversion (the system was later proved to be inconsistent by Kleene and Rosser). Gödel was anxious to generalize his discoveries, and extended the results to a wider class of systems in papers in 1932 and 1934. He also suggested that his methods would be applicable to standard systems of set theory (however, it was only after the satisfactory characterization of decidability and the Church-Turing thesis a few years later that it was possible to give a fully general formulation of the incompleteness theorems (see above); this was first done in Kleene 1936). The eminent set-theorist Ernst Zermelo directed some rather harsh criticism towards Gödel's work, but the two also corresponded on the topic. Zermelo seems to have had serious difficulties in understanding the relevant concepts and results.

In March 1933, Gödel received a letter from Paul Finsler, from Zürich, who suggested that he had already earlier (in Finsler 1926) done closely related work but with a more general relevance. Gödel replied that Finsler's system was not really defined at all. In his heated response, Finsler claimed that it was not necessary to be able to study a system for it to be sharply defined, and that there was no difference in principle between his ideas and Gödel's. In retrospect, it is quite clear that the approaches of Finsler and Gödel were very different: for Gödel's work, the notion of formalized system was essential, whereas Finsler rejected the very notion as artificially restrictive. In fact, it is far from clear that Finsler's ideas make any sense—whatever vague analogies there may be between them and Gödel's proof.

On the other hand, it is fair to say that Emil Post had in some respects anticipated Gödel's discoveries. He obtained abstract versions of incompleteness results apparently already in 1922. In particular, he observed that his methods would provide a statement undecidable in Principia Mathematica. These results were, however, based on Post's own version of the “Church-Turing thesis”, with which he was dissatisfied, and his work was left unpublished. It was reported much later in (Post 1941).

The correctness of Gödel's theorems remained the subject of lively debate throughout the 1930s (see Dawson 1985). In 1939, Hilbert and Bernays' second volume of Die Grundlagen der Mathematik appeared, including a detailed proof of the second incompleteness theorem. Thereafter, serious opposition to Gödel's conclusions disappeared at least among those who were working actively in mathematical logic and the foundations of mathematics. However, in more philosophical circles, some resistance remained. Most famously, Wittgenstein made some critical remarks concerning Gödel's theorem in his posthumously published Remarks on the Foundations of Mathematics. The dominant initial reaction was that Wittgenstein simply failed to understand the result. More charitable interpretations have emerged, and the debate is still very much alive (see the section on Gödel and undecidable propositions in the entry on Wittgenstein's philosophy of mathematics).

6. Philosophical Implications—Real and Alleged

6.1 Philosophy of Mathematics

Of the various fields of philosophy, Gödel's theorems are obviously most immediately relevant for the philosophy of mathematics. To begin with, they pose, at least prima facie, serious problems for Hilbert's program (this issue is discussed in some detail in the section on the impact of incompleteness in the entry on Hilbert's Program). Then again, they have important consequences for intuitionism (see the entry on intuitionism in the philosophy of mathematics) (see also Gödel 1933, 1941; Raatikainen 2005).

There has been some dispute on the issue as to whether Gödel's theorems conclusively refute logicism (see the entry on logicism). Henkin (1962) and Musgrave (1977), for example, argue it does; Sternfeld (1976) and Rodríguez-Consuegra (1993) disagree (see also Hellman 1981; Raatikainen 2005).

Gödel himself developed an argument against the conventionalist philosophy of mathematics of logical positivism, and of Carnap's in particular, based on the incompleteness results (Gödel 1953/9). It is discussed in Goldfarb and Ricketts 1992; Ricketts 1995; Goldfarb 1995; Crocco 2003; Awodey & Carus 2003, 2004; Tennant 2008.

6.2 Self-evident and analytical truths

One can also give more general epistemological interpretations of Gödel's theorems. Quine and Ullian (1978), for example, consider the traditional philosophical picture that all truths could be proved by self-evident steps from self-evident truths and observation. They then point out that even the truths of elementary number theory are presumably not in general derivable by self-evident steps from self-evident truths (Quine & Ullian 1978: 64–65.) Hilary Putnam (1975) in turn submits that, under a certain natural understanding of “analytic”, there must be, by Gödel's theorems, synthetic truths in mathematics. In fact, Gödel himself made remarks in a very similar spirit that even the theory of integers is demonstrably non-analytic (Gödel 1944).

6.3 ‘Gödelian’ arguments against mechanism

There have been repeated attempts to apply Gödel's theorems to demonstrate that the powers of the human mind outrun any mechanism or formal system. Such a Gödelian argument against mechanism was considered, if only in order to refute it, already by Turing in the late 1940s (see Piccinini 2003). An unqualified anti-mechanist conclusion was drawn from the incompleteness theorems in a widely read popular exposition, Gödel's Theorem, by Nagel and Newman (1958). Shortly afterwards, J.R. Lucas (1961) famously proclaimed that Gödel's incompleteness theorem

proves that Mechanism is false, that is, that minds cannot be explained as machines.

He stated that

given any machine which is consistent and capable of doing simple arithmetic, there is a formula it is incapable of producing as being true … but which we can see to be true.

More recently, very similar claims have been put forward by Roger Penrose (1989, 1994). John Searle (1997) has joined the discussion and partly defended Penrose against his critics. Crispin Wright (1994, 1995) has endorsed related ideas from an intuitionistic point of view (for criticism, see Detlefsen 1995). They all insist that Gödel's theorems imply that the human mind infinitely surpasses the power of any finite machine or formal system.

These Gödelian anti-mechanist arguments are, however, problematic, and there is wide consensus that they fail. The standard response to this argument goes along the following lines (this objection goes back to Putnam 1960; see also Boolos 1968, Shapiro 1998): The argument assumes that for any formalized system, or a finite machine, there exists the Gödel sentence which is unprovable in that system, but which the human mind can see to be true. Yet Gödel's theorem has in reality a conditional form, and the alleged truth of the Gödel sentence of a system depends on the assumption of the consistency of the system. The anti-mechanist's argument thus also requires that the human mind can always see whether or not a given formalized theory is consistent. However, this is highly implausible (cf. Davis 1990). Lucas, Penrose and others have attempted to reply to such criticism (see, e.g., Lucas 1996; Penrose 1995, 1997). For detailed criticism of Penrose, see Boolos 1990; Davis 1990, 1993; Feferman 1995; Lindström 2001; Pudlák 1999; Shapiro 2003; many of these considerations are also relevant for what Lucas says).

6.4 Gödel and Benacerraf on Mechanism and Platonism

Interestingly, Gödel himself also presented an anti-mechanist argument although it was more cautious and only published posthumously (in his Collected Works, Vol. III, in 1995). That is, in his 1951 Gibbs lecture, Gödel drew the following disjunctive conclusion from the incompleteness theorems:

either … the human mind (even within the realm of pure mathematics) infinitely surpasses the power of any finite machine, or else there exist absolutely unsolvable diophantine problems.

Gödel speaks about this statement as a “mathematically established fact” (Gödel 1951; for more discussion on Gödel's disjunctive claim, see, e.g., Shapiro 1998). According to Gödel, the second alternative

seems to disprove the view that mathematics is only our own creation … that mathematical objects and facts … exist objectively and independently of our mental acts and decisions.

Gödel was nonetheless inclined to deny the possibility of absolutely unsolvable problems, and although he did believe in mathematical Platonism, his reasons for this conviction were different, and he did not maintain that the incompleteness theorems alone establish Platonism. Thus Gödel believed in the first disjunct, that the human mind infinitely surpasses the power of any finite machine. Still, this conclusion of Gödel follows, as Gödel himself clearly explains, only if one denies, as does Gödel, the possibility of humanly unsolvable problems. It is not a necessary consequence of incompleteness theorems.

Now Gödel was, unlike the later advocates of the so-called Gödelian anti-mechanist argument, sensitive enough to admit that both mechanism and the alternative that there are humanly absolutely unsolvable problems are consistent with his incompleteness theorems. His fundamental reasons for disliking the latter alternative are much more philosophical. Gödel thought in a somewhat Kantian way that human reason would be fatally irrational if it asked questions it could not answer (for critical discussion, see Kreisel 1967; Boolos 1995; Raatikainen 2005).

As a reaction to Lucas' argument, but before the publication of Gödel's Gibbs Lecture, Paul Benacerraf (1967) put forward more qualified conclusions that interestingly resemble some ideas of Gödel. He argued that it is consistent with all the facts that I am indeed a Turing machine, but that I cannot ascertain which one. For some critical discussion, see Chihara 1972 and Hanson 1971.

6.5 Mysticism and the existence of God?

Sometimes quite fantastic conclusions are drawn from Gödel's theorems. It has been even suggested that Gödel's theorems, if not exactly prove, at least give strong support for mysticism or the existence of God. These interpretations seem to assume one or more misunderstandings which have already been discussed above: it is either assumed that Gödel provided an absolutely unprovable sentence, or that Gödel's theorems imply Platonism, or anti-mechanism, or both.

For more discussion about the philosophical aspects of the incompleteness theorems, see Raatikainen 2005 and Franzén 2005.

Further reading

A standard reference for the incompleteness theorems is:

  • Smoryński, C., 1977, “The incompleteness theorems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 821–866 [available online].

There are several introductory textbooks in mathematical logic which give a good exposition of the incompleteness theorems and related topics; for example:

  • Boolos, G., and R. Jeffrey, 1989, Computability and Logic, 3rd revised edition, Cambridge: Cambridge University Press.
  • Enderton, H., 1972, A Mathematical Introduction to Logic, New York: Academic Press.
  • Van Dalen, D., 2004, Logic and Structure, 4th edition, Berlin: Springer.

Two books that are dedicated to the incompleteness theorems are:

  • Smullyan, R., 1991, Gödel's Incompleteness Theorems, Oxford: Oxford University Press.
  • Smith, P., 2007, An Introduction to Gödel's Theorems, Cambridge: Cambridge University Press.

Another useful book on the incompleteness theorems and related topics is:

  • Murawski, R., 1999, Recursive Functions and Metamathematics: Problems of Completeness and Decidability, Gödel's Theorems. Dordrecht: Kluwer.

A comprehensive, more advanced book on these themes is:

  • Hájek, P. and Pudlák, P., 1993, Metamathematics of First-Order Arithmetic, Berlin: Springer.

Another useful book, including also some more advanced topics is:

  • Franzén, T., 2004, Inexhaustibility: A Non-Exhaustive Treatment, Lecture Notes in Logic 16, ASL, Wellesley: A.K. Peters.

The more philosophical aspects around the incompleteness theorems are surveyed in the following two sources:

  • Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel's Incompleteness Theorems,” Revue Internationale de Philosophie, 59: 513–534 [available online].
  • Franzén, T., 2005, Gödel's Theorem: An Incomplete Guide to its Use and Abuse, Wellesley: A.K. Peters.

The latter also provides a very accessible informal and yet reliable explanation of the incompleteness theorems.

Bibliography

  • Auerbach, David, 1985, “Intensionality and the Gödel theorems,” Philosophical Studies, 48 (3):337–51.
  • –––, 1992, “How to say things with formalisms,” in Proof, Logic, and Formalization, M. Detlefsen (ed.), London: Routledge, 77–93 [available online].
  • Awodey, S. & A.W. Carus, 2003, “Carnap versus Gödel on Syntax and Tolerance,” in Logical Empiricism: Historical and Contemporary Perspectives, P. Parrini et al. (eds.), Pittsburgh: University of Pittsburgh Press, pp. 57–64 [available online].
  • –––, 2004, “How Carnap Could Have Replied to Gödel,” in S. Awodey and C. Klein (eds.), Carnap Brought Home: The View from Jena, LaSalle, IL: Open Court, pp. 203–223 [available online].
  • Barzin, M., 1940, “Sur la portée du théorème de M. Gödel,” Académie Royale de Belgique, Bulletin de la Classe des Sciences, Series 5, 26: 230–39.
  • Benacerraf, P., 1967, “God, the Devil, and Gödel,” The Monist, 51: 9–32 [available online].
  • Bezboruah, A. and J.C. Shepherdson, 1976, “Gödel's Second Incompleteness Theorem for Q,” The Journal of Symbolic Logic, 41: 503–512.
  • Boolos, G., 1968, “Review of ‘Minds, Machines and Gödel’, by J.R. Lucas, and ‘God, the Devil, and Gödel’,” Journal of Symbolic Logic, 33: 613–15.
  • –––, 1990, “On ‘Seeing’ the Truth of Gödel Sentence,” Behavioral and Brain Sciences, 13: 655–656.
  • –––, 1995, “Introductory Note to *1951,” in Gödel 1995: 290–304.
  • Boolos, G. and R. Jeffrey, 1989, Computability and logic, 3rd revised edition, Cambridge: Cambridge University Press.
  • Carnap, R., 1934, Logische Syntax der Sprache, Vienna: Julius Springer.
  • Chihara, C., 1972, “On Alleged Refutations of Mechanism Using Gödel's Incompleteness Results,” Journal of Philosophy, 69: 507–26.
  • Church, A., 1936a, “An Unsolvable Problem of Elementary Number Theory,” American Journal of Mathematics, 58: 354–363. Republished in Davis 1965, 89–107.
  • –––, 1936b, “A Note on Entscheidungsproblem,” Journal of Symbolic Logic, 1: 40–41; correction, ibid., 101–102. Republished in Davis 1965, 110–115.
  • Cohen, P. J., 1963, “The Independence of the Continuum Hypothesis I,” Proceedings of the National Academy of Sciences, (U.S.A.), 50(6): 1143–48.
  • –––, 1964, “The Independence of the Continuum Hypothesis II,” Proceedings of the National Academy of Sciences, (U.S.A.), 51(1): 105–110.
  • Crocco, G., 2003, “Gödel, Carnap, and the Fregean Heritage,” Synthese, 137: 21–41.
  • Davis, M., 1965, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Hewlett, NY: Raven Press.
  • –––, 1973, “Hilbert's Tenth Problem is Unsolvable,” The American Mathematical Monthly, 80: 233–269.
  • –––, 1977, “Unsolvable Problems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 567–594.
  • –––, 1990, “Is Mathematical Insight Algorithmic?” Behavioral and Brain Sciences, 13: 659–660.
  • –––, 1993, “How Subtle is Gödel's Theorem? More on Roger Penrose,” Behavioral and Brain Sciences, 16: 611–612.
  • Davis, M., H. Putnam, and J. Robinson, 1961, “The decision problem for exponential diophantine equations,” Annals of Mathematics (2), 74(3): 425–436.
  • Dawson, J., 1985, “The Reception of Gödel's Incompleteness Theorems,” PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1984, vol. II, pp. 253–271.
  • –––, 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, Natick, MA: A. K. Peters.
  • Detlefsen, M., 1979, “On Interpreting Gödel's Second Theorem,” Journal of Philosophical Logic, 8(1): 297–313.
  • –––, 1986, Hilbert's Program: An Essay in Mathematical Instrumentalism, Dordrecht: Reidel.
  • –––, 1990, “On an Alleged Refutation of Hilbert's Program Using Gödel's First Incompleteness Theorem,” Journal of Philosophical Logic, 19(4): 343–377.
  • –––, 1995, “Wright on the Non-mechanizability of Intuitionist Reasoning,” Philosophia Mathematica, 3(1): 103–118.
  • –––, 2001, “What Does Gödel's Second Theorem Say?” Philosophia Mathematica, 9: 37–71.
  • Dyson, V., J.P. Jones, and J.C. Shepherdson, 1982, “Some Diophantine Forms of Gödel's Theorem,” Archiv für Mathematische Logik und Grundlagenforschung, 22: 51–60.
  • Ehrenfeucht, A. and S. Feferman, 1960, “Representability of recursively enumerable sets in formal theories”, Arch. Math. Logik Grundlag., 5(1–2), 37–41.
  • Feferman, S., 1960, “Arithmetization of Metamathematics in a General Setting,” Fundamenta Mathematicae, 49: 35–92.
  • –––, 1982, “Inductively Presented Systems and the Formalization of Meta-mathematics,” in Logic Colloquium ’80, D. van Dalen et al. (eds.), Amsterdam: North-Holland, pp. 95–128.
  • –––, 1989a, “Finitary Inductively Presented Logics,” in Logic Colloquium ‘88, R. Ferro, et al. (eds.), Amsterdam: North-Holland, pp. 191–220. [available online]
  • –––, 1989b, “Infinity in Mathematics: Is Cantor Necessary?” Philosophical Topics, 17(2): 23–45.
  • –––, 1995, “Penrose's Gödelian argument: A Review of Shadows of Mind, by Roger Penrose,” Psyche, 2 (7).
  • –––, 1997, “My Route to Arithmetization,” Theoria, 63: 168–181.
  • Finsler, P., 1926, “Formale Beweise und die Entscheidbarkeit,” Mathematische Zeitschrift, 25: 676–82.
  • Fitting, M., 2007, Incompleteness in the land of sets, London: College Publications. Series: Studies in logic ; v. 5.
  • Franks, C., 2009, The Autonomy of Mathematical Knowledge. Hilbert's Program Revisited, Oxford: Oxford University Press.
  • Gaifman, H., 2006, “Naming and Diagonalization, From Cantor to Gödel to Kleene,” Logic Journal of the IGPL, 14: 709–728. [available online]
  • Gentzen, G., 1936, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen, 112: 493–565.
  • Gödel, K., 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik Physik, 38: 173–198. English translation in van Heijenoort 1967, 596–616, and in Gödel 1986, 144–195.
  • –––, 1932, “Über Vollständigkeit und Widerspruchsfreiheit,” Ergebnisse eines mathematischen Kolloquiums, 3: 12–13. English translation “On Completeness and Consistency” in Gödel 1986: 235–7.
  • –––, 1933, “The Present Situation in Foundations of Mathematics,” in Gödel 1995: 45–53.
  • –––, 1934, “On Undecidable Propositions of Formal Mathematical Systems” (mimeographed lecture notes; taken by S. Kleene and J. Rosser), reprinted with corrections in Davis 1965, 41–81, and Gödel 1986, 346–371.
  • –––, 1935, “Review of Carnap 1934,” in Gödel 1986: 389.
  • –––, 1941, “In What Sense is Intuitionistic Logic Constructive?” in Gödel 1995: 189–200.
  • –––, 1944, “Russell's Mathematical Logic,” in The Philosophy of Bertrand Russell, P. A. Schilpp (ed.), Evanston, Il.: Northwestern University, pp. 125–153. Reprinted in Gödel 1990: 119­–141.
  • –––, 1951, “Some Basic Theorems on the Foundations of Mathematics and their Implications” (Gibbs Lecture), in Gödel 1995: 304­–323.
  • –––, 1953/9, “Is Mathematics a Syntax of Language?,” lecture manuscript (two versions), in Gödel 1995: 334–362.
  • –––, 1963, “Note added 28 August 1963” (to Gödel 1931), in Gödel 1986: 195.
  • –––, 1986, Collected Works I. Publications 1929–1936, S. Feferman et al. (eds.), Oxford: Oxford University Press.
  • –––, 1990, Collected Works II. Publications 1938–1974, S. Feferman et al. (eds.), Oxford: Oxford University Press.
  • –––, 1995, Collected Works III. Unpublished Essays and Lectures, S. Feferman et al. (eds.), Oxford: Oxford University Press.
  • Goldfarb, W., 1995, “Introductory Note to *1953/9,” in Gödel 1995: 324–334.
  • Goldfarb, W. and T. Ricketts, 1992, “Carnap and the Philosophy of Mathematics,” in Science and Subjectivity, D. Bell and W. Vossenkuhl (eds.), Berlin: Akademie Verlag, pp. 61–78.
  • Gómez Torrente, M., 2004, “The Indefinability of Truth in the Wahrheitsbegriff,” Annals of Pure and Applied Logic, 126(1–3): 27–37. [available online]
  • Goodstein, R., 1944, “On the Restricted Ordinal Theorem,” The Journal of Symbolic Logic, 9: 33–41.
  • Grelling, K., 1937, “Gibt es eine Gödelsche Antinomie?,” Theoria, 3: 297–306.
  • Hanson, W.H., 1971, “Mechanism and Gödel's theorems,” The British Journal for the Philosophy of Science, 22: 9–16.
  • Hellman, G., 1981, “How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism,” Nous, 15: 451–468.
  • Helmer, O., 1938, “Perelman versus Gödel,” Mind, 46: 58–60.
  • Henkin, L., 1952, “Problem,” The Journal of Symbolic Logic, 17: 160.
  • –––, 1962, “Are Mathematics and Logic Identical?” Science, 138: 788–794.
  • Hilbert, D., 1928, “Die Grundlagen der Mathematik,” Abhandlungen aus dem Mathematischen Seminar der Hamburgischen Universität, 6: 65–85. English translation in van Heijenoort 1967.
  • Hilbert, D. and P. Bernays, 1939, Grundlagen der Mathematik, vol. 2, Berlin: Springer.
  • Jeroslow, R., 1973, “Redundancies in the Hilbert-Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem,” Journal of Symbolic Logic, 38: 359–367.
  • Kaye, R., 1991, Models of Peano Arithmetic, (Oxford Logic Guides), Oxford: Clarendon Press.
  • Kirby, L. and J. Paris, 1982, “Accessible Independence Results for Peano Arithmetic,” Bull. London. Math. Soc., 14: 285–93.
  • Kleene, S.C., 1936, “General recursive functions of natural numbers,”, Mathematische Annalen 112(1): 727–742.
  • –––,1937a, “Review of Perelman 1936,” Journal of Symbolic Logic, 2: 40–41.
  • –––, 1937b, “Review of Helmer 1937,” Journal of Symbolic Logic, 2: 48–49.
  • –––, 1986, “Introductory note to 1930b, 1931 and 1932b”, in Gödel 1986, pp. 126–141.
  • Kreisel, G., 1953, “On a Problem of Henkin's,” Proc. Netherlands Acad. Sci. 56: 405–406.
  • –––, 1958, “Mathematical significance of consistency proofs,” The Journal of Symbolic Logic, 23: 159–182.
  • –––, 1967, “Mathematical Logic: What Has it Done For the Philosophy of Mathematics?” in Bertrand Russell: Philosopher of the Century, R. Schoenman (ed.), London: George Allen and Unwin.
  • Kruskal, J.B., 1960, “Well-quasi-ordering, the Tree Theorem, and Vazsonyi's Conjecture,” Transactions of the American Mathematical Society, 95 (2): 210–225.
  • Lindström, P., 2001, “Penrose's New Argument,” Journal of Philosophical Logic, 30(3): 241–250.
  • Lucas, J. R., 1961, “Minds, Machines, and Gödel,” Philosophy, 36(137): 112–137 [available online].
  • –––, 1996, “Minds, Machines, and Gödel: A Retrospect,” in Machines and Thought. The Legacy of Alan Turing, Vol. 1, P.J.R. Millican and A. Clark (eds.), Oxford: Oxford University Press, 103–124.
  • Löb, M. H., 1955, “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic, 20: 115–118.
  • Mancosu, P., 1999, “Between Vienna and Berlin: The Immediate Reception of Gödel's Incompleteness Theorems,” History and Philosophy of Logic, 20: 33–45.
  • Martin, D., 1977, “Descriptive Set Theory: Projective Sets,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, 783–815.
  • Martin, D. and Steel, J., 1988, “Projective Determinacy,” Proceedings of the National Academy of Sciences, (U.S.A.), 85: 6582–86.
  • –––, 1989, “A Proof of Projective Determinacy,” Journal of the A.M.S., 2: 71–125.
  • Matiyasevich, Y., 1970, “Diofantovost’ perechislimykh mnozhestv,” Dokl. Akad. Nauk SSSR, 191(2): 297–282 (Russian). (English translation, 1970, “Enumerable sets are Diophantine,” Soviet Math. Dokl., 11(2): 354–358.)
  • –––, 1993, Hilbert's Tenth Problem, Cambridge, MA: MIT Press.
  • Milne, P., 2007, “On Gödel Sentences and What They Say,” Philosophia Mathematica, 15: 193–226.
  • Montague, R., 1962, “Theories Incomparable with Respect to Relative Interpretability,” The Journal of Symbolic Logic, 27: 195–211.
  • Murawski, R., 1998, “Undefinability of Truth. The Problem of Priority: Tarski vs. Gödel,” History and Philosophy of Logic, 19: 153–160.
  • –––, 1999, Recursive Functions and Metamathematics: Problems of Completeness and Decidability, Gödel's Theorems, Dordrecht: Kluwer.
  • Musgrave, A., 1977, “Logicism Revisited,” British Journal for the Philosophy of Science, 28: 99–127.
  • Nagel, E. and J.R. Newman, 1958, Gödel's Proof, New York: New York University Press.
  • Paris, J. and L. Harrington, 1977, “A Mathematical Incompleteness in Peano Arithmetic,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 1133–1142 [available online].
  • Paris, J. and L. Kirby, 1978, “Sn Collection Schema in Arithmetic,” in Logic Colloquium ’77, A. McIntyre et al. (eds.), Amsterdam: North-Holland, pp. 199–209.
  • Parsons, C., 1970, “On Number Choice Schema and its Relation to Induction,” in Intuitionism and Proof Theory, Kino et al. (eds.), Amsterdam: North-Holland, pp. 459–473.
  • Penrose, R., 1989, The Emperor's New Mind: Concerning Computers, Minds, and the Laws of Physics, New York: Oxford University Press.
  • –––, 1994, Shadows of the Mind: A Search for the Missing Science of Consciousness, New York: Oxford University Press
  • –––, 1995, “Beyond the Doubting of a Shadow: A Reply to Commentaries of Shadows of the Mind,” Psyche, Vol 2.
  • –––, 1997, “On understanding understanding”, International Studies in the Philosophy of Science, 11: 7–20.
  • Perelman, C., 1936, “L'Antinomie de M. Gödel,” Académie Royale de Belgique. Bulletin de la Classe des Sciences (Series 5), 22: 730–36.
  • Piccinini, G., 2003, “Alan Turing and the Mathematical Objection,” Minds and Machines, 13: 23–48.
  • Post, E., 1941, “Absolutely Unsolvable Problems and Relatively Unsolvable Propositions: Account of an Anticipation,” published in Davis 1965, 338–433.
  • Presburger, M., 1929, “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt,” Sprawozdanie z I Kongresu Matematyków Krajów Slowiańskich, (= Comptes-rendus du I Congrès Mathématiciens des Pays Slaves), Warsaw, pp. 92–101. English translation, 1991,“On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation,” History and Philosophy of Logic, 12(2): 225–232.
  • Pudlák, P., 1996, “On the Length of Proofs of Consistency,” Collegium Logicum, Annals of the Kurt-Gödel-Society, 2: 65–86.
  • –––, 1999, “A Note on Applicability of the Incompleteness Theorem to Human Mind,” Annals of Pure and Applied Logic, 96: 335–342.
  • Putnam, H., 1960, “Minds and machines,” in Dimensions of Mind, S. Hook (ed.), New York: New York University Press. Reprinted in H. Putnam, 1975, Mind, Language, and Reality. Philosophical Papers, Vol 2, Cambridge: Cambridge University Press, pp. 325–341.
  • –––, 1975, “What is Mathematical Truth?” Historia Mathematica, 2: 529–545. Reprinted in H. Putnam, 1975, Mathematics, Matter and Method. Philosophical Papers, Vol 1, Cambridge: Cambridge University Press, pp. 60–78.
  • Quine, W.V. and J.S. Ullian, 1978, The Web of Belief, 2nd ed., New York: Random House.
  • Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel's Incompleteness Theorems,” Revue Internationale de Philosophie, 59: 513–534.
  • Ramsey, F. P., 1930, “On a Problem of Formal Logic,” Proceedings of the London Mathematical Society, series 2, 30: 264–286.
  • Ricketts, T., 1995, “Carnap's Principle of Tolerance, Empiricism, and Conventionalism,” in Reading Putnam, P. Clark & B. Hale (eds.), Cambridge: Blackwell, pp. 176–200.
  • Rodríguez-Consuegra, F., 1993, “Russell, Gödel and Logicism,” in Philosophy of Mathematics, J. Czermak (ed.), Vienna: Hölder-Pichler-Tempsky, pp. 233–42. Reprinted in, 1998, Bertrand Russell: Critical Assessments, A. Irvine (ed.), vol. 2: Logic and mathematics, London: Routledge, pp. 320–29.
  • Roeper, P., 2003, “Giving an Account of Provability within a Theory,” Philosophia Mathematica, 11: 332–340.
  • Rosser, J. B., 1936, “Extensions of Some Theorems of Gödel and Church,” Journal of Symbolic Logic, 1: 87–91.
  • –––, 1938, “Review: Kurt Grelling, Gibt es eine Godelsche Antinomie? [Grelling 1937/8],” Journal of Symbolic Logic, 3(2): 86.
  • Searle, J., 1997, “Roger Penrose, Kurt Gödel, and the Cytoskeletons,” in J. Searle: Mystery of Consciousness, New York: New York Review of Books, pp. 55–93.
  • Shapiro, S., 1998, “Incompleteness, Mechanism, and Optimism,” Bulletin of Symbolic Logic, 4: 273–302.
  • –––, 2003, “Mechanism, Truth and Penrose's New Argument,” Journal of Philosophical Logic, 32(1): 19–42.
  • Simpson, S.G., 1985, “Nonprovability of Certain Combinatorial Properties of Finite Trees,” in Harvey Friedman's Research on the Foundations of Mathematics, L. Harrington et al. (eds.), Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, pp. 87–117
  • –––, 1999, Subsystems of Second Order Arithmetic, Berlin: Springer.
  • Skolem, T., 1930, “Über einige Satzfunktionen in der Arithmetik,” Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I, no. 7, 1–28. Reprinted in T. Skolem, 1970, Selected Works in Logic, (J. Fenstad, editor), Oslo: Universitetsforlaget, pp. 281–306.
  • Smoryński, C., 1977, “The Incompleteness Theorems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 821–865.
  • –––, 1981, “Fifty Years of Self-reference in Arithmetic,” Notre Dame Journal of Formal Logic, 22(4): 357–374.
  • –––, 1991, “The Development of Self-reference: Löb's Theorem,” in Perspectives on the History of Mathematical Logic, T. Drucker (ed.), Birkhauser, pp. 111–133.
  • Smullyan, R., 1992, Gödel's Incompleteness Theorems, Oxford: Oxford University Press.
  • Solovay, R.M., 1970, “A Model of Set Theory in which Every Set of Reals is Lebesgue Measurable,” Annals of Mathematics, 92: 1–56.
  • Sternfeld, R., 1976, “The Logistic Thesis,” in Studien zu Frege/Studies on Frege I, M. Schirn (ed.), Stuttgart-Bad Cannstatt: Frommann-Holzboog, pp. 139–160.
  • Tarski, A., 1948, A Decision Method for Elementary Algebra and Geometry, manuscript. Santa Monica, CA: RAND Corp., 1948. Republished as A Decision Method for Elementary Algebra and Geometry, 2nd ed. Berkeley, CA: University of California Press, 1951.
  • Tarski, A., A. Mostowski, and R.M. Robinson, 1953, Undecidable Theories, Amsterdam: North-Holland.
  • Tennant, Neil, 2008, “Carnap, Gödel, and the Analyticity of Arithmetic”, Philosophia Mathematica, 16: 100–112.
  • Turing, A.M., 1936–7, “On Computable Numbers, with an Application to the Entscheidungsproblem,” Proceedings of the London Mathematical Society, Series 2, 42: 230–265; correction, ibid., 43: 544–546. Republished in Davis 1965, 115–154.
  • Van Heijenoort, J. (ed.), 1967, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press.
  • Visser, A., 2011, “Can We Make the Second Incompleteness Theorem Coordinate Free,” Journal on Logic and Computation, 21(4): 543–560.
  • Woodin, H., 1988, “Supercompact Cardinals, Sets of Reals, and Weakly Homogeneous Trees,” Proceedings of the National Academy of Sciences, (U.S.A.), 85: 6587–91.
  • Wright, C., 1994, “About ‘The Philosophical Significance of Gödel's Theorem’: Some Issues,” in The Philosophy of Michael Dummett, B. McGuinness and G. Oliveri (eds.) Dordrecht: Kluwer, pp. 167–202.
  • –––, 1995, “Intuitionists are not (Turing) Machines,” Philosophia Mathematica, 3: 86–102.
  • Zach, R., 2005, “Paper on the Incompleteness Theorems,” in Landmark Writings in Western Mathematics, I. Grattan-Guinness (ed.), Amsterdam: Elsevier, pp. 917–25 [available online].

Other Internet Resources

Acknowledgments

The author would like to thank Richard Zach for his careful and valuable comments on the earlier drafts of this entry. The author and SEP editors would like to thank Richard O'Callaghan for bringing to our attention that, in an earlier version of the supplement on the Diagonalization Lemma, the definition of the substitution function, although standard, didn't suffice for the purposes of the proof.

Copyright © 2015 by
Panu Raatikainen <panu.raatikainen@helsinki.fi>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing the directive]