Belief that all methods of finitary reasoning used in metatheory are formalizable

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.

• I think some of what you are asking is essentially the question of Church's Thesis: what is and what is not an algorithm? Goedel's recursive functions (later generalized), Turing machines, Church's lambda-definability, they all turn out to be equivalent. Church's thesis is that the concept of procedure/algorithm (which is supposed to include all methods of finitary reasoning) is indeed captured by these formalizations. But this cannot be proven, it can only be disproven. But given that many independent attempts have all ended up coinciding, many/most people believe it is in fact true. Oct 31, 2018 at 5:41
• Essentially all the work we do in the metatheory - finitistic or not - is formalizable in ZFC, just as almost all mathematics is formalizable in ZFC, sometimes with the addition of large cardinal axioms. The more interesting issue is not whether the metatheory is formalizable in strong theories, but whether the finitistic part of the metatheory is formalizable in weak theories such as PRA. We know that all the results of a basic standard logic course can be formalized in $\mathsf{ACA}_0$, a system of second-order arithmetic that is equiconsistent with PA. Oct 31, 2018 at 14:03