Reflection calculus and conservativity spectra

L. D. Beklemishev

Trudy Matematicheskogo Instituta imeni V.A. Steklova, Tome 73 (2018) no. 4, pp. 569-613

Résumé

Strictly positive logics have recently attracted attention both in the description logic and in the provability logic communities for their combination of efficiency and sufficient expressivity. The language of Reflection Calculus, $\mathrm{RC}$, consists of implications between formulas built up from propositional variables and the constant ‘true’ using only conjunction and diamond modalities which are interpreted in Peano arithmetic as restricted uniform reflection principles. The language of $\mathrm{RC}$ is extended by another series of modalities representing the operators associating with a given arithmetical theory $T$ its fragment axiomatized by all theorems of $T$ of arithmetical complexity $\Pi^0_n$ for all $n>0$. It is noted that such operators, in a strong sense, cannot be represented in the full language of modal logic. A formal system $\mathrm{RC}^\nabla$ is formulated that extends $\mathrm{RC}$ and is sound and (it is conjectured) complete under this interpretation. It is shown that in this system one is able to express the iterations of reflection principles up to any ordinal $\varepsilon_0$. Second, normal forms are provided for its variable-free fragment. This fragment is thereby shown to be algorithmically decidable and complete with respect to its natural arithmetical semantics. In the last part of the paper the Lindenbaum–Tarski algebra of the variable-free fragment of $\mathrm{RC}^\nabla$ and its dual Kripke structure are characterized in several natural ways. Most importantly, elements of this algebra correspond to the sequences of proof-theoretic $\Pi^0_{n+1}$-ordinals of bounded fragments of Peano arithmetic called conservativity spectra, as well as to points of Ignatiev's well-known Kripke model. Bibliography: 46 titles.

Détail

Keywords: strictly positive modal logic, reflection principle, conservativity, ordinal.
Mots-clés : RC

Bibliographie

[1] L. Beklemishev, “Iterated local reflection versus iterated consistency”, Ann. Pure Appl. Logic, 75:1-2 (1995), 25–48 | DOI | MR | Zbl

[2] L. D. Beklemishev, “Proof-theoretic analysis by iterated reflection”, Arch. Math. Logic, 42:6 (2003), 515–552 | DOI | MR | Zbl

[3] L. D. Beklemishev, “Provability algebras and proof-theoretic ordinals. I”, Ann. Pure Appl. Logic, 128:1-3 (2004), 103–123 | DOI | MR | Zbl

[4] L. D. Beklemishev, “Reflection principles and provability algebras in formal arithmetic”, Russian Math. Surveys, 60:2 (2005), 197–268 | DOI | DOI | MR | Zbl

[5] L. D. Beklemishev, “The Worm principle”, Logic colloquium{' }02 (Münster, Germany, August 3–11, 2002), Lect. Notes Log., 27, Assoc. Symbol. Logic, La Jolla, CA, 2006, 75–95 ; Preprint, Logic Group Preprint Series, 219, Utrecht Univ., Utrecht, 2003, 23 pp. https://dspace.library.uu.nl/handle/1874/27024 | MR | Zbl

[6] L. Beklemishev, “Calibrating provability logic: from modal logic to reflection calculus”, Advances in Modal Logic, Copenhagen, 2012, v. 9, Coll. Publ., London, 2012, 89–94 | MR | Zbl

[7] L. Beklemishev, “Positive provability logic for uniform reflection principles”, Ann. Pure Appl. Logic, 165:1 (2014), 82–105 | DOI | MR | Zbl

[8] L. D. Beklemishev, “Proof theoretic analysis by iterated reflection”, Turing's revolution, Birkhäuser/Springer, Cham, 2015, 225–270 | DOI | MR | Zbl

[9] L. D. Beklemishev, “On the reflection calculus with partial conservativity operators”, Logic, language, information, and computation, Lecture Notes in Comput. Sci., 10388, Springer, Berlin, 2017, 48–67 | DOI | MR | Zbl

[10] L. D. Beklemishev, “On the reduction property for GLP-algebras”, Dokl. Math., 95:1 (2017), 50–54 | DOI | DOI | MR | Zbl

[11] L. D. Beklemishev, “A note on strictly positive logics and word rewriting systems”, Larisa Maximova on implication, interpolation, and definability, Outstanding Contributions to Logic, 15, Springer, Cham, 2018, 61–70 | DOI

[12] L. D. Beklemishev, “A universal algebra for the variable-free fragment of $\mathrm{RC}^\nabla$”, Logical Foundations of Computer Science, Lecture Notes in Comput. Sci., 10703, Springer, Cham, 2018, 91–106 | DOI | MR | Zbl

[13] L. D. Beklemishev, A universal Kripke frame for the variable-free fragment of $\mathrm{RC}^\nabla$, 2018, 5 pp., arXiv: 1804.02641

[14] L. D. Beklemishev, D. Fernández-Duque, J. J. Joosten, “On provability logics with linearly ordered modalities”, Studia Logica, 102:3 (2014), 541–566 ; (2012), 28 pp., arXiv: 1210.4809 | DOI | MR | Zbl

[15] L. D. Beklemishev, J. J. Joosten, M. Vervoort, “A finitary treatment of the closed fragment of Japaridze's provability logic”, J. Logic Comput., 15:4 (2005), 447–463 | DOI | MR | Zbl

[16] L. D. Beklemishev, A. A. Onoprienko, “On some slowly terminating term rewriting systems”, Sb. Math., 206:9 (2015), 1173–1190 | DOI | DOI | MR | Zbl

[17] G. Boolos, The logic of provability, Cambridge Univ. Press, Cambridge, 1993, xxxvi+276 pp. | MR | Zbl

[18] A. Chagrov, M. Zakharyaschev, Modal logic, Oxford Logic Guides, 35, Oxford Univ. Press, New York, 1997, xvi+605 pp. | MR | Zbl

[19] E. V. Dashkov, “On the positive fragment of the polymodal provability logic $\mathrm{GLP}$”, Math. Notes, 91:3 (2012), 318–333 | DOI | DOI | MR | Zbl

[20] A. de Almeida Borges, J. J. Joosten, The Worm calculus, 2018, 19 pp., arXiv: 1803.10543v1

[21] G. Japaridze, D. de Jongh, “The logic of provability”, Handbook of Proof Theory, Stud. Logic Found. Math., 137, North-Holland, Amsterdam, 1998, 475–546 | DOI | MR | Zbl

[22] S. Feferman, “Arithmetization of metamathematics in a general setting”, Fund. Math., 49 (1960), 35–92 | DOI | MR | Zbl

[23] S. Feferman, “Transfinite recursive progressions of axiomatic theories”, J. Symbolic Logic, 27:3 (1962), 259–316 | DOI | MR | Zbl

[24] D. Fernández-Duque, J. J. Joosten, “Models of transfinite provability logic”, J. Symbolic Logic, 78:2 (2013), 543–561 | DOI | MR | Zbl

[25] E. Goris, J. J. Joosten, “A new principle in the interpretability logic of all reasonable arithmetical theories”, Log. J. IGPL, 19:1 (2011), 14–17 | DOI | MR | Zbl

[26] P. Hájek, F. Montagna, “The logic of $\Pi_1$-conservativity”, Arch. Math. Logic, 30:2 (1990), 113–123 | DOI | MR | Zbl

[27] P. Hájek, F. Montagna, “The logic of $\Pi_1$-conservativity continued”, Arch. Math. Logic, 32:1 (1992), 57–63 | DOI | MR | Zbl

[28] P. Hájek, P. Pudlák, Metamathematics of first-order arithmetic, Perspect. Math. Logic, Springer-Verlag, Berlin, 1993, xiv+460 pp. | MR | Zbl

[29] E. Hermo Reyes, J. J. Joosten, The logic of Turing progressions, 2017 (v1 – 2016), 33 pp., arXiv: 1604.08705v2

[30] E. Hermo Reyes, J. J. Joosten, Relational semantics for the Turing Schmerl calculus, 2018 (v1 – 2017), 17 pp., arXiv: 1709.04715

[31] T. Icard, “A topological study of the closed fragment of GLP”, J. Logic Comput., 21:4 (2011), 683–696 | DOI | MR | Zbl

[32] K. N. Ignatiev, Partial conservativity and modal logics, Preprint X-91-04, ITLI Prepublication Series, Institute for Language, Logic, and Information, Univ. of Amsterdam, Amsterdam, 1991, 43 pp. https://eprints.illc.uva.nl/id/eprint/597

[33] K. N. Ignatiev, “On strong provability predicates and the associated modal logics”, J. Symbolic Logic, 58:1 (1993), 249–290 | DOI | MR | Zbl

[34] M. Jackson, “Semilattices with closure”, Algebra Universalis, 52:1 (2004), 1–37 | DOI | MR | Zbl

[35] G. K. Dzhaparidze, Modalno-logicheskie sredstva issledovaniya dokazuemosti, Diss. ... kand. filos. nauk, MGU, M., 1986, 177 pp.

[36] J. J. Joosten, “Turing–Taylor expansions of arithmetical theories”, Studia Logica, 104:6 (2016), 1225–1243 | DOI | MR | Zbl

[37] S. Kikot, A. Kurucz, Y. Tanaka, F. Wolter, M. Zakharyaschev, “On the completeness of $\mathrm{EL}$-equiations: first results”, Advances in modal logic, Short papers (Budapest, 2016), v. 11, Coll. Publ., London, 2016, 82–87

[38] S. Kikot, A. Kurucz, Y. Tanaka, F. Wolter, M. Zakharyaschev, Kripke completeness of strictly positive modal logics over meet-semilattices with operators, 2017, 54 pp., arXiv: 1708.03403

[39] G. Kreisel, A. Lévy, “Reflection principles and their use for establishing the complexity of axiomatic systems”, Z. Math. Logik Grundlagen Math., 14 (1968), 97–142 | DOI | MR | Zbl

[40] F. Pakhomov, “On the complexity of the closed fragment of Japaridze's provability logic”, Arch. Math. Logic, 53:7-8 (2014), 949–967 | DOI | MR | Zbl

[41] F. N. Pakhomov, “On elementary theories of ordinal notation systems based on reflection principles”, Proc. Steklov Inst. Math., 289 (2015), 194–212 | DOI | DOI | MR | Zbl

[42] I. Shapirovsky, “PSPACE-decidability of Japaridze's polymodal logic”, Advances in modal logic (Nancy, 2008), v. 7, Coll. Publ., London, 2008, 289–304 | MR | Zbl

[43] C. Smoryński, Self-reference and modal logic, Universitext, Springer-Verlag, Berlin, 1985, xii+333 pp. | DOI | MR | Zbl

[44] A. M. Turing, “System of logic based on ordinals”, Proc. London Math. Soc. (2), 45:3 (1939), 161–228 | DOI | MR | Zbl

[45] A. Visser, “An overview of interpretability logic”, Advances in modal logic (Berlin, 1996), v. 1, CSLI Lecture Notes, 87, CSLI Publ., Stanford, CA, 1998, 307–359 | MR | Zbl

[46] A. Visser, An overview of interpretability logic, Preprint, Logic Group Preprint Series, 174, Utrecht Univ., Utrecht, 2008, 23\;pp. https://dspace.library.uu.nl/handle/1874/26867