We know from Godel's theorems that interesting logics can not prove their own consistency, so whenever we want to prove the consistency of such a logic $L$, we need to take a step back, place this logic inside a metalogic $M$ and do the proof there. Which is, although not totally surprising, quite disappointing. What I want to understand is the relationship between the logics $L$ and $M$. So here are some questions about that:
- What would be a minimal metalogic which can prove consistency of PA?
- What would be a minimal metalogic which can prove consistency of ZF(C)?
- What would be a minimal metalogic which can prove Godel's theorems?
Update: It turns out that my questions are not well-posed, since 'minimal' does not mean anything unless we define what are acceptable metalogics and how to compare them. Some useful ideas extracted from the comments: Ordinal Analysis (for measuring and comparing strength of various logics) and Reverse Mathematics (for detailed analysis of the role of various axioms in arithmetic), but also Proof Theory in general. Thank you all for contributing.