DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2023.27

Cyclic Proofs for Arithmetical Inductive Definitions

Authors: Anupam Das and Lukas Melgaard

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.FSCD.2023.27,
  author =	{Das, Anupam and Melgaard, Lukas},
  title =	{{Cyclic Proofs for Arithmetical Inductive Definitions}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.27},
  URN =		{urn:nbn:de:0030-drops-180119},
  doi =		{10.4230/LIPIcs.FSCD.2023.27},
  annote =	{Keywords: cyclic proofs, inductive definitions, arithmetic, fixed points, proof theory}
}

Search Results

Documents authored by Melgaard, Lukas

Cyclic Proofs for Arithmetical Inductive Definitions

Abstract

Cite as

Thanks for your feedback!

Could not send message