In https://plato.stanford.edu/entries/hilbert-program/ it is written that:
"Gödel had found the same result already independently: the second incompleteness theorem, asserting that the system of Principia does not prove the formalization of the claim that the system of Principia is consistent (provided it is). All the methods of finitary reasoning used in the consistency proofs up till then were believed to be formalizable in Principia, however. Hence, if the consistency of Principia were provable by the methods used in Ackermann's proofs, it should be possible to formalize this proof in Principia; but this is what the second incompleteness theorem states is impossible."
The crucial sentence for me is "All the methods of finitary reasoning used in the consistency proofs up till then were believed to be formalizable in Principia, however."
Do we still believe that all of the methods of finitary reasoning used in metatheory are formalizable in formal theories like PA or ZFC? What kind of evidence do we have here?
Intuitively, for me to accept the failure of Hilbert's program I would have to somehow convince myself that metatheory is formalizable in formal theory (I am not even sure what that means). But, I have doubts because some metatheory is being written in natural language in an intuitive way, such as, what is a proof, what is a deduction, what is a formula and so on. How can one formalize this in PA? I feel that we can formalize things about natural numbers which we use intuitively in metatheory by some PRA and then encode it in PA. But I am not sure whether we can formalize everything in metatheory in some formal system.
I hope my question is clear and I would be happy for any kind of suggestions and advice here.