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)?
I would appreciate your help and comments!
 A: 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.
