Hostname: page-component-54dcc4c588-ff9ft Total loading time: 0 Render date: 2025-10-08T09:09:42.527Z Has data issue: false hasContentIssue false
  • English
  • Français

MODULAR SEQUENT CALCULI FOR INTERPRETABILITY LOGICS

Part of: Proof theory and constructive mathematics General logic

Published online by Cambridge University Press:  08 August 2025

COSIMO PERINI BROGI ,
SARA NEGRI  and
NICOLA OLIVETTI
COSIMO PERINI BROGI*
Affiliation:
IMT SCHOOL FOR ADVANCED STUDIES LUCCA PIAZZA S.FRANCESCO, 19, 55100 LUCCA LU, ITALY
SARA NEGRI
Affiliation:
UNIVERSITY OF GENOA VIA BALBI, 5, 16126 GENOVA GE, ITALY E-mail: sara.negri@unige.it
NICOLA OLIVETTI
Affiliation:
AIX-MARSEILLE UNIVERSITY JARDIN DU PHARO, 58 BOULEVARD CHARLES LIVON 13007 MARSEILLE, FRANCE E-mail: nicola.olivetti@univ-amu.fr
*
E-mail: cosimo.perinibrogi@imtlucca.it
Get access Rights & Permissions [Opens in a new window]

Abstract

An original family of labelled sequent calculi $\mathsf {G3IL}^{\star }$ for classical interpretability logics is presented, modularly designed on the basis of Verbrugge semantics (a.k.a. generalised Veltman semantics) for those logics. We prove that each of our calculi enjoys excellent structural properties, namely, admissibility of weakening, contraction and, more relevantly, cut. A complexity measure of the cut is defined by extending the notion of range previously introduced by Negri w.r.t. a labelled sequent calculus for Gödel–Löb provability logic, and a cut-elimination algorithm is discussed in detail. To our knowledge, this is the most extensive and structurally well-behaving class of analytic proof systems for modal logics of interpretability currently available in the literature.

Keywords

interpretability logicsstructural proof theorycut-eliminationVerbrugge semanticsmodal logics for metamathematics

MSC classification

Primary: 03F05: Cut-elimination and normal-form theorems 03F07: Structure of proofs 03F45: Provability logics and related algebras (e.g., diagonalizable algebras)
Secondary: 03B45: Modal logic (including the logic of norms) 03F25: Relative consistency and interpretations

Information

Type
Research Article
Information
The Review of Symbolic Logic , Volume 18 , Issue 3 , September 2025 , pp. 704 - 743
Check for updates
Copyright
© The Author(s), 2025. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

BIBLIOGRAPHY

Areces, C., Hoogland, E., & de Jongh, D. (2000). Interpolation, definability and fixed points in interpretability logics. In Zakharyaschev, M., Segerberg, K., de Rijke, M., and Wansing, H., editors. Advances in Modal Logic, Vol. 2. Stanford, California: CSLI Publications, pp. 53–76.Google Scholar
Berarducci, A. (1990). The interpretability logic of Peano arithmetic. The Journal of Symbolic Logic, 55(3), 1059–1089.CrossRefGoogle Scholar
Bilkova, M., Goris, E., & Joosten, J. J. (2004). Smart Labels. Liber Amicorum for Dick de Jongh. Amsterdam, NL: Institute for Logic, Language and Computation.Google Scholar
Bilotta, A., Maggesi, M., Perini Brogi, C., & Quartini, L. (2024). Growing HOLMS, a HOL light library for modal systems. In Porello, D., Vinci, C., and Zavatteri, M., editors. Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2024, Bolzano, Italy, November 28-29, 2024, volume 3904 of CEUR Workshop Proceedings, Aachen, DE, pp. 41–48. CEUR-WS.org.Google Scholar
Boolos, G. (1995). The Logic of Provability. New York, USA: Cambridge University Press.Google Scholar
Bou, F., & Joosten, J. J. (2011). The closed fragment of IL is PSPACE hard. Electronic Notes in Theoretical Computer Science, 278, 47–54.CrossRefGoogle Scholar
de Jongh, D., & Veltman, F. (1990). Provability logics for relative interpretability. In Petkov, P. P., editor. Mathematical Logic. Boston, MA: Springer US, pp. 31–42.CrossRefGoogle Scholar
de Jongh, D., & Veltman, F. (1999). Modal completeness of ILW. In Gerbrandy, D., Marx, M. J., de Rijke, M., and Venema, Y., editors, Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday. Amsterdam: Amsterdam University Press.Google Scholar
Girlando, M., Negri, S., & Olivetti, N. (2021). Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics. Journal of Logic and Computation, 31(3), 947–997.CrossRefGoogle Scholar
Girlando, M., Negri, S., Olivetti, N., & Risch, V. (2018). Conditional beliefs: from neighbourhood semantics to sequent calculus. The Review of Symbolic Logic, 11(4), 736–779.CrossRefGoogle Scholar
Goris, E., Bílková, M., Joosten, J. J., & Mikec, L. (2020). Assuring and critical labels for relations between maximal consistent sets for interpretability logics. arXiv preprint, arXiv:2003.04623.Google Scholar
Goris, E., & Joosten, J. (2008). Modal matters for interpretability logics. Logic Journal of the IGPL, 16(4), 371–412.CrossRefGoogle Scholar
Goris, E., & Joosten, J. J. (2020). Two new series of principles in the interpretability logic of all reasonable arithmetical theories. The Journal of Symbolic Logic, 85(1), 1–25.CrossRefGoogle Scholar
Hakli, R., & Negri, S. (2012). Does the deduction theorem fail for modal logic? Synthese, 187(3), 849–867.CrossRefGoogle Scholar
Hakoniemi, T. A., & Joosten, J. J. (2016). Labelled tableaux for interpretability logics. In Liber Amicorum Alberti: A Tribute to Albert Visser (Tributes; No. 30), Rickmansworth UK: College Publications.Google Scholar
Iwata, S., Kurahashi, T., & Okawa, Y. (2024). The fixed point and the Craig interpolation properties for sublogics of IL. Archive for Mathematical Logic, 63(1), 1–37.CrossRefGoogle Scholar
Joosten, J. J., Rovira, J. M., Mikec, L., & Vuković, M. (2024). An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics. In Bezhanishvili, N., Iemhoff, R., and Yang, F., editors. Dick de Jongh on Intuitionistic and Provability Logics. Cham: Springer International Publishing, pp. 111–153.Google Scholar
Joosten, J. J., & Visser, A. (2000). The interpretability logic of all reasonable arithmetical theories. Erkenntnis, 53, 3–26.CrossRefGoogle Scholar
Kurahashi, T., & Okawa, Y. (2021). Modal completeness of sublogics of the interpretability logic IL. Mathematical Logic Quarterly, 67(2), 164–185.CrossRefGoogle Scholar
Maggesi, M., & Perini Brogi, C. (2021). A formal proof of modal completeness for provability logic. In Cohen, L., and Kaliszyk, C., editors. 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl: Schloss Dagstuhl—Leibniz-Zentrum für Informatik, pp. 26:1–26:18.Google Scholar
Maggesi, M., & Perini Brogi, C. (2023). Mechanising Gödel-Löb provability logic in HOL light. Journal of Automated Reasoning, 67(3), 29.CrossRefGoogle Scholar
Mikec, L. (2022). Complexity of the interpretability logics ILW and ILP. Logic Journal of the IGPL, 31(1), 194–213.CrossRefGoogle Scholar
Mikec, L., Joosten, J. J., & Vuković, M. (2020a). A W-flavoured series of interpretability principles. In Short Papers, Advances in Modal Logic, AiML 2020, pp. 60–64.Google Scholar
Mikec, L., Joosten, J. J., & Vuković, M. (2020b). On ILWR-frames. Logic and Applications LAP 2020, 50.Google Scholar
Mikec, L., Pakhomov, F., & Vuković, M. (2019). Complexity of the interpretability logic IL. Logic Journal of the IGPL, 27(1), 1–7.Google Scholar
Mikec, L., Perkov, T., & Vuković, M. (2017). Decidability of interpretability logics $IL{M}_0$ and $IL{W}^{\ast }$ . Logic Journal of the IGPL, 25(5), 758–772.CrossRefGoogle Scholar
Mikec, L., & Vuković, M. (2020). Interpretability logics and generalised Veltman semantics. The Journal of Symbolic Logic, 85(2), 749–772.CrossRefGoogle Scholar
Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34(5), 507–544.CrossRefGoogle Scholar
Negri, S. (2014a). Proof analysis beyond geometric theories: From rule systems to systems of rules. Journal of Logic and Computation, 26(2), 513–537.CrossRefGoogle Scholar
Negri, S. (2014b). Proofs and countermodels in non-classical logics. Logica Universalis, 8(1), 25–60.CrossRefGoogle Scholar
Negri, S. (2017). Proof theory for non-normal modal logics: The neighbourhood formalism and basic results. IfCoLog Journal of Logics and their Applications, 4(4), 1241–1286.Google Scholar
Negri, S., & von Plato, J. (2008). Structural Proof Theory. Cambridge, UK: Cambridge University Press.Google Scholar
Negri, S., & von Plato, J. (2011). Proof Analysis: A Contribution to Hilbert’s Last Problem. Cambridge, UK: Cambridge University Press.CrossRefGoogle Scholar
Okawa, Y. (2024). Unary interpretability logics for sublogics of the interpretability logic IL. Studia Logica, 112(3), 693–721.CrossRefGoogle Scholar
Perini Brogi, C. (2022). Investigations of proof theory and automated reasoning for non-classical logics. PhD thesis, University of Genoa.Google Scholar
Perini Brogi, C., De Nicola, R., & Inverso, O. (2024). Simpson’s proof systems for process verification: A fine-tuning (short paper). In de’Liguoro, U., Palazzo, M., and Roversi, L., editors. Proceedings of the 25th Italian Conference on Theoretical Computer Science, Torino, Italy, September 11-13, 2024, volume 3811 of CEUR Workshop Proceedings, Aachen, DE, pp. 292–299. CEUR-WS.org.Google Scholar
Perkov, T., & Vuković, M. (2016). Filtrations of generalized Veltman models. Mathematical Logic Quarterly, 62(4–5), 412–419.CrossRefGoogle Scholar
Rovira, J. M., Mikec, L., & Joosten, J. J. (2020). Generalised veltman semantics in agda. In Short Papers, Advances in Modal Logic, AiML 2020, pp. 86–90.Google Scholar
Sasaki, K. (2002). A cut-free sequent system for the smallest interpretability logic. Studia Logica, 70(3), 353–372.CrossRefGoogle Scholar
Shavrukov, V. Y. (1988). The logic of relative interpretability over Peano arithmetic. Preprint, Steklov Mathematical Institute, Moscow.Google Scholar
Shavrukov, V. Y. (1997). Interpreting reflexive theories in finitely many axioms. Fundamenta Mathematicae, 152(2), 99–116.Google Scholar
Smorynski, C. (1977). The Incompleteness Theorems, Studies in Logic and the Foundations of Mathematics, 90, Amsterdam, NL: Elsevier, pp. 821–865.Google Scholar
Smorynski, C. (2012). Self-Reference and Modal Logic. New York, USA: Springer Science & Business Media.Google Scholar
Smullyan, R. M. (1968). Analytic cut. The Journal of Symbolic Logic, 33(4), 560–564.CrossRefGoogle Scholar
Solovay, R. M. (1976). Provability interpretations of modal logic. Israel Journal of mathematics, 25(3–4), 287–304.CrossRefGoogle Scholar
Švejdar, V. (1991). Some independence results in interpretability logic. Studia Logica, 50(1), 29–38.CrossRefGoogle Scholar
Tarski, A. (1933). The concept of truth in formalized languages. In Corcoran, J., editor (1983). Logic, Semantics, Metamathematics: papers from 1923 to 1938. United Kingdom: Hackett Publishing Company, pp. 152–278.Google Scholar
Tarski, A., Mostowski, A., & Robinson, R. M. (1953). Undecidable Theories, Vol. 13. Amsterdam, NL: Elsevier.Google Scholar
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic Proof Theory, 43. Cambridge, UK: Cambridge University Press.CrossRefGoogle Scholar
Verbrugge, L. (1992). Verzamelingen-Veltman frames en modellen (set Veltman frames and models). Unpublished manuscript.Google Scholar
Verbrugge, R. L. (2017). Provability logic. In Zalta, E. N., editor. The Stanford Encyclopedia of Philosophy. Stanford, California: Metaphysics Research Lab, Stanford University. fall 2017 edition.Google Scholar
Vickers, S. (2014). Continuity and geometric logic. Journal of Applied Logic, 12(1), 14–27.CrossRefGoogle Scholar
Visser, A. (1988). Preliminary notes on interpretability logic. Logic group preprint series, 29, Department of Philosophy, University of Utrecht, Utrecht NL.Google Scholar
Visser, A. (1990). Interpretability logic. In Petkov, P.P. editor, Mathematical Logic. (pp. 175–209). Boston, MA: Springer US.Google Scholar
Visser, A. (1997). An overview of interpretability logic. Logic Group Preprint Series, 174, Department of Philosophy, University of Utrecht, Utrecht NL.Google Scholar
Vuković, M. (1999). The principles of interpretability. Notre Dame Journal of Formal Logic, 40(2), 227–235.CrossRefGoogle Scholar
Zambella, D. (1992). On the proofs of arithmetical completeness for interpretability logic. Notre Dame Journal of Formal Logic, 33(4), 542–551.CrossRefGoogle Scholar