Representation matters in cyclic proof theory

Abstract

Cyclic proof systems allowderivations whose underlying structure is a finite graph, rather than a well-founded tree. The soundness of cyclic proofs is usually ensured by imposing additional conditions beyond well-formedness. Distinct cyclic representations of the same logic can be obtained by combining the same stock of logical rules with different soundness conditions. This thesis is a compilation of work in cyclic proof theory with a focus on the representation of cyclic proofs. The perspective is justified two-fold: First, the choice of representation of cyclic proofs has significant impact on proof theoretic investigations of cyclic proofs, dictating the effort required to derive desired results. Second, arguments which focus on the ‘cyclic’ aspects of cyclic proof systems, such as proof representations, rather than relying on specifics of logics, transfer more easily between different logics. This thesis makes several contributions to the field of cyclic proof theory. First, we present a method for generating reset proof systems, a representation of cyclic proofs which has previously been key to proof theoretic investigations, from cyclic proof systems with global trace conditions, by far the most common representation of cyclic proofs in the literature. Because the method is presented in a generic manner, this yields reset proof systems for most logics considered in the cyclic proof theory literature. Second, we transfer a proof method of the equivalence of cyclic and ‘inductive’ proof systems, first employed by Sprenger and Dam, to the setting of Heyting and Peano arithmetic. Whereas previous proofs of this equivalence for arithmetic theories have relied on intricate arithmetical formalisations of meta-mathematical concepts, our proof operates at the level of cyclic proof representations. Third, using insights into the aforementioned proof method, we put forward a novel form of representation for cyclic proof systems which is of interest to cyclic proof theory beyond the proving of cyclic-inductive equivalences.