Cyclic Proofs for Arithmetical Inductive Definitions

Anupam Das; Lukas Melgaard

doi:10.4230/LIPIcs.FSCD.2023.27

Cyclic Proofs for Arithmetical Inductive Definitions

Anupam Das^*, Lukas Melgaard^*

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

25 Downloads (Pure)

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	https://doi.org/10.4230/LIPIcs.FSCD.2023.27
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

Access to Document

10.4230/LIPIcs.FSCD.2023.27Licence: Creative Commons: Attribution (CC BY)

DasA2023CyclicFinal published version, 838 KBLicence: Creative Commons: Attribution (CC BY)

Structure vs. Invariants in Proofs (StrIP)
Das, A.
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

@inproceedings{e3e6060f1f8d46bb9b0879c6d013e6d3,

title = "Cyclic Proofs for Arithmetical Inductive Definitions",

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{\textquoteright}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.",

keywords = "arithmetic, cyclic proofs, fixed points, inductive definitions, proof theory",

author = "Anupam Das and Lukas Melgaard",

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: {\textcopyright} Anupam Das and Lukas Melgaard.; 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023 ; Conference date: 03-07-2023 Through 06-07-2023",

year = "2023",

month = jun,

day = "28",

doi = "10.4230/LIPIcs.FSCD.2023.27",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl",

editor = "Marco Gaboardi and {van Raamsdonk}, Femke",

booktitle = "8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)",

address = "Germany",

}

Das, A & Melgaard, L 2023, Cyclic Proofs for Arithmetical Inductive Definitions. in M Gaboardi & F van Raamsdonk (eds), 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)., 27, Leibniz International Proceedings in Informatics, LIPIcs, vol. 260, Schloss Dagstuhl, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, Rome, Italy, 3/07/23. https://doi.org/10.4230/LIPIcs.FSCD.2023.27

Cyclic Proofs for Arithmetical Inductive Definitions. / Das, Anupam; Melgaard, Lukas.
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). ed. / Marco Gaboardi; Femke van Raamsdonk. Schloss Dagstuhl, 2023. 27 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 260).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Cyclic Proofs for Arithmetical Inductive Definitions

AU - Das, Anupam

AU - Melgaard, Lukas

N1 - 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.

PY - 2023/6/28

Y1 - 2023/6/28

N2 - 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.

AB - 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.

KW - arithmetic

KW - cyclic proofs

KW - fixed points

KW - inductive definitions

KW - proof theory

UR - http://www.scopus.com/inward/record.url?scp=85166029258&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSCD.2023.27

DO - 10.4230/LIPIcs.FSCD.2023.27

M3 - Conference contribution

AN - SCOPUS:85166029258

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

A2 - Gaboardi, Marco

A2 - van Raamsdonk, Femke

PB - Schloss Dagstuhl

T2 - 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023

Y2 - 3 July 2023 through 6 July 2023

ER -

Cyclic Proofs for Arithmetical Inductive Definitions

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this