# 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.

-
(4): The auxiliary functions in the usual proofs of the Incompleteness Theorem are all primitive recursive. Many presentations don't bother to point this out, indeed don't bother to define primitive recursive. This is because primitive recursiveness is viewed as a less important level than it used to be. –  André Nicolas Aug 26 '11 at 17:32
(5): Tarski was after Hilbert and Godel. –  Kaveh Sep 1 '11 at 5:47
(4): we don't even need primitive recursiveness, much less is sufficient, but depending on the context simpler arguments which might assume more might be used. –  Kaveh Sep 1 '11 at 5:49
(3): I think the title of Godel's paper refers to Hilbert's system. –  Kaveh Sep 1 '11 at 5:49
(2): For metamathematics it seems that he was OK with bounded quantification, what is problematic is quantification on infinite sets. –  Kaveh Sep 1 '11 at 5:51