zbMATH — the first resource for mathematics

The logic of \(\Pi_ 1\)-conservativity. (English) Zbl 0713.03007
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^*\).
Reviewer: H.C.M.de Swart

03B45 Modal logic (including the logic of norms)
Full Text: DOI
[1] Berarducci, A.: The interpretability logic of Peano arithmetic. Thesis, University of California at Berkeley 1989 (to appear as an article J. Symb. Logic)
[2] de Jongh, D., Veltman, F.: Provability logics for relative interpretability. In: Proceedings of Heyting ’88 (Bulgaria) (to appear) · Zbl 0794.03026
[3] Guaspari, D.: Partially conservative extensions of arithmetic. Trans. Am. Math. Soc.254, 47–68 (1979) · Zbl 0417.03030
[4] Guaspari, D., Solovay, R.M.: Rosser sentences. Ann. Math. Logic16, 81–99 (1979) · Zbl 0426.03062
[5] Hájek, P.: On interpretability in set theories. I, II. Commentat.Math. Univ. Carol.12, 73–79 (1971);13, 445–455 (1972) · Zbl 0231.02087
[6] Hájek, P.: On interpretability in theories containing arithmetic. II.Commentat.Math. Univ. Carol.22, 677–688 (1981)
[7] Hájek, P.: Partial conservativity revisited. Commentat. Math. Univ. Carol.28, 679–690 (1987) · Zbl 0679.03025
[8] Hájek, P.: On logic in fragments of arithmetic (manuscript)
[9] Hájek, P., Kučera, A.: On recursion theory inI1. J. Symb. Logic54, 576–589 (1989) · Zbl 0703.03019
[10] Hájek, P., Pudlák, P.: The metamathematics of Peano arithmetic (a book in preparation)
[11] Savrukov, V.Yu.: The logic of relative interpretability over Peano arithmetic (preprint in Russian, Moscow 1988)
[12] Sieg, W.: Fragments of arithmetic. Ann. Pure Appl. Logic28, 33–71 (1985) · Zbl 0558.03029
[13] Smoryński, C.: An ubiquitous fixed point calculation (unpublished, 1981?)
[14] Smoryński, C.: Self-reference and modal logic. Berlin Heidelberg New York: Springer 1985 · Zbl 0596.03001
[15] Solovay, R.M.: Provability interpretations of modal logic. Isr. J. Math.25, 287–304 (1976) · Zbl 0352.02019
[16] Svejdar, V.: Modal analysis of generalized Rosser sentences. J. Symb. Logic48, 986–999 (1983) · Zbl 0543.03010
[17] Visser, A.: Preliminary notes on interpretability logic. Logic Group Preprint Series University of Utrecht No. 29, 1988
[18] Visser, A.: Interpretability logic. Logic Group Preprint Series University of Utrecht 1988
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.