2026-07-26T23:09:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22782 2025-02-03T10:18:31Z ddc:004 open_access

Exponential Lower Bounds on Definable Fixed Points Papafilippou, Konstantinos Fernández-Duque, David Modal logic Provability Logic Fixed-Point Theorem mu-calculus Interpolation Succinctness 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Konstantinos Papafilippou and David Fernández-Duque 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.25 urn:nbn:de:0030-drops-227827 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.25 eng https://creativecommons.org/licenses/by/4.0/legalcode