Formalizing metamathematics

I am reading historical/philosophical stuff on the concept of "metamathematics" and am by now quite confused. Several questions emerged, but they are probably somehow confused and interrelated, I apologize.

  1. Hilbert demands that metamathematical reasoning should be "contentual" and/or "finitary". Yet, he seems nowhere to make quite explicit what he takes as "contentual" or "finitary".
  2. On the other hand, "finitary" arithmetic seems "ok" for him. Also, he seems to develop the notion of primitive recursive functions/predicates. Yet, he does nowhere declare that this is the proper formal framework for metamathematics?
  3. It is also said that primitive recursive arithmetics is the proper formal framework for metamathemtics. But does e.g. Gödel in the incompleteness paper really work with that system?
  4. In textbooks, (general) recursive, not primitive recursive functions are sometimes used in the proof of Gödel's incompleteness theorems. So, is in these cases something like "recursive arithmetics" assumed?
  5. What I gather as a principal philosophical stance of Hilbert is that the methods of metamathematics must be "weaker" as the methods in the theory studied. But Tarski says that the meta-language necessarily has to be "richer" than the object-language. How does this go together with Hilbert's demands?

Again, I apologize for too many or confused questions.


Solution 1:

You may be interested in Richard Zach's thesis: Hilbert’s Finitism: Historical, Philosophical, and Metamathematical Perspectives.