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

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