Cyclic Systems for Arithmetic Theories of Inductive Definitions

Add to your list(s) Download to your calendar using vCal

• Lukas Holter Melgaard (University of Birmingham)
• Friday 02 December 2022, 13:30-14:20
• LG23, Computer Science // Zoom.

If you have a question about this talk, please contact George Kaye.

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

In recent years we have seen increasing interest in cyclic proof systems. These are systems where proofs can be non-wellfounded, i.e. contain infinite branches, but nonetheless have only finitely many distinct sub-proofs. This non-wellfoundedness allows them to simulate inductive arguments without need for explicit induction axioms. Naturally some appropriate correctness criterion is required to prevent fallacious reasoning, usually in the form of some ω-regular property of infinite branches (the trace condition).

In this work we develop a cyclic version of the theory ID1 , called CID1 . ID1 is a well-known arithmetic theory that extends PA by arithmetical inductive definitions. CID1 is a cyclic version of ID1 similar to how the theory of cyclic arithmetic (CA) was developed as a cyclic version of PA by Simpson. The system is similar in spirit to Brotherston’s cyclic system for ordinary inductive definitions over first-order logic.

Our main results are the soundness of CID1 (with respect to the standard model) and that ID1 and CID1 prove the same arithmetical sentences. Both results are proved similarly to the case of CA and PA at a high level, but provide significant new technical challenges at the low level.

To prove soundness we assume the existence of a proof of a false statement and then construct an infinite false branch that, under the trace condition, yields a contradiction. In contrast to the case of CA infinite ‘false branches’ are not completely ruled out by the trace condition and so we have to be more careful to choose a branch with the appropriate properties. This is similar in complexity to the countermodel branch construction required for logics with more complex fixed pionts, such as the μ-calculus.

To show conservativity we employ a metamathematical argument, formalising the soundness of CID1 within (a theory conservative over) ID1 and then appeal to reflection. The big challenge for this approach, as compared to the similar argument for CA, is that the closure ordinals of our inductive definitions (up to Church-Kleene) far exceed the proof theoretic ordinal of the theory (Bachmann-Howard) and so explicit induction on their notations is not possible for the soundness argument. Thus a different approach is required, namely requiring a formalisation of the theory of (recursive) ordinals at the object level. We expect that similar results carry over to IDn, the theory of n (nestings of) inductive definitions, for each n ∈ ω and thus ID＜ω, but this is currently work-in-progress.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, Computer Science // Zoom
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.