Contributed Talks 22
Chair: Marianna Girlando
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
16:30 
Dominik Wehr, Unravelling cyclic arithmetic 
Cyclic proof systems admit derivations whose underlying structures are finite graphs rather than finite trees. Such proof systems are especially wellsuited to treating fixed points or (co)inductively defined concepts. A key problem of cyclic proof theory is proving the equivalence of cyclic and noncyclic proof systems for the same logic. The literature is the most developed for cyclic proof systems of Peano arithmetic, for which three distinct approaches to obtaining this equivalence are known: one based on the reverse mathematics of \(\omega\)automata theory [1,2], one based on infinite Ramsey theory [3] and one based on ‘unfolding’ proofs to exhibit certain structural properties [4]. In this talk, I will describe and compare all three approaches, illustrating the breadth of methods being brought to bear in cyclic proof theory. Bibliography


16:55 
Armand Feuilleaubois, Cyclic cut elimination for the stratified fragment of the modal μcalculus 
Authors: Armand Feuilleaubois and Thomas Studer Kloibhofer and Afshari presented in [1] a new cut elimination procedure for annotated cyclic proofs of a temporal modal logic using only the eventually operator, \(F\). This method has the advantage of preserving the regularity of the proof throughout the cut elimination process. We present a cut elimination procedure for the stratified fragment of the modal \(\mu\)calculus, based on the method of Kloibhofer and Afshari in [1]. The stratified fragment of the modal \(\mu\)calculus, as defined by Jäger, Kretz, and Studer in [2], is the fragment such that formulas \(\mu X.\mathcal{A}[X]\), \(\nu X.\mathcal{A}[X]\), with \(\mathcal{A}[X]\) positive in the variable \(X\), may only contain subformulas \(\mu Y.\mathcal{B}[Y]\), \(\nu Y.\mathcal{B}[Y]\) where \(X\) does not appear as a free variable. Thus, the meaning of an inner nested fixed point will not depend on the outer fixed point within which it is nested. This fragment itself contains as fragments CTL, PDL, and the logic of common knowledge. Thus, we also obtain cut elimination for these fragments. Bibliography


17:20 
Lukas Melgaard, Cyclic proofs for arithmetic with least and greatest fixed points 
Authors: Lukas Melgaard and Gianluca Curzi We investigate the cyclic proof theory of \(\mu \mathrm{PA}\), a theory that extends Peano Arithmetic with least and greatest fixed point operators. Our cyclic system \(\mathrm{C} \mu \mathrm{PA}\) subsumes Simpson’s cyclic arithmetic [3] and the stronger \(\mathrm{CID}_{< \omega}\) from [1]. Our main result is that the inductive system \(\mu \mathrm{PA}\) and the cyclic system \(\mathrm{C} \mu \mathrm{PA}\) prove the same arithmetical theorems. We conduct a metamathematical argument inspired by those in [3,1] for Cyclic Arithmetic to formalize the soundness of cyclic proofs within secondorder arithmetic by a form of induction on closure ordinals and then appealing to conservativity results. Since the closure ordinals of our inductive definitions far exceed the recursive ordinals we cannot rely on ordinal notations and must instead formalize a theory of ordinals within secondorder arithmetic. This is similar to what is done in [1] for \(\mathrm{CID}_{< \omega}\) except here we also need to use the reverse mathematics of a more powerful version of KnasterTarski as seen in [2]. Bibliography


17:45 
Sebastian Enqvist, Herbrand schemes for cyclic proofs 
Authors: Bahareh Afshari, Sebastian Enqvist and Graham Leigh Recent work by Afshari et al. introduce a notion of Herbrand schemes for firstorder logic by associating a higherorder recursion scheme to a sequent calculus proof. Calculating the language of associated Herbrand schemes directly yields Herbrand disjunctions. As such, these schemes can be seen as programs extracted from proofs. Here, this computational interpretation is explored further by removing the restriction of acyclicity from Herbrand schemes which amounts to admitting recursively defined programs. It is shown that the notion of proof corresponding to these generalised Herbrand schemes is cyclic proofs, considered here in the context of classical theories of inductively defined predicates. In particular, for proofs with end sequents of a form generalising the notion of \(\Sigma_1\)sequents in the firstorder setting, Herbrand schemes derive a language of witnesses from cyclic proofs via a simulation of nonwellfounded cut elimination. Thus Herbrand schemes can be used to directly compute the “Herbrand content” of cyclic proofs. This is based on unpublished work, for which a preprint is available at: https://eprints.illc.uva.nl/id/eprint/2292/1/Herbrand_schemes_for_cyclic_proofs.pdf 

18:10 
Gianluca Curzi, Nonwellfounded parsimonious proofs and nonuniform complexity 
Authors: Matteo Acclavio, Gianluca Curzi and Giulio Guerrieri Cyclic and nonwellfounded prooftheory has established itself as an ideal framework for studying (co)inductive reasoning, hence to express computationally (co)recursion mechanisms under the CurryHoward correspondence paradigm. In [3] the second author showed how cyclic proofs can be employed in computational complexity, yielding an implicit characterisation of the polynomial time computable functions (\(\mathbf{FP}\)) inspired by Bellantoni and Cook’s algebra of safe recursion [2]. In a follow up paper [4], a characterisation of the class of functions computed by polynomialsize circuits (\(\mathbf{FP}/\mathsf{poly}\)) has been presented, where nonuniformity in complexity theory is modelled via nonwellfounded proofs. In this paper we investigate the complexitytheoretical aspects of cyclic and nonwellfounded proofs in the context of parsimonious logic, a variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data (see, e.g., [1]). We present nonwellfounded parsimonious proof systems capturing the classes \(\mathbf{FP}\) and \(\mathbf{FP}/\mathsf{poly}\), essentially restating the results in [1] for parsimonious logic to a nonwellfounded prooftheoretic setting. Soundness is established via a polynomial modulus of continuity for continuous cutelimination. Completeness relies on an encoding of polynomial Turing machines with advice. Bibliography
