Cyclic Proof Theory

Abstract

Cyclic proofs are graphs, rather than trees, requiring additional soundness conditions to distinguish proofs from mere derivations. Using an abstract notion of cyclic proof system (CPS), this dissertation presents uniform results about different methods of representing the same CPS.

We prove that every traditional CPS can be represented as two other types of CPS: Reset proofs, which 'localise' soundness using a mechanism of sequent annotations, and stack-controlled proofs, introduced in this thesis, which align the cyclic and inductive structure of proofs.

Using stack-controlled proofs, we obtain multiple further results: a new translation from cyclic to 'plain' Heyting arithmetic; a correspondence between fragments of cyclic Peano arithmetic and the inductive fragments I$\Pi_n$; a proof-theoretic consistency argument for and ordinal annotation of cyclic Peano arithmetic; a general soundness argument for CPS which avoids the use of classical principles.

Reset proofs are employed to give a constructive analysis of the most common soundness condition for CPS. The condition is equivalent to the additive Ramsey theorem, the combination of two novel principles and, under unique choice, the LPO. The soundness condition can be constructivised by restricting it to periodic paths.