×

zbMATH — the first resource for mathematics

Cyclic arithmetic is equivalent to Peano arithmetic. (English) Zbl 06720996
Esparza, Javier (ed.) et al., 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. Berlin: Springer (ISBN 978-3-662-54457-0/pbk; 978-3-662-54458-7/ebook). Lecture Notes in Computer Science 10203, 283-300 (2017).
Summary: Cyclic proof provides a style of proof for logics with inductive (and coinductive) definitions, in which proofs are cyclic graphs representing a form of argument by infinite descent. It is easily shown that cyclic proof subsumes proof by (co)induction. So cyclic proof systems are at least as powerful as the corresponding proof systems with explicit (co)induction rules. Whether or not the converse inclusion holds is a non-trivial question. In this paper, we resolve this question in one interesting case. We show that a cyclic formulation of first-order arithmetic is equivalent in power to Peano arithmetic. The proof involves formalising the meta-theory of cyclic proof in a subsystem of second-order arithmetic.
For the entire collection see [Zbl 1360.68010].

MSC:
68Qxx Theory of computing
Software:
Cyclist
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baelde, D.: On the proof theory of regular fixed points. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 93–107. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02716-1_8 · Zbl 1260.03108 · doi:10.1007/978-3-642-02716-1_8
[2] Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: Talbot, J.-M., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, vol. 62, pp. 42:1–42:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016) · Zbl 1370.03077
[3] Berardi, S., Tatsuta, M.: Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. In: Esparza, J., Murawski, A.S. (Eds.) FOSSACS 2017. LNCS, vol. 10203, pp. 301–317. Springer, Heidelberg (2017) · Zbl 06720997
[4] Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78–92. Springer, Heidelberg (2005). doi: 10.1007/11554554_8 · Zbl 1142.03366 · doi:10.1007/11554554_8
[5] Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh, November 2006
[6] Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: Proceedings of POPL-35, pp. 101–112. ACM (2008) · Zbl 1295.68156 · doi:10.1145/1328438.1328453
[7] Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131–146. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22438-6_12 · Zbl 1341.68184 · doi:10.1007/978-3-642-22438-6_12
[8] Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 68–84. Springer, Cham (2014). doi: 10.1007/978-3-319-10936-7_5 · Zbl 06349451 · doi:10.1007/978-3-319-10936-7_5
[9] Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350–367. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-35182-2_25 · Zbl 06152982 · doi:10.1007/978-3-642-35182-2_25
[10] Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: Proceedings of LICS-22, pp. 51–60. IEEE Computer Society, July 2007 · Zbl 1242.03084 · doi:10.1109/LICS.2007.16
[11] Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Logic Comput. 21(6), 1177–1216 (2011) · Zbl 1242.03084 · doi:10.1093/logcom/exq052
[12] Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \[ \upmu \] -calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273–284. Springer, Heidelberg (2006). doi: 10.1007/11944836_26 · Zbl 1163.03308 · doi:10.1007/11944836_26
[13] Fortier, J., Santocanale, L.: Cuts for circular proofs: semantics and cut-elimination. In: Computer Science Logic 2013 (CSL 2013), CSL 2013, 2–5 September 2013, Torino, Italy, pp. 248–262 (2013) · Zbl 1356.03098
[14] Kaye, R.: Models of Peano Arithmetic. Number 15 in Oxford Logic Guides. Oxford University Press, Oxford (1991)
[15] Kolodziejczyk, L.A., Michalewski, H., Pradic, P., Skrzypczak, M.: The logical strength of Büchi’s decidability theorem. In: Talbot, J.-M., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, vol. 62, pp. 36:1–36:16. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016) · Zbl 1370.03058
[16] Martin-Löf, P.: Haupstatz for the intuitionistic theory of iterated inductive def initions. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 179–216. North Holland (1971) · doi:10.1016/S0049-237X(08)70847-4
[17] Mio, M., Simpson, A.: A proof system for compositional verification of probabilistic concurrent processes. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 161–176. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-37075-5_11 · Zbl 1260.68273 · doi:10.1007/978-3-642-37075-5_11
[18] Niwiński, D., Walukiewicz, I.: Games for the \[ \mu \] -calculus. Theoret. Comput. Sci. 163, 99–116 (1997) · Zbl 0872.03017 · doi:10.1016/0304-3975(95)00136-0
[19] Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 357–371. Springer, Heidelberg (2002). doi: 10.1007/3-540-45931-6_25 · Zbl 1077.03515 · doi:10.1007/3-540-45931-6_25
[20] Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Logic. Association for Symbolic Logic, New York (2009) · doi:10.1017/CBO9780511581007
[21] Sprenger, C., Dam, M.: A note on global induction mechanisms in a \[ \mu \] -calculus with explicit approximations. Theor. Inform. Appl. 37, 365–399 (2003) · Zbl 1111.68518 · doi:10.1051/ita:2003024
[22] Sprenger, C., Dam, M.: On the structure of inductive reasoning: circular and tree-shaped proofs in the \[ \upmu \] calculus. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 425–440. Springer, Heidelberg (2003). doi: 10.1007/3-540-36576-1_27 · Zbl 1029.03016 · doi:10.1007/3-540-36576-1_27
[23] Stratulat, S.: Structural vs. cyclic induction: a report on some experiments with Coq. In: SYNASC 2016: Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 27–34. IEEE Computer Society (2016) · doi:10.1109/SYNASC.2016.018
[24] Studer, T.: On the proof theory of the modal mu-calculus. Stud. Logica. 89(3), 343–363 (2008) · Zbl 1163.03014 · doi:10.1007/s11225-008-9133-6
[25] Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, pp. 133–192. Elsevier Science Publishers, Amsterdam (1990)
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.