Abstract cyclic proofs

Abstract

Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by imposing a soundness condition on derivations. The most common such condition is the global trace condition (GTC), a condition on the infinite paths through the derivation graph. 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 a Ramsey-style trace condition. Furthermore, we connect our notion of trace to automata theory and prove that verifying the GTC for abstract cyclic proofs with certain trace conditions is PSPACE-complete.

1. Introduction

In a cyclic proof system, proofs are finite graphs which represent the ill-founded derivations obtained by unravelling them. Broadly speaking, the logics benefiting from cyclic proofs often feature notions of (co-)induction or fixed points (e.g., Brotherston 2006; Das 2021; Fortier and Santocanale 2013; Niwiński and Walukiewicz 1996; Simpson 2017; Sprenger and Dam 2003). Differing from conventional proof systems, cyclic systems typically eschew explicit induction axioms which can instead be simulated by cyclic derivations. Cut-free cyclic proof systems lend themselves well to proof theoretic investigations (e.g., Afshari and Leigh 2017; Afshari et al. 2021; Marti and Venema 2021) and proof search procedures (e.g., Brotherston et al. 2011, 2012; Tellez and Brotherston 2017).

Since cyclic proofs contain infinite paths, their soundness cannot be reduced to the local soundness of their derivation rules. Instead, one usually needs to impose further soundness conditions on these paths. The most common such condition is known as the global trace condition (GTC). While the concrete formulation of the trace condition differs between logics, it usually adheres to a certain form: a path satisfies the trace condition if it has a suffix along which some parameter (such as a term or fixed-point quantifier) can be traced and which progresses (e.g., decreases or is unfolded) infinitely often.

Motivated by this structural similarity, Brotherston (2006) developed an abstract framework to uniformly represent and reason about cyclic proof systems. The formalism has been used to give a general proof of the decidability of proof checking for cyclic proofs and to study various transformations of cyclic derivations which maintain the GTC. While Brotherston’s notion of trace condition encompasses most cyclic proof systems in the literature, it does not readily capture the common trace condition of $\mu$ -calculi, which hold a prominent position in cyclic proof theory.

This article introduces an abstract representation of cyclic proof systems which extends Brotherston’s approach. It is formed by an abstract, category theoretical rendition of cyclic derivations and their trace conditions. By replacing Brotherton’s notion of single progress points with a more nuanced, algebraic notion of progress, we are able to succinctly express most trace conditions, including those of $\mu$ -calculi. Our categorical formalism, in addition, allows for the composition of trace information, yielding two novel results: derivation compression and an alternative soundness condition. Derivation compression allows a cyclic derivation with n simple cycles to be represented as a graph of size O(n), which we believe should yield performance-gains in implementations of, for example, cyclic proof checking algorithms. Second, we give a soundness condition on derivations that induces a proof checking algorithm reliant on Ramsey’s theorem instead of automata-theoretic machinery. While a similar condition has been known in the field of program termination (Lee et al. 2001), this is, to the best of our knowledge, the first time such a condition has been considered for cyclic proofs. Furthermore, we reprove some known results to demonstrate applicability of our representation in cyclic proof theory: we show decidability of proof checking and regularisability of ill-founded proofs in finite proof systems via automata theory. Lastly, we show that the proof checking problem for our abstract notion of proof is PSPACE-complete.

Overview.

In Section 2, we introduce cyclic proof systems, the modal $\mu$ -calculus serving as a concrete example which is frequently revisited throughout the rest of the article. Section 3 presents our abstract notion of trace condition which is then used in Section 4 to introduce an abstract notion of cyclic derivation. In Section 5, we give a soundness condition, equivalent to the GTC, inspired by a result from program termination. Section 6 relates our abstract notion of trace to prevalent uses of automata theory in cyclic proof theory. In Section 7, we give a proof of the PSPACE-completeness of checking the GTC of abstract cyclic proofs with certain kind of trace conditions. We close with a discussion of related and future work in Section 8.

This article is an extended version of Afshari and Wehr (2022) with the following notable additions.

1. (1) The notion of trace interpretations is introduced in Section 3 to formally express the connection of concrete and abstract cyclic proofs.

2. (2) The connection between our notion of trace categories and the most common uses of automata theory in cyclic proof theory is included in Section 6.

3. (3) Section 7 is extended to incorporate a complete proof of PSPACE-hardness. By applying the automata-theoretic results of Section 6, it is shown that proof checking for certain trace categories is in PSPACE.

2. Cyclic Proof Systems

We begin by giving a general account of cyclic proof systems and their associated notion of cyclic proof. We illustrate the definitions by presenting a cyclic proof system for the modal $\mu$ -calculus from the literature.

A tree is a finite, non-empty set of sequences $T\subseteq \omega^*$ which is prefix closed, that is, if $tn \in T$ for $t \in \omega^*$ and $n \in \omega$ then $t \in T$ as well. We call $t \in T$ a node of T and any $tn \in T$ a child of t. A node $t\in T$ is a leaf of T if it has no children. The root of any tree T thus is the empty sequence $\varepsilon \in \omega^*$ . A cyclic tree is a pair $C = (T, \beta)$ consisting of a tree T and a partial function $\beta \colon \mathrm{Leaf}(T) \to T$ mapping (some) leaves of T to nodes of T with $\beta(s) \not\in \mathrm{dom}(\beta)$ for all $s \in \mathrm{dom}(\beta)$ . Each $s \in\mathrm{dom}(\beta)$ is called a bud and $\beta(s)$ its companion.

A derivation system is a triple consisting of a set of sequents , a set $\mathcal{R}$ of derivation rules and a rule interpretation such that for each $r \in \mathcal{R}$ , for some $n \in \omega$ . In this case, we call $\Gamma$ the conclusion of r and the $\Delta_i$ its premises. Henceforth, we refer to a derivation system simply by $\mathcal{R}$ . An $\mathcal{R}$ -pre-proof is a triple $\Pi = (C, \lambda, \delta)$ consisting of a cyclic tree $C = (T, \beta)$ together with a labelling such that $\lambda(t) = \lambda(\beta(t))$ for every $t \in \mathrm{dom}(\beta)$ . $\delta : T \setminus \mathrm{dom}(\beta) \to \mathcal{R}$ is a function with $\rho(\delta(t)) = (\Gamma,\Delta_1, \ldots, \Delta_n)$ , $\lambda(t) = \Gamma$ and $\lambda(ti)=\Delta_i$ where $\mathrm{Chld}(t) =\{t1, \ldots, tn\}$ for each $t \in \mathrm{dom}(\delta)$ . The sequent $\lambda(\varepsilon)$ is called the endsequent of $\Pi$ .

We denote by the set of $\mathcal{R}$ -pre-proofs. A cyclic proof system is a tuple consisting of a derivation system and a set called $\mathcal{R}$ -proofs. A pre-proof is said to satisfy the soundness condition of $\mathcal{R}$ if is an $\mathcal{R}$ -proof. An $\mathcal{R}$ -proof with endsequent $\Gamma$ is called a proof of $\Gamma$ . We extend the naming convention for derivation systems to cyclic derivation systems, referring to by $\mathcal{R}$ .

To illustrate these notions, we present a cyclic proof system for the modal $\mu$ -calculus. It will also serve as an example motivating the abstract definitions of Sections 3 and 4. This presentation of the system is taken from Afshari and Leigh (2017) and is an adaptation of the tableaux of Niwiński and Walukiewicz (1996). The choice of logic for this example is secondary, the main focus being the cyclic aspects of the proof system.

For a set of propositional letters and a countable set of variables, the $\mu$ -formulas are given by the following grammar:

If occur in $\varphi$ , we say x subsumes y, writing $x <_\varphi y$ , if $\sigma y.\psi$ occurs as a subformula of $\varphi$ for some $\sigma \in \{\mu, \nu\}$ and $\psi$ , and furthermore x is free in $\sigma y.\psi$ . If the relation $<_\varphi$ is a strict preorder, we call $\varphi$ well-named. In the remainder of this article, we assume all $\mu$ -formulas are well-named. This is a reasonable restriction as any $\mu$ -formula is $\alpha$ -equivalent to a well-named one. Any $\mu$ -formula is positive in all variables. The fixed-point formulas $\mu x.\varphi$ and $\nu x.\varphi$ denote, respectively, the least and greatest fixed point of the semantic counterpart to the function $x\mapsto\varphi(x)$ . These are well defined by the observation on positivity and the Knaster–Tarski theorem. The semantics of the modalities and connectives are as in the modal logic K.

The derivation rules of the cyclic $\mu$ -calculus are given in Fig. 1. The sequents of this calculus are finite sets of $\mu$ -formulas. Not all pre-proofs derive valid endsequents. For example, $\mu x.\Box x$ is invalid but is concluded by the $\mu$ -pre-proof given in Fig. 2. It is thus necessary to impose an additional soundness condition which delineates $\mu$ -proofs from $\mu$ -pre-proofs.

Figure 1. Derivation rules of the modal $\mu$ -calculus. $\Gamma$ ranges over finite sets of formulas; $\varphi[\psi / x]$ denotes the standard substitution of $\psi$ for x in $\varphi$ .

Figure 2. A $\mu$ -pre-proof of an invalid $\mu$ -formula. The dashed arrow represents the bud-companion relation $\beta$ .

A branch through a pre-proof $((T, \beta), \lambda, \delta)$ is an infinite sequence $t \in T^\omega$ such that $t_0 = \varepsilon$ and for any $t_i$ , either (a) $t_{i + 1} \in \mathrm{Chld}(t_i)$ or (b) $t_i \in \mathrm{dom}(\beta)$ and $t_{i + 1} = \beta(t_i)$ . This induces the sequence with $\Gamma_i := \lambda(t_i)$ and the partially defined $r : \omega \to \mathcal{R}$ with $r_i:= \delta(t_i)$ , both of which we use interchangeably with $t \in T^\omega$ to denote a branch.

Given a branch $(\Gamma_i)_{i \in \omega}$ through a $\mu$ -pre-proof, a formula $\varphi' \in \Gamma_{i + 1}$ is called a precursor of $\varphi \in \Gamma_i$ , written $\varphi' \leftarrow_i\varphi$ , if $t_{i + 1} \in \mathrm{Chld}(t_i)$ and either $\varphi$ is principal in $r_i$ , that is, $\varphi$ is ‘altered by $r_i$ ’, and $\varphi'$ is one of the residual formulas, or $\varphi$ is not principal in $r_i$ and $\varphi = \varphi'$ . If $t_i \in \mathrm{dom}(\beta)$ and $\varphi = \varphi'$ then $\varphi' \leftarrow_i \varphi$ as well. A sequence of formulas $(\varphi_i)_{i \in \omega}$ is called a trace along $(\Gamma_i)_{i \in \omega}$ if $\varphi_{i + 1} \leftarrow_i \varphi_{i}$ for all $i \in \omega$ . It is easily observed that the subsumption order is preserved along traces, that is, $\mathord{<_{\varphi_{i + 1}}} \subseteq \mathord{<_{\varphi_i}}$ whenever $\varphi_{i + 1} \leftarrow_i \varphi_i$ , which is why we henceforth associate with each trace $(\varphi_i)_{i \in \omega}$ a global subsumption order $\mathord{<_\varphi} := \mathord{<_{\varphi_0}} = \bigcup_{i \in \omega} \mathord{<_{\varphi_i}}$ .

Let $(\Gamma_i)_{i \in \omega}$ be a branch through a $\mu$ -pre-proof and $(\varphi_i)_{i \in \omega}$ a trace along it. The trace is called a $\nu$ -trace if there exists an such that $\varphi_i = \nu x.\psi$ and $\varphi_{i + 1} = \psi[\varphi_i / x]$ for infinitely many $i \in \omega$ , and furthermore for any if there are infinitely many $\varphi_i = \mu y.\theta$ then $x <_{\varphi} y$ . In other words, there is a greatest fixed-point variable x that occurs infinitely often and subsumes all infinitely occurring $\mu$ -variables. A $\mu$ -proof is a $\mu$ -pre-proof that satisfies the global trace condition, that is, every infinite branch has a $\nu$ -trace. As the unique branch through the pre-proof in the example of Fig. 2 does not have a $\nu$ -trace, it fails to be a proof.

At this point, we want to clearly distinguish between a ‘trace condition’ and a ‘global trace condition’. A trace condition is a specification of which traces along infinite branches of a pre-proof are considered progressing. A global trace condition is a certain type of condition on cyclic proofs, usually formulated via a trace condition, used to ensure soundness of proofs. Alternative soundness conditions have been considered, such as the reset condition (Jungteerapanich 2009), induction orders (Sprenger and Dam 2003) and trace manifolds (Brotherston 2006). These soundness conditions are often still defined in reference to a trace condition, or at least its implicit notion of progress. It is, therefore, possible for two differently formulated soundness conditions for a certain derivation system to share the same underlying trace condition. For example, this is the case for the GTC of the $\mu$ -proofs specified above and the reset proof system for the modal $\mu$ -calculus given by Stirling (2013).

3. Abstracting the Trace Condition

In this section, we demonstrate our formalism for capturing the trace conditions of cyclic proof systems. It encompasses two levels of abstraction: The notion of a trace category which captures what it means to be a trace condition, and a family of concrete trace categories, generated by the notion of an activation algebra.

An abstract notion of trace condition requires an abstract notion of branches through a proof. Working in a category theoretical framework, we observe that branches are infinite sequences of rule applications and identify them with infinite sequences of morphisms called paths. A trace condition is then a condition on such paths which is invariant under certain path transformations.

A semi-category is a category which may not have (all) identity morphisms. That is, a semi-category $\mathcal{C}$ consists of a collection of objects $\mathrm{Ob}(\mathcal{C})$ and collections of morphisms between each pair of objects $X, Y \in\mathrm{Ob}(\mathcal{C})$ . There is a composition which is associative. A semi-functor is a semi-category homomorphism. That is, for semi-categories $\mathcal{C}, \mathcal{D}$ , a semi-functor $F : \mathcal{C} \to \mathcal{D}$ consists of a map on objects $F_0 : \mathrm{Ob}(\mathcal{C}) \to \mathrm{Ob}(\mathcal{D})$ and a further map $F_2$ on morphisms of C such that for $f : X \to Y$ we have $F_1(f) : F_0(X)\to F_0(Y)$ . $F_1$ distributes over the composition operation, that is, $F_1(g \circ f) = F_1(g) \circ F_1(f)$ . As is also common for standard functors, we denote both $F_0$ and $F_1$ by F.

The standard $<$ -ordering of the natural numbers $\omega$ induces a semi-category whose objects are the natural numbers and in which there is a (unique) morphism between n and m, denoted ‘ $n < m : n \to m$ ’, if $n < m$ . The $\leq$ -ordering induces an analogous proper category. In this article, we denote both of these categories by $\omega$ ; which one is meant will be clear from the context.

A path through a category $\mathcal{T}$ is a functor $P \colon \omega \to \mathcal{T}$ . Given $P, P' \colon \omega \to \mathcal{T}$ , we call P a subpath of P’, written $P \subseteq P'$ , if there is a semi-functor $S \colon \omega \to \omega$ between the $\omega$ -semi-categories such that $P = P' \circ S$ . The transitive, symmetric closure of $\subseteq$ is denoted $\sim$ . This means $P \subseteq P'$ holds if P’ can be transformed into the P by applying a combination of two path transformations: (1) discarding a finite prefix of path P’, for example, by taking $S(m) := m + n$ . (2) Composing morphisms along P’. For example, if P’ is of the form

$$X_0^0 \xrightarrow{R^0_0} X_0^1 \xrightarrow{R^1_0} \cdots X_0^{n_0} \xrightarrow{R_0^{n_0}} X_1^0 \xrightarrow{R_1^0} \cdots X_1^{n_1} \xrightarrow{R_1^{n_1}} X_2^0 \xrightarrow{R_2^0} \cdots X_2^{n_2} \xrightarrow{R_2^{n_2}} ...$$

then $P \subseteq P'$ for the path P below

$$X_0^0 \xrightarrow{R^{n_0}_0 \circ \cdots \circ R^0_0} X_1^0 \xrightarrow{R^{n_1}_1 \circ \cdots \circ R^{0}_1 } X_2^0 \xrightarrow {R^{n_2}_2 \circ \cdots \circ R^{0}_2 } ...$$

witnessed by $S(i) := \sum_{j < i} (n_j + 1)$ .

Definition 3.1. Given a category $\mathcal{T}$ , a trace condition is a predicate on paths invariant under $\sim$ . That is, for any two paths $P \sim P'$ the trace condition holds for P if and only if it holds for P’.

A trace category is a category equipped with a trace condition.

Note that the notion of trace category in the above definition is unrelated to the ‘traced monoidal categories’ of Joyal et al. (1996).

Remark 3.1. Any trace condition is invariant under taking suffixes and composition. All concrete trace conditions in the literature are closed under taking suffixes, making closure under suffixes a natural criterion for identifying trace conditions.

Composition of rules along branches is not part of cyclic proof systems and hence there is a priori no precedent for it. The cumulative nature of trace conditions, however, suggests that composition of traces should not invalidate them. Indeed, all trace categories which we use to model concrete trace conditions from the literature have a trace condition closed under composition. Furthermore, it is precisely this closure condition that has proven instrumental in deriving new results in our framework.

The remainder of this section is concerned with defining a family of concrete trace categories which can model the trace conditions of many cyclic proof systems we know of.

Definition 3.2. An activation algebra is a tuple $\mathcal{A} = (A, \leq, \vee, 0, \alpha)$ consisting of a finite semilattice $(A, \leq, \vee, 0)$ and an activation element $\alpha \in A$ where $0 \neq \alpha$ . We often write $\mathcal{A}$ to refer to the carrier set A.

Definition 3.3. Let $\mathcal{A}$ be an activation algebra. The $\mathcal{A}$ -activated trace category $\mathcal{T}_\mathcal{A}$ has as its objects the finite sets. The morphisms between sets X, Y are relations $R \subseteq X \times \mathcal{A} \times Y$ . The identities are $1_X := \{(x, 0, x) ~|~ x \in X\}$ . We often write $x R^a y$ to mean $(x, a, y) \in R$ . Given morphisms $R \colon X \to Y, R' \colon Y \to Z$ , their composition is specified by $(x, c, z) \in R' \circ R$ iff

$$\exists y \in Y \exists a, b \in A.\;(x, a, y) \in R \mathrm{ and } (y, b, z) \in R' \mathrm{ and } a \vee b = c.$$

A path $P \colon \omega \to \mathcal{T}_\mathcal{A}$ satisfies the trace condition if there exists a subpath $P' \subseteq P$ and a sequence $\sigma \colon \Pi i \in \omega. P'(i)$ along it such that $\sigma_i P'(i < i + 1)^\alpha \sigma_{i + 1}$ for all $i \in \omega$ .

Example 3.1. The simplest example of an activation algebra is given by the simplest semilattice of at least two elements: the binary Boolean algebra $\mathbb{B} = \{\top, \bot\}$ . The choice $\alpha := \top$ is forced as necessarily $\bot = 0 \neq \alpha$ . This activation algebra is implicit in Brotherston’s (2006) abstract notion of trace and suffices to model most trace conditions in the literature.

Example 3.2. The activation algebra used to formalise the trace condition of the modal $\mu$ -calculus is the three-value failure algebra $\mathbb{F} := (\{0, 1, 2\}, \leq, \vee, 0, 1)$ . In this algebra, the value 2 can be used to represent a ‘failure’ state (see the proof of Proposition 3.1).

Example 3.3. More complex examples are the ‘k out of n’ algebras for $0 < k \leq n$ given by ${n \choose k} := (A, \leq, \vee, \emptyset, \alpha)$ where $A := \{X \subseteq n ~|~ \left|X\right| < k\} \cup \{\alpha\}$ , the order $\leq$ is such that $X \leq Y$ iff $X \subseteq Y$ for $X, Y \subseteq n$ , and $a \leq \alpha$ for all $a \in A$ . More concretely, observe the Hasse diagram of ${3 \choose 2}$ .

The idea behind ${n \choose k}$ is to view the singleton sets $\{i\}$ as ‘events’ which can occur along a trace. To achieve activation, k distinct ‘events’ need to take place along a segment. As opposed to $\mathbb{B}$ and $\mathbb{F}$ , we are not yet aware of a cyclic proof system whose trace condition is best expressed in terms of some ${n \choose k}$ (except of course ${1 \choose 1}$ which the same as $\mathbb{B}$ ). We conjecture that cyclic proof systems whose trace condition is naturally modelled in some non-trivial ${n \choose k}$ would require a kind of fairness condition of their progressing traces.

Lemma 3.1. The trace condition in Definition 3.3 is well defined, that is, it fulfils the invariance condition of Definition 3.1.

Proof. It suffices to prove invariance under $\subseteq$ . Let $P \subseteq Q$ with $P = Q \circ S$ . Suppose P satisfies the trace condition meaning there exists $P' \subseteq P$ with $P' = P \circ S'$ and a validating sequence $\sigma$ . Then, $P' \subseteq Q$ via $P' = Q \circ S \circ S'$ , meaning $\sigma$ is a validating sequence through a subpath of Q as well.

For the converse direction, let $P = Q \circ S$ and suppose Q satisfies the trace condition as witnessed by $Q' = Q \circ S'$ and a sequence $\sigma \colon \Pi i \in \omega. Q'(i)$ . It remains to show that there is $P' \subseteq P$ and a suitable sequence $\sigma'' : \Pi i \in \omega.P'(i)$ along it. By fixing $b := S'(0)$ and analysing Definition 3.3, one can conclude there are two sequences $\sigma' \colon \Pi i \in \omega. Q(b + i)$ and $a \colon \omega \to \mathcal{A}$ such that $\sigma'_i\, Q(b + i < b + i + 1)^{a_i}\,\sigma'_{i + 1}$ with $a_i \leq \alpha$ . For $i_j := S'(j) - b$ , we then have $\sigma'_{i_j} = \sigma_j$ and $\bigvee_{i = i_j}^{i < i_{j + 1}} a_i = \alpha$ . Now construct the following sequence:

\begin{align*} k_0 & \,:= \mathrm{least } i \in \omega \mathrm{ such that } S(i) \geq b \\ k_{n + 1} & \,:= \mathrm{least } i > k_n \mathrm{ s.t. } S(k_n) \leq S'(j) < S'(j + 1) \leq S(i) \mathrm{ for some } j \in \omega \end{align*}

We claim setting $S''(i) := S(k_i)$ induces the desired subpath $P' := Q \circ S'' P$ with $P'(i) = P(k_i)$ as witnessed by $\sigma'' \colon \Pi i \in \omega. P'(i)$ given by $\sigma''_{i} := \sigma'_{S(k_i)}$ . For this, we need to check that $\sigma''_{i + 1}\,P'(i < i + 1)^\alpha\,\sigma''_{i + 1}$ . Let $j \in \omega$ be such that $S''(i) \leq S'(j) < S'(j + 1) \leq S''(i + 1)$ . Then, $P'(i < i + 1) = Q(b + i_{j + 1} \leq S(k_{i + 1})) \circ Q(b + i_j < b + i_{j + 1}) \circ Q(S(k_i) \leq b + i_j)$ , meaning

$$\left(\sigma''_i, \underbrace{\bigvee_{l = b + i_{j + 1}}^{l < S(k_{i + 1})} a_{l - b}}_{\leq \alpha} \vee \underbrace{\bigvee_{l = i_j}^{l < i_{j + 1}} a_l}_{= \alpha} \vee \underbrace{\bigvee_{l = S(k_i)}^{l < b + i_{j}} a_{l - b}}_{\leq \alpha}, \underbrace{\sigma'_{k_{i + 1} - b}}_{= \sigma''_{i + 1}}\right) \in P'(i < i + 1)$$

and thus $(\sigma''_i, \alpha, \sigma''_{i + 1}) \in P'(i < i + 1)$ as desired.

We now proceed to demonstrate how trace categories can be used to specify the trace conditions and, thereby, the GTCs of cyclic proof systems. Fix a derivation system and a trace category $\mathcal{T}$ . A trace interpretation $\iota : \mathcal{R} \to \mathcal{T}$ consists of a function mapping sequents to their trace sets and for each rule $r\in \mathcal{R}$ with $\rho(r) = (\Gamma, \Delta_1,\ldots, \Delta_n)$ a morphism $r_i : \iota(\Gamma) \to \iota(\Delta_i)$ for each $1 \leq i \leq n$ called a trace map. Let $(C, \lambda, \delta)$ be a pre-proof and $t \in T^\omega$ be a branch through C. Its corresponding path $P : \omega \to \mathcal{T}$ is defined as follows:

$$P(i) := \iota(\lambda(\pi_i)) \qquad P(i < i + 1) := \begin{cases} r_j : \iota(\lambda(\pi_i)) \to \iota(\lambda(\pi_{i + 1})) & \pi_i \not\in \mathrm{Leaf}(T) \mathrm{ and } \pi_{i + 1} = \pi j \\ 1_{P(i)} & \pi_i \in \mathrm{dom}(\beta) \end{cases}$$

This induces a cyclic proof system in which contains those $\mathcal{R}$ -pre-proofs for which every induced path $P : \omega \to \mathcal{T}$ through them satisfies the trace condition of $\mathcal{T}$ .

In the following, we demonstrate how to specify the trace condition for the modal $\mu$ -calculus by a trace interpretation $\iota : \mu \to \mathbb{F}$ .

Definition 3.4. The trace interpretation $\iota \colon \mu \to \mathcal{T}_\mathbb{F}$ is given by in which . For each $r \in \mu$ with $\rho(r) = (\Gamma, \Delta_1, \ldots, \Delta_n)$ , the trace maps $r_i \colon \iota(\Gamma) \to \iota(\Delta)$ are defined by $ r_i := \{((\varphi, x), a^*, (\varphi', x)) ~|~ \varphi' \leftarrow_r^i \varphi \} $ where $a^*$ is defined by:

$$ a^* := \begin{cases} 2, & \mathrm{ if }r \mathrm{ instance of } \mu, \varphi = \mu y.\theta, \varphi' = \theta[\mu y.\theta / y] \mathrm{ and } y <_{\varphi} x, \\ 1, & \mathrm{ if } r \mathrm{ instance of } \nu, \varphi = \nu x.\theta, \varphi' = \theta[\nu x. \theta / x], \\ 0, & \mathrm{ otherwise.} \end{cases} $$

Proposition 3.1. The notion of $\mu$ -proofs and that induced by $\iota : \mu \to \mathbb{F}$ coincide.

Proof. It suffices to prove that a branch $(\Gamma_i)_{i \in \omega}$ through a $\mu$ -pre-proof has a $\nu$ -trace if and only if its induced path $P \colon \omega \to \mathcal{T}_\mathbb{F}$ satisfies the trace condition of $\mathcal{T}_\mathbb{F}$ .

Suppose $(\Gamma_i)_{i \in \omega}$ has a $\nu$ -trace $(\varphi_i)_{i \in \omega}$ . Then there exists bounded by a $\nu$ -quantifier and an increasing sequence $(j_i)_{i \in \omega}$ such that

1. (i) $\varphi_{j_i} = \nu x.\psi$ and $\varphi_{j_i + 1} = \psi[\varphi_{j_i} / x]$ , and

2. (ii) no formula $\mu y.\theta$ with $y <_{\varphi} x$ is unfolded along $(\varphi_{i})_{i>j_0}$ .

The subpath $P \circ S \subseteq P$ induced by $S(i) := j_{i}$ and the sequence $\sigma_i := (\varphi_{j_{i}}, x)$ witness that P satisfies the trace condition: clearly always $(\sigma_i, a, \sigma_{i + 1}) \in P(j_{i}, j_{i + 1})$ for some $a \in \mathbb{F}$ . We know $1 \leq a$ since between $\Gamma_{j_i}$ and $\Gamma_{j_{i + 1}}$ , $\nu x.\psi$ is unfolded, and further $a < 2$ , as no $\mu y.\theta$ with $y <_{\varphi} x$ is unfolded after $j_0$ , yielding $a = 1$ as desired.

Conversely, suppose P satisfied the trace condition. Then there exist $S \colon \omega \to \omega$ and $\sigma \colon \Pi i \in \omega.~P(S(i))$ such that $(\sigma_{i}, 1, \sigma_{i + 1}) \in P(S(i < i + 1))$ for every $i \in \omega$ . Necessarily, $\sigma_i = (\varphi_i, x)$ for some fixed $\nu$ -variable x and $\varphi_i \in \Gamma_{S(i)}$ . Furthermore, because the activation algebra element along that trace is precisely 1, we can conclude that between $\Gamma_{S(i)}$ and $\Gamma_{S(i + 1)}$ :

1. (i) the formula $\nu x.\psi$ corresponding to x in $\varphi_i$ is unfolded (as $1 \leq \alpha$ ),

2. (ii) no $\mu y.\theta$ with $y <_{\varphi} x$ is unfolded (as $\alpha < 2$ ).

By scrutinising the derivation rules, it can be deduced that $\varphi_{S(0)}$ can be ‘traced back’ to some $\varphi \in \Gamma_0$ and subsequently completed into a trace $(\varphi'_i)_{i \in \omega}$ along $(\Gamma_i)_{i \in \omega}$ with $\varphi'_{S(i)} = \varphi_i$ . By the observations above, this must be a $\nu$ -trace.

Remark 3.2. We have claimed that the trace condition given for the modal $\mu$ -calculus in Section 2 cannot be represented naturally in terms of the activation algebra $\mathbb{B}$ . From the description in Section 2, it is clear that any natural representation of it as $\iota : \mu \to \mathcal{T}_\mathbb{B}$ must coincide with the trace interpretation given in Definition 3.4 on trace objects and relations. That is, $\iota(\Gamma)$ must be the set (or equivalent) and for a derivation rule with $\rho(r) = (\Gamma, \Delta_1, \ldots, \Delta_n)$ any $((\varphi, x), a, (\varphi', y)) \in r_i : \iota(\Gamma) \to \iota(\Delta_i)$ should be such that $\varphi' \leftarrow_r^i \varphi$ and $x = y$ . It thus remains to describe how to assign the values a in the triples in $r_i$ . Clearly, non-unfolding rules should assign $a = 0$ and $\nu$ -unfoldings $a = 1$ . For $\mu$ -unfoldings, if such an unfolding occurs infinitely often, the trace should be ‘spoiled’. Neither an assignment of $a = 0$ nor $a = 1$ can model this behaviour. The assignment of $a = f$ in Definition 3.4 on the other hand, succinctly takes care of this case.

For further examples of modelling of the trace conditions of cyclic proof systems in trace categories, in particular, those of cyclic arithmetic (Simpson 2017), $\mathrm{HFL}_\mathbb{N}$ (Kori et al. 2021) and Grzegorczyk modal logic (Savateev and Shamkanov 2021), we refer the reader to Wehr (2021).

We close this section by stressing that the purpose of activation algebras is to specify trace conditions of cyclic proof systems in a natural manner. Indeed, if naturality is of no concern, the following result shows that the trace category $\mathcal{T}_\mathbb{B}$ , or equivalently the formalism of Brotherston (2006), is sufficient to model the majority of trace conditions from the literature, including that of the modal $\mu$ -calculus.

Concretely, the notion of naturality we allude to here is embodied in the fact that the information of traces may be separated into two parts: the elements of the trace sets signify which objects is being tracked, while the elements of the activation algebra describe how progress of these trace objects is detected. Indeed, Theorem 3.1 is achieved by collapsing this separation. An example of the importance of maintaining this distinction is given by (Leigh and Wehr 2023): the article describes how to generate so-called reset proof systems for cyclic proof systems whose trace condition is specified in terms of a trace interpretation into some $\mathcal{A}$ -activated category. One of the examples considered there is the modal $\mu$ -calculus. The trace interpretation in terms of $\mathbb{F}$ (as in Definition 3.4) leads to a very natural reset system, whereas the reset system induced by the trace interpretation into $\mathbb{B}$ given by Theorem 3.1 would be highly artificial.

Theorem 3.1. For any activation algebra $\mathcal{A}$ , there exists a function I mapping objects of $\mathcal{T}_\mathcal{A}$ to objects of $\mathcal{T}_\mathbb{B}$ and maps $R : X \to Y$ in $\mathcal{T}_\mathcal{A}$ to maps $I(R) : I(X) \to I(Y)$ in $\mathcal{T}_\mathbb{B}$ . Furthermore, associate to each path $P : \omega \to \mathcal{T}_\mathcal{A}$ a path $\hat{P} : \omega \to \mathcal{T}_\mathbb{B}$ given by $\hat{P}(i) := I(P(i))$ and $\hat{P}(i < i + 1) := I(P(i < i + 1))$ . Then P satisfies the trace condition iff $\hat{P}$ does.

Proof. Writing $\mathcal{A} = (A, \leq, \vee, 0, \alpha)$ , take $I(X) := X \times A$ and, for $R : X \to Y$ ,

$$ I(R) :=~ \{((x, a), \bot, (y, a \vee b)) ~|~ a \in A, x R^b y\} \cup~ \{((x, a), \top, (y, 0)) ~|~ a \in A, x R^b y, a \vee b = \alpha\} $$

Suppose that P satisfied the trace condition. That means there is a subpath $P \circ S$ and a sequence $\sigma : \Pi i \in \omega. P(S(i))$ such that $\sigma_{i} P(S(i))^\alpha \sigma_{i + 1}$ . We claim that $\hat{P} \circ S$ is the witnessing subpath of P with the sequence $\hat{\sigma} : \Pi i \in \omega. \hat{P}(S(i))$ given by $\hat{\sigma_i} := (\sigma_i, 0)$ . We prove that $\hat{\sigma}_{i} \hat{P}(S(i < i + 1))^{\top} \hat{\sigma}_{i + 1}$ : There must be $\sigma_i = x_0, ..., x_n = \sigma_{i + 1}$ and $a_0, ..., a_{n - 1}$ for $n := S(i + 1) - S(i)$ and $b := S(i)$ such that $x_j P(b + j)^{a_j} x_{j + 1}$ and $\alpha = \bigvee_{j < n} a_j$ . Then define $\hat{x}_j := (x_j, \bigvee_{k < j - 1}a_k)$ and observe that $\hat{\sigma}_i = \hat{x}_0 \hat{P}(b)^{\bot} \hat{x}_1 \hat{P}(b + 1)^{\bot} ... \hat{x}_{n - 1} \hat{P}(b + n - 1)^{\top} (x_n, 0) = \hat{\sigma}_{i + 1}$ because $\hat{x}_{n-1} = (x_{n-1}, \bigvee_{k < n - 2} a_k)$ and $(\bigvee_{k < n - 2} a_k) \vee a_{n - 1} = \alpha$ .

Conversely, suppose that $\hat{P}$ satisfied the trace condition. Then there is a subpath $\hat{P} \circ S$ and a sequence $\hat{\sigma} : \Pi i \in \omega. \hat{P}(S(i))$ such that $\hat{\sigma}_i \hat{P}(S(i < i + 1))^{\top} \hat{\sigma}_{i + 1}$ . There must be $\sigma_i = (x_0, a_0), ..., (x_n, a_n) = \sigma_{i + 1}$ and $b_0, ..., b_{n - 1} \in \mathbb{B}$ for $n := S(i + 1) - S(i)$ and $k := S(i)$ such that $(x_j, a_j) \hat{P}(k + j)^{b_j} (x_{j + 1}, a_{j + 1})$ and $\top = \bigvee_{j < n} b_j$ . Per construction, the latter means there is some $J < n$ such that $(x_J, a_J) \hat{P}(k + J)^\top (x_{J + 1}, 0)$ . Consider analogous $\sigma_{i + 1} = (x'_0, a'_0), \ldots, (x'_m, a'_m) = \sigma_{i + 2} $ and $b'_0, ..., b'_{m - 1} \in \mathbb{B}$ such that $(x'_j, a'_j) \hat{P}(k' + j)^{b'_j} (x'_{j + 1}, a'_{j + 1})$ with $k' := S(i + 1)$ , yielding an analogous J’ such that $(x'_{J'}, a'_{J'}) \hat{P}(k + J')^\top (x_{{J'} + 1}, 0)$ . Intuitively, this means that the $a_j$ and $a'_j$ between $(x_{J + 1}, 0)$ and $(x'_{J' + 1}, 0)$ ‘accumulate’ activation algebra elements up to $\alpha$ . That is, there must be $c_0, \ldots, c_{l - 1} \in A$ with $l := n - (J + 1) + (J' + 1)$ such that $\alpha = \bigvee_{j < l} c_j$ and $x_{J + 1} P(k + J + 1 < k + J + 2)^{c_0} \ldots P(k + n - 1 < k + n)^{c_{n - J - 1}} x_n = x'_0 P(k' < k' + 1)^{c_{n - J}} \ldots P(k' \!+ J' < k' + J'\!+ 1)^{c_{l-1}} x'_{J' \!+ 1}$ . In other words, $x_{J + 1} P(k + J + 1 < k' + J' + 1)^\alpha x'_{J' + 1}$ , which can be extended to $x_0 P(k < k' + m)^\alpha x'_m$ by observing that necessarily $a_j < \alpha$ and $a'_j < \alpha$ for all $j < n$ and $j < m$ , respectively, for the original trace along $\hat{P}$ to be successful. Based on this observation, we may conclude that the subpath $P \circ S'$ of P with $S'(i) = S(2i)$ satisfies the trace condition for the sequence $\sigma' : \Pi i \in \omega. P(S'(i))$ with $\sigma'_i := \pi_1(\sigma_{2i})$ , that is, $\pi_1(\sigma_{2i}) P(S(2i < 2i + 2))^\alpha \pi_1(\sigma_{2i + 2})$ as demonstrated above.

Remark 3.3. The statement of Theorem 3.1 is given in terms of functions, rather than functors. This is so because the resulting functions fail to be functors on both accounts: preserving identities and distributing over composition. The failure of identity preservation is easily observed. Notice that any $I(1_X)$ will contain triples of the form $((x, \alpha), \top, (x, 0))$ which the identities of $\mathcal{T}_\mathbb{B}$ do not contain. This issue could be alleviated by taking the definition to be

\begin{align*} I(R) :=~ & \{((x, a), \bot, (y, a \vee b)) ~|~ a \in A, x R^b y\} \\ \cup~ & \{((x, a), \top, (y, 0)) ~|~ a \in A \setminus \{\alpha\}, x R^b y, a \vee b = \alpha\} \end{align*}

instead, that is, explicitly excluding that kind of transition. However, as this still does not resolve the distributivity over composition, we chose to forgo this in favour of a simpler definition and proof.

The failure of distributivity over composition is a bit more subtle. For this, suppose there were $a < b < c < \alpha \in A$ such that $a \vee b = \alpha$ and consider $R := \{(\star, b, \star)\} $ and $ R' := \{(\star, c, \star)\}$ . Then clearly, $(\star, a) \, I(R)^{\top}\, (\star, 0)\, I(R')^{\bot}\, (\star, c)$ . However, as $R' \circ R = \{(\star, b \vee c, \star)\}$ , the only two transitions possible via $I(R' \circ R)$ are $(\star, a)\, I(R' \circ R)^{\bot}\, (\star, \alpha)$ and $(\star, a)\, I(R' \circ R)^{\top}\, (\star, 0)$ . Thus, $I(R') \circ I(R) \neq I(R'\circ R)$ .

4. Abstract Cyclic Derivations

This section combines the abstract notions of branches, traces and the trace condition into an abstract presentation of cyclic derivations. Abstract cyclic derivations (ACDs) are pairs $(C, \mathrm{Tr})$ of cyclic trees C and maps Tr which ‘decorate’ the edges of C with maps of a trace category. Such an ACD is considered to be a proof if all paths which can be generated by traversing C satisfy the trace condition imposed by the trace category. To express these ideas in a category theoretical manner, we begin by giving a categorical representation of cyclic trees, by defining the (semi-)category induced by the finite paths through these trees.

Fix a cyclic tree $C = (T, \beta)$ . The finite paths from s to t, denoted by $\mathrm{Path}_C(s, t) \subseteq T^+$ , are defined as the smallest sets satisfying the following three conditions:

1. (1) For any $s \in T$ , we have $s \in \mathrm{Path}_C(s, s)$ ,

2. (2) For any $t, u \in T$ with u child of t, if $p \in \mathrm{Path}_C(s, t)$ then $pu \in \mathrm{Path}_C(s, u)$ ,

3. (3) For any $t \in \mathrm{dom}(\beta)$ , if $p \in \mathrm{Path}_C(s, t)$ then $p\beta(t) \in \mathrm{Path}_C(s, \beta(t))$ .

The category $\mathcal{P}_C$ of paths through $C = (T, \beta)$ has the nodes of T as its objects and fixes . The identities are $1_s = s \colon s \to s$ and, given morphisms $p \colon s \to t$ and $q \colon t \to u$ , we define $q \circ p = pq'$ where $q = tq'$ for $q' \in T^*$ . The semi-category $\mathcal{P}^S_C$ of progressing paths is the same as $\mathcal{P}_C$ except that .

The informal notion of ‘decorating a cyclic tree with trace information’ can thus be expressed as a functor.

Definition 4.1. An abstract cyclic derivation over a trace category $\mathcal{T}$ is a pair $(C, \mathrm{Tr})$ consisting of a cyclic tree $C = (T, \beta)$ and a functor $\mathrm{Tr} \colon \mathcal{P}_C \to \mathcal{T}$ such that for any $s \in \mathrm{dom}(\beta)$ , $\mathrm{Tr}(s) = \mathrm{Tr}(\beta(s))$ and $\mathrm{Tr}(s\beta(s)) = 1_{\mathrm{Tr}(s)}$ .

We delineate the abstract cyclic proofs from mere ACDs via a GTC.

Definition 4.2. Let D be an ACD given by $(C, \mathrm{Tr} \colon \mathcal{P}_C \to \mathcal{T})$ . A path through D is a path $P : \omega \to \mathcal{T}$ such that there exists a semi-functor $P' \colon \omega \to \mathcal{P}^S_C$ with $P = \mathrm{Tr} \circ P'$ . D satisfies the GTC if every path through D satisfies the trace condition of $\mathcal{T}$ . We call an ACD satisfying the GTC an abstract cyclic proof.

Requiring P’ to be a semi-functor in the definition above rules out constant ‘paths’ obtained via $P(i) := \mathrm{Tr}(s), P(i < i + 1):= 1_{\mathrm{Tr}(s)}$ which are not generated by traversing the ACD along any branch of the cyclic tree.

As ACDs serve as an abstract representation of pre-proofs, each pre-proof naturally induces an ACD.

Definition 4.3. Let be a cyclic proof system whose soundness condition is induced by a trace interpretation $\iota : \mathcal{R} \to \mathcal{T}$ . Any pre-proof $(C, \lambda, \delta)$ induces an abstract cyclic derivation $(C, \mathrm{Tr})$ with

\begin{align*} \mathrm{Tr}(s) := \iota(\lambda(s)) \qquad \quad \mathrm{Tr}(s < si) := r_i : \iota(\lambda(s)) \to \iota(\lambda(si)) \mathrm{ where } r = \delta(s)\end{align*}

Example 4.1. Consider the $\mu$ -pre-proof and its corresponding ACD depicted in Fig. 3. For the sake of readability, we have opted to write the carrier sets of the ACD as simple sets of variables x, y, etc., instead of sets of pairs $(\varphi, x), (\psi, y)$ , etc., since each variable occurs in only one of the formulas in the sequent. Fully specified, the first set should be $\{(\nu x.x, x), (\mu y.\nu z.y, z)\}$ . The annotated morphisms are $1 := \{(x, 0, x), (z, 0, z)\}$ , $ R_x := \{(x, 1, x), (z, 0, z)\}$ , $R_y := \{(x, 0, x), (z, 2, z)\}$ and $R_z := \{(x, 0, x), (z, 1, z)\}$ .

Figure 3. A $\mu$ -proof and its corresponding ACD, discussed in Example 4.1.

Note that $(z, 2, z) \in R_y$ as $y <_\varphi z$ with $\varphi := \mu y.\nu z.y$ . The $\mu$ -pre-proof above has only one branch $\Gamma$ which has one $\nu$ -trace (that on x) and is thus a proof. Similarly, its corresponding path $\hat{\Gamma} : \omega \to \mathcal{T}_\mathbb{F}$ is a path through the ACD and satisfies the trace condition with $S(i) := 5i$ and $\sigma := i \mapsto x$ . In principle, verifying that the ACD is a proof would require checking infinitely many other paths P. This is because paths through ACDs need not start at their root and a step $P(i < i + 1)$ may correspond to a path segment $p \in \mathrm{Path}_C(s, t)$ with $\left|p\right| > 2$ . However, as all such paths are subpaths of $\hat{\Gamma}$ , they satisfy the trace condition by subpath invariance. Indeed, this observation extends to arbitrary ACDs obtained by transforming concrete cyclic derivations: any path through an ACD is always a subpath of $\hat{\Gamma}$ for some branch $\Gamma$ through the corresponding concrete cyclic derivation. This means that the GTC in Definition 4.2, although it may have seemed stricter than needed, corresponds precisely to that of concrete cyclic proof systems.

We close this section by showing that, via composition of trace maps, ACDs can be transformed into equivalent ACDs whose number of nodes $\left|T\right|$ is linear in their number of cyclic edges $\left|\beta\right|$ . For ACDs generated from concrete cyclic derivations, as defined in Definition 4.3, this will usually result in a drastic reduction of $\left|T\right|$ . The procedure can be viewed as a sort of ‘compression algorithm’ which could prove useful for implementing programs, such as proof checking (cf. Theorem 5.3), that have $\left|T\right|$ as one of their complexity parameters. Indeed, it seems the automated theorem prover CYCLIST already relies on a similar optimisation (see Brotherston et al. 2012, Section 4.2) though we are not aware of a formal characterisation of this optimisation in the literature. An example illustrating the procedure is given in Figure 4.

Figure 4. Compressing an ACD via the procedure outlined in the proof of Theorem 4.1.

Theorem 4.1. Any $D = ((T, \beta), \mathrm{Tr})$ can be transformed into $D' = ((T', \beta'), \mathrm{Tr}')$ such that D’ is a proof if and only if D is a proof and $\left|T'\right| \leq 2 \left|\beta\right| + 1$ .

Proof. Fix $B := \mathrm{im}(\beta) \cup \mathrm{dom}(\beta) \cup \{\varepsilon ~|~ \nexists s \in \mathrm{im}(\beta).\forall t \in \mathrm{im}(\beta) \cup \mathrm{dom}(\beta).~s \leq t\}$ , where $s <t$ if t is a proper prefix of s. We now construct a sequence of partial maps $(f_i \colon B \to \omega^*)_i$ . Fix $f_0(s) := \varepsilon$ where s is the $<$ -least element of B. To construct $f_{n + 1}$ consider each $s \in \mathrm{dom}(f_n)$ , that is, every $s \in B$ which was added by the previous construction step. For each such s, let $\{t_0, \ldots, t_n\} \subseteq B$ be all $t \in B$ such that s can reach t without crossing any other node from B (formally, if there is $spt \in \mathrm{Path}_C(s, t)$ with $p \in (T \setminus B)^*$ ) and set $f_{n + 1}(t_i) := f_n(s)i$ . Fixing $f := \bigcup_{n \leq \left|B\right|}f_n$ and $T' := \mathrm{im}(f)$ , observe that $f \colon B \to T'$ is a $<$ -isomorphism between B and T’. Thus $C' := (T', \beta' := f \circ \beta \circ f^{-1})$ is a cyclic tree with $\beta'(x) = y$ iff $\beta(f^{-1}(x)) = f^{-1}(y)$ . Also, clearly $\left|T'\right| = \left|B\right| \leq 2 \left|\beta\right| + 1$ .

To extend C’ to an ACD D’, take $\mathrm{Tr}'(s) := \mathrm{Tr}(f^{-1}(s))$ for $s \in T'$ . For any $s < t \in T'$ , observe that per construction of T’, there exists a unique path $f^{-1}(s)p_{st}f^{-1}(t) \in \mathrm{Path}_C(f^{-1}(s), f^{-1}(t))$ with the property that $p_{st} \in (T \setminus B)^*$ . Pick $\mathrm{Tr}'(st) := \mathrm{Tr}(f^{-1}(s)p_{st}f^{-1}(t))$ and note that this is both well defined and fully specifies $\mathrm{Tr}' \colon \mathcal{P}_{C'} \to \mathcal{T}$ . The claim now follows from the following fact, which is easily verified: for any path P through D, there exists a path $P' \sim P$ through D’ and vice versa.

5. A Ramsey-based Soundness Condition

This section presents a soundness condition on pre-proofs which is equivalent to the common global trace condition. It is similar to the condition put forward by Lee et al. (2001) for the purpose of program termination based on the size-change principle, a condition analogous to the trace conditions of cyclic proof systems such those put forward in Sprenger and Dam (2003) and Simpson (2017). The correctness proof of the soundness condition relies on Ramsey’s (1930) theorem, rather than the automata-theoretic methods prevalent in cyclic proof theory. We employ the notation $[A]^n := \{X \subseteq A ~|~ \left|X\right| = n\}$ .

Theorem 5.1. Ramsey’s theorem. Let A be a countable set, C finite and $n \in \omega$ . For any colouring $f \colon [A]^n \to C$ , there exists a colour $c \in C$ and a countable $B \subseteq A$ such that $f(X) = c$ for any $X \in [B]^n$ .

The central insight motivating the soundness condition is that the Ramsey theorem guarantees the existence of certain well-behaved subpaths of paths through -finite categories. For every $R \colon X \to X$ in a category $\mathcal{T}$ , the periodic R path is $R^\omega \colon \omega \to \mathcal{T}$ with by $R^\omega(i) := X$ and $R^\omega(i < i + 1) := R$ . A morphism $R \colon X \to X$ is idempotent if $R = R \circ R$ .

Lemma 5.1. Let $P \colon \omega \to \mathcal{T}$ be a path and $X \in \mathrm{Ob}(\mathcal{T})$ such that $P(i) = X$ infinitely often. If is finite, then $R^\omega \subseteq P$ for some idempotent $R \colon X \to X$ .

Proof. $P(i) = X$ holding infinitely often means there exists $Q \subseteq P$ such that $Q(i) = X$ for all $i \in \omega$ . Then $Q(\{i, j\}) := Q(i < j)$ induces a colouring on $\omega$ . By the Ramsey theorem, there exists and an infinite $M \subseteq \omega$ such that $Q(i < j) = R$ for $i < j \in M$ . Then, $R^\omega = Q \circ S$ where $S(i) := \mathrm{ the } i\mathrm{th least } m \in M$ . The idempotence of R follows as $R = Q(S(0 < 2)) = Q(S(1 < 2)) \circ Q(S(0 < 1)) = R \circ R$ .

Similarly to Definition 4.2, we limit our attention to the image of the trace functor $\widehat{\mathrm{T}}\mathrm{r} \colon \mathcal{P}^S_C \to \mathcal{T}$ restricted to the category of progressing paths. Fixing some ACD $(C, \mathrm{Tr}),$ we thus write for , that is, the set of all trace maps that can be generated by walking along some path $p \in \mathrm{Path}_C(s, t)$ with $\left|p\right| >1$ .

Definition 5.1. Let $(C, \mathrm{Tr})$ be an ACD such that for every $u \in \mathrm{dom}(\beta)$ , is finite. Then it satisfies the Ramsey trace condition if for every $u \in \mathrm{dom}(\beta)$ and every idempotent , the path $R^\omega \colon \omega \to \mathcal{T}$ satisfies the trace condition.

Theorem 5.2. Let $(C, \mathrm{Tr})$ be an ACD such that for every $u \in \mathrm{dom}(\beta)$ , is finite. Then it satisfies the GTC if and only if it satisfies the Ramsey trace condition.

Proof. First, suppose D satisfies the GTC. Then pick $u \in \mathrm{dom}(\beta)$ and . As R is in the image of $\hat{\mathrm{Tr}}$ , we know that there exists some $p \in \mathrm{Path}_C(u, u)$ with $\left|p\right| > 1$ and $\mathrm{Tr}(p) = R$ . Then $R^\omega = \mathrm{Tr} \circ p^\omega$ , meaning $R^\omega$ is a path through D and thus satisfies the trace condition.

Conversely, if D satisfies the Ramsey trace condition and pick some path $\mathrm{Tr} \circ P$ for $P \colon \omega \to \mathcal{P}_C^S$ . Clearly, there exists $P \subseteq P'$ with $\left|P'(i < i + 1)\right| = 2$ for all $i \in \omega$ , that is, a representation of P which does not ‘skip’ any nodes. As P’ describes an infinite path through C, there needs to be some $u \in \mathrm{dom}(\beta)$ with $P'(i) = u$ for infinitely many $i \in \omega$ and thus by Lemma 5.1 an idempotent $R \colon \mathrm{Tr}(u) \to \mathrm{Tr}(u)$ such that $R^\omega \subseteq \mathrm{Tr} \circ P' \supseteq \mathrm{Tr} \circ P$ . By the Ramsey trace condition, $R^\omega$ satisfies the trace condition, meaning $\mathrm{Tr} \circ P$ does so as well.

Remark 5.1. By restricting our attention to , we guarantee that $1_{\mathrm{Tr}(u)}$ can only occur in if there is some $p \in \mathrm{Path}_C(u, u)$ such that $\mathrm{Tr}(p) = 1_{\mathrm{Tr}(u)}$ . This is important as in most sensible trace categories – including all trace categories defined in this article – the path $1_{\mathrm{Tr}(u)}^\omega$ does not satisfy the trace condition. Naïvely including $1_{\mathrm{Tr}(u)}$ in the collection of idempotent morphisms to consider when checking for GTC satisfaction would thus invalidate the condition given above.

Note that this soundness condition can only be stated in a setting like ours, in which the composition of trace maps is considered. This is because the closed collection of compositions, in this case the -set, gives rise to the finite colouring required to apply the Ramsey theorem. The Ramsey trace condition induces a novel algorithm for checking whether an ACD is a proof. This algorithm is analogous to that given for program termination by Lee et al. (2001). A more careful analysis of algorithms of this type in the realm of cyclic proofs is undertaken by Cohen et al. (2024).

Theorem 5.3. Let $\mathcal{T}$ be such that

1. (1) from $R \colon X \to Y$ and $R' \colon Y \to Z$ one can compute $R' \circ R \colon X \to Z$ ,

2. (2) for $R, R' \colon X \to Y$ one can decide whether $R = R'$ , and

3. (3) for idempotent $R \colon X \to X$ one can decide whether $R^\omega \colon \omega \to \mathcal{T}$ satisfies the trace condition.

Further let $D = (C, \mathrm{Tr} \colon \mathcal{P}_C \to \mathcal{T})$ be an ACD with Tr computable and such that for every $u, v \in T$ the set is finite. Then it is decidable whether D is a proof.

Proof. By Theorem 5.2, we know that it suffices to check that for each $u \in \mathrm{dom}(\beta)$ and for all idempotent , $R^\omega$ satisfies the trace condition. Thus, simply compute all of the -sets and then check each idempotent endomorphism via procedure (3). The -sets are computed by an iterative procedure with base cases:

$$H^0(u, v) := \{\mathrm{Tr}(uv) ~|~ \mathrm{if } v \mathrm{ child of } u\} \cup \{1_{\mathrm{Tr}(u)} ~|~ \mathrm{if } u \in \mathrm{dom}(\beta) \mathrm{ and } \beta(u) = v \}$$

and the iterative steps, using the procedure from assumption (1),

$$H^{i + 1}(u, v) := H^i(u, v) \cup \{R \circ R' ~|~ w \in T, R' \in H^i(u, w), R \in H^i(w, v)\}. $$

We carry out the procedure until $H^i(u, v) = H^{i + 1}(u, v)$ for all $u, v \in T$ , that is, until a fixed point is reached, which can be detected using procedure (2). That such a fixed point will be reached is guaranteed by the finiteness of the . It is easily observed that . Now check whether D satisfies the Ramsey trace condition by using the procedure (3) on all $R \in H(u, u)$ for $u \in \mathrm{dom}(\beta)$ that satisfy $R = R \circ R$ , which can be detected by using the procedures (1) and (2).

Remark 5.2. As the assumptions of Theorem 5.3 are phrased in terms of computability, nothing more can be said about the complexity of the procedure in general. In Section 7, we prove the GTC, and equivalently the RTC, to be PSPACE-complete for the category $\mathcal{T}_\mathcal{A}$ of any activation algebra $\mathcal{A}$ . The witnessing decision procedure in PSPACE (see Lemma 7.4) is based on infinite word automata. Lee et al. (2001) demonstrate how an approach similar to Theorem 5.3 can be carried out in PSPACE by constructing the -sets ‘not all at once’.

While the GTC and RTC are equivalent, it may seem that a procedure designed for verification of the RTC could be more efficient than one implemented in terms of the GTC, based on the fact that in the RTC case a property is only checked per simple cycle (rather than every possible path). However, every morphism of a simple cycle’s -set must be checked, which can lead to an exponential blowup in cases such as $\mathcal{T}_\mathbb{B}$ . As pointed out above, procedures in PSPACE ‘designed for’ both are known.

Corollary 5.1. Let $\mathcal{A}$ be a activation algebra. It is decidable whether an ACD $(C, \mathrm{Tr} \colon \mathcal{P}_C \to \mathcal{T}_\mathcal{A})$ is a proof.

Proof. Simply observe that $\mathcal{T}_\mathcal{A}$ satisfies the criteria above. Notably, for an idempotent $R \colon X \to X$ in $\mathcal{T}_\mathcal{A}$ , one can decide whether $R^\omega$ satisfies the trace condition by checking if there exists an $x \in X$ such that $(x, \alpha, x) \in R$ .

Corollary 5.2. It is decidable whether a $\mu$ -pre-proof constitutes a $\mu$ -proof.

Proof. For a $\mu$ -pre-proof $\Pi$ , compute its induced ACD $\hat\Pi$ over $\mathcal{T}_\mathbb{F}$ as in Definition 4.3 and then decide whether $\hat\Pi$ satisfies the GTC via Corollary 5.1. The decision extends to $\Pi$ via Proposition 3.1.

6. Relating Trace Categories and Automata Theory

This section connects our abstract framework for cyclic derivations to automata theory, a field instrumental to cyclic proof theory. The main theorems of this section are abstractions of properties common to many cyclic proof systems. They serve to illustrate that ACDs allow reasoning uniformly about a large class of cyclic proof systems by abstracting away the logic-specific details.

The main point of interaction between cyclic proofs and automata theory is based on the observation that the trace condition of cyclic proof systems tends to be $\omega$ -regular. That is, the branches of cyclic proofs which satisfy the trace condition can be recognised by infinite word automata. We thus begin by recalling Büchi-automata, one of the classes of automata characterising $\omega$ -regularity. A Büchi-automaton is a tuple $\frak{B} = (\Sigma, Q, \Delta, s, F)$ consisting of a finite alphabet $\Sigma$ , a finite set of states Q, a starting state $s \in Q$ , a transition relation $\Delta \subseteq Q \times \Sigma\times Q$ and a set $F \subseteq Q$ called the acceptance condition.

Given a Büchi-automaton $\frak{B}$ and a word $\sigma \in \Sigma^\omega$ , a sequence $\rho \in Q^\omega$ is called a run of $\frak{B}$ on $\sigma$ if $\rho_0 = q_0$ and for each $i \in \omega$ we have $(\rho_i, \sigma_i, \rho_{i + 1}) \in \Delta$ . A run $\rho$ is accepting if there is some $q \in F$ such that $\rho_i = q$ for infinitely many $i \in \omega$ . A word $\sigma$ is accepted by $\frak{B}$ if there exists an accepting run of $\frak{B}$ on $\sigma$ . The set $L(\frak{B}) :=\{\sigma \in \Sigma^\omega ~|~ \sigma \mathrm{ is accepted by } \frak{B}\}$ is the language of $\frak{B}$ .

For most cyclic proof systems, given a cyclic pre-proof, there exists a infinite word automaton which recognises precisely the branches through that pre-proof that satisfy the trace condition (see Niwiński and Walukiewicz 1996 and Sprenger and Dam 2003 for examples of such constructions). This principle is extended to the setting of trace categories below.

Definition 6.1. Fix a trace category $\mathcal{T}$ . Its trace condition is $\omega$ -regular if, for any finite set M of morphisms of $\mathcal{T}$ and starting object $S \in \mathrm{Ob}(\mathcal{T})$ , there exists a Büchi-automaton $\frak{B}$ such that

This notion of $\omega$ -recognisably captures most uses of automata theory in the cyclic proof theory literature. For example, it allows us to carry out the most common proof of the decidability of the GTC in our abstract setting.

Theorem 6.1. Let the trace condition of $\mathcal{T}$ be $\omega$ -regular in a computable manner, that is, the recognising automaton $\frak{B}$ for every set M of morphisms and $S \in \mathrm{Ob}(\mathcal{T})$ can be computed. It is decidable whether an ACD $D = (C, \mathrm{Tr} : \mathcal{P}_C \to \mathcal{T})$ satisfies the GTC.

Proof. For $C = (T, \beta)$ , consider the set of trace maps along the edges of D:

$$M := \{\mathrm{Tr}(uv) ~|~ u \in T, v \in \mathrm{Chld}(u)\} \cup \{1_{\mathrm{Tr}(u)} ~|~ u \in \mathrm{dom}(\beta)\}$$

which is finite as T is. Compute the recognising automaton $\frak{B}$ for $S := \mathrm{Tr}(\varepsilon)$ and construct a second Büchi-automaton $\frak{A} = (T, M, \varepsilon, \Delta, T)$ with

$$\Delta := \{(u, \mathrm{Tr}(uv), v) ~|~ u \in T, v \in \mathrm{Chld}(u)\} \cup \{(u, 1_{\mathrm{Tr}(u)}, \beta(u)) ~|~ u \in \mathrm{dom}(\beta)\}$$

$\frak{A}$ accepts precisely the sequences of morphisms along the infinite branches of D. Thus, deciding whether D satisfies the GTC reduces to deciding $L(\frak{B}) \subseteq L(\frak{A})$ . Such inclusions between Büchi-automata are decidable (McNaughton 1966).

As a consequence of the Ramsey trace condition Theorem 5.2, every trace category with finite -sets has an $\omega$ -regular trace condition. Note that under computability conditions analogous to those of Theorem 5.3, the $\omega$ -recognisability proven below is ‘computable’ as required for Theorem 6.1. Notably, the result below applies (in a computable manner) to every $\mathcal{A}$ -activated trace category.

Theorem 6.2. Let $\mathcal{T}$ be a trace category with finite for every $X, Y \in \mathrm{Ob}(\mathcal{T})$ . Then its trace condition is $\omega$ -regular.

Proof. As a corollary to Lemma 5.1, a path $P \colon \omega \to \mathcal{T}$ satisfies the trace condition iff there exists an idempotent $R \colon X \to X$ in $\mathcal{T}$ such that $R^\omega \subseteq P$ and $R^\omega$ satisfies the trace condition. Fix some finite M and $S \in \mathrm{Ob}(\mathcal{T})$ . Define $O := \{\mathrm{dom}(R) ~|~ R \in M\} \cup \{\mathrm{cod}(R) ~|~ R \in M\}$ . Define the set of good, idempotent morphisms on $X \in O$ as:

and construct a Büchi-automaton $\frak{B} = (M, Q, \Delta, F, S)$ with

Q is finite as O and each of the are. First, note that $\frak{B}$ clearly rejects every sequence $\pi \in M^\omega$ which does not represent a well-formed path starting at S. It thus remains to show $\frak{B}$ accepts a path $P \colon \omega \to \mathcal{T}$ iff it is such that $R^\omega \subseteq P$ for some and $X \in O$ . First, suppose $R^\omega = P \circ S$ as desired. Then an accepting run on the sequence $\pi_i := P(i < i + 1)$ is obtained by:

1. • Taking (a)-transitions, reading $\pi[0, S(1) - 1]$ , then taking a (b)-transition on $P(S(1) - 1, S(1))$ , the ‘first part of’ $P(S(1) < S(2))$ : $(X, Y, R, P(S(1) < S(1) + 1))$ where $R \colon X \to X$ . For this, note that $S(1) - 1 \geq 0$ because $S(0) < S(1)$ . Continue reading $\pi[S(1), S(2) - 1]$ , reaching (X, X, R, R) as $P(S(1) < S(2)) = R$ .

2. • From then on, taking (c)-transitions, reading $\pi[S(i), S(i + 1) - 1]$ , always arriving at (X, X, R, R) as $P(S(i < i + 1)) = R$ .

This run is accepting as $(X, X, R, R) \in F$ is passed infinitely often. For the converse direction, simply observe that every accepting run on $\frak{B}$ needs to be structured as above, that is, eventually ‘picking’ an $X \in O$ and via a (b)-transition and then ‘assembling’ R along $\pi$ infinitely often via (c)-transitions, thereby demonstrating $R^\omega \subseteq P$ .

Remark 6.1. The converse of Theorem 6.2 need not hold. Consider a trace category $\mathcal{T}$ with $\omega$ -regular trace condition. Then , where is the usual category of sets, can be equipped with an $\omega$ -regular trace condition, namely that of its first component. However, the -sets of are not all finite.

Remark 6.2. It is also possible to construct recognising Büchi-automata for $\mathcal{T}_\mathcal{A}$ more directly in terms of $\mathcal{A}$ . Roughly, the states of such automata are triples $\Sigma X \in O.~X \times \mathcal{A}$ which take transitions $((X, x, a), R : X \to Y, (Y, y, a \vee b))$ for $(x, b, y) \in R$ . Whenever the third component reaches $\alpha$ , it is reset to 0, crossing a state in the acceptance condition F. The resulting automata resemble more closely the automata constructions usually found in the cyclic proof theory literature. The full details of this automata construction can be found in Wehr (2021, Proposition 5.11).

The second result connecting the theories of cyclic proofs and automata we cover in this section relates cyclic proofs and $\infty$ -proofs. $\infty$ -proofs allow ill-founded, finitely branching derivation trees and thus require a soundness condition, similar to cyclic proofs. From this point of view, cyclic proofs are simply regular $\infty$ -proofs, that is, those which are representable as finite graphs. The result states that on finite derivation systems, the cyclic and $\infty$ -proof systems induced by a trace interpretation prove the same sequents. This property does generally not hold for infinite derivation systems: for example, in cyclic arithmetic (Simpson 2017), the $\infty$ -proofs prove all true sentences of first-order arithmetic, whereas the cyclic proofs only prove the same sentences as Peano arithmetic. We begin by formally defining $\infty$ -proof systems and the infinite tree Büchi-automata, which play a key role in the result’s proof.

Given a derivation system , an $\infty$ -derivation is a triple $(T, \lambda, \delta)$ consisting of a (possibly infinite) tree T and functions and $\delta : T \to \mathcal{R}$ such that for every $t\in T$ with $\mathrm{Chld}(t) = \{t1, \ldots, tn\}$ the functions $\lambda$ and $\delta$ agree: $\rho(\delta(t)) = (\lambda(t), \lambda(t1), \ldots, \lambda(tn))$ . In other words, an $\infty$ -derivation is a derivation which might have infinite branches. Denote the set of $\infty$ -proofs in $\mathcal{R}$ by . An $\infty$ -proof system is a tuple consisting of a derivation system and a set of $\infty$ -derivations called $\infty$ -proofs. An $\infty$ -proof $\Pi = (T,\lambda, \delta)$ with $\lambda(\varepsilon) = \Gamma$ is called a proof of $\Gamma$ . Analogously to the case for cyclic proof systems, a derivation system and a trace interpretation $\iota : \mathcal{R} \to \mathcal{T}$ induce an $\infty$ -proof system in which iff every path along its branches satisfies the trace condition of $\mathcal{T}$ .

For a finite alphabet $\Sigma$ , a $\Sigma$ -labelled tree is a pair $(T,\lambda \colon T \to \Sigma)$ for a tree T. A $\Sigma$ -labelled tree $(T, \lambda)$ is a subtree of $\Sigma$ -labelled $(T', \lambda')$ if it is a ‘suffix’ of T’, that is, there exists some $t \in T'$ such that $T = \{ts \in T' ~|~ s \in T'\}$ and $\lambda(s) = \lambda'(ts)$ . A Büchi tree automaton is a tuple $\frak{A} = (\Sigma, Q, \Delta, s, F)$ consisting of a finite alphabet $\Sigma$ , a set of states Q, a set of transitions $\Delta \subseteq Q \times \Sigma \times Q^*$ , a starting state $s \in Q$ and an acceptance condition $F \subseteq Q$ . Let $(T, \lambda)$ be a $\Sigma$ -labelled tree. A run of $\frak{A}$ on $(T,\lambda)$ is a Q-labelling $\rho \colon T \to Q$ of T such that $\rho(\varepsilon) = s$ and for each $t \in T$ with $\mathrm{Chld}(t) = \{t1, \ldots,tn\}$ the transition $(\rho(t), \lambda(t), \rho(t1), \ldots, \rho(tn)) \in\Delta$ . A run is accepting if for every infinite branch $b \in T^\omega$ of T, there exists a $q \in F$ such that $\rho(b_i) = q$ infinitely often. A $\Sigma$ -labelled tree $(T, \lambda)$ is accepted by $\frak{A}$ if there is an accepting run of $\frak{A}$ on it. The set $L(\frak{A}) :=\{(T, \lambda) ~|~ (T, \lambda) \mathrm{ is accepted by }\frak{A}\}$ is the language of $\frak{A}$ .

Theorem 6.3. Let be a derivation system with $\mathcal{R}$ finite. Fix a trace interpretation $\iota : \mathcal{R} \to \mathcal{T}$ such that the trace condition of $\mathcal{T}$ is $\omega$ -regular. Then any sequent is proven by a cyclic proof iff it is proven by an $\infty$ -proof.

Proof. For the left-to-right direction, simply observe that unfolding the cyclic proof yields an $\infty$ -derivation satisfying the trace condition induced by $\iota$ .

Conversely, note that any $\infty$ -derivation $(T, \lambda, \delta)$ in $\mathcal{R}$ thus constitutes a $\mathcal{R}$ -labelled tree $(T, \delta)$ . We begin by constructing a Büchi tree automaton which accepts precisely the $\infty$ -proofs of $\Gamma$ , represented as $\mathcal{R}$ -labelled trees. By $\omega$ -regularity of $\mathcal{T}$ , there exists a Büchi-automaton $\frak{A} = (Q, M, \Delta, s, F)$ for $M := \{ r_i : \iota(\Gamma) \to \iota(\Delta_i) ~|~ r \in \mathcal{R}, \rho(r) = (\Gamma, \Delta_1, \ldots, \Delta_n), i \leq n\}$ and $S := \iota(\Gamma)$ . From it, the desired Büchi tree automaton is constructed, taking

$$ \Delta_\frak{B} := \bigcup_{r \in \mathcal{R}} \left \{ \bigg((\Gamma, q), r, \Big((\Sigma_1, q_1), ..., (\Sigma_n, q_n)\Big)\bigg) ~\middle|~ \begin{array}{l} q \in Q \mathrm{ and } \rho(r) = (\Gamma, \Sigma_1, \ldots, \Sigma_n) \mathrm{ and}\\ (q, r_i : \iota(\Gamma) \to \iota(\Sigma_i), q_i) \in \Delta \mathrm{ for each } i \end{array} \right \}. $$

That is, the automaton takes transition steps corresponding to the derivation rule $r \in \mathcal{R}$ labelling the tree, ‘walking the state from Q along according to $\frak{A}$ ’ for the trace maps $r_i$ chosen by the trace interpretation $\iota$ .

For the correctness of the automaton, observe that by the choice of $\Delta_\mathcal{B}$ , $\frak{B}$ has a run an $\mathcal{R}$ -labelled tree if it constitutes an $\infty$ -derivation with endsequent $\Gamma$ , that is, its rules were applied with matching premises and conclusions. Furthermore, such a run is accepting if and only if the run of the $\mathcal{T}$ -path induced by each infinite branch of the $\infty$ -derivation is accepted by $\frak{A}$ . Thus, $\frak{B}$ accepts precisely the $\infty$ -proofs of $\Gamma$ .

Because there is a $\infty$ -proof of $\Gamma$ , the language $L(\frak{B})$ of $\frak{B}$ is not empty. It is a classic result of infinite tree automata theory (see e.g., Corollary 8.20 in Nieer 2002) that in such a case, $L(\frak{B})$ contains a regular tree $\Pi$ . Such regular trees can be represented as finite graphs, allowing the proof $\Pi$ to be represented as a cyclic proof $\Pi'$ . As any element of $L(\frak{B})$ is a proof of $\Gamma$ , so is $\Pi'$ .

An application of the result above is establishing the equivalence between cyclic proof systems with and without a Cut-rule. Many Cut-elimination procedures for cyclic proof systems in the literature are corecursive algorithms which lazily transform cyclic proofs with Cut-applications into $\infty$ -proofs without Cuts (e.g., Baelde et al. 2016; Fortier and Santocanale 2013; Savateev and Shamkanov 2021). If the Cut-free fragment of the derivation system is finite, the result above can then be applied to conclude that there must also exist a Cut-free cyclic proof. An example of the result being applied in this way is given by Savateev and Shamkanov (2021). A disadvantage of this method of Cut-elimination is that the Cut-free cyclic proof need not be related to the original Cut-free $\infty$ -proof. This means this Cut-elimination result does not preserve computational content.

The automata construction employed in the proof of Theorem 6.3 also yields a decision procedure for provability in the cyclic and $\infty$ -proof systems. The result again requires some light computability assumptions.

Corollary 6.1. Let be a derivation system with $\mathcal{R}$ finite. Fix a trace interpretation $\iota : \mathcal{R} \to \mathcal{T}$ such that the trace condition of $\mathcal{T}$ is $\omega$ -regular in a computable manner and for any $r \in \mathcal{R}$ with $\rho(r) = (\Gamma, \Delta_1, \ldots, \Delta_n)$ the $r_i : \iota(\Gamma) \to \iota(\Delta_i)$ can be computed. Then it is decidable whether is provable in the induced cyclic and $\infty$ -proof systems.

Proof. The proof of Theorem 6.3 constructs a Büchi tree automaton $\frak{B}$ such that $L(\frak{B})$ is precisely the $\infty$ -proofs of $\Gamma$ . By the computability assumptions, the automaton $\frak{B}$ can be computed. As the emptiness problem for parity tree automata is decidable (Rabin 1969), one can thus decide if there exists an $\infty$ -proof of $\Gamma$ by deciding whether $L(\frak{B})$ is empty.

Corollary 6.2. The $\mu$ -sequents provable by the cyclic proof system and $\infty$ -proof system induced by the trace interpretation in Definition 3.4 coincide. Furthermore, the provability of a $\mu$ -sequent is decidable.

Proof. As noted above, $\mathcal{T}_\mathbb{F}$ is $\omega$ -regular in a computable manner. It is also clear that the trace interpretation $\iota : \mu \to \mathcal{T}_\mathbb{F}$ is computable as required by Corollary 6.1. The derivation system given for the modal $\mu$ -calculus in Fig. 1 is not finite. However, because it is Cut-free, one can restrict the sequents occurring in a $\infty$ -derivation of a $\mu$ -sequent $\Gamma$ to the so-called Fischer–Ladner closure of $\Gamma$ . This closure is well known to be finite, as for example argued by Kozen (1983). Thus, it suffices to consider a finite fragment of the derivation system given in Fig. 1 for each sequent $\Gamma$ , meaning Theorem 6.3 and Corollary 6.1 apply.

7. PSPACE-Completeness of Cyclic Proof Checking

In addition to putting forward the size-change criterion for program termination, Lee et al. (2001) also prove that the associated decision is PSPACE-complete. This result has been transferred to the setting of cyclic proofs by Nollet et al. (2019) who prove that checking the GTC of linear logic with least and greatest fixed points ( $\mu$ MALL) is PSPACE-complete. We extend this result to ACDs over $\mathcal{T}_\mathcal{A}$ . The proof of PSPACE-hardness proceeds analogously to Nollet et al. (2019) by a reduction to Boole program termination. Indeed, the ACDs given in Definition 7.2 are obtained by representing the cyclic derivations given by Nollet et al. as ACDs, applying the compression procedure (Theorem 4.1) and removing some spurious elements from their trace sets.

Definition 7.1. A program is a numbered sequence of instructions $1: I_1;\; 2: I_2; \ldots;\; m : I_m$ composed according to the following grammar

where the labels $\ell, \ell' \in \{0, \ldots, m\}$ and the variables X stem from some stock of variable letters.

Fix a program p of length m making use of the variables $\Xi := \{X_1, \ldots, X_n\}$ . Given assignments $\sigma, \sigma' : \Xi \to \mathbb{B}$ and labels $\ell, \ell' \in \{0, \ldots, m\}$ , we write $(\ell, \sigma) \leadsto (\ell', \sigma')$ if $\ell \neq 0$ and either:

1. (1) the instruction labelled by $\ell$ in p is $X := \neg X$ for some $X \in \Xi$ , $\ell' \equiv \ell + 1 \mod (m + 1)$ and $\sigma' = \sigma[X \mapsto \neg \sigma(X)]$ , or

2. (2) the instruction labelled by $\ell$ in p is for some $X \in \Xi$ , $\ell' = \ell_{\sigma(X)}$ and $\sigma' = \sigma$ .

We write $(\ell, \sigma) \leadsto^* (\ell', \sigma')$ if there are $\ell_1, \ldots, \ell_k$ and $\sigma_1, \ldots, \sigma_k$ such that $(\ell, \sigma) \leadsto (\ell_1, \sigma_1)$ and $(\ell_i, \sigma_i) \leadsto (\ell_{i + 1}, \sigma_{i + 1})$ and $(\ell_k, \sigma_k) \leadsto (\ell', \sigma')$ . To make the labels explicit, we sometimes write $(\ell, \sigma) \leadsto^*_{\ell \ell_1 \ldots \ell_k, \ell'} (\ell', \sigma')$ .

Writing $\phi $ for the constant assignment $ x \mapsto 0$ , define

For the remainder of this section, we fix some program $p = 1 : I_1, \ldots, m :I_m$ making use of variables $X_1, \ldots, X_n$ .

Definition 7.2. The ACD associated with p is $[\![ p ]\!] := (C, \mathrm{Tr} : \mathcal{P}_C \to \mathcal{T}_\mathcal{A})$ for an arbitrary activation algebra $\mathcal{A}$ can be sketched as follows.

Every node s of C shares the same trace values $\mathrm{Tr}(s) = \{X_1^+, X_1^-, \ldots, X_n^+, X_n^-, R, G_0, \ldots, G_m\}$ . The ‘subtrees’ $[\![ 0 ]\!]$ and $[\![ \ell : I_\ell ]\!]$ each comprise of one or two buds whose companion is the root of $[\![ p ]\!]$ (drawn in white below). We refer to these buds by the names written above them. The $\mathcal{T}_\mathcal{A}$ -morphisms ‘decorating’ the subtrees’ edges are written next to them. For notational convenience, we often treat $\ell^+$ and $\ell^-$ as the label $\ell$ .

The morphisms are specified below. A dashed line between A and B indicates the pair (A, 0, B), a bold line the pair $(A, \alpha, B)$ and the absence of a connecting line between A and B the absence of all pairs (A, c, B). In $R_\neg$ , $\ell' = \ell + 1 \mod m + 1$ .

Write B for the set of names for buds of $[\![ p ]\!]$ , that is,

Any path through $[\![ p ]\!]$ corresponds to an infinite sequence $\ell \in B^\omega$ describing the sequence in which the buds of $[\![ p ]\!]$ are passed to generate said path. For this reason, we treat such sequences and paths $P : \mathcal{P}_C \to \mathcal{T}_\mathcal{A}$ interchangeably. The property central to the reduction is that if , then $[\![ p ]\!]$ does not satisfy the trace condition. Thus, sequences $\ell \in B^\omega$ representing unsuccessful runs will satisfy the trace condition. The various aspects of the trace maps given in Definition 7.2 can thus be reframed as ensuring certain conditions on such $\ell \in V^\omega$ .

We begin by showing that all sequences $\ell \in B^\omega$ $\ell \in B^\omega$ which eventually diverge or do not even adhere to the control structure of p have progressing traces through R or the $G_i$ s, respectively. For this, we define the control-graph of p as $G =(B, E)$ with

where, if , then pairs $(\ell_1, \ell_2)$ are included as $(\ell_1,\ell_2^+)$ and $(\ell_1,\ell_2^-)$ . For a sequence $\ell$ of labels from B (finite or infinite), $\ell$ is a path through G, writing $\ell \in G$ , if for each $i < \left|\ell\right|$ , $(\ell_i, \ell_{i +1}) \in E$ .

Lemma 7.1. Let $\ell \in B^\omega$ be a path through $[\![ p ]\!]$ . Then,

1. (1) $\ell$ has a progressing trace along R iff eventually 0 never occurs along $\ell$ .

2. (2) $\ell$ has a progressing trace along the $G_0, \ldots, G_m$ iff no suffix of $\ell$ is a path through G.

Proof.

1. (1) Observe that R-traces are interrupted by $R_0$ whenever a path passes through $0 \in B$ and are activated when passing through any other bud.

2. (2) An activation on a G-trace takes place whenever it ‘jumps incorrectly’. That is, if $(\ell_i, \ell_{i + 1}) \not\in E$ , then there is an activating trace from $G_{\ell_i}$ to $G_{\ell_{i + 1}}$ in the trace maps of the subtree $[\![ \ell_i ]\!]$ . Thus, a progressing trace through the Gs indicates that such violations take place infinitely often, meaning no suffix of $\ell$ can be a path through G. Conversely, no suffix of $\ell$ being a path through G indicates infinitely many violations taking place.

The only paths through $[\![ p ]\!]$ which remain unclassified are of the shape $u0u_10u_20u_30\ldots$ where each $u_i0$ describes a potential run of p which at least is a path through the control-graph of p. We continue by analysing the traces on the $X_i^\bullet$ along such potential runs. Consider a sequence $u = \ell_0 \ldots \ell_n \in B^{n + 1}$ and denote by $R^i$ the morphism in $[\![ p ]\!]$ from the root to the bud $\ell_i$ . In the following, we denote the trace map of the sequence u by $R_u:= R^{n - 1} \circ \ldots \circ R^0 \circ R_0$ .

Lemma 7.2. Let $u \in (B \setminus \{0\})^+$ with $\left|u\right| = n + 1$ be such that 0 u is a path through G. Then

1. (1) There is no $X_j^\bullet \in \mathrm{Tr}(\varepsilon)$ and no activation algebra element c such that $(X_i^+, c, X_j^\bullet) \in R_{u}$ .

2. (2) There are no $X^\bullet_i, X^\bullet_j \in \mathrm{Tr}(\varepsilon)$ with $i \neq j$ and $(X^\bullet_i, c, X^\bullet_j) \in R_{u}$ for any activation algebra element c.

3. (3) If $(\ell_0, \phi) \leadsto^*_{u} (\ell_n, \sigma)$ for some $\sigma$ then for each $X_i$ , there is exactly one $a^+_i$ and exactly one $a^-_i$ such that $(X^-_i, a^+_i, X^+_i) \in R_{u}$ and $(X^-_i, a^-_i, X^-_i) \in R_{u}$ . Furthermore,

   1. – if $\sigma(X_i) = 0$ then $a^+_i = \alpha$ and $a^-_i = 0$

   2. – if $\sigma(X_i) = 1$ then $a^-_i = \alpha$ and $a^+_i = 0$

4. (4) If there is no $\sigma$ such that $(\ell_0, \phi) \leadsto^*_{u} (\ell_n, \sigma)$ , then there exists some $X_i$ such that $(X_i^-, 1, X_i^+), (X_i^-, 1, X_i^-) \in R_{u}$

Proof.

1. (1) Observe that $R_0$ , the map from the root to 0, interrupts all traces starting at the $X_i^+$ .

2. (2) Observe that all trace maps in $[\![ p ]\!]$ only ever connect trace values corresponding to the same variable $X_i$ .

3. (3) At the beginning of a -run, all variables are 0. This is mirrored by $R_0$ in the sense of (2), as it connects each $X^{-}_i$ to the $X^{\bullet}_i$ according to the first clause. We continue by reasoning inductively along the run $(\ell_0, \phi) \leadsto^*_{u} (\ell_n, \sigma)$ , performing a case distinction on the final transition $(\ell_{n - 1}, \sigma') \leadsto (\ell_n, \sigma)$ . The negation step inverts the value $\sigma'(X_i)$ of some variable $X_i$ . This is mirrored in $R_{\neg}$ by ‘swapping’ the traces on $X_i^+$ and $X_i^-$ which preserves the property. For the -instruction, observe that $(\ell_{n - 1}, \sigma') \leadsto (\ell_n, \sigma)$ means branch dictated by $\sigma(X_i)$ is taken (i.e., $\ell_{n - 1}$ is some $\ell^+$ and $\sigma(X_i) = 1$ ). Then the trace of the $X_i^\bullet$ dual to $\sigma(X_i)$ is activated (i.e., $X_i^-$ if $\sigma(X_i) = 1$ ), preserving the property.

4. (4) We again reason inductively on u. If $\left|u\right| = 1$ , then $(\ell_0, \phi) \leadsto^*_{u} (\ell_0, \phi)$ , meaning the claim does not apply. Thus, $u = u'\ell_n$ for some $u' \in (B \ \{0\})^+$ and we perform a case distinction on whether there exists a $\sigma$ such that $(\ell_0, \phi) \leadsto^*_{u'} (\ell_{n - 1}, \sigma)$ . If there exists no such $\sigma$ , this property holds for $R_{u'}$ per inductive hypothesis and it is easily observed that any possible choice of $R^{n - 1}$ preserves the property for $R_{u'\ell_{n}}$ . If $(\ell_0, \phi) \leadsto^*_{u'} (\ell_{n - 1}, \sigma)$ then, as $(\ell_{n - 1}, \ell_n) \in E$ , this must mean that and $\ell_{n - 1}$ is the ‘incorrect bud’ (i.e., $\ell_{n - 1}$ is some $\ell^+$ and $\sigma(X_i) = 0$ ). In such cases, the $X_i^\bullet$ corresponding to the value of $\sigma(X_i)$ is activated by $R^{n - 1}$ (i.e., $X_i^-$ if $\sigma(X_i) = 0$ ). Combining this with what is known about $R_{u'}$ by property (3), this means that $(X_i^-, \alpha, X_i^-), (X_i^-, \alpha, X_i^+) \in R_{u}$ .

With this classification of the potential runs, we can connect the trace condition on branches not covered by Lemma 7.1 to the runs of the program p.

Lemma 7.3. Let $\ell \in B^\omega$ be a path through $[\![ p ]\!]$ which does not have a progressing trace along R or the $G_0, \ldots, G_m$ . Then, $\ell = u 0 u_1 0 u_2 0 u_3 0 \ldots$ with each $u_i \in (B - \{0\})^+$ . Furthermore, $\ell$ does not satisfy the trace condition iff from some $N \in \omega$ onwards, $(1, \phi) \leadsto^*_{u_i} (0, \phi)$ for all $i > N$ .

Proof. That $\ell = u 0 u_1 0 u_2 0 \ldots$ follows directly from Lemma 7.1.

First suppose that $(1, \phi) \leadsto^*_{u_i} (0, \phi)$ for $i > N$ . As -programs are deterministic, this means $u_i = u$ for all $i > N$ and some fixed u. From Lemma 7.2 (3), it follows that for every $X_j$ we have $(X_j^-, \alpha, X_j^+), (X_j^-, 0, X_j^-) \in R_{u}$ . By Lemma 7.2 (1), the trace on $X_j^+$ is interrupted in $R_0$ . Thus, there can be no progressing trace along any $X_j^+,X_j^-$ along the path $0 u 0 u \ldots$ . Then, because of the previous results, there is no progressing trace along any of the elements of $\mathrm{Tr}(\varepsilon)$ meaning $\ell$ does not satisfy the trace condition.

Conversely, suppose that infinitely many of the $u_i$ did not satisfy $(1, \phi) \leadsto^*_{u_i} (0, \phi)$ . There are two possibilities for such $u_i$ s: either there is some $\sigma \neq \phi$ with $(1, \phi) \leadsto^*_{u_i}(0, \sigma)$ or not. In the former case, there thus must be some $X_j$ with $\sigma(X_j) = 1$ , meaning $(X_j^-, 1, X_j^-) \in R_{u_i}$ . In the latter case, there also must be some $X_j$ with $(X_j^-, 1, X_j^-)$ . As the traces on $X_j^-$ are never interrupted, if infinitely many such ‘deviant’ runs exist along $\ell$ , some $X_j^-$ must be activated infinitely often, as there are only finitely many variables. Then, $\ell$ satisfies the trace condition.

Corollary 7.1. For any given program p, iff $[\![ p ]\!]$ does not satisfy the trace condition of $\mathcal{T}_\mathcal{A}$ .

Theorem 7.1. Verifying the trace condition on ACDs in $\mathcal{T}_\mathcal{A}$ for any $\mathcal{A}$ is PSPACE-hard.

Proof. A -program can be transformed into the ACD given in Definition 7.2 in LOGSPACE. By Corollary 7.1, this constitutes a LOGSPACE-reduction of a PSPACE-hard problem () to cyclic proof checking in $\mathcal{T}_\mathcal{A}$ for any $\mathcal{A}$ .

Remark 7.1. The PSPACE-hardness result in Theorem 7.1 is only given in terms of a concrete family of trace categories, the activation algebra induced $\mathcal{T}_\mathcal{A}$ . It remains an open question if a more general condition on trace categories can be found which would yield PSPACE-hardness.

-set finiteness of a trace category $\mathcal{T}$ does not entail PSPACE-hardness. For instance, consider a -set finite trace category $\mathcal{T}$ in which every path satisfies the trace condition and which thus makes checking it trivially O(1). This example also illustrates that $\omega$ -regularity of the trace condition of $\mathcal{T}$ does not entail PSPACE-hardness.

Remark 7.2. Theorem 7.1 does not directly imply that the proof checking of any concrete cyclic proof system is PSPACE-hard, even if its trace condition can be expressed in terms of $\mathcal{A}$ . Instead, Theorem 7.1 only proves that there exist ‘suitably small’ ACDs over $\mathcal{A}$ whose GTC satisfaction codes the termination of -programs. To extend this result to a concrete cyclic proof system, one must prove that for any -program p, there exists a ‘suitably small’ cyclic proof whose (compressed) ACD is $[\![ p ]\!]$ . Usually, this can be accomplished by finding formulas which can produce various traces. For example, for the variables, the following ‘trace gadgets’ are required:

To conclude PSPACE-completeness, it remains to show that proof checking for $\mathcal{T}_\mathcal{A}$ -ACDs is in PSPACE.

Lemma 7.4. For a given ACD $D = (C, \mathrm{Tr} : \mathcal{P}_C \to \mathcal{T}_\mathcal{A})$ , the verification whether it constitutes an abstract cyclic proof can be carried out in PSPACE.

Proof. Following the proof of Theorem 6.1, one can verify whether D is a proof by deciding whether the language of a Büchi-automaton $\frak{A}$ recognising all paths through D is included in the language of a Büchi-automaton $\frak{B}$ recognising all paths consisting of morphisms from Tr which satisfy the trace condition of $\mathcal{T}_\mathcal{A}$ . The language inclusion problem for regular languages is known to be in PSPACE (Kupferman and Vardi 1996). Thus, it remains to find automata $\frak{A}$ and $\frak{B}$ adhering to the aforementioned specifications whose sizes are polynomial in the size of D. The automaton $\frak{A}$ given in Theorem6.1 is already suitable for this. On the other hand, the automaton $\frak{B}$ constructed according to Theorem 6.2 is too large, as its set of states contains the sets for each set X of trace values in the image of Tr, whose size is exponential in the size of X. However, the $\mathcal{T}_\mathcal{A}$ -specific construction for the $\frak{B}$ given in Wehr (2021, Proposition 5.11) is of size polynomial to the size of D. Thus, there are suitable automata such that deciding $L(\frak{A}) \subseteq L(\frak{B})$ decides whether D is a proof, meaning this can be decided in PSPACE.

Corollary 7.2. The problem of verifying whether an ACD over $\mathcal{T}_\mathcal{A}$ is a proof is PSPACE-complete.

The fact that proof checking for $\mathcal{T}_\mathcal{A}$ -ACDs is in PSPACE extends to a concrete cyclic proof system $\mathcal{R}$ much more readily than PSPACE-hardness. The only restriction is that the set of trace values of each $\mathcal{R}$ -sequent is of polynomial size and that the trace data of an $\mathcal{R}$ -pre-proof can be computed in PSPACE. All cyclic proof systems we know of satisfy these properties.

Lemma 7.5. Let be a cyclic proof system whose trace condition is given by a trace interpretation $\iota : \mathcal{R} \to \mathcal{T}_\mathcal{A}$ . Suppose that $\iota$ is such that for sequents the set $\iota(\Gamma)$ of trace values in $\Gamma$ is of size polynomial to the size of $\Gamma$ and can be computed from $\Gamma$ in PSPACE. Suppose further that for each rule $r \in \mathcal{R}$ with $\rho(r) = (\Gamma, \Delta_1, \ldots, \Delta_n)$ , the maps $r_i : \iota(\Gamma) \to \iota(\Delta_i)$ can be computed in PSPACE. Then deciding whether an $\mathcal{R}$ -pre-proof is a proof is in PSPACE.

Proof. Given an $\mathcal{R}$ -pre-proof $\Pi = (C, \lambda, \delta)$ , simply compute its induced ACD $D = (C, \mathrm{Tr} : \mathcal{P}_C \to \mathcal{T}_\mathcal{A})$ as described in Definition 4.3. By the assumptions about $\iota$ , D can be computed in PSPACE. Thus, if D is of size polynomial to the size of $\Pi$ , checking whether $\Pi$ is an $\mathcal{R}$ -proof can be carried out in PSPACE as described in Lemma 7.4. As C is simply ‘copied’, it suffices to show that Tr is of polynomial size. Per assumption, each $\mathrm{Tr}(s)$ is $\iota(\lambda(s))$ and thus of polynomial size of the sequent $\lambda(s)$ which is accounted for in the size of $\Pi$ . Similarly, $\mathrm{Tr}(s \, si) \subseteq \mathrm{Tr}(s) \times \mathcal{A} \times \mathrm{Tr}(si)$ for each $s \in C$ and $si \in \mathrm{Chld}(s)$ and is thus of polynomial size to $\max\{\left|\lambda(s)\right|, \left|\lambda(si)\right|\}$ . As this data suffices to code Tr, D overall is of polynomial size to $\Pi$ as desired.

Corollary 7.3. Verifying whether a $\mu$ -pre-proof is a proof is in PSPACE.

8. Conclusion

The derivations of cyclic proof systems, which are finite, directed graphs, rather than finite trees, may not be sound, that is, they might conclude invalid sequents. Thus, cyclic proof systems distinguish between pre-proofs (well-formed derivations) and proofs (sound, well-formed derivations). The most common method is to impose a global trace condition: for a pre-proof to be a proof, all of its infinite branches must satisfy a so-called trace condition. We capture this trace condition in categorical terms: infinite branches are represented by paths, functors $P : \omega \to \mathcal{T}$ from the preorder category on $\omega$ to a trace category $\mathcal{T}$ . A trace category $\mathcal{T}$ is a category equipped with a trace condition, a predicate on paths through $\mathcal{T}$ which is closed under taking suffixes and internal composition. We further define a family of trace categories $\mathcal{T}_\mathcal{A}$ whose morphisms are relations between finite sets annotated with an activation algebra $\mathcal{A}$ : a finite $\vee$ -semilattice with a distinguished activation element $\alpha$ . A path through $\mathcal{T}_\mathcal{A}$ satisfies the trace condition if it carries an infinite sequence of connected elements which attains the activation value $\alpha$ infinitely often. Almost all notions of trace from the literature can be represented naturally in terms of some $\mathcal{T}_\mathcal{A}$ . Notably, the usual trace condition for the cyclic systems of $\mu$ -calculi is given in terms of the three-value failure algebra $\mathbb{F}$ .

Using this abstracted notion of trace, a pre-proof with underlying graph C may be represented as an annotation of C with maps of a trace category $\mathcal{T}$ . In categorical terms, the latter is a functor $\mathrm{Tr} : \mathcal{P}_C \to \mathcal{T}$ from the category of finite paths through C into $\mathcal{T}$ . When representing a pre-proof in this manner, all details unrelated to the trace condition are abstracted away, leading us to call such functors abstract cyclic derivation. The requirement of trace conditions being closed under internal composition allows us to prove the following two novel results in cyclic proof theory.

1. • Compression: ACDs may be ‘compressed’ to trace-condition-equivalent ACDs over graphs whose size is linear in the number of simple cycles in C (Theorem 4.1).

2. • Ramsey-style soundness: An ACD $\mathrm{Tr} : \mathcal{P}_C \to \mathcal{T}$ is a proof (i.e., every path through it satisfies the trace condition) if and only if for every idempotent endomorphism $R : X \to X$ in the image of Tr, the periodic path $R^\omega :\omega \to \mathcal{T}$ (which simply repeats R) satisfies the trace condition (Theorem 5.2).

We also prove some well-known results of cyclic proof theory in terms of our abstract notion of trace and derivation in order to demonstrate the adequacy of our notions for tackling questions of cyclic proof theory and connect them to the wider field. In Section 6, we consider trace categories with $\omega$ -regular trace conditions, connecting ACDs with $\omega$ -automata theory. As a result of the Ramsey-style soundness condition, every trace category with finite -sets, including all $\mathcal{T}_{\mathcal{A}}$ , has an $\omega$ -regular trace condition. We prove the following results using automata theory.

1. • Decidability: If the trace condition of $\mathcal{T}$ is $\omega$ -regular in a ‘computable’ manner, the GTC of ACDs on $\mathcal{T}$ is decidable (Theorem 6.1).

2. • Regularisation: If a proof system is finite (i.e., the set of sequents occurring in a proof is finite), then every sequent provable via a ill-founded proof is provable via a cyclic proof (Theorem 6.3).

In Section 7, we generalise a result about the cyclic proof system for multiplicative-additive linear logic with fixed points ( $\mu$ MALL) by Nollet et al. (2019) to obtain.

1. • PSPACE-completeness: The problem of deciding whether an ACD over $\mathcal{T}_\mathcal{A}$ satisfies the GTC is PSPACE-complete (Theorem 7.1 & Lemma 7.4).

The above result is proven in such a way that the decision problem being in PSPACE readily transfers to concrete cyclic proof systems with a $\mathcal{T}_\mathcal{A}$ -trace condition. Transferring PSPACE-hardness, however, requires certain assumptions on the concrete cyclic proof system.

8.1 Related work

Definitions and results in this article originate from Wehr’s Masters thesis (Wehr 2021), although most have undergone significant changes. The thesis contains results that are not presented in this article, including a categorical treatment of a further three cyclic proof systems: cyclic arithmetic (Simpson 2017), $\mathrm{HFL}_\mathbb{N}$ (Kori et al. 2021) and Grzegorczyk modal logic (Savateev and Shamkanov 2021).

To the best of our knowledge, Brotherston (2006) is the only previous work on abstracting cyclic proofs. The present article can be viewed as an extension of Brotherston’s in two ways: first, his abstract notion of derivation is closer to the common definition of pre-proofs, being presented in terms of abstract sequents and derivation rules. Crucially, this bars him from considering the composition of trace information, which enabled us to derive the ACD compression result (Theorem 4.1) and the alternative soundness condition (Theorem 5.2). Second, Brotherston only considers trace conditions expressed in terms of the Booleans $\mathbb{B}$ which, as we have remarked, is insufficient to directly express the trace condition of the modal $\mu$ -calculus, a problem our activation algebras alleviate.

Lee et al. (2001) propose a termination criterion for first-order programs called the size-change principle. This criterion can be considered an instance of the $\mathcal{T}_\mathbb{B}$ trace condition. The authors give a decision procedure for the size-change principle which is a variant of the decision procedure for the Ramsey trace condition we give in Theorem 5.3, specialised to $\mathcal{T}_\mathbb{B}$ . They also prove PSPACE-completeness of their criterion by reducing it to termination. This argument has been adapted by Nollet et al. (2019) to the cyclic proof system for multiplicative, additive linear logic with fixed points ( $\mu$ MALL) which we in turn adapted to ACDs in Section 7.

The Ramsey trace condition (Definition 5.1) is not the first application of Ramsey’s theorem in the field of cyclic proof theory. Notably, existing proofs of the equivalence of (extensions of) cyclic arithmetic and (extensions of) Peano arithmetic (Berardi and Tatsuta 2017; Das 2020; Simpson 2017) rely on (arithmetised) variants of Ramsey’s theorem for concluding provability in Peano arithmetic from cyclic provability. In their proofs, it is applied to ‘internalise’ the soundness justification given by the GTC into non-cyclic PA proofs.

Cohen et al. (2024) use a variant of Brotherston’s framework, that is, $\mathcal{T}_\mathbb{B}$ in our setting, to carry out a parameterised analysis of the worst-case complexity of various methods for checking soundness of cyclic proofs. The two parameters they considered, presented in terms of an ACD $(C, \mathrm{Tr} : \mathcal{P}_C \to\mathcal{T}_\mathbb{B})$ with $C = (T, \beta)$ , are vertex count $n = \left|T\right|$ and vertex width $w = \max_{t \in T} \left|\mathrm{Tr}(t)\right|$ . They find that many checking procedures, such as those based on automata akin to those sketched in Remark 6.2 and the Ramsey decision procedure of Section 5, are polynomial in vertex count n and exponential in vertex width w. They also propose an optimisation to the Ramsey decision procedure, called Order-reduced Transitive Looping procedure, which reduces the exponential degree in the vertex width w. We conjecture that all of their results can be extended to arbitrary $\mathcal{T}_\mathcal{A}$ .

In some sense, every cyclic proof system in the literature might be considered related work, as one can ask whether its trace condition can be modelled by our formalism. For most cyclic proof system we are aware of, including all those referred to in this article, this seems to be the case with three exceptions: The first is the bouncing-thread trace condition of Baelde et al. (2022) which considers traces that do not reside along the branches of a pre-proof. The second is the limit condition, presented by Hazard and Kuperberg (2022) in their system for transfinite word languages, which has traces running through multiple separate pre-proofs. The third are the higher-dimensional trace conditions of the hypersequent calculi of Das and Girlando (2022) and Afshari et al. (2023).

Since the publication of the conference version of this article, further work using the proposed framework of $\mathcal{A}$ -activated categories has been carried out by Leigh and Wehr (2023). The article covers reset proof systems, cyclic proof systems with a soundness that can be verified in polynomial time and which have proven fruitful for proof-theoretic investigation (see, e.g., Afshari and Leigh 2017; Afshari et al. 2021; Marti and Venema 2021). In the article, it is shown that for each cyclic proof system whose GTC is specified in terms of some $\mathcal{T}_\mathcal{A}$ , there exists an associated reset proof system which proves the same theorems. To obtain the reset proof system, the original proof system is equipped with an annotation mechanism which is derived from the trace sets and trace maps of the trace interpretation. In this application, the ‘naturality’ of a trace interpretation culminates in a natural reset proof system.