Logic Colloquium 2024

Contributed Talk

Contributed Talks 22

Chair: Marianna Girlando

  Friday, 16:30, J330 ! Live

Time allocation: 20 minutes per speaker; 5 minutes for each changeover

Talks in this session


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.


  1. Alex Simpson,Cyclic Arithmetic Is Equivalent to Peano Arithmetic,Foundations of Software Science and Computation Structures 2017,doi: 10.1007/978-3-662-54458-7_17
  2. Anupam Das_On the logical complexity of cyclic arithmetic_,Logical Methods in Computer Science,doi: 10.23638/LMCS-16(1:1)2020
  3. Stefano Berardi, Makoto Tatsuta,Equivalence of inductive definitions and cyclic proofs under arithmetic,Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Sciencedoi: 10.5555/3329995.3330049
  4. Graham E. Leigh, Dominik Wehr,Unravelling Cyclic First-Order Arithmetic,Representation Matters in Cyclic Proof Theory(licentiate thesis), https://hdl.handle.net/2077/75984

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.


  1. Afshari, Bahareh, and Kloibhofer, Johannes,Cut elimination for Cyclic Proofs: A case study in temporal logic,Proceedings of the 12th International Workshop on Fixed Points in Computer Science(Naples),EPTCS Proceedings,2024.
  2. Jaeger, Gerhard, and Kretz, Mathis, and Studer, Thomas,Cut–Free Axiomatizations for Stratified Modal Fixed Point Logic,Proceedings of Methods for Modalities 4(H. Schlingloff, editor),2005,pp. 125–143.

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


  1. A. Das and L. Melgaard,Cyclic Proofs for Arithmetical Inductive Definitions,8th International Conference on Formal Structures for Computation and Deduction, {FSCD},vol. 260,Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik,2023,pp. 27:1–27:18.
  2. G. Curzi and A. Das,Computational expressivity of (circular) proofs with fixed points,2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),IEEE,2023,pp. 1–13.
  3. Alex Simpson,Cyclic Arithmetic Is Equivalent to Peano Arithmetic,Foundations of Software Science and Computation Structures - 20th International Conference, {FOSSACS},vol. 10203,Lecture Notes in Computer Science,2017,pp. 283–300.

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


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.


  1. D. Mazza and K. Terui,Parsimonious Types and Non-uniform Computation,Automata, Languages, and Programming - 42nd International Colloquium,{ICALP},vol. 9135,Springer, 2015,pp. 350–361.
  2. S. Bellantoni and S. Cook,A New Recursion-Theoretic Characterization of the Polytime Functions (Extended Abstract),Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing,Association for Computing Machinery, 1992,pp. 283–293.
  3. G. Curzi andA. Das,Cyclic Implicit Complexity,Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science,Association for Computing Machinery,2022,pp. 1–13.
  4. G. Curzi andA. Das,Non-Uniform Complexity via Non-Wellfounded Proofs,31st {EACSL} Annual Conference on Computer Science Logic, {CSL}vol. 252,Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik,2023,pp. 16:1–16:18.

 Overview  Program