{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T09:39:27Z","timestamp":1776850767575,"version":"3.51.2"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005774","name":"Universitat de Barcelona","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005774","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2026,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We determine the strictly positive fragment\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{QPL}^+(\\textsf{HA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:msup>\n                              <mml:mi>QPL<\/mml:mi>\n                              <mml:mo>+<\/mml:mo>\n                            <\/mml:msup>\n                            <mml:mrow>\n                              <mml:mo>(<\/mml:mo>\n                              <mml:mi>HA<\/mml:mi>\n                              <mml:mo>)<\/mml:mo>\n                            <\/mml:mrow>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    of the quantified provability logic\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{QPL}(\\textsf{HA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>QPL<\/mml:mi>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mi>HA<\/mml:mi>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    of Heyting Arithmetic. We show that\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{QPL}^+(\\textsf{HA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:msup>\n                              <mml:mi>QPL<\/mml:mi>\n                              <mml:mo>+<\/mml:mo>\n                            <\/mml:msup>\n                            <mml:mrow>\n                              <mml:mo>(<\/mml:mo>\n                              <mml:mi>HA<\/mml:mi>\n                              <mml:mo>)<\/mml:mo>\n                            <\/mml:mrow>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is decidable and that it coincides with\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{QPL}^+(\\textsf{PA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:msup>\n                              <mml:mi>QPL<\/mml:mi>\n                              <mml:mo>+<\/mml:mo>\n                            <\/mml:msup>\n                            <mml:mrow>\n                              <mml:mo>(<\/mml:mo>\n                              <mml:mi>PA<\/mml:mi>\n                              <mml:mo>)<\/mml:mo>\n                            <\/mml:mrow>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , which is the strictly positive fragment of the quantified provability logic of of Peano Arithmetic. This positively resolves a previous conjecture of the authors described in [14]. On our way to proving these results, we carve out the strictly positive fragment\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{PL}^+(\\textsf{HA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:msup>\n                              <mml:mi>PL<\/mml:mi>\n                              <mml:mo>+<\/mml:mo>\n                            <\/mml:msup>\n                            <mml:mrow>\n                              <mml:mo>(<\/mml:mo>\n                              <mml:mi>HA<\/mml:mi>\n                              <mml:mo>)<\/mml:mo>\n                            <\/mml:mrow>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    of the provability logic\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{PL}(\\textsf{HA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>PL<\/mml:mi>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mi>HA<\/mml:mi>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    of Heyting Arithmetic, provide a simple axiomatization, and prove it to be sound and complete for two types of arithmetical interpretations. The simple fragments presented in this paper should be contrasted with a recent result by Mojtahedi [43], where an axiomatization for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{PL}(\\textsf{HA})$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>PL<\/mml:mi>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mi>HA<\/mml:mi>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is provided. This axiomatization, although decidable, is of considerable complexity.\n                  <\/jats:p>","DOI":"10.1007\/s11225-024-10152-y","type":"journal-article","created":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T12:17:46Z","timestamp":1730290666000},"page":"263-295","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic"],"prefix":"10.1007","volume":"114","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5152-198X","authenticated-orcid":false,"given":"Ana","family":"de Almeida Borges","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost J.","family":"Joosten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,30]]},"reference":[{"issue":"3","key":"10152_CR1","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.2307\/2274475","volume":"55","author":"SN Artemov","year":"1990","unstructured":"Artemov, S.N., and G. K. Japaridze, Finite Kripke models and predicate logics of provability, Journal of Symbolic Logic 55(3):1090\u20131098, 1990.","journal-title":"Journal of Symbolic Logic"},{"key":"10152_CR2","unstructured":"Artemov, S.N., Nonarithmeticity of truth predicate logics of provability, Doklady Akademii Nauk SSSR 284(2):270\u2013271, 1985, in Russian, English translation in Soviet Mathematics Doklady 33:403\u2013405, 1985."},{"issue":"6","key":"10152_CR3","first-page":"1289","volume":"290","author":"SN Artemov","year":"1986","unstructured":"Artemov, S.N., Numerically correct logics of provability. Doklady Akademii Nauk SSSR 290(6):1289\u20131292, 1986. In Russian.","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"10152_CR4","unstructured":"Artemov, S.N., and L.D. Beklemishev, Provability logic, in D. Gabbay, and F. Guenthner, (eds.), Handbook of Philosophical Logic vol. 13, 2nd edn., Springer, Dordrecht, Netherlands, 2004, pp. 229\u2013403."},{"key":"10152_CR5","unstructured":"Beklemishev, L.D., Veblen hierarchy in the context of provability algebras, provability, in Russian, in P. H\u00e1jek, L. Vald\u00e9s-Villanueva, and D. Westerst\u00e5hl, (eds.), Logic, Methodology and Philosophy of Science, Proceedings of the Twelfth International Congress, Kings College Publications, Oviedo, Spain, 2004, pp. 65\u201378."},{"key":"10152_CR6","doi-asserted-by":"publisher","unstructured":"de Almeida Borges, A., and J.J. Joosten, An escape from Vardanyan\u2019s Theorem, The Journal of Symbolic Logic 88(4):1613\u20131638, 2023 https:\/\/doi.org\/10.1017\/jsl.2022.38.","DOI":"10.1017\/jsl.2022.38"},{"key":"10152_CR7","doi-asserted-by":"crossref","unstructured":"Mojtahedi, M., On Provability Logic of HA. arXiv:2206.00445 [math.LO] 2022.","DOI":"10.1007\/978-3-030-53654-1_9"},{"key":"10152_CR8","volume-title":"The Logic of Provability","author":"GS Boolos","year":"1993","unstructured":"Boolos, G.S., The Logic of Provability, Cambridge University Press, Cambridge, 1993."},{"key":"10152_CR9","unstructured":"Vardanyan, V.A., Arithmetic complexity of predicate logics of provability and their fragments, in Russian, Doklady Akad. Nauk SSSR 288(1):11\u201314, 1986, English translation in Soviet Mathematics Doklady 33:569\u2013572, 1986."},{"key":"10152_CR10","doi-asserted-by":"publisher","first-page":"165","DOI":"10.2307\/2273871","volume":"52","author":"GS Boolos","year":"1987","unstructured":"Boolos, G.S., and V. R. McGee, The degree of the set of sentences of predicate provability logic that are true under every interpretation, The Journal of Symbolic Logic 52:165\u2013171, 1987.","journal-title":"The Journal of Symbolic Logic"},{"key":"10152_CR11","series-title":"Scientific Council of the USSR Academy of Sciences on the complex problem \"Cybernetics\", in Russian","first-page":"46","volume-title":"Questions of Cybernetics: Complexity of Computation and Applied Mathematical Logic","author":"VA Vardanyan","year":"1988","unstructured":"Vardanyan, V.A., Bounds on the arithmetical complexity of predicate logics of provability, in S.N. Adyan, (ed.), Questions of Cybernetics: Complexity of Computation and Applied Mathematical Logic, vol. 134 of Scientific Council of the USSR Academy of Sciences on the complex problem \u201cCybernetics\u201d, in Russian, Academy of Sciences of the USSR, Moscow, Russia, 1988, pp. 46\u201372."},{"key":"10152_CR12","unstructured":"Berarducci, A., $${\\Sigma }^0_n$$-interpretations of modal logic, Bollettino dell\u2019Unione Matematica Italiana 7(3-A):177\u2013184, 1989."},{"issue":"5","key":"10152_CR13","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/s00153-006-0328-0","volume":"45","author":"A Visser","year":"2006","unstructured":"Visser, A., and M. Jonge, No escape from Vardanyan\u2019s theorem, Archive for Mathematical Logic 45(5):539\u2013554, 2006.","journal-title":"Archive for Mathematical Logic"},{"key":"10152_CR14","unstructured":"Yavorsky, R.E., On arithmetical completeness of first-order logics of provability, in F. Wolter, H. Wansing, M. de Rijke, and M. Zakharyaschev, (eds.), Advances in Modal Logic 3, World Scientific Publishing Co. Pte. Ltd., Leipzig, Germany, 2002, pp. 1\u201316."},{"issue":"4","key":"10152_CR15","doi-asserted-by":"publisher","first-page":"513","DOI":"10.18778\/0138-0680.2021.18","volume":"50","author":"Y Hao","year":"2021","unstructured":"Hao, Y., and G. Tourlakis, An arithmetically complete predicate modal logic, Bulletin of the Section of Logic 50(4), 513\u2013541, 2021.","journal-title":"Bulletin of the Section of Logic"},{"key":"10152_CR16","first-page":"606","volume":"36","author":"DHJ Jongh","year":"1970","unstructured":"Jongh, D.H.J., The maximality of the intuitionistic predicate calculus with respect to Heyting\u2019s Arithmetic, The Journal of Symbolic Logic 36:606, 1970.","journal-title":"The Journal of Symbolic Logic"},{"key":"10152_CR17","volume-title":"Admissibility of Logical Inference Rules","author":"VV Rybakov","year":"1997","unstructured":"Rybakov, V.V., Admissibility of Logical Inference Rules, Elsevier, Amsterdam, 1997."},{"issue":"1","key":"10152_CR18","doi-asserted-by":"publisher","first-page":"281","DOI":"10.2307\/2694922","volume":"66","author":"R Iemhoff","year":"2001","unstructured":"Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66(1): 281\u2013294, 2001.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"10152_CR19","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1090\/S0002-9939-1973-0432406-2","volume":"39","author":"J Myhill","year":"1973","unstructured":"Myhill, J., A note on indicator functions, Proceedings of the American Mathematical Society 39(1): 181\u2013183, 1973.","journal-title":"Proceedings of the American Mathematical Society"},{"issue":"8","key":"10152_CR20","doi-asserted-by":"publisher","first-page":"2877","DOI":"10.1073\/pnas.72.8.2877","volume":"72","author":"H Friedman","year":"1975","unstructured":"Friedman, H., The disjunction property implies the numerical existence property, Proceedings of the National Academy of Sciences 72(8):2877\u20132878, 1975.","journal-title":"Proceedings of the National Academy of Sciences"},{"key":"10152_CR21","unstructured":"Leivant, D., Absoluteness in Intuitionistic Logic, vol. 73 of Mathematical Centre Tract, Amsterdam, Netherlands, 1979 (the thesis was originally published in 1975)."},{"key":"10152_CR22","unstructured":"Visser, A., Evaluation, provably deductive equivalence in Heyting\u2019s Arithmetic of substitution instances of propositional formulas, Logic Group Preprint Series\u00a04, Faculty of Humanities, Philosophy, Utrecht University, Utrecht, Netherlands, 1985."},{"key":"10152_CR23","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/S0168-0072(01)00081-1","volume":"114","author":"A Visser","year":"2002","unstructured":"Visser, A., Substitutions of $${\\Sigma }^0_1$$-sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic, Annals of Pure and Applied Logic 114:227\u2013271, 2002.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10152_CR24","unstructured":"de Almeida Borges, A., Suitable logics: provability, temporal laws, and formalization, PhD thesis, University of Barcelona, 2023. https:\/\/mat.ub.edu\/pop\/doctorat\/tesis\/Thesis_Ana_Almeida.pdf."},{"key":"10152_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-22156-3","volume-title":"Metamathematics of First Order Arithmetic","author":"P H\u00e1jek","year":"1993","unstructured":"Japaridze, G.K., The polymodal provability logic, in Intensional Logics and Logical Structure of Theories: Material from the Fourth Soviet-Finnish Symposium on Logic, Telavi, May 20\u201324, 1985, in Russian, Metsniereba, Telavi, Georgia, 1988, pp. 16\u201348."},{"key":"10152_CR26","doi-asserted-by":"crossref","unstructured":"Hughes, G.E., and M.J. Cresswell, A New Introduction to Modal Logic, Routledge, London, United Kingdom, 1996.","DOI":"10.4324\/9780203290644"},{"issue":"3","key":"10152_CR27","doi-asserted-by":"publisher","first-page":"428","DOI":"10.2178\/bsl\/1122038996","volume":"11","author":"R Kontchakov","year":"2005","unstructured":"Kontchakov, R., A. Kurucz, and M. Zakharyaschev, Undecidability of first-order intuitionistic and modal logics with two variables, Bulletin of Symbolic Logic 11(3):428\u2013438, 2005.","journal-title":"Bulletin of Symbolic Logic"},{"issue":"4","key":"10152_CR28","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/s11225-018-9815-7","volume":"107","author":"M Rybakov","year":"2019","unstructured":"Rybakov, M., and D. Shkatov, Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter, Studia Logica 107(4):695\u2013967, 2019.","journal-title":"Studia Logica"},{"issue":"3","key":"10152_CR29","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.2307\/2695115","volume":"66","author":"F Wolter","year":"2001","unstructured":"Wolter, F., and M. Zakharyaschev, Decidable fragments of first-order modal logics, The Journal of Symbolic Logic 66(3):1415\u20131438, 2001.","journal-title":"The Journal of Symbolic Logic"},{"key":"10152_CR30","unstructured":"de Almeida Borges, A., and J.J. Joosten, Quantified Reflection Calculus with One Modality, in N. Olivetti, R. Verbrugge, S. Negri, and G. Sandu, (eds.), Advances in Modal Logic 13, College Publications, Helsinki, Finland, 2020, pp. 13\u201332."},{"issue":"3\u20134","key":"10152_CR31","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1134\/S0001434612030029","volume":"91","author":"EV Dashkov","year":"2012","unstructured":"Dashkov, E.V., On the positive fragment of the polymodal provability logic GLP, Mathematical Notes 91(3-4):318\u2013333, 2012.","journal-title":"Mathematical Notes"},{"key":"10152_CR32","unstructured":"Beklemishev, L.D., Calibrating Provability Logic: From Modal Logic to Reflection Calculus, in T. Bolander, T. Bra\u00fcner, T.S. Ghilardi, and L. Moss, (eds.), Advances in Modal Logic 9, College Publications, London, United Kingdom, 2012, pp. 89\u201394."},{"issue":"6","key":"10152_CR33","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1093\/jigpal\/jzu018","volume":"22","author":"D Fern\u00e1ndez-Duque","year":"2014","unstructured":"Fern\u00e1ndez-Duque, D., and J.J. Joosten, Well-orders in the transfinite Japaridze algebra, Logic Journal of the IGPL 22(6):933\u2013963, 2014. https:\/\/doi.org\/10.1093\/jigpal\/jzu018","journal-title":"Logic Journal of the IGPL"},{"key":"10152_CR34","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s11225-013-9490-7","volume":"102","author":"LD Beklemishev","year":"2014","unstructured":"Beklemishev, L.D., D. Fern\u00e1ndez-Duque, and J.J. Joosten, On provability logics with linearly ordered modalities, Studia Logica 102:541\u2013566, 2014. https:\/\/doi.org\/10.1007\/s11225-013-9490-7","journal-title":"Studia Logica"},{"issue":"3","key":"10152_CR35","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"RE Ladner","year":"1977","unstructured":"Ladner, R.E., The computational complexity of provability in systems of modal propositional logic, SIAM Journal on Computing 6(3):467\u2013480, 1977.","journal-title":"SIAM Journal on Computing"},{"key":"10152_CR36","doi-asserted-by":"crossref","unstructured":"Beklemishev, L.D., A note on strictly positive logics and word rewriting systems, in S. Odintsov, (ed.), Larisa Maximova on Implication, Interpolation, and Definability, vol. 15 of Outstanding Contributions to Logic, Springer, Berlin, 2018, pp. 61\u201370.","DOI":"10.1007\/978-3-319-69917-2_4"},{"key":"10152_CR37","unstructured":"Beklemishev, L.D., Strictly positive provability logics: Recent progress and open questions, Moscow, Russia, 2021. http:\/\/yongcheng.whu.edu.cn\/webPageContent\/Goedel2021\/ Goedel-Lev.pdf"},{"key":"10152_CR38","unstructured":"Gabbay, D.M., A. Kurucz, F. Wolter, and M. Zakharyaschev, Many-dimensional Modal Logics: Theory and Applications, Elsevier North Holland, Boston, 2003."},{"key":"10152_CR39","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s11225-005-3702-8","volume":"81","author":"T Litak","year":"2005","unstructured":"Litak, T. and F. Wolter, All finitely axiomatizable tense logics of linear time flows are coNP-complete. Studia Logica 81:153\u2013165, 2005. https:\/\/doi.org\/10.1007\/s11225-005-3702-8","journal-title":"Studia Logica"},{"key":"10152_CR40","doi-asserted-by":"publisher","first-page":"952","DOI":"10.1134\/S0001434618050322","volume":"103","author":"MV Svyatlovskiy","year":"2018","unstructured":"Svyatlovskiy, M.V., Axiomatization and polynomial solvability of strictly positive fragments of certain modal logics, Mathematical Notes 103:952\u2013967, 2018. https:\/\/doi.org\/10.1134\/S0001434618050322","journal-title":"Mathematical Notes"},{"issue":"7\u20138","key":"10152_CR41","doi-asserted-by":"publisher","first-page":"949","DOI":"10.1007\/s00153-014-0397-4","volume":"53","author":"F Pakhomov","year":"2014","unstructured":"Pakhomov, F., On the complexity of the closed fragment of Japaridze\u2019s provability logic, Archive for Mathematical Logic 53(7-8):949\u2013967, 2014.","journal-title":"Archive for Mathematical Logic"},{"key":"10152_CR42","unstructured":"Shapirovsky, I., PSPACE-decidability of Japaridze\u2019s Polymodal Logic, in C. Areces, and R. Goldblatt, (eds.), Advances in Modal Logic 7, College Publications, Nancy, France, 2008, pp. 289\u2013304."},{"issue":"2","key":"10152_CR43","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1017\/jsl.2019.22","volume":"84","author":"S Kikot","year":"2019","unstructured":"Kikot, S., A. Kurucz, Y. Tanaka, F. Wolter, and M. Zakharyaschev, Kripke completeness of strictly positive modal logics over meet-semilattices with operators, The Journal of Symbolic Logic 84(2):533\u2013588, 2019.","journal-title":"The Journal of Symbolic Logic"},{"key":"10152_CR44","doi-asserted-by":"crossref","unstructured":"Fagin, R., J.Y. Halpern, Y. Moses and Vardi, M.Y., Reasoning About Knowledge, MIT Press, Cambridge, 1995.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"10152_CR45","first-page":"83","volume":"16","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A., Semantical considerations on modal logic, Acta Philosophica Fennica 16:83\u201394, 1963.","journal-title":"Acta Philosophica Fennica"},{"key":"10152_CR46","unstructured":"Gabbay, D.M., V.B. Shehtman, and D.P. Skvortsov, Quantification in Nonclassical Logic, Volume 1, vol. 153 of Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam, Netherlands, 2009."},{"key":"10152_CR47","doi-asserted-by":"crossref","unstructured":"Goldblatt, R., Quantifiers, Propositions and Identity, Admissible Semantics for Quantified Modal and Substructural Logics, Cambridge University Press, New York, 2011.","DOI":"10.1017\/CBO9780511862359"},{"key":"10152_CR48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-22156-3","volume-title":"Metamathematics of First Order Arithmetic","author":"P H\u00e1jek","year":"1993","unstructured":"H\u00e1jek, P., and P. Pudl\u00e1k, Metamathematics of First Order Arithmetic. Springer, Berlin, 1993."},{"key":"10152_CR49","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, vol. 344 of Lecture Notes in Mathematics, Springer, Berlin, 1973.","DOI":"10.1007\/BFb0066739"},{"key":"10152_CR50","first-page":"33","volume":"28","author":"RM Solovay","year":"1976","unstructured":"Solovay, R.M., Provability interpretations of modal logic, Israel Journal of Mathematics 28:33\u201371, 1976.","journal-title":"Israel Journal of Mathematics"},{"key":"10152_CR51","doi-asserted-by":"publisher","first-page":"952","DOI":"10.1134\/S0001434618050322","volume":"103","author":"MV Svyatlovskiy","year":"2018","unstructured":"Jongh, D., M. Jumelet, and F. Montagna, On the proof of Solovay\u2019s theorem, Studia Logica 50:51\u201369, 1991.","journal-title":"Mathematical Notes"},{"key":"10152_CR52","doi-asserted-by":"crossref","unstructured":"Kurahashi, T., On predicate provability logics and binumerations of fragments of Peano Arithmetic. Arithmetic, Archive for Mathematical Logic 52:871\u2013880, 2013.","DOI":"10.1007\/s00153-013-0349-4"},{"key":"10152_CR53","doi-asserted-by":"publisher","unstructured":"Kurahashi, T., On inclusions between quantified provability logics, Studia Logica 110:165\u2013188, 2022 https:\/\/doi.org\/10.1007\/s11225-021-09957-y.","DOI":"10.1007\/s11225-021-09957-y"},{"key":"10152_CR54","doi-asserted-by":"crossref","unstructured":"Montagna, F., The predicate modal logic of provability, Notre Dame Journal of Formal Logic 25(2):179\u2013189, 1984.","DOI":"10.1305\/ndjfl\/1093870577"},{"key":"10152_CR55","unstructured":"McGee, V.R., Truth and necessity in partially interpreted languages, PhD thesis, University of California, Berkeley, 1985."},{"key":"10152_CR56","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/S0168-0072(01)00081-1","volume":"114","author":"A Visser","year":"2002","unstructured":"Fujiwara, M., and T. Kurahashi, Prenex normalization and the hierarchical classification of formulas. arXiv:2302.11808 [math.LO] 2023.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"5","key":"10152_CR57","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/s00153-006-0328-0","volume":"45","author":"A Visser","year":"2006","unstructured":"Friedman, H., Classically and intuitionistically provably recursive functions, in D.S. Scott, and G.H. M\u00fcller, (eds.), Higher Set Theory, vol. 699 of Lecture Notes in Mathematics, Springer, Oberwolfach, Germany, 1978, pp. 21\u201328.","journal-title":"Archive for Mathematical Logic"},{"issue":"6","key":"10152_CR58","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1016\/j.apal.2019.02.001","volume":"170","author":"A Visser","year":"2019","unstructured":"Kreisel, G., On the interpretation of non-finitist proofs - Part I, The Journal of Symbolic Logic 16(4): 241\u2013267, 1951 https:\/\/doi.org\/10.1017\/S0022481200100581.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"10152_CR59","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.2307\/2695115","volume":"66","author":"F Wolter","year":"2001","unstructured":"Kuroda, S., Intuitionistische Untersuchungen der formalistischen Logik, Nagoya Mathematical Journal 2:35\u201347, 1951 https:\/\/doi.org\/10.1017\/S0027763000010023.","journal-title":"The Journal of Symbolic Logic"},{"key":"10152_CR60","doi-asserted-by":"crossref","unstructured":"Visser, A., and J. Zoethout, Provability logic and the completeness principle, Annals of Pure and Applied Logic 170(6):718\u2013753, 2019.","DOI":"10.1016\/j.apal.2019.02.001"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-024-10152-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-024-10152-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-024-10152-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T08:40:19Z","timestamp":1776847219000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-024-10152-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,30]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4]]}},"alternative-id":["10152"],"URL":"https:\/\/doi.org\/10.1007\/s11225-024-10152-y","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,30]]},"assertion":[{"value":"12 February 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 October 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}