On the logical complexity of cyclic arithmetic.

*(English)*Zbl 07155168Summary: We study the logical complexity of proofs in cyclic arithmetic \((\mathsf{CA})\), as introduced by A. Simpson in [Lect. Notes Comput. Sci. 10203, 283–300 (2017; Zbl 06720996)], in terms of quantifier alternations of formulae occurring. Writing \(C\Sigma_n\) for (the logical consequences of) cyclic proofs containing only \(\Sigma_n\) formulae, our main result is that \(I\Sigma_{n+1}\) and \(C\Sigma_n\) prove the same \(\Pi_{n+1}\) theorems, for all \(n\geq 0\). Furthermore, due to the ‘uniformity’ of our method, we also show that \(\mathsf{CA}\) and Peano Arithmetic \(( \mathsf{PA} )\) proofs of the same theorem differ only exponentially in size.

The inclusion \(I\Sigma_{n+1} \subseteq C\Sigma_n\) is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of \(\mathsf{PA}\) proofs. It improves upon the natural result that \(I\Sigma_n\) is contained in \(C\Sigma_n\). The converse inclusion, \(C\Sigma_n \subseteq I\Sigma_{n+1} \), is obtained by calibrating the approach of [Simpson, loc. cit.] with recent results on the reverse mathematics of Büchi’s theorem in [L. Kołodziejczyk et al., Log. Methods Comput. Sci. 15, No. 2, Paper No. 16, 31 p. (2019; Zbl 07058775)], and specialising to the case of cyclic proofs. These results improve upon the bounds on proof complexity and logical complexity implicit in [Simpson, loc. cit.] and also an alternative approach due to S. Berardi and M. Tatsuta [“Equivalence of inductive definitions and cyclic proofs under arithmetic”, in: Proceedings of the 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017. IEEE Digital Library. 1–12 (2017; doi:10.1109/LICS.2017.8005114)].

The uniformity of our method also allows us to recover a metamathematical account of fragments of \(\mathsf{CA} \); in particular we show that, for \(n\geq 0\), the consistency of \(C\Sigma_n\) is provable in \(I\Sigma_{n+2}\) but not \(I\Sigma_{n+1} \). As a result, we show that certain versions of McNaughton’s theorem (the determinisation of \(\omega \)-word automata) are not provable in \(\mathsf{RCA}_0\), partially resolving an open problem from [Kołodziejczyk et al., loc. cit.].

The inclusion \(I\Sigma_{n+1} \subseteq C\Sigma_n\) is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of \(\mathsf{PA}\) proofs. It improves upon the natural result that \(I\Sigma_n\) is contained in \(C\Sigma_n\). The converse inclusion, \(C\Sigma_n \subseteq I\Sigma_{n+1} \), is obtained by calibrating the approach of [Simpson, loc. cit.] with recent results on the reverse mathematics of Büchi’s theorem in [L. Kołodziejczyk et al., Log. Methods Comput. Sci. 15, No. 2, Paper No. 16, 31 p. (2019; Zbl 07058775)], and specialising to the case of cyclic proofs. These results improve upon the bounds on proof complexity and logical complexity implicit in [Simpson, loc. cit.] and also an alternative approach due to S. Berardi and M. Tatsuta [“Equivalence of inductive definitions and cyclic proofs under arithmetic”, in: Proceedings of the 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017. IEEE Digital Library. 1–12 (2017; doi:10.1109/LICS.2017.8005114)].

The uniformity of our method also allows us to recover a metamathematical account of fragments of \(\mathsf{CA} \); in particular we show that, for \(n\geq 0\), the consistency of \(C\Sigma_n\) is provable in \(I\Sigma_{n+2}\) but not \(I\Sigma_{n+1} \). As a result, we show that certain versions of McNaughton’s theorem (the determinisation of \(\omega \)-word automata) are not provable in \(\mathsf{RCA}_0\), partially resolving an open problem from [Kołodziejczyk et al., loc. cit.].

##### Software:

Cyclist
PDF
BibTeX
XML
Cite

\textit{A. Das}, Log. Methods Comput. Sci. 16, No. 1, Paper No. 1, 39 p. (2020; Zbl 07155168)

Full Text:
arXiv

##### References:

[1] | [AL17]Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modalµ-calculus. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. |

[2] | [AL18]Albert Atserias and Massimo Lauria. Circular (yet sound) proofs.CoRR, abs/1802.05266, 2018. |

[3] | [BBC08]James Brotherston, Richard Bornat, and Cristiano Calcagno. Cyclic proofs of program termination in separation logic. InProceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles · Zbl 1295.68156 |

[4] | [BDP11]James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. InCADE-23 - 23rd International Conference on Automated Deduction, · Zbl 1341.68184 |

[5] | [BDS16]David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August · Zbl 1370.03077 |

[6] | [BGP12]James Brotherston, Nikos Gorogiannis, and Rasmus L. Petersen. A generic cyclic theorem prover. InProgramming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, |

[7] | [Bro05]James Brotherston. Cyclic proofs for first-order logic with inductive definitions. InAutomated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, pages 78-92, 2005. · Zbl 1142.03366 |

[8] | [Bro06]James Brotherston.Sequent calculus proof systems for inductive definitions. PhD thesis, University of Edinburgh, 2006. |

[9] | [BS07]James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, |

[10] | [BS11]James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent.J. Log. Comput., 21(6):1177-1216, 2011. · Zbl 1242.03084 |

[11] | [BT17a]Stefano Berardi and Makoto Tatsuta. Classical system of Martin-L¨of’s inductive definitions is not equivalent to cyclic proof system. InFoundations of Software Science and Computation · Zbl 06720997 |

[12] | [BT17b]Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, · Zbl 06720997 |

[13] | [Bus95]Samuel R. Buss. The witness function method and provably recursive functions of Peano arithmetic. InStudies in Logic and the Foundations of Mathematics, volume 134, pages 29-68. Elsevier, 1995. · Zbl 0829.03036 |

[14] | [Bus98]Samuel R. Buss, editor.Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics 137. Elsevier, 1998. · Zbl 0898.03001 |

[15] | [CK02]Peter Clote and Evangelos Kranakis.Boolean Functions and Computation Models. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2002. · Zbl 1016.94046 |

[16] | [CN10]Stephen Cook and Phuong Nguyen.Logical Foundations of Proof Complexity. Cambridge University Press, New York, NY, USA, 1st edition, 2010. · Zbl 1206.03051 |

[17] | [DBHS16] Amina Doumane, David Baelde, Lucca Hirschi, and Alexis Saurin. Towards completeness via proof search in the linear timeµ-calculus: The case of B¨uchi inclusions. InProceedings of the 31st · Zbl 1401.68193 |

[18] | [DHL06]Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear timeµ-calculus. InFSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th · Zbl 1163.03308 |

[19] | [Dou17]Amina Doumane. Constructive completeness for the linear-timeµ-calculus. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. |

[20] | [DP17]Anupam Das and Damien Pous. A cut-free cyclic proof system for Kleene algebra. InAutomated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, |

[21] | [For14]J´erˆome Fortier.Puissance expressive des preuves circulaires. (Expressive Power of Circular Proofs). PhD thesis, Aix-Marseille University, Aix-en-Provence, France, 2014. |

[22] | [FS13]J´erˆome 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, · Zbl 1356.03098 |

[23] | [Hir14]Denis R. Hirschfeldt.Slicing the truth: On the computable and reverse mathematics of combinatorial principles. World Scientific, 2014. · Zbl 1304.03001 |

[24] | [HP93]Petr H´ajek and Pavel Pudl´ak.Metamathematics of First-Order Arithmetic. Perspectives in mathematical logic. Springer, 1993. |

[25] | [Kay91]Richard Kaye.Models of Peano Arithmetic. Oxford Logic Guides 15. Oxford University Press, 1991. |

[26] | [KMPS19] Leszek Ko lodziejczyk, Henryk Michalewski, Pierre Pradic, and Micha l Skrzypczak. The logical strength of B¨uchi’s decidability theorem. volume Volume 15, Issue 2, May 2019. · Zbl 07058775 |

[27] | [KPW95]Jan Kraj´ıˇcek, Pavel Pudl´ak, and Alan Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle.Random Structures & Algorithms, 7(1):15-39, |

[28] | [Kra95]Jan Kraj´ıˇcek.Bounded arithmetic, propositional logic, and complexity theory. Cambridge University |

[29] | [McN66]Robert McNaughton. Testing and generating infinite sequences by a finite automaton.Information and Control, 9(5):521-530, 1966. · Zbl 0212.33902 |

[30] | [ML71]Per Martin-L¨of. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J.E. Fenstad, editor,Proceedings of the Second Scandinavian Logic Symposium, volume 63 ofStudies · Zbl 0231.02040 |

[31] | [NST18]R´emi Nollet, Alexis Saurin, and Christine Tasson. Local validity for circular proofs in linear logic with fixed points. In27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 35:1-35:23, 2018. |

[32] | [NW96]Damian Niwinski and Igor Walukiewicz. Games for theµ-calculus.Theor. Comput. Sci., 163(1&2):99-116, 1996. · Zbl 0872.03017 |

[33] | [Par71]Rohit Parikh. Existence and feasibility in arithmetic.J. Symb. Log., 36(3):494-508, 1971. · Zbl 0243.02037 |

[34] | [Par72]Charles Parsons. On n-quantifier induction.The Journal of Symbolic Logic, 37(3):466-482, 1972. |

[35] | [PBI93]Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle.Computational Complexity, 3:97-140, 1993. 10.1007/BF01200117. · Zbl 0784.03034 |

[36] | [PW81]Jeff B. Paris and Alex J. Wilkie. ∆0sets and induction.Open Days in Model Theory and Set Theory, W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, eds, pages 237-248, 1981. |

[37] | [RB17]Reuben N. S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. InProceedings of the 6th ACM SIGPLAN Conference on Certified |

[38] | [San02]Luigi Santocanale. A calculus of circular proofs and its categorical semantics. InFoundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002, · Zbl 1077.03515 |

[39] | [Sch77]Kurt Sch¨utte.Proof Theory. Grundlehren der mathematischen Wissenschaften 225. Springer Berlin Heidelberg, 1977. Translation of Beweistheorie, 1968. |

[40] | [SD03]Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: Circular and tree-shaped proofs in theµ-calculus. InFoundations of Software Science and Computational · Zbl 1029.03016 |

[41] | [Sim09]Stephen G. Simpson.Subsystems of second order arithmetic, volume 1. Cambridge University Press, 2009. · Zbl 1181.03001 |

[42] | [Sim17]Alex Simpson. Cyclic arithmetic is equivalent to Peano arithmetic. InFoundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Proceedings, · Zbl 06720996 |

[43] | [Str17]Sorin Stratulat. Cyclic proofs with ordering constraints. InAutomated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Bras´ılia, Brazil, |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.