I am trying to clear up my understanding of
- a way to formalize Mathematics
- How proof theory is build upon this
Say i want to formalize Mathematics so that i can have a computer or just an extraordinarily patient human that doesn't know any Mathematics (lets call him Dan) check my proof. First i have to pick a sequent calculus $K$ and a compatible Metatheory say ZF.
Q1: If i was a constructivist i might pick a different $K$ than if i wasn't, right?
Then i need to tell Dan what a Variable, Term, Formula and free Variable is in my sequent calculus and the allowed syntactic Manipulation rules and what a correct derivation is.
Q2: This requires Dan to understand the concept of Definition by recursion, right? (Because term Formula, free Variable are all Notions defined via recursion.)
If i wasn't trying to read books about set theory i would be done now. I could formalise all my Mathematics and ask Dan to verify my proofs. Now to part two of my questions: If i want to prove Statements about formal Systems i first need to implement formal systems in my formalization. E.g i use certain pairs of natural numbers and act like they are "symbols" and i use certain sequences of such pairs to talk about formulas and finally define the notion of Interpretation and Structure. This gives me a way to "plug in" objects from my MetaZF to my Structure and to talk about sentences like "[sequence of symbols] holds in Structure S"
Q3: Dan would say "[sequence of symbols] holds in Structure S" holds if i can supply him a proof of "Interpretation([sequence of symbols])" in my sequence calculus, right?
Q4: "We work in ZF" in a book like Kunens Set-Theory means that he picks the Metatheory ZF along with a classical compatible sequent calculus right?
Q5: To add to confusion we can also introduce the concept of sequent calculus in our formalization and then make Statements about how sequent calculus (in the formalization) and Interpretations relate. Is this the way e.g. Gödels completeness theorem is to be understood?
Q6: Some people pick Metatheorys like Peano Arithmetic instead of ZF. What is the Motivation behind this? As i see it, using ZF as Meta has the advantage of keeping all other Mathematics in the same system (Dan doesn't need to learn new rulesets). Doing some Maths by using PA makes it sort of incomparable to the rest doesn't it? I mean i could probably also do all of my Mathematics in a formalization of ZF (with PA as Meta) but why would i?