# 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

##### MSC:
 03B45 Modal logic (including the logic of norms)
Full Text:
##### References:
  Berarducci, A.: The interpretability logic of Peano arithmetic. Thesis, University of California at Berkeley 1989 (to appear as an article J. Symb. Logic)  de Jongh, D., Veltman, F.: Provability logics for relative interpretability. In: Proceedings of Heyting ’88 (Bulgaria) (to appear) · Zbl 0794.03026  Guaspari, D.: Partially conservative extensions of arithmetic. Trans. Am. Math. Soc.254, 47–68 (1979) · Zbl 0417.03030  Guaspari, D., Solovay, R.M.: Rosser sentences. Ann. Math. Logic16, 81–99 (1979) · Zbl 0426.03062  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  Hájek, P.: On interpretability in theories containing arithmetic. II.Commentat.Math. Univ. Carol.22, 677–688 (1981)  Hájek, P.: Partial conservativity revisited. Commentat. Math. Univ. Carol.28, 679–690 (1987) · Zbl 0679.03025  Hájek, P.: On logic in fragments of arithmetic (manuscript)  Hájek, P., Kučera, A.: On recursion theory inI1. J. Symb. Logic54, 576–589 (1989) · Zbl 0703.03019  Hájek, P., Pudlák, P.: The metamathematics of Peano arithmetic (a book in preparation)  Savrukov, V.Yu.: The logic of relative interpretability over Peano arithmetic (preprint in Russian, Moscow 1988)  Sieg, W.: Fragments of arithmetic. Ann. Pure Appl. Logic28, 33–71 (1985) · Zbl 0558.03029  Smoryński, C.: An ubiquitous fixed point calculation (unpublished, 1981?)  Smoryński, C.: Self-reference and modal logic. Berlin Heidelberg New York: Springer 1985 · Zbl 0596.03001  Solovay, R.M.: Provability interpretations of modal logic. Isr. J. Math.25, 287–304 (1976) · Zbl 0352.02019  Svejdar, V.: Modal analysis of generalized Rosser sentences. J. Symb. Logic48, 986–999 (1983) · Zbl 0543.03010  Visser, A.: Preliminary notes on interpretability logic. Logic Group Preprint Series University of Utrecht No. 29, 1988  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.