2026-07-25T09:26:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19413 2024-03-06T11:03:59Z ddc:004 open_access

Comparing Infinitary Systems for Linear Logic with Fixed Points Das, Anupam De, Abhishek Saurin, Alexis linear logic fixed points non-wellfounded proofs omega-branching proofs analytical hierarchy Extensions of Girard’s linear logic by least and greatest fixed point operators (μMALL) have been an active field of research for almost two decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we compare the relative expressivity, at the level of provability, of two complementary infinitary proof systems: finitely branching non-wellfounded proofs (μMALL^∞) vs. infinitely branching well-founded proofs (μMALL_{ω,∞}). Our main result is that μMALL^∞ is strictly contained in μMALL_{ω,∞}. For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that yields a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on μMALL^∞ provability from Π⁰₁-hard to Σ¹₁-hard, by encoding a sort of Büchi condition for Minsky machines. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anupam Das and Abhishek De and Alexis Saurin 2023 Is Part Of LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2023.40 urn:nbn:de:0030-drops-194131 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.40 eng https://creativecommons.org/licenses/by/4.0/legalcode