2
$\begingroup$

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

I would appreciate your help and comments!

$\endgroup$
9
  • 2
    $\begingroup$ 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. $\endgroup$
    – Derek Elkins left SE
    Oct 29, 2018 at 21:46
  • $\begingroup$ @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? $\endgroup$
    – Daniels Krimans
    Oct 29, 2018 at 21:48
  • $\begingroup$ 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. $\endgroup$
    – Derek Elkins left SE
    Oct 29, 2018 at 21:56
  • $\begingroup$ @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? $\endgroup$
    – Daniels Krimans
    Oct 29, 2018 at 21:59
  • $\begingroup$ 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. $\endgroup$
    – Derek Elkins left SE
    Oct 29, 2018 at 22:11

1 Answer 1

Reset to default
2
$\begingroup$

Short answer. Sure, we can prove that, e.g., Peano Arithmetic is consistent if we stand outside the theory and help ourselves to a sufficiently strong background theory to work in. But Gödel's second theorem tells us that this metatheory will have to be in some respects stronger than Peano Arithmetic itself to do the trick. Which probably isn't much help if we were worried about the consistency of Peano Arithmetic in the first place, for the worries will carry over to the stronger theory.

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.

Long answer: Not here but in Ch. 37 (in particular) of the second edition of my Introduction to Gödel's Theorems (should be in any academic library)! Which shows the story is a bit more complicated in interesting ways, though the short take-home message is much the same.

$\endgroup$
7
  • $\begingroup$ Thanks for the answer. ''Gödel's second theorem tells us that the metatheory will have to be in some respects stronger than Peano Arithmetic''. How do you conclude that it has to be stronger? Why weaker one would not suffice? I think I have read that Godels theorem can be proven in PRA metatheory which is weaker than PA $\endgroup$
    – Daniels Krimans
    Oct 30, 2018 at 2:00
  • 2
    $\begingroup$ @DanielsKrimans He is talking about proving the consistency of PA, not the incompleteness theorem. $\endgroup$
    – spaceisdarkgreen
    Oct 30, 2018 at 7:24
  • 1
    $\begingroup$ Careful! Yes, a very weak background theory -- acceptable even to a finitist -- is enough to prove e.g. (G): PA cannot prove Con(PA). There's no wriggle room. We have to accept (G). But now what does (G) tell us? That PA can't prove Con(PA). It requires something stronger than PA (at least in some respects) to prove the consistency of PA. Likewise, that weak background proves (G'): ZFC cannot prove Con(ZFC). So it requires something stronger than ZFC to prove the consistency of ZFC. So a finitistically acceptable metatheory can't prove the consistency of ZFC. $\endgroup$
    – Peter Smith
    Oct 30, 2018 at 7:26
  • 1
    $\begingroup$ @DanielsKrimans You indeed seem a bit confused about Hilbert's program. Read plato.stanford.edu/entries/hilbert-program $\endgroup$
    – Peter Smith
    Oct 30, 2018 at 7:49
  • 1
    $\begingroup$ @DanielsKrimans See e.g. William Tait's "Finitism" Journal of Philosophy, 1981, 534-556 (available through your uni's Jstor), reprinted in a follow-up paper in Tait's book The Provenance of Pure Reason (OUP 2005) $\endgroup$
    – Peter Smith
    Oct 31, 2018 at 8:27

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .