Did the Incompleteness Theorems Refute Hilbert's Program?

Did Gödel's theorems spell the end of Hilbert's program altogether? From one point of view, the answer would seem to be yes—what the theorems precisely show is that mathematics cannot be formally reconstructed strictly on the basis of concrete intuition of symbols.

Gödel himself remarked that it was largely Turing's work, in particular the “precise and unquestionably adequate definition of the notion of formal system” given in Turing 1937, which convinced him that his incompleteness theorems, being fully general, refuted the Hilbert program. (See the supplemental note to Gödel 1931 added in August 1963, p. 195 of Gödel 1986. See also Gödel's correspondence with Nagel, p. 145 and 147, Gödel 2003b. Gödel had informally convinced himself of this already in 1933, see p.52 of his *1933o.) However there are many subtleties here involving various salient features of formalizations of the notion of computability. For example, Sieg has pointed out (2006) that Gödel's identification of the general notion of formal system with Turing machines is problematic, resting as it does on an absolute notion of computable function. This is because the notion of formal system is to be defined in terms of the notion of absolute computability, whereas the notion of formal system seems to be needed in order to prove the absoluteness of the notion of computability.

In connection with the impact of the Second Incompleteness Theorem on the Hilbert program, although this is mostly taken for granted, some have questioned whether Gödel's second theorem establishes its claim in full generality. As Bernays noted in Hilbert and Bernays 1934, the theorem permits generalizations in two directions: first, the class of theories to which the theorem applies can be broadened to a wider class of theories. Secondly, a more general notion of consistency could be introduced, than what was indicated by Gödel in his 1931 paper. That is, the theorem could be extended to any formula expressing the consistency of the relevant theory.

The latter type of generalization brought to the fore the question of the intensional adequacy of a theory's proof concept. We take a moment to describe what this means. As Feferman noted in his (1960) (following Bernays) there is an important distinction between the two incompleteness theorems. As we have seen, Gödel's First Incompleteness Theorem exhibits a sentence G in the language of the relevant theory, which is undecided by the theory. Nothing about the correctness of the claim that e.g. Peano arithmetic is incomplete, turns on the meaning of G, however the term “meaning” is construed. Feferman points out that this is not the case with the second theorem, where the general claim, namely that any sufficiently strong theory cannot prove “its own consistency,” must depend on the meaning of the consistency statement as read by the theory. That is, we should grant the meta-theoretical claim that a theory T cannot prove its own consistency only when there is a sentence both which T “recognizes” as a consistency statement, and which T cannot prove. This is not to question the legitimacy of Gödel's second theorem of course, but rather to point to possible limitations on its range of application—an observation Gödel himself made in his 1931 paper, as we have noted.

The criteria for a theory T's “recognizing” its consistency statement as such are met just in case it can be proved in T that its proof predicate satisfies the three Hilbert-Bernays derivability conditions as given in Hilbert and Bernays 1934. The concept of provability in T, and thus the concept of T's consistency, is then said to be “intensionally adequate,” that is fully expressive of the notion of consistency involved.

In his paper Feferman treats the problem, how to show that the derivability conditions are satisfied in relevant cases. In particular, Feferman pointed to intensional problems connected to the notion of axiomhood by exhibiting a non-standard though extensionally (i.e., numerically) correct binumeration of the arithmetic theory T under consideration, for which the (intensionally incorrect) consistency statement can be proved by T. He then went on to give a systematic, general treatment which ruled out such pathological examples.

Detlefsen offered (1986) a different critique of intensional adequacy, drawing more emphatically the distinction between the Second Incompleteness Theorem itself, as a mathematical theorem, and the wider, proto-philosophical claim that “every set of propositions sufficient to make a formula of T a fit expression of T's consistency is also sufficient to make that formula unprovable in T (if T is consistent).” In Detlefsen's view, particularly the third derivability condition is problematic and not fully justified.

Subsequent developments focused on weak arithmetic theories, that is, the issue whether intensionally correct versions of Gödel's Second Incompleteness Theorem exist not only for Peano arithmetic but for weaker arithmetic theories as well, i.e., theories for which a case can more easily be made, that they are genuinely finitary.^[1]

Intensional adequacy aside, from other perspectives it would appear that the Hilbert program was not unfeasible, if a wider notion of finitary is admitted. For some those relativizations represent too radical a departure from the program in its original formulation. The reader is referred to the contemporary discussion of these matters. In particular, for a discussion of relativised Hilbert programs the reader is referred to Feferman 1988.

We end this consideration of the Second Incompleteness Theorem by noting that there are semantic proofs of consistency of course. In this connection a simple semantic proof of the Second Incompleteness Theorem, which Kripke attributes to Kuratowski, might be worth mentioning. The Kuratowski argument is the following: Set theory cannot prove that set theory is consistent in the strong sense that some V_α is a model of set theory. For suppose it does. Then there is α such that V_α is a model of set theory. Hence there is also in V_α some β<α such that V_β is a model of set theory. Continuing in this way we get an infinite descending sequence of ordinals, a contradiction. See Kripke 2009.

For further discussion, see the entry on Hilbert's Program.