Questions

Things I’m confused about.

• I’m uncomfortable with theorems in the meta-logic. How do you define the meta-logic without infinite recursion (meta-meta, etc.)? Godel incompleteness, etc. are NOT theorems in the logic, but the meta-logic—if you want them as theorems in the logic then you have to define the logic inside the logic—there’s no reflection, right? Because that would be \(\square A to A\).
• What did I mean by reflection?
• Nesting is unsatisfactory…
• Is \(PA\vdash A\implies PA\vdash B \iff PA\vdash \square A \to \square B\) a theorem in the meta-logic?
• Is \(PA\vdash \square A\implies PA\vdash A\) a theorem in the meta-logic? An axiom?
• How do you define “truth” in the meta-logic?
• Is \(\square \square A \to \square A\) a theorem?
• Is \(PA\vdash \square A \to \square B, PA\vdash A \implies PA\vdash B\)? How about \(PA\vdash \square (\square A \to \square B)\wedge \square A \to \square B\)?
• Can you add quantifiers? Is it true that \(\forall x, \square P(x) \imples \square \forall x, P(x)\)? My guess is not (at least, it can’t be proved). Should \(\square\) be Bew here? I think you’re not allowed to use \(\square\) here, but that’s ok, you can state it with Bew. \(\square\) is interpreted as \(Bew(\ce{})\) in PA, right?
• Is \((\square A \to \square B) \to \square (A\to B)\) a theorem?