The logic of \(\Pi_ 1\)-conservativity (Q749519)

From MaRDI portal
scientific article
Language Label Description Also known as
English
The logic of \(\Pi_ 1\)-conservativity
scientific article

    Statements

    The logic of \(\Pi_ 1\)-conservativity (English)
    0 references
    0 references
    0 references
    0 references
    1990
    0 references
    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^*\).
    0 references
    0 references
    modal propositional provability logic
    0 references
    Interpretability Logic with Montagna's principle
    0 references
    fragment of Peano arithmetic
    0 references
    arithmetical pc- interpretations
    0 references
    arithmetical completeness theorem
    0 references
    0 references