See GÖDEL’ S INCOMPLETENESS. THEOREM. Gödel’s incompleteness theorems, two theorems formulated and proved by the Austrian logician Kurt Gödel (1906–78) in his famous 1931 paper ‘Über formal unentscheidbare Sätze der Principia Mathematica und vervandter Systeme I,’ probably the most celebrated results in the whole of logic. They are aptly referred to as ‘incompleteness’ theorems since each shows, for any member of a certain class of formal systems, that there is a sentence formulable in its language that it cannot prove, but that it would be desirable for it to prove. In the case of the first theorem (G1), what cannot be proved is a true sentence of the language of the given theory. G1 is thus a disappointment to any theory constructor who wants his theory to tell the whole truth about its subject. In the case of the second theorem (G2), what cannot be proved is a sentence of the theory that ‘expresses’ its consistency. G2 is thus a disappointment to those who desire a straightforward execution of Hilbert’s Program.
The proofs of the incompleteness theorems can be seen as based on three main ideas. The first is that of a Gödel numbering, i.e., an assignment of natural numbers to each of the various objects (i.e., the terms, formulas, axioms, proofs, etc.) belonging to the various syntactical categories of the given formal system T (referred to here as the ‘represented theory’) whose metamathematics is under consideration. The second is that of a representational scheme. This includes (i) the use of the Gödel numbering to develop number-theoretic codifications of various of the metamathematical properties pertaining to the represented theory, and (ii) the selection of a theory S (hereafter, the ‘representing theory’) and a family of formulas from that theory (the ‘representing formulas’) in terms of which to register as theorems various of the facts concerning the metamathematical properties of the represented theory thus encoded. The basic result of this representational scheme is the weak representation of the set of (Gödel numbers of) theorems of T, where a set L of numbers is said to be weakly represented in S by a formula ‘L(x)’ of S just in case for every number n, n1 L if and only if ‘L([n])’ is a theorem of S, where ‘[n]’ is the standard term of S that, under the intended interpretation of S, designates the number n. Since the set of (Gödel numbers of) theorems of the represented theory T will typically be recursively enumerable, and the representing theory S must be capable of weakly representing this set, the basic strength requirement on S is that it be capable of weakly representing the recursively enumerable sets of natural numbers. Because basic systems of arithmetic (e.g. Robinson’s arithmetic and Peano arithmetic) all have this capacity, Gödel’s theorems are often stated using containment of a fragment of arithmetic as the basic strength requirement governing the capacities of the representing theory (which, of course, is also often the represented theory). More on this point below. The third main idea behind the incompleteness theorems is that of a diagonal or fixed point construction within S for the notion of unprovability-in-T; i.e., the formulation of a sentence Gödel of S which, under the given Gödel numbering of T, the given representation of T ‘s metamathematical notions in S, and the intended interpretation of the language of S, says of itself that it is not provable-in-T. Gödel is thus false if provable and unprovable if true. More specifically, if ‘ProvT(x)’ is a formula of S that weakly represents the set of (Gödel numbers of) theorems of T in S, then Gödel can be any formula of S that is provably equivalent in S to the formula ‘- ProvT ([Gödel])’. Given this background, G1 can be stated as follows: If (a) the representing theory S is any subtheory of the represented theory T (up to and including the represented theory itself), (b) the representing theory S is consistent, (c) the formula ‘ProvT (x)’ weakly represents the set of (Gödel numbers of) theorems of the represented theory T in the representing theory S, and (d) Gödel is any sentence provably equivalent in the representing theory S to ‘ProvT ([Gödel])’, then neither Gödel nor -Gödel is a theorem of the representing theory S.
The proof proceeds in two parts. In the first part it is shown that, for any representing theory S (up to and including the case where S % T ), if S is consistent, then -Gödel is not a theorem of S. To obtain this in its strongest form, we pick the strongest subtheory S of T possible, namely S % T, and construct a reductio. Thus, suppose that (1) -Gödel is a theorem of T. From (1) and (d) it follows that (2) ‘ProvT([Gödel])’ is a theorem of T. And from (2) and (c) (in the ‘if’ direction) it follows that (3) Gödel is a theorem of T. But (1) and (3) together imply that the representing theory T is inconsistent. Hence, if T is consistent, -Gödel cannot be a theorem of T.
In the second part of the proof it is argued that if the representing theory S is consistent, then Gödel is not a theorem of it. Again, to obtain the strongest result, we let S be the strongest subtheory of T possible (namely T itself) and, as before, argue by reductio. Thus we suppose that (A) Gödel is a theorem of S (% T ). From this assumption and condition (d) it follows that (B) ‘-Provr ([Gödel])’ is a theorem of S (% T ). By (A) and (c) (in the ‘only if’ direction) it follows that (C) ‘ProvT ([Gödel])’ is a theorem of S (% T ). But from (B) and (C) it follows that S (% T ) is inconsistent. Hence, Gödel is not provable in any consistent representing theory S up to and including T itself.
The above statement of G1 is, of course, not the usual one. The usual statement suppresses the distinction stressed above between the representing and represented theories and collaterally replaces our condition (c) with a clause to the effect that T is a recursively axiomatizable extension of some suitably weak system of arithmetic (e.g. Robinson’s arithmetic, primitive recursive arithmetic, or Peano arithmetic). This puts into a single clause what, metamathematically speaking, are two separate conditions – one pertaining to the representing theory, the other to the represented theory. The requirement that T be an extension of the selected weak arithmetic addresses the question of T’s adequacy as a representing theory, since the crucial fact about extensions of the weak arithmetic chosen is that they are capable of weakly representing all recursively enumerable sets. This constraint on T’s capabilities as a representing theory is in partnership with the usual requirement that, in its capacity as a represented theory, T be recursively axiomatizable. For T’s recursive axiomatizability ensures (under ordinary choices of logic for T ) that its set of theorems will be recursively enumerable – and hence weakly representable in the kind of representing theory that it itself (by virtue of its being an extension of the weak arithmetic specified) is. G1 can, however, be extended to certain theories whose sets of (Gödel numbers of) theorems are not recursively enumerable. When this is done, the basic capacity required of the representing theory is no longer merely that the recursively enumerable sets of natural numbers be representable in it, but that it also be capable of representing various non-recursively enumerable sets, and hence that it go beyond the weak arithmetics mentioned earlier. G2 is a more demanding result that G1 in that it puts significantly stronger demands on the formula ‘ProvT (x)’ used to express the notion of provability for the represented theory T. In proving G1 all that is required of ‘ProvT (x)’ is that it weakly represent θ (% the set of Gödel numbers of theorems of T); i.e., that it yield an extensionally accurate registry of the theorems of the represented theory in the representing theory. G2 places additional conditions on ‘ProvT (x)’; conditions which result from the fact that, to prove G2, we must codify the second part of the proof of G1 in T itself. To do this, ‘ProvT (x)’ must be a provability predicate for T. That is, it must satisfy the following constraints, commonly referred to as the Derivability Conditions (for ‘ProvT (x)’): (I) If A is a theorem of the represented theory, then ‘ProvT ([A])’ must be a theorem of the representing theory. (II) Every instance of the formula ‘ProvT ([A P B]) P (ProvT ([A]) P ProvT ([B]))’ must be a theorem of T. (III) Every instance of the formula ‘ProvT ([A]) P ProvT ([ProvT ([A])])’ must be a theorem of T. (I), of course, is just part of the requirement that ‘ProvT ([A])’ weakly represent T’s theoremset in T. So it does not go beyond what is required for the proof of G1. (II) and (III), however, do. They make it possible to ‘formalize’ the second part of the proof of G1 in T itself. (II) captures, in terms of ‘ProvT (X)’, the modus ponens inference by which (B) is derived from (A), and (III) codifies in T the appeal to (c) used in deriving (C) from (A).
The result of this ‘formalization’ process is a proof within T of the formula ‘ConT P Gödel’ (where ConT is a formula of the form ‘- ProvT ([#])’, with ‘ProvT (x)’ a provability predicate for T and ‘[#]’ the standard numeral denoting the Gödel number # of some formula refutable