The logic of \(\Pi_ 1\)-conservativity (Q749519): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 02:07, 5 March 2024
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
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
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