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!