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.
- 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".
- 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?
- 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?
- 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?
- 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.