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 well-suited to treating fixed points or (co-)inductively defined concepts. A key problem of cyclic proof theory is proving the equivalence of cyclic and non-cyclic 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 second-order 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 second-order 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 Knaster-Tarski 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 first-order logic by associating a higher-order 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 first-order setting, Herbrand schemes derive a language of witnesses from cyclic proofs via a simulation of non-wellfounded 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, Non-wellfounded parsimonious proofs and non-uniform complexity |
|
Authors: Matteo Acclavio, Gianluca Curzi and Giulio Guerrieri Cyclic and non-wellfounded proof-theory has established itself as an ideal framework for studying (co)inductive reasoning, hence to express computationally (co)recursion mechanisms under the Curry-Howard 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 polynomial-size circuits (\(\mathbf{FP}/\mathsf{poly}\)) has been presented, where non-uniformity in complexity theory is modelled via non-wellfounded proofs. In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded 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 non-wellfounded parsimonious proof systems capturing the classes \(\mathbf{FP}\) and \(\mathbf{FP}/\mathsf{poly}\), essentially restating the results in [1] for parsimonious logic to a non-wellfounded proof-theoretic setting. Soundness is established via a polynomial modulus of continuity for continuous cut-elimination. Completeness relies on an encoding of polynomial Turing machines with advice. Bibliography
|