Document Open Access Logo

Exponential Lower Bounds on Definable Fixed Points

Authors Konstantinos Papafilippou , David Fernández-Duque

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.25.pdf
  • Filesize: 0.89 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Complexity theory and logic
Keywords
  • Modal logic
  • Provability Logic
  • Fixed-Point Theorem
  • mu-calculus
  • Interpolation
  • Succinctness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

It is known that the μ-calculus is no more expressive than basic modal logic over the class of finite partial orders, as well as over the class of finite, strict partial orders. Nevertheless, we show that the μ-calculus is exponentially more succinct, even when a reflexive modality is added as primitive. As corollaries, we obtain a lower bound for the fixed-point theorem for Gödel-Löb logic and a variant for Grzegorczyk logic, as well as lower bounds on interpolants for the interpolation theorem of Gödel-Löb logic.

Cite As Get BibTex

Konstantinos Papafilippou and David Fernández-Duque. Exponential Lower Bounds on Definable Fixed Points. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.25

Author Details

Konstantinos Papafilippou
  • Department of Mathematics, University of Ghent, Belgium
David Fernández-Duque
  • Department of Philosophy, University of Barcelona, Spain

Funding

This work has been partially supported by FWO-FWF grant G030620N/I4513N and SNSF-FWO Lead Agency Grant 200021L_196176/G0E2121N.

References

  1. M. Adler and N. Immerman. An n! lower bound on formula size. ACM Transactions on Computational Logic, 4(3):296-314, 2003. URL: https://doi.org/10.1145/772062.772064.
  2. Gaëlle Fontaine Balder ten Cate and Tadeusz Litak. Some modal aspects of xpath. Journal of Applied Non-Classical Logics, 20(3):139-171, 2010. URL: https://doi.org/10.3166/JANCL.20.139-171.
  3. Claudio Bernardi. The fixed-point theorem for diagonalizable algebras. Studia Logica, 34(3):239-251, 1975. URL: https://doi.org/10.1007/bf02125226.
  4. Claudio Bernardi. The uniqueness of the fixed-point in every diagonalizable algebra. Studia Logica, 35(4):335-343, 1976. URL: https://doi.org/10.1007/bf02123401.
  5. E.W. Beth. On padoa’s method in the theory of definition. Indagationes Mathematicae (Proceedings), 56:330-339, 1953. URL: https://doi.org/10.1016/S1385-7258(53)50042-3.
  6. A. Blass. Infinitary combinatorics and modal logic. Journal of Symbolic Logic, 55(2):761-778, 1990. URL: https://doi.org/10.2307/2274663.
  7. G. S. Boolos. The Logic of Provability. Cambridge University Press, 1993. Google Scholar
  8. A. Chagrov and M. Zakharyaschev. Modal Logic, volume 35 of Oxford logic guides. Oxford University Press, 1997. Google Scholar
  9. A. Dawar and M. Otto. Modal characterisation theorems over special classes of frames. Annals of Pure and Applied Logic, 161:1-42, 2009. URL: https://doi.org/10.1016/J.APAL.2009.04.002.
  10. K. Eickmeyer, M. Elberfeld, and F. Harwath. Expressivity and succinctness of order-invariant logics on depth-bounded structures. In Proceedings of MFCS 2014, pages 256-266, 2014. Google Scholar
  11. David Fernández-Duque and Petar Iliev. Succinctness in subsystems of the spatial μ-calculus. FLAP, 5(4):827-874, 2018. URL: https://www.collegepublications.co.uk/downloads/ifcolog00024.pdf.
  12. David Fernández-Duque and Konstnatinos Papafilippou. The universal tangle for spatial reasoning. In Sarah Alice Gaggl, Maria Vanina Martinez, and Magdalena Ortiz, editors, Logics in Artificial Intelligence - 18th European Conference, JELIA 2023, Dresden, Germany, September 20-22, 2023, Proceedings, volume 14281 of Lecture Notes in Computer Science, pages 814-827. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43619-2_55.
  13. S. Figueira and D. Gorín. On the size of shortest modal descriptions. Advances in Modal Logic, 8:114-132, 2010. Google Scholar
  14. T. French, W. van der Hoek, P. Iliev, and B. Kooi. Succinctness of epistemic languages. In T. Walsh, editor, Proceedings of IJCAI, pages 881-886, 2011. Google Scholar
  15. Dov M. Gabbay and Larisa Maksimova. Interpolation and Definability: Modal and Intuitionistic Logics. Oxford University Press, May 2005. URL: https://doi.org/10.1093/acprof:oso/9780198511748.001.0001.
  16. Zachary Gleit and Warren Goldfarb. Characters and fixed-points in provability logic. Notre Dame Journal of Formal Logic, 31(1):26-36, 1989. URL: https://doi.org/10.1305/ndjfl/1093635330.
  17. M. Grohe and N. Schweikardt. The succinctness of first-order logic on linear orders. Logical Methods in Computer Science, 1:1-25, 2005. Google Scholar
  18. L. Hella and M. Vilander. The succinctness of first-order logic over modal logic via a formula size game. In Advances in Modal Logic, volume 11, pages 401-419, 2016. Google Scholar
  19. A. Razborov. Applications of matrix methods to the theory of lower bounds in computational complexity. Combinatorica, 10(1):81-93, 1990. URL: https://doi.org/10.1007/BF02122698.
  20. Lisa Reidhaar-Olson. A new proof of the fixed-point theorem of probability logic. Notre Dame J. Formal Log., 31:37-43, 1989. URL: https://api.semanticscholar.org/CorpusID:7685381, URL: https://doi.org/10.1305/NDJFL/1093635331.
  21. Giovanni Sambin. An effective fixed-point theorem in intuitionistic diagonalizable algebras. Studia Logica, 35(4):345-361, 1976. URL: https://doi.org/10.1007/bf02123402.
  22. Craig Smoryński. Modal logic and self-reference. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, pages 1-53. Springer Netherlands, Dordrecht, 2004. URL: https://doi.org/10.1007/978-94-017-0466-3_1.
  23. R. M. Solovay. Provability interpretations of modal logic. Israel Journal of Mathematics, 25:287-304, 1976. Google Scholar
  24. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5(2):285-309, 1955. URL: https://projecteuclid.org:443/euclid.pjm/1103044538.
  25. W. van der Hoek, P. Iliev, and B. Kooi. On the relative succinctness of modal logics with union, intersection and quantification. In Proceedings of AAMAS, pages 341-348, 2014. Google Scholar
  26. VII Soviet Symposium on Logic. On modal ‘‘companions’’ of superintuitionistic logics, Kiev, 1976. Russian. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact