Document Open Access Logo

On the Logical Strength of Confluence and Normalisation for Cyclic Proofs

Author Anupam Das

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.29.pdf
  • Filesize: 0.88 MB
  • 23 pages

Document Identifiers

Author Details

Anupam Das
  • 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

I would like to thank Denis Kuperberg, Laureline Pinault and Damien Pous for several interesting discussions on this and related topics. I am also grateful to the anonymous reviewers for their helpful feedback and suggestions.

Cite As Get BibTex

Anupam Das. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.29

Abstract

In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic.

We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity.

A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Proof theory
  • Theory of computation → Higher order logic
  • Theory of computation → Lambda calculus
Keywords
  • confluence
  • normalisation
  • system T
  • circular proofs
  • reverse mathematics
  • type structures

Metrics

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

Related Versions

  • This work is based on part of the following preprint, where related results, proofs and examples may be found.
  • Extended Version https://arxiv.org/abs/2012.14421

References

  1. 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.
  2. Jeremy Avigad and Solomon Feferman. Gödel’s functional ("dialectica") interpretation. Handbook of Proof Theory, 137:337-405, 1998. Google Scholar
  3. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for infinitary and circular proofs. CoRR, abs/2005.08257, 2020. URL: http://arxiv.org/abs/2005.08257.
  4. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29-September 1, 2016, Marseille, France, pages 42:1-42:17, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  5. 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, 2017. URL: https://doi.org/10.1109/LICS.2017.8005114.
  6. James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31-August 5, 2011. Proceedings, pages 131-146, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_12.
  7. James Brotherston, Nikos Gorogiannis, and Rasmus L. Petersen. A generic cyclic theorem prover. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, pages 350-367, 2012. URL: https://doi.org/10.1007/978-3-642-35182-2_25.
  8. 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, 2007. URL: https://doi.org/10.1109/LICS.2007.16.
  9. 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.
  10. Samuel R. Buss, editor. Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics 137. Elsevier, 1998. Google Scholar
  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. Anupam Das. A circular version of Gödel’s T and its abstraction complexity, 2021. URL: http://arxiv.org/abs/2012.14421.
  13. Anupam Das, Amina Doumane, and Damien Pous. Left-handed completeness for kleene algebra, via cyclic proofs. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume 57 of EPiC Series in Computing, pages 271-289. EasyChair, 2018. URL: https://easychair.org/publications/paper/SDqf.
  14. Anupam Das and Damien Pous. A cut-free cyclic proof system for Kleene algebra. In Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, pages 261-277, 2017. URL: https://doi.org/10.1007/978-3-319-66902-1_16.
  15. Anupam Das and Damien Pous. Non-wellfounded proof theory for (kleene+action)(algebras+lattices). In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 19:1-19:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.19.
  16. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  17. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  18. Amina Doumane. Constructive completeness for the linear-time μ-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.8005075.
  19. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013), September 2-5, 2013, Torino, Italy, pages 248-262, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.248.
  20. Petr Hájek and Pavel Pudlák. Metamathematics of First-Order Arithmetic. Perspectives in mathematical logic. Springer, 1993. URL: http://www.springer.com/mathematics/book/978-3-540-63648-9.
  21. J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and λ-Calculus. Cambridge University Press, USA, 1986. Google Scholar
  22. Denis R. Hirschfeldt. Slicing the truth: On the computable and reverse mathematics of combinatorial principles. World Scientific, 2014. Google Scholar
  23. S.C. Kleene. Introduction to Metamathematics. Bibliotheca Mathematica. North Holland, 7 edition, 1980. Google Scholar
  24. Ulrich Kohlenbach. Applied Proof Theory - Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77533-1.
  25. 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.
  26. Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs, System T, and the Power of Contraction. Proceedings of the ACM on Programming Languages, 2021. URL: https://doi.org/10.1145/3434282.
  27. John Longley and Dag Normann. Higher-Order Computability. Theory and Applications of Computability. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47992-6.
  28. 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.
  29. Charles Parsons. On n-quantifier induction. The Journal of Symbolic Logic, 37(3):466-482, 1972. Google Scholar
  30. Frank Pfenning. A proof of the church-rosser theorem and its representation in a logical framework. Technical report, Carnegie-Mellon University, Pittsburgh. Department of Computer Science., 1992. Google Scholar
  31. Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 357-371. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_25.
  32. B. Scarpellini. A model for barrecursion of higher types. Compositio Mathematica, 23(1):123-153, 1971. URL: http://eudml.org/doc/89072.
  33. Alex Simpson. Cyclic arithmetic is equivalent to Peano arithmetic. In Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Proceedings, pages 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  34. Stephen G. Simpson. Subsystems of second order arithmetic, volume 1. Cambridge University Press, 2009. Google Scholar
  35. 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.
  36. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  37. Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2003. Google Scholar
  38. Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics. Springer, 1 edition, 1973. URL: http://gen.lib.rus.ec/book/index.php?md5=5E0718442C0178C4B23065E54AC7889C.
  39. Chuangjie Xu. A syntactic approach to continuity of T-definable functionals. Logical Methods in Computer Science, Volume 16, Issue 1, 2020. URL: https://doi.org/10.23638/LMCS-16(1:22)2020.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact