Projects per year
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.
Original language | English |
---|---|
Title of host publication | 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) |
Editors | Marco Gaboardi, Femke van Raamsdonk |
Publisher | Schloss Dagstuhl |
Number of pages | 18 |
ISBN (Electronic) | 9783959772778 |
DOIs | |
Publication status | Published - 28 Jun 2023 |
Event | 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023 - Rome, Italy Duration: 3 Jul 2023 → 6 Jul 2023 |
Publication series
Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Publisher | Schloss Dagstuhl |
Volume | 260 |
ISSN (Electronic) | 1868-8969 |
Conference
Conference | 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023 |
---|---|
Country/Territory | Italy |
City | Rome |
Period | 3/07/23 → 6/07/23 |
Bibliographical note
Funding Information:Funding This work was supported by a UKRI Future Leaders Fellowship, “Structure vs. Invariants in Proofs”, project reference MR/S035540/1.
Publisher Copyright:
© Anupam Das and Lukas Melgaard.
Keywords
- arithmetic
- cyclic proofs
- fixed points
- inductive definitions
- proof theory
ASJC Scopus subject areas
- Software
Fingerprint
Dive into the research topics of 'Cyclic Proofs for Arithmetical Inductive Definitions'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Structure vs. Invariants in Proofs (StrIP)
Das, A. (Principal Investigator)
1/05/20 → 31/07/24
Project: Research Councils