Why does Gödel’s Second Incompleteness Theorem undermine Hilbert’s program

incompletenesslogicproof-theory

Recall that Gödel's First Incompleteness Theorem (denote GIT1) states, roughly, any axiomatic system $S$ stronger than Peano Arithmetic (PA) cannot be "covered" by finitely many axioms.
GIT2 states, roughly, that furthermore such $S$ cannot prove, within itself, its own consistency (denote $\mathrm{cons}\; S$).
And it is often said that GIT1, together with GIT2, invalidates Hilbert's program (HP).

It's rather obvious to me that GIT1 declares HP to be problematic, if not impossible.
But what GIT2 says of HP, is less obvious.
Indeed, even if $\mathrm{cons}\; S$ were a theorem within S, that is

$$\models_S \mathrm{cons}\; S$$

and suppose we do not know GIT2.
Then, it is possible that $S$ is inconsistent, and a contradiction formula is a theorem in $S$, which in turn entails $\mathrm{cons}\; S$.
Thus, it seems, whether $\mathrm{cons}\; S$ is a theorem or not, is not very important.
If so, GIT2 does not really tell us much by saying that $\mathrm{cons}\; S$ is not a theorem in $S$.

So how was GIT2 a bad news to Hilbert's view?

Best Answer

First, as others have pointed out, your characterization of GIT1 is not right. What it actually roughly says is that any complete and consistent theory stronger than PA cannot be generated by a decidable set of axioms. This does kill the prospects of a single formal system that decides “all of mathematics” which was one of Hilbert’s loftier goals.$^*$

But another big aspect was to have a finitary proof on the consistency of such a system that underlies mathematics, which still makes sense as a goal even if that system is necessarily incomplete. For example. we could say the system is ZFC, which we know allows us to formalize most of known mathematics, even if we also know there are statements it can’t decide (provided it is consistent).

I have a few qualms with the argument that a proof of Con(S) in S would not tell us much, but for the most part I agree, so I’ll grant it for the purposes of this answer. However, the goal is much more ambitious than this: we want to prove the consistency of our system of mathematics (say ZFC) in a very weak finitary theory of arithmetic (say PRA), not merely in ZFC. Surely it would be desirable and meaningful if that could be carried out. However, if GIT2 tells us ZFC can’t prove it, then certainly a weaker theory like PRA can’t either. So GIT2 is indeed bad news for this aspect of the program.

$^*$ I’m a lousy mathematician but an even worse historian. What I say is based on my understanding from the folklore of what Hilbert’s Program was and may or may not correlate with anything Hilbert actually said or believed.