Abstract Cyclic Proofs

Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by a condition on the paths through the derivation graph, known as the global trace condition. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: First, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing the Ramsey trace condition.