# Why Godel's theorem influences Hilbert's programme?

I have trouble understanding why it is being said that Godel's incompleteness theorem shows that Hilbert's programme is essentially impossible.

So, if I understand Godel's second incompleteness theorem, it says that sufficiently strong theorems such as Peano Arithmetic cannot prove its consistency within itself.

But isn't Hilbert's programme that we prove consistency using finitary means in metatheory? It seems to me that Godel's theorem implies that we cannot prove the consistency of the theory within the formal theory. But what about proving the consistency of the theory using metatheory (which is outside of the formal theory)?

• For the purposes of Hilbert's programme, your metatheory would itself presumably be a formal theory. So, yes, you can prove the consistency of, say, PA in a metatheory, but how do you know your metatheory is consistent? The standard scenario in that case is proving the consistency of PA within ZFC, another formal theory. Oct 29, 2018 at 21:46
• @DerekElkins But isn't the whole point of metatheory to be not formal theory, but, say, be intuitive reasoning about finite strings which we have intuition for because, for example, they could be checked in the real world by just writing these finite strings? Oct 29, 2018 at 21:48
• Arguably, but Gödel's theorem suggests that many of the formalizations of those "intuitions about finite strings" are either inconsistent or incomplete. That means that either we very much need to scale back what we "intuitively" believe about finite strings, or there are things about finite strings that we believe that are unformalizable. This is not an exhaustive listing of alternatives, but regardless, some serious reflection is needed. If you do consider things "true" which are verifiable in the real (physical) world, then you go beyond finitism to ultrafinitism. Oct 29, 2018 at 21:56
• @DerekElkins I don't understand why do you say that we need formalizations of our intuitions? Formalizing some theory means that there is metatheory which talks about how it is formalized. That means if we formalize metatheory we need metametatheory, and so on. So in the end we still have something that relies purely on our intuition and is not formalized. Isn't that true? Oct 29, 2018 at 21:59
• I didn't say we needed to formalize our intuitions, just that the systems we usually present as formalizations of our intuitions of finite strings are, in fact, subject to Gödel's theorem. Formal systems that are conservative enough not to run afoul of Gödel are usually viewed as too weak to actually do math in as well as justify some of our other intuitions. One (overly colorful) way to frame this is that Hilbert thought he could battle ambiguities with infinities based in the "finite", but the battle lines are actually drawn within the "finite". Somewhere. Oct 29, 2018 at 22:11

And the argument generalises. Hilbert's Program was to make it safe to play the game of infinitary mathematics (e.g. even wildly infinitary full set theory) by standing outside the theory and using uncontroversial weak mathematics to at least prove the consistency of the infinitary theory. Gödel tells us this can't be done. A consistency proof for a theory $$T$$ requires more oomph than is available in $$T$$, so we certainly can't prove $$T$$'s consistency in a much weaker theory.