Document Open Access Logo

Cyclic Proofs for Arithmetical Inductive Definitions

Authors Anupam Das , Lukas Melgaard

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.27.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Author Details

Anupam Das
  • University of Birmingham, UK
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.

Acknowledgements

The authors would like to thank Graham Leigh and Colin Riba for several interesting conversations about (arithmetical) inductive definitions.

Cite AsGet BibTex

Anupam Das and Lukas Melgaard. Cyclic Proofs for Arithmetical Inductive Definitions. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 27:1-27:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.27

Abstract

We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain "impredicative" theories; moreover, our cyclic systems naturally subsume Simpson’s Cyclic Arithmetic. Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within second-order arithmetic by a form of induction on closure ordinals, thence appealing to conservativity results. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty: the closure ordinals of our inductive definitions (around Church-Kleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around Bachmann-Howard), so explicit induction on their notations is not possible. For this reason, we rather rely on formalisation of the theory of (recursive) ordinals within second-order arithmetic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • cyclic proofs
  • inductive definitions
  • arithmetic
  • fixed points
  • proof theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Bahareh Afshari, Sebastian Enqvist, and Graham E Leigh. Cyclic proofs for the first-order μ-calculus. Logic Journal of the IGPL, August 2022. jzac053. 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. 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.
  4. 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.
  5. Stefano Berardi and Makoto Tatsuta. Intuitionistic podelski-rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers, volume 11202 of Lecture Notes in Computer Science, pages 13-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00389-0_3.
  6. Stefano Berardi and Makoto Tatsuta. Classical system of martin-lof’s inductive definitions is not equivalent to cyclic proofs. Log. Methods Comput. Sci., 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:10)2019.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. Anupam Das. On the logical complexity of cyclic arithmetic. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:1)2020.
  12. Solomon Feferman, W Sieg, and W Buchholz. Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Springer, 1981. Google Scholar
  13. Gerhard Jäger. Fixed points in peano arithmetic with ordinals. Ann. Pure Appl. Log., 60(2):119-132, 1993. URL: https://doi.org/10.1016/0168-0072(93)90039-G.
  14. Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The logical strength of büchi’s decidability theorem. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 36:1-36:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.36.
  15. 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.
  16. Robert S. Lubarsky. μ-definable sets of integers. Journal of Symbolic Logic, 58:291-313, 1993. Google Scholar
  17. Michael Möllerfeld. Generalized inductive definitions. PhD thesis, WWU Münster, 2002. URL: https://nbn-resolving.de/urn:nbn:de:hbz:6-85659549572.
  18. 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.
  19. Michael Rathjen and Wilfried Sieg. Proof Theory. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Winter 2022 edition, 2022. Google Scholar
  20. 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.
  21. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. 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 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  22. Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer, 1999. Google Scholar
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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