DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2025.25

Exponential Lower Bounds on Definable Fixed Points

Authors: Konstantinos Papafilippou and David Fernández-Duque

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{papafilippou_et_al:LIPIcs.CSL.2025.25,
  author =	{Papafilippou, Konstantinos and Fern\'{a}ndez-Duque, David},
  title =	{{Exponential Lower Bounds on Definable Fixed Points}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.25},
  URN =		{urn:nbn:de:0030-drops-227827},
  doi =		{10.4230/LIPIcs.CSL.2025.25},
  annote =	{Keywords: Modal logic, Provability Logic, Fixed-Point Theorem, mu-calculus, Interpolation, Succinctness}
}

Search Results

Documents authored by Papafilippou, Konstantinos

Exponential Lower Bounds on Definable Fixed Points

Abstract

Cite as

Thanks for your feedback!

Could not send message