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^*\).
- Fragments of arithmetic
- scientific article; zbMATH DE number 4112583 (Why is no real title available?)
- scientific article; zbMATH DE number 218496 (Why is no real title available?)
- scientific article; zbMATH DE number 3365265 (Why is no real title available?)
- Modal analysis of generalized rosser sentences
- On recursion theory in IΣ1
- Partially Conservative Extensions of Arithmetic
- Provability interpretations of modal logic
- Rosser sentences
- Self-reference and modal logic
- Interpretability in PRA
- On the \(\Sigma{}^ 0_ 1\)-conservativity of \(\Sigma{}^ 0_ 1\)- completeness
- \(\Pi_ 2^ 1\)-logic and uniformization in the analytical hierarchy
- The logic of \(\Pi_ 1\)-conservativity continued
- A smart child of Peano's
- Lewis meets Brouwer: constructive strict implication
- Obituary: Franco Montagna (1948--2015)
- A simple proof of arithmetical completeness for \(\Pi_ 1\)-conservativity logic
- A short note on essentially \(\Sigma_1\) sentences
- On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories
- Self provers and \(\Sigma_{1}\) sentences
- Franco Montagna's work on provability logic and many-valued logic
- An inside view of EXP; or, The closed fragment of the provability logic of IΔ0 + Ω1 with a prepositional constant for EXP
- scientific article; zbMATH DE number 3557755 (Why is no real title available?)
- scientific article; zbMATH DE number 1215477 (Why is no real title available?)
- Provability and interpretability logics with restricted realizations
- scientific article; zbMATH DE number 218496 (Why is no real title available?)
- Interpretability over peano arithmetic
- Interpreting GPFCSP within the LΠ ½ logic framework
- Reflection calculus and conservativity spectra
- Modal completeness of sublogics of the interpretability logic IL
- Unary interpretability logics for sublogics of the interpretability logic \textbf{IL}
- An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics
- Transductions in arithmetic
This page was built for publication: The logic of \(\Pi_ 1\)-conservativity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q749519)
