Document Open Access Logo

A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Authors Alexis Saurin , Esaïe Bauer

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.17.pdf
  • Filesize: 0.91 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
Keywords
  • cut elimination
  • exponential modalities
  • fixed-points
  • linear logic
  • light logics
  • mu-calculus
  • non-wellfounded proofs
  • proof theory
  • sequent calculus
  • subexponentials
  • super exponentials

Metrics

Abstract

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. 
Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. 
More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal μ-calculus.

Cite As Get BibTex

Alexis Saurin and Esaïe Bauer. A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 17:1-17:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.17

Author Details

Alexis Saurin
  • Université Paris Cité & CNRS & INRIA, Pl. Aurélie Nemours, 75013 Paris, France
Esaïe Bauer
  • Université Paris Cité, Pl. Aurélie Nemours, 75013 Paris, France

Funding

This work was partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.

References

  1. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533375.
  2. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In CSL 2016, volume 62 of LIPIcs, pages 42:1-42:17, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  3. Patrick Baillot. On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy. Information and Computation, 241:3-31, 2015. URL: https://doi.org/10.1016/j.ic.2014.10.005.
  4. Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Information and Computation, 261:55-77, 2018. Developments in Implicit Computational Complexity (DICE) 2014 and 2015. URL: https://doi.org/10.1016/j.ic.2018.05.005.
  5. Esaïe Bauer and Alexis Saurin. On the cut-elimination of the modal μ-calculus: Linear logic to the rescue. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures, pages 133-154, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-90897-2_7.
  6. Esaïe Bauer and Olivier Laurent. Super exponentials in linear logic. Electronic Proceedings in Theoretical Computer Science, 353:50-73, December 2021. URL: https://doi.org/10.4204/eptcs.353.3.
  7. Esaïe Bauer and Alexis Saurin. A uniform cut-elimination theorem for linear logics with fixed points and super exponentials, 2025. URL: https://doi.org/10.48550/arXiv.2506.14327.
  8. Aloïs Brunel and Kazushige Terui. Church => Scott = Ptime: an application of resource sensitive realizability. In Patrick Baillot, editor, Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010, volume 23 of EPTCS, pages 31-46, 2010. URL: https://doi.org/10.4204/EPTCS.23.3.
  9. Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions. Annals of Pure and Applied Logic, 163(3):266-290, 2012. URL: https://doi.org/10.1016/j.apal.2011.09.003.
  10. Agata Ciabattoni, Lutz Straßburger, and Kazushige Terui. Expanding the realm of systematic proof theory. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, pages 163-178, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-04027-6_14.
  11. Agata Ciabattoni and Kazushige Terui. Modular cut-elimination: Finding proofs or counterexamples. In Miki Hermann and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 135-149, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11916277_10.
  12. Ugo Dal Lago and Patrick Baillot. On light logics, uniform encodings and polynomial time. Mathematical Structures in Computer Science, 16(4):713-733, 2006. URL: https://doi.org/10.1017/S0960129506005421.
  13. Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. IC, 183(1):123-137, May 2003. URL: https://doi.org/10.1016/S0890-5401(03)00010-5.
  14. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: Linear logic. J. Symb. Log., 62(3):755-807, 1997. URL: https://doi.org/10.2307/2275572.
  15. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  16. Jean-Yves Girard. Light linear logic. IC, 143(2):175-204, June 1998. URL: https://doi.org/10.1006/inco.1998.2700.
  17. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  18. Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318(1-2):163-180, June 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.018.
  19. Lê Thành Dũng Nguyen. On the elementary affine lambda-calculus with and without fixed points. Electronic Proceedings in Theoretical Computer Science, 298:15-29, August 2019. URL: https://doi.org/10.4204/eptcs.298.2.
  20. Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In PPDP 2009, pages 129-140, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1599410.1599427.
  21. Luca Roversi and Luca Vercelli. Safe recursion on notation into a light logic by levels. In Patrick Baillot, editor, Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010, volume 23 of EPTCS, pages 63-77, 2010. URL: https://doi.org/10.4204/EPTCS.23.5.
  22. Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points. In Automated Reasoning with Analytic Tableaux and Related Methods, pages 203-222. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43513-3_12.
  23. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  24. Kazushige Terui. Which structural rules admit cut elimination? an algebraic criterion. Journal of Symbolic Logic, 72(3):738-754, 2007. URL: https://doi.org/10.2178/jsl/1191333839.
  25. Kazushige Terui. Proof theory and algebra in substructural logics. In Kai Brünnler and George Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 20-20, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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