Document Open Access Logo

Cyclic Proof Theory of Generalised Inductive Definitions

Authors Gianluca Curzi , Lukas Melgaard

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.15.pdf
  • Filesize: 1 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Higher order logic
Keywords
  • cyclic proofs
  • positive inductive definitions
  • arithmetic
  • fixed points
  • proof theory
  • reset proof systems

Metrics

Abstract

We study cyclic proof systems for μPA, an extension of Peano arithmetic by generalised inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic Π^1_2-CA₀ by Möllerfeld.
The main result of this paper is that cyclic and inductive μPA have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam’s systems for first-order μ-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within Π^1_2-CA₀, leveraging Möllerfeld’s conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem.
As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for μPA prove the same theorems. 
This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson’s Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.

Cite As Get BibTex

Gianluca Curzi and Lukas Melgaard. Cyclic Proof Theory of Generalised Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.15

Author Details

Gianluca Curzi
  • Gothenburg University, Sweden
Lukas Melgaard
  • University of Birmingham, UK

Funding

This work was supported by a UKRI Future Leaders Fellowship, "Structure vs Invariants in Proofs" (project reference MR/S035540/1), by the Wallenberg Academy Fellowship Prolongation project "Taming Jörmungandr: The Logical Foundations of Circularity" (project reference 251080003), and by the VR starting grant "Proofs with Cycles in Computation" (project reference 251088801).

Acknowledgements

We would like to thank Anupam Das for his continuous support, and Graham Leigh for his valuable suggestions during the development of this paper.

References

  1. Bahareh Afshari, Sebastian Enqvist, and Graham E. Leigh. Cyclic proofs for the first-order μ-calculus. Log. J. IGPL, 32(1):1-34, 2024. URL: https://doi.org/10.1093/JIGPAL/JZAC053.
  2. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  3. Bahareh Afshari and Graham E. Leigh. Lyndon interpolation for modal μ-calculus. In Language, Logic, and Computation: 13th International Tbilisi Symposium, TbiLLC 2019, Batumi, Georgia, September 16–20, 2019, Revised Selected Papers, pages 197-213, Berlin, Heidelberg, 2019. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-98479-3_10.
  4. Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. Uniform interpolation from cyclic proofs: The case of modal μ-calculus. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, pages 335-353, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-86059-2_20.
  5. Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. Math. Struct. Comput. Sci., 34(7):552-577, 2024. URL: https://doi.org/10.1017/S0960129524000070.
  6. Stefano Berardi and Makoto Tatsuta. Classical system of martin-löf’s inductive definitions is not equivalent to cyclic proof system. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 301-317, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_18.
  7. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005114.
  8. James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, pages 78-92. Springer, 2005. URL: https://doi.org/10.1007/11554554_8.
  9. James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 131-146. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_12.
  10. James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 51-62. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.16.
  11. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput., 21(6):1177-1216, 2011. URL: https://doi.org/10.1093/LOGCOM/EXQ052.
  12. Gianluca Curzi and Anupam Das. Computational expressivity of (circular) proofs with fixed points. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175772.
  13. Gianluca Curzi and Lukas Melgaard. Cyclic proof theory of positive inductive definitions, 2025. URL: https://doi.org/10.48550/arXiv.2507.13057.
  14. Anupam Das. On the logical complexity of cyclic arithmetic. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:1)2020.
  15. Anupam Das. On the logical strength of confluence and normalisation for cyclic proofs. In Naoki Kobayashi, editor, FSCD '21, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 29:1-29:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.29.
  16. Anupam Das and Lukas Melgaard. Cyclic proofs for arithmetical inductive definitions. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 27:1-27:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.27.
  17. Jacobus W de Bakker and Dana Scott. A theory of programs. In IBM seminar, Vienna, 1969. Google Scholar
  18. Solomon Feferman, W Sieg, and W Buchholz. Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Springer, 1981. Google Scholar
  19. Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The logical strength of Büchi’s decidability theorem. Log. Methods Comput. Sci., 15(2), 2019. URL: https://doi.org/10.23638/LMCS-15(2:16)2019.
  20. Graham E. Leigh and Dominik Wehr. From GTC to : Generating reset proof systems from cyclic proof systems. Ann. Pure Appl. Log., 175(10):103485, 2024. URL: https://doi.org/10.1016/J.APAL.2024.103485.
  21. Robert S. Lubarsky. μ-definable sets of integers. Journal of Symbolic Logic, 58:291-313, 1993. URL: https://doi.org/10.2307/2275338.
  22. Johannes Marti and Yde Venema. A focus system for the alternation-free μ-calculus. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, pages 371-388, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-86059-2_22.
  23. Michael Möllerfeld. Generalized inductive definitions. PhD thesis, University of Münster, Germany, 2003. URL: https://nbn-resolving.org/urn:nbn:de:hbz:6-85659549572.
  24. Damian Niwinski and Igor Walukiewicz. Games for the mu-calculus. Theor. Comput. Sci., 163(1&2):99-116, 1996. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  25. Michael Rathjen. Recent advances in ordinal analysis: Π¹₂-CA and related systems. Bulletin of Symbolic Logic, 1(4):468-485, 1995. URL: https://doi.org/10.2307/421132.
  26. Reuben N. S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 53-65. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018623.
  27. Harold Schellinx. Basic proof theory, A.S. troelstra and h. schwichtenberg. J. Log. Lang. Inf., 7(2):221-223, 1998. URL: https://doi.org/10.1023/A:1008226228293.
  28. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, FOSSACS '17, Held as Part of ETAPS '17, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  29. Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer, 1999. Google Scholar
  30. Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: Circular and tree-shaped proofs in the μ-calculus. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 425-440. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_27.
  31. Christoph Sprenger and Mads Dam. On global induction mechanisms in a μ-calculus with explicit approximations. RAIRO Theor. Informatics Appl., 37(4):365-391, 2003. URL: https://doi.org/10.1051/ita:2003024.
  32. Thomas Studer. On the proof theory of the modal mu-calculus. Stud Logica, 89(3):343-363, 2008. URL: https://doi.org/10.1007/s11225-008-9133-6.
  33. Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 491-508. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_30.
  34. Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. J. Autom. Reason., 64(3):555-578, 2020. URL: https://doi.org/10.1007/s10817-019-09532-0.
  35. Sergei Tupailo. On the intuitionistic strength of monotone inductive definitions. J. Symb. Log., 69(3):790-798, 2004. URL: https://doi.org/10.2178/jsl/1096901767.
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