top of page

Gödel's First Incompleteness Theorem and Hilbert's Programme

Both the first and second Incompleteness Theorems (hereafter, ‘G1’ and ‘G2’ respectively) presented by mathematician Kurt Gödel attack David Hilbert’s programme (‘HP’) for the foundations of mathematics (Giaquinto, 1983). Gödel’s theorems in fact showed that Hilbert’s optimism was unfounded (Zach, 2003). G2, in particular, is notorious for sinking HP (Paseau, 2011), but is too much emphasis placed on the severity of G2, compared to that of G1? Perhaps. This article indeed aims to show that (i) G1—as well as G2—presents a significant challenge to HP, and (ii) one must not simply assume that HP survives G1 in order for the G2 argument to arise (Paseau, 2011). Rather, G1 presents a serious challenge to Hilbert before G2. G2 therefore arguably refines G1, as the article will discuss.

The article will start by briefly outlining HP. Hilbert’s consistency and conservativeness constraints shall first be addressed here, as is the very purpose of HP. Hilbert (1922) insisted on a proof of conservativeness, hence this feature will go on to utilise Craig Smorynski’s (1977) work to explain how G1 successfully provides a direct counterexample to the desired conservation result. Michael Detlefsen’s (1990) claim that G1 is mistaken (i.e. when it claims that it sinks Hilbert’s programme with the conservation condition) will then be considered. More specifically, Detlefsen’s two-pronged argument and modification of Hilbertian Instrumentalism will be examined. The article will then respond to this, however, arguing that G1 (unlike what Detlefsen proposes) poses a serious threat to the completeness of HP. In sum, although the fundamentals of Instrumentalism might survive G1, Hilbert’s particular formalist account must be revised to do this. Gödel’s First Incompleteness Theorem, contrary to popular belief, thus also presents a serious challenge to Hilbert’s Programme.

Figure 1. Mathematician and Logician Kurt Gödel (Balaguer, 2023).

Hilbert’s Distinction Between ‘Real’ and ‘Ideal’ Mathematics

Bertrand Russell’s (1902) destructive paradox, discovered in 1901, resulted in a broad shift to Intuitionism in mathematics. As an approach to account for the foundations of mathematics, Intuitionism holds that mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fundamental principles claimed to exist in an objective reality (Brouwer, 1952). The paradox, which caused a shift into this school of thought, notably motivates programmes like Hilbert’s (1922) since HP aims to show how and why the infinitary portion of mathematics is meaningless (i.e., ‘meaningless’ since one cannot intuitively comprehend the infinite — hence a shift to Intuitionism). Despite Hilbert’s devotion to intuition here, he nevertheless maintained—as Øystein Linnebo (2017) cites—that “mathematical analysis is a symphony of the infinite” (p. 56). HP is thus a polished development of formalism. As suggested by the name, ‘formalist’ approaches to mathematics are concerned with the formal parts of mathematics. So, it is not the mathematical symbols that are significant, but their formal manipulation (Detlefsen, 1993). To arrive at his programme of ‘real’ (finitary) mathematics (‘HP’), Hilbert marries term formalism with game formalism (or at least their most appealing aspects) to overcome the challenges each notion faces separately. Whereas the term formalist identifies the entities of mathematics with their names (i.e., mathematics is about characters or symbols), the so-called game formalist likens the practice of mathematics to a game played with linguistic characters (Shapiro, 2000). Importantly for HP, both ‘term’ and ‘game’ formalism face serious difficulties. The former, for instances, faces barriers concerning the mathematics uninvolved with symbols (for example, real numbers), and the latter is oversimplified (i.e., how do axiomatic system games in mathematics differ from other sorts of games?) (Shapiro, 2000). Whilst term and game formalism deserve careful attention in another paper, it is important to note that Hilbert combines attractive elements from both which make up his programme. Various ideas from term formalism can account for finitary mathematics and its foundational axioms (Linnebo, 2017). In turn, ideas from game formalism can account for infinitary mathematics. As reflected by his belief that all of the strictly meaningful parts of mathematics are grounded in intuition, Hilbert (1922) was largely influenced by Immanuel Kant. Obviously, one has neither intuition nor experience of the infinite. As such, intuitions are only ever, in principle, of a finitary nature. This is the purpose of HP: it aims to show that, for any mathematical claim to be meaningful, it must be finitary. The two go hand in hand.

Even still, Hilbert also recognises the usefulness of infinitary mathematics (Linnebo, 2017). He thus proposes ‘ideal’ (infinitary) mathematics. With the use of ‘ideals’ in HP, one can have strictly meaningless claims in mathematics, but claims that are nevertheless useful and important. Ideals are useful fictions that are used frequently, such as negative, irrational, imaginary, ideal, and transfinite numbers. Crucially in HP, one can therefore formalise the language and theory of infinitary (meaningless) mathematics (Detlefsen, 1993). Put differently, one can expand one’s language to allow talk of such numbers and formulate a theory in this language that describes them. There are, however, important proof conditions for this to work. There are two proofs that Hilbert insisted on —namely, a consistency proof and a conservativeness proof. Firstly, the use of ideal elements must be consistent with the finitary (meaningful) mathematics (i.e., finitary mathematics must be able to prove its own consistency). Secondly, ideal mathematics must be conservative over the real part (Paseau, 2011). Hilbert’s aim, therefore, was not merely to show that formalised mathematics is consistent, but to do so in a specific way by showing that ideal mathematics can never lead to conclusions that are not in accord with real mathematics (Smorynski, 1977).

Figure 2. German mathematician David Hilbert (Kaplansky, 2023).

Since Gödel’s (1931) Second Incompleteness Theorem showed that no single formal system can prove its own consistency (G2 revealed that any formal system that can formulate its own consistency can prove its own consistency if and only if it is inconsistent), it is clear how G2 attacks HP. It is generally accepted that HP is dead because of G2, since Hilbert insisted on proof of consistency. Yet, G1 does something similar but with the conservativeness proof, which Hilbert also insisted on. Curiously, however, little attention is paid to the serious challenge G1 presents to HP as well as—and before—G2. Though this article, by and large, is not suggesting that G2 does not sink HP, it is simply showing how G1 is also a threat. G1 is therefore discussed next.

Gödel’s First Incompleteness Theorem

As mentioned, Hilbert (1922) insists that ideal mathematics must be conservative over the real part. This is to say that, for HP to succeed, whenever formalised ideal mathematics proves a real formula P, P itself (or the finitary proposition it expresses) must be ‘finitarily’ provable. Conservativeness is thus an instrumentalist constraint (Paseau, 2011). It is the type of real statement the ideal part of HP must deliver if it is to discharge its instrumental role successfully (i.e. since HP sees the more theoretical—ideal—parts of mathematics as an instrument for proving truths in the more elementary—real—parts). Likewise, the type of argument required to show that the instrumentalist constraint is satisfied is the instrumentalist argument. G1 attacks the conservativeness constraint to reveal the impossibility of the instrumentalist argument.

Figure 3. Georg Cantor, mathematician and founder of Set Theory (Encyclopedia Britannica, 2023).

According to Smorynski (1977), the real formulas in HP include not just numerical equalities and combinations thereof, but also general formulas with free variables but without unbounded quantifiers. G1 states that for any sufficiently strong, consistent formal theory S there is a sentence GS which is true but not derivable in S. Hence, GS is a real sentence according to Smorynski’s definition. Smorynksi (1977) writes the following:

Now consider a theory T which formalises ideal mathematics and its sub-theory S which formalises real mathematics. S satisfies the conditions of G1 and hence S does not derive GS. Yet, T, being a formalisation of all of mathematics (including what is required to see that GS is true), does derive GS (p. 823).

One has a real statement which is provable in ideal mathematics and not in real mathematics. Smorynksi (1977) later argues that:

Gödel destroyed Hilbert's Programme with his First Incompleteness Theorem by which he produced a sentence satisfying a sufficiently narrow criterion of meaningfulness and which, though readily recognized as true - hence a theorem of the transfinite system T, was unprovable in S. In short, he produced a direct counterexample to Hilbert's desired conservation result (p. 825).

What HP identifies as ‘ideal’ mathematics must be a conservative extension of what it identifies as ‘real’ mathematics. G1 is thus a serious issue when it provides the direct counterexample to this (above). Indeed, Hilbert (1922) himself insisted on a proof of consistency and conservativeness, as Alexander Paseau (2011) cites:

For there is a condition, a single but absolutely necessary one, to which the use of the method of ideal elements is subject, and that is the proof of consistency; for, extension by the addition of ideals is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain (p. 146).

Figure 4. Albert Einstein and Kurt Gödel (Murphy, 2014).

As argued by Paseau (2011), Hilbert appears to conflate consistency with reliability. Yet, on the assumption of real-completeness and classical logic, consistency and conservativeness are equivalent; and Hilbert had a proof-based conception of real truth, which collapses conservativeness into reliability. Most importantly, Hilbert insists on said proof of consistency and conservativeness. The proof of conservativeness is therefore just as essential for HP to succeed. G1 here is a threat to HP as such, but controversy remains regarding the severity of the threat (particularly compared to G2).

Detlefsen’s Argument

Detlefsen is bold and unique when he argues that neither G1 nor G2 challenge HP. Detlefsen, for instance, has even been described as the last son of Hilbert(‘s Programme) (Choi, 1997). The article shall now consider Detlefsen’s argument regarding G1, which opposes Smorynski's view.

Figure 5. John von Neumann, regarded as having perhaps the widest coverage of any mathematician of his time (Veisdal, 2021).

Detlefsen (1990) defends HP by adapting Hilbertian Instrumentalism and denying that ideal mathematics must be conservative over the real part. Instead, all that is required is real-soundness (Zach, 2003), something that the article will return to later. Hilbertian instrumentalism, according to Detlefsen (1990), generally requires only that the ideal theory does not prove anything which conflicts with the real theory; it is not required that it proves only real statements, which the real theory also proves.

Firstly, it is worth noting the important steps towards Detlefsen’s (1990) defence since he begins by analysing the characteristics of formal systems of ideal mathematics qua instruments. He claims that, even though Set Theory (i.e., the branch of mathematical logic that studies sets, informally described as collections of objects) is generally accepted as a formalisation of infinitary mathematics, only certain parts of Set Theory are in fact instrumentally useful (Detlefsen, 1990). As Richard Zach (2003) points out, Detlefsen has two important points illustrating this:

  1. Ideal proofs of real theorems which are more complex than any real proof of the same theorem do not yield an instrumental advantage, and hence are not instrumentally useful; and

  2. ideal proofs which are too long or complex to be comprehended by humans, and hence never play a role in actual mathematical reasoning, are also of no instrumental value.

The proof of the conservativeness of the ideal theory over real mathematics is only required for the instrumentally useful part. Detlefsen (1990) introduces his term Hilbertian residue for that part of ideal mathematics that is instrumentally useful and hence in need of proof-theoretic justification (i.e., proof of conservativeness and consistency). In this vein, consistency proof is only required for the Hilbertian residue, not for all ideal mathematics.

Figure 6. Gödel's First Incompleteness Theorem (Veisdal, 2019).

Detlefsen argues that Gödel’s Incompleteness Theorems only apply under certain conditions, claiming that G1 and G2 apply only when the theory in question contains enough basic arithmetic to carry out Gödel coding, formalisation of a proof predicate, and to prove the diagonal lemma (Zach, 2003). On Detlefsen’s (1990) account, the Hilbertian residue of a theory thus needn’t contain a sufficiently strong arithmetical sub-theory because of point (1) above.

Detlefsen goes on to argue that G1, therefore, does not affect HP. To reiterate, Smorynski’s (1977) argument is that G1 is a serious problem for HP since it can show that it is possible to have a real statement provable in ideal mathematics and not in real mathematics. On this view, as the article has discussed, G1 thus shows the conservativeness proof to be impossible since ideal mathematics is not always a conservative extension of what it identifies as ‘real’ mathematics. Yet in Detlefsen’s view, this article has noted, this simply doesn’t matter. Detlefsen (1990), brilliantly, creates and introduces the term ‘Hilbertian residue’ which may account for the part of mathematics that requires proof-theoretic justification because it is instrumentally useful. Indeed, as has been aforementioned, this is the only part of mathematics that requires proof-theoretic justification (i.e., a proof of conservativeness and consistency). On Detlefsen’s account, one must not assume that all ideal mathematics requires proof-theoretic justification. A great deal of HP is unaffected by G1 as a result, he argues.

Figure 7. Michael Detlefsen, known for his work in the philosophy and history of mathematics and philosophical logic (Weinberg, 2019).

Detlefsen (1990) later refers to Smorynksi-completeness (‘S-C’), the assumption stating that, in order to be adequate, an ideal theory must prove all recognisably true real sentences of its language. However, on an instrumentalist conception of ideal mathematics, Detlefsen (1990) holds that the goal of ideal theorising is the relatively modest one of proving more efficiently what real theorising would only prove less efficiently. Hence, there is no basis in the Hilbertian instrumentalistic programme for requiring that the ideal theory prove more real results than the real theory that it is intended to replace —there is not any evident need for the ideal theory T to prove a given sentence unless S also proves it (Detlefsen, 1990). S-C is therefore called into doubt.

By denying that ideal mathematics must be conservative over the real part, Detlefsen objects to the idea that G1 has any impact at all on HP. He argues that the basic constraint on ideal theorising is that of a soundness condition requiring that ideal mathematics need not prove any real theorem that is refutable by real means. Detlefsen (1990) writes that “...whereas such a soundness condition naturally gives rise to a corresponding conservation condition in the case of observation statements, it does not do so in the case of real propositions” (p. 350). Hence, not only does the Hilbertian instrumentalistic programme described (and tweaked) by Detlefsen call the legitimacy of S-C into doubt, but the conservation condition too.

Figure 8. According to some, imaginary numbers can describe the fundamental shape of nature (Padavic-Callaghan, 2022).

A significant part of Detlefsen’s two-pronged argument is that Hilbertian instrumentalism requires only that the ideal theory not prove anything which conflicts with the real theory (Zach, 2003). Thus, crucially, it is not required that all its real theorems are also provable by real means. Every proof is finite. Given enough time and effort, it can be proved. Hence, only a finite number of theorems will be proved, but infinitely many can be proved. The two points below outline Detlefsen’s (1990) two-pronged argument:

  1. Firstly, S-C demands that all classically true real sentences formulable in L(T) also be provable in T. Indeed, whilst Detlefsen acknowledges that S-C is attractive to a mathematical realist (i.e., whose primary duties lie in constructing a theory which brings all truths pertaining to its subject matter under its purview). However, the instrumentalist’s responsibilities are entirely different: to replace a less efficient means for identifying a given body of truths with a more efficient one. Such a task creates absolutely no obligation for one to prove anything more than is provable by the more ‘cumbersome’ methods that one would replace. Since G is not provable by real means, there is no reason why an ideal theory should be required to prove G either (Detlefsen, 1990).

  2. Secondly, ideal mathematics should not need to be a conservative extension of real mathematics. Detlefsen (1990) here rejects the suggestion that Hilbert was committed to the finitary decidability of real propositions and that his commitment to real-soundness should therefore be seen as engendering a commitment to real-conservation. G1 does not destroy hope for HP since Hilbert was more deeply committed to real-soundness, not real conservation (or so the story goes).

Figure 9. New research tightens the argument that imaginary numbers—denoted as i—are vital to quantum theory (Bedford, 2022).

Was Conservation Necessary for Hilbert?

Detlefsen (1990) claims that G2 presents a serious challenge, but G1 does not. He then boldly concludes that neither G1 nor G2 destruct Hilbertian instrumentalism in the end (despite the serious challenge G2 presents, Hilbertian Instrumentalism survives). The argument, however, is far-fetched. This article has taken a similar approach to Smorynksi, that it is G1 that initially challenged HP. In this view, G2 is a refinement of G1, even though the scope of the article has not involved any exploration of G2 specifically. Indeed, the proofs of Gödel’s theorems are finitary, but Detlefsen’s argument—that this saves HP—is a step too far. The argument is certainly unique and interesting, but it also revises HP by restructuring it and denying its purposes. There, of course, might still be hope for the underlying structure of finitary and ideal mathematics, but Hilbert’s particular programme is undeniably seriously affected by G1. It is therefore important to return to Smorynski’s (1977) argument, that Gödel destroyed HP with his First Incompleteness Theorem via "a sentence satisfying a sufficiently narrow criterion of meaningfulness and which, though recognised as true (hence a theorem of the transfinite system T), was unprovable in S" (p. 825). Unless the fundamental aims of Hilbert’s instrumentalism are ignored, it is very difficult to deny that Gödel produced a direct counterexample to Hilbert’s desired conservation result.

Detlefsen does not show that G1 fails to defeat HP. Instead, Detlefsen’s very own and reconstructed Hilbertian Instrumentalism escapes the argument from G1. Detlefsen’s work is notably similar to other post-Gödelian work on HP thusly. These have generally taken one of the following three forms: attempts to extend Hilbert’s (1922) finitism to stronger constructivist bases capable of proving more than is provable by strictly finitary means; attempts to show that for a significant family of ideal systems there are ways of ‘reducing’ their consistency problems to those of theories possessing more elementary (if not altogether finitary) justifications; and attempts by the so-called ‘reverse mathematics’ school to show that the traditionally identified ideal theories do not need to be as strong as they are in order to serve their mathematical purposes (Zach, 2003).

Figure 10. Diagram of Russell's Paradox, which is responsible for the historic shift towards Instrumentalism (Dikkala, 2014).

Attempts to reconcile HP with G1 or G2 either weaken HP and/or change it entirely. Hilbert’s formal programme does not have the resources to prove its own consistency or provide proof of conservativeness, yet mainly—ironically—because it is strong enough to contain finitary arithmetic. Hence, when Detlefsen (1990) attempts to modify HP so it can escape G1 (and therefore G2), although the modification might even prove successful, this does not allude to the idea that G1 does not present a serious challenge to HP in the first place.

Hilbert’s undying faith in completeness and thus insistency on proof of consistency and conservativeness are affected by G1. As such, G1 does present a challenge to HP when it provides a true real statement which is provable in ideal mathematics but not in real numbers (Smorynski, 1977). Simply, it is the case that Gödel produced a direct counterexample to Hilbert’s desired conservation result. Detlefsen’s (1990) modification does not change the fact that G1 creates serious issues for Hilbert's Programme, whether this applies to his reconstruction of HP or not.

Figure 11. Hilbert's 'Hotel Paradox', illustrating the counterintuitive property of infinite sets (Berry, 2017).


This article has not argued that G1 presents more of a challenge to HP than G2. Further, it does not deny that a post-Gödelian mathematical instrumentalist could potentially accept G1. Alternatively, this feature has argued that G1 presents a serious challenge to HP, despite attention oftentimes placed on the severity of G2 only. The investigation started by presenting HP, which involved (i) clarifying Hilbert’s (1922) distinction between ‘real’ and ‘ideal’ mathematics, and (ii) explaining Hilbert's aims: proof of consistency and conservativeness as conditions for strictly meaningful mathematics. For HP to succeed, whenever formalised ideal mathematics proves a real formula P, P itself (or the finitary proposition it expresses) must be finitarily provable. Hence, Hilbert does insist that ideal mathematics must be conservative over the real part.

The article went on to look at Gödel’s First Incompleteness Theorem in light of Hilbert’s conservation desire. It made use of Smorynski’s (1977) argument that G1 destructs HP before G2. Smorynski (1977) notably points out that one can have a real statement which is provable in ideal mathematics and not in real mathematics because of G1. One must therefore adapt HP, or tweak (or deny) Hilbert’s aims, in order to escape the direct counterexample presented by G1. The article has argued that this is precisely what Detlefsen (1990) does, in particular when he argues that ideal mathematics should not need to be a conservative extension of real mathematics. This is merely denying Hilbert’s conservation desire by changing HP. Was proof of conservativeness necessary to fulfil Hilbert’s aims? Yes. Suffice it to say, G1 presents a serious challenge to HP.

Bibliographical References

Brouwer, L. E. J. (1952). Historical background, principles and methods of intuitionism. South African journal of science, 49(3-4), 139-146.

Choi, B. I. (1997). From consistency to incompleteness: A philosophical study of Hilbert's Program and Goedel's Incompleteness Theorem. University of California, Berkeley.

Detlefsen, M. (1990). On an alleged refutation of Hilbert's Program using Gödel’s First Incompleteness Theorem. Journal of Philosophical Logic, 19(4), 343-377.

Detlefsen, M. (1993). Hilbert's formalism. Revue internationale de philosophie, 47(186 (4)), 285–304.

Giaquinto, M. (1983). Hilbert's philosophy of mathematics. The British journal for the philosophy of science, 34(2), 119-132.

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

Hilbert, D. (1922). Neubegründung der Mathematik: Erste Mitteilung. Abhandlungen aus dem Seminar der Hamburgischen Universität, 1, 157–177. Series of talks given at the University of Hamburg, July 25–27, 1921. Reprinted with notes by Bernays in Hilbert (1935, 157–177). English translation in Mancosu (1998a, 198–214) and Ewald (1996, 1115–1134).

Linnebo, Ø. (2017). Philosophy of Mathematics. Princeton University Press.

Paseau, A. (2011). Mathematical instrumentalism, Gödel’s theorem, and inductive evidence. Studies in History and Philosophy of Science Part A, 42(1), 140-149.

Russell, B. (1902). Letter to Frege. In Jean van Heijenoort (ed.), From Frege to Gödel. Cambridge. Mass.: Harvard University Press, 1967, 124–125.

Shapiro, Stewart (2001). Thinking about Mathematics. Oxford University Press.

Smorynski, C. (1977). The incompleteness theorems. In Jon Barwise (ed.), Handbook of Mathematical Logic. North-Holland, 821–865.

Zach, R. (2003). The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program. Synthese, 137(1/2), 211-259.

Visual Sources


Author Photo

Rebecca Ivory

Arcadia _ Logo.png

Arcadia has an extensive catalog of articles on everything from literature to science — all available for free! If you liked this article and would like to read more, subscribe below and click the “Read More” button to discover a world of unique content.

Let the posts come to you!

Thanks for submitting!

  • Instagram
  • Twitter
  • LinkedIn
bottom of page