The logic of \(\Pi_ 1\)-conservativity (Q749519): Difference between revisions

The modal propositional provability logic L (or G) has the following axioms: (L1) tautologies, (L2) \(\square (A\to B)\to (\square A\to \square B)\), (L3) \(\square A\to \square \square A\) and (L4) \(\square (\square A\to A)\to \square A\). Its deduction rules are modus ponens and generalizations (if \(\vdash A\), then \(\vdash \square A)\). The interpretability logic IL extends the language with the binary modality \(\triangleright\) and has the following extra axioms: (J1) \(\square (A\to B)\to (A\triangleright B)\), (J2) \((A\triangleright B \& B\triangleright C)\to (A\triangleright C)\), (J3) \((A\triangleright C \& B\triangleright C)\to (A\vee B\triangleright C)\), (J4) \(A\triangleright B\to (\diamondsuit A\to \diamondsuit B)\) and (J5) \(\diamondsuit A\triangleright A\). ILM (Interpretability Logic with Montagna's principle) results by adding the axiom \((A\triangleright B)\to (A \& \square C)\triangleright (B \& \square C).\) \(I\Sigma_ 1\) is the fragment of Peano arithmetic with induction restricted to \(\Sigma_ 1\)-formulas. Let \(T\supseteq I\Sigma_ 1\) be \(\Sigma_ 1\)-sound. An arithmetical p(artial) c(onservativity) interpretation of ILM in T is by definition a mapping * associating with each formula of ILM a sentence of T such that (1) * commutes with the connectives, (2) \((\square A)^*:=\Pr_ T(A^*)\), where \(\Pr_ T\) is the provability predicate of T, and (3) \((A\triangleright B)^*:=(\forall z\Pi_ 1\)-sentence) \((\Pr_ T(B^*\to z)\to \Pr_ T(A^*\to z))\), i.e., the \(\Pi_ 1\)-consequences of \(T+A^*\) include the \(\Pi_ 1\)-consequences of \(T+B^*.\) ILM is sound for arithmetical pc-interpretations, i.e., if ILM\(\vdash A\), then \(T\vdash A^*\) for each *. The authors prove in this paper the following arithmetical completeness theorem. If \(T\supseteq I\Sigma_ 1\) is \(\Sigma_ 1\)-sound, then ILM is complete with respect to arithmetical pc-interpretations, i.e., if not ILM\(\vdash A\), then there is a pc- interpretation * such that not \(T\vdash A^*\).