PROOF SYSTEMS FOR TWO-WAY MODAL MU-CALCULUS

Abstract

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.

1 Introduction

The modal $\mu $ -calculus is an extension of basic modal logic with least and greatest fixpoint operators. The additional operators are given an interpretation that breaks the locality of modal logic. Notably, the calculus can express all bisimulation-invariant monadic second-order properties [11]. As a consequence, well-studied modal logics such as the temporal logics $\mathsf {LTL}$ , $\mathsf {CTL}$ , and $\mathsf {CTL}^*$ and the program logic $\mathsf {PDL}$ can be translated into the $\mu $ -calculus. Many theoretical results on the modal $\mu $ -calculus have been established through its connection with automata theory and the theory of infinite games [8], the central observation being that every formula can be represented as an alternating tree automaton, and vice versa, such that the automaton accepts an infinite tree if and only if the tree is a model of the formula [10, 22].

The two-way modal $\mu $ -calculus, also known as the full $\mu $ -calculus, is an extension of the $\mu $ -calculus with modal operators for converses of accessibility relations. Thus, in addition to the standard modalities $[a]$ and ${\langle {a}\rangle }$ that quantify over a-successors (states reachable via a single a-labeled transition), the two-way $\mu $ -calculus includes modalities $[\breve {a}]$ and ${\langle {\breve {a}}\rangle }$ quantifying over a-predecessors. A central result, due to Vardi [21], is that the satisfiablity problem for the two-way $\mu $ -calculus is decidable in exponential time. To prove this result, Vardi introduces a notion of (alternating) two-way automaton and shows that for every formula of the two-way $\mu $ -calculus there is a two-way automaton that accepts an infinite tree if and only if the tree encodes a model of the formula. The decidability result then follows with a construction that provides for every two-way automaton an equivalent nondeterministic parity tree automaton. Vardi’s construction does not induce a translation of two-way $\mu $ -calculus formulas into equivalent $\mu $ -calculus formulas. The translation merely preserves satisfiability and validity. Indeed, two-way $\mu $ -calculus is strictly more expressive than its “one-way” fragment, for instance, it lacks the finite model property [20].

We present a sound and complete sequent calculus for the two-way $\mu $ -calculus. The proof theory of the logic has not been extensively explored. It is still an open question whether the calculus is complete with respect to a Hilbert-style axiomatisation that includes Kozen’s induction rule for the fixpoint operators. A complete finitary Hilbert-style axiomatisation of “flat” fragments is given in [7] and a cyclic system for the alternation-free fragment in [15]. A sound and complete infinitary proof system for the full calculus is provided in [2]. The system we present here is finitary. More precisely, proofs are represented as finite (cyclic) graphs with a local correctness criterion on simple cycles.

The proof system we introduce is a variant of systems developed for the modal $\mu $ -calculus by Dam and Gurov [5] and for the first-order $\mu $ -calculus by Dam and Sprenger [18]. It further incorporates ideas developed by Jungteerapanich [12] and Stirling [19], using a derivation rule influenced by the Safra-construction for $\omega $ -automata to formulate the correctness criterion on cycles. This approach has been utilised in [1] to introduce a path-based cyclic proof system for first-order $\mu $ -calculus that is complete for the fragment corresponding to the one-way $\mu $ -calculus.

The distinguishing feature of the proof systems developed by Dam and Gurov is to work in an extended syntax with explicit variables referring to ordinal approximants of least fixed-points, permitting the expression of propositions like “the least fixed point of the map $x\mapsto \varphi (x)$ is reached at a smaller ordinal than the least fixed point of $x \mapsto \psi (x)$ .” This added expressive power plays a crucial role in our completeness proof, allowing us to build small saturated sets of formulas, called tiles, from which a tree-like counter-model for an unprovable formula is constructed step by step. The added difficulty in the counter-model construction (compared to the modal $\mu $ -calculus) is that what is true at a vertex in the tree-model depends on both successors and predecessors of the vetex, a condition that needs to be taken into account in the saturation process.

The heart of Vardi’s decision procedure for the two-way $\mu $ -calculus is the use of auxiliary second-order variables as part of an extended alphabet for simulating non-determinism, allowing the simulating automaton to guess partial information about “loops” that can occur as a result of an alternating two-way automaton traversing the tree in both directions, i.e., ancestor to descendant or descendant to ancestor. These variables can then be projected away. In our setting, the “guessing” happens in the form of cuts on formulas that encode (via ordinal variables) information about fixpoint unfoldings. We do not know whether our system is complete without the cut rule. A crucial part of our completeness argument, however, shows that the cut formulas can be chosen to belong to a relatively small finite set. Therefore, although the proof system is not cut-free, it does support automatic proof search.

Outline

The structure of this paper is as follows: In Section 2 we discuss the necessary preliminaries related to the two-way $\mu $ -calculus and annotated formulas. Section 3 contains the definition of our cyclic proof system. In Section 4 we prove that this system is sound. The completeness proof consists of two parts: In Section 5 we first show completeness for a particular class of non-wellfounded proofs, which we call slim proofs. In Section 6 we then show that every slim proof can be transformed into a cyclic proof in our system.

2 Two-way $\mu $ -calculus

The syntax of the two-way $\mu $ -calculus makes use of the following non-logical symbols: a countably infinite set $\mathrm {Prop}$ of propositional constants or proposition letters (denoted $p, q, p_0, \ldots $ ), with an involution $p \mapsto \overline {p}$ ; a countably infinite set $\mathrm {Act}$ of action symbols (denoted $a, b, a_0, \dotsc $ ), with an involution $a \mapsto \breve {a}$ ; and a countably infinite set $\mathrm {FV}$ of fixed point variable symbols (denoted $x, y, z, \dotsc $ ).

It will be convenient for us to work with formulas that are in negation normal form. That is, the set of (plain) two-way $\mu $ -calculus formulas is given by the following grammar:

We will need the following basic syntactic definitions. The set $\mathit {Sfor}(\varphi )$ of subformulas of $\varphi $ is defined as usual. The set of variables that occur in $\varphi $ is denoted by $\mathrm {Var}(\varphi )$ . Since the fixpoint operators $\mu $ and $\nu $ bind the variables that they occur with, we can define in a standard way the notions of free and bound variables; a sentence is a formula without free variables. The unfolding of a fixpoint formula $\sigma x\, \varphi $ is the formula $\varphi [\sigma x\, \varphi /x]$ that we obtain by substituting $\sigma x\, \varphi $ for x in $\varphi $ ; here we ensure that this substitution never causes variable capture (so that no renaming of variables is needed). The closure $\mathrm {Clos}(\Gamma )$ of a set $\Gamma $ of formulas is defined as the smallest set of formulas that is closed under taking Boolean subformulas, modal subformulas, unfoldings of fixpoint formulas, and single negations. It is well-known that for every formula $\varphi $ the closure $\mathrm {Clos}(\{\varphi \})$ is a finite set.

The semantics of formulas is given in terms of models $M = (W,R,V)$ , where W is any set, R provides for every $a \in \mathrm {Act}$ a relation $R_{a} \subseteq W \times W$ such that $R_{\breve {a}}$ is the converse $R_{\breve {a}} = \{(v,w) \mid (w,v) \in R_{a} \}$ of $R_{a}$ for all $a \in \mathrm {Act}$ , and $V : \mathrm {Prop} \to \mathcal {P} W$ is any function. The elements of W are called worlds, the relation $R_{a}$ is the accessibility relation for a, and the function V is the valuation function.

The semantic clauses for the two-way $\mu $ -calculus are completely standard. The Boolean and modal connectives are interpreted as in modal logic, where the relation $R_{a}$ is used for the modality $\langle a \rangle $ . The semantic value of the fixpoint formulas $\mu x \, \varphi $ and $\nu x \, \varphi $ are the least and greatest fixpoints of the monotone map that describes the interpretation of $\varphi $ as depending on an interpretation of the variable x. A precise formulation of the semantic clauses is given in the following subsection. The two-way $\mu $ -calculus introduced here is a fragment of the language of annotated formulas that is discussed in the following subsection.

2.1 Annotated formulas

The proof systems that we shall introduce here admit formulas with quantified versions of the fixpoint operators, involving a countable set $\mathrm {OV}$ of ordinal variables (denoted $\kappa , \lambda , \kappa _0, \ldots $ ). Since we will also allow quantifiers over these ordinal variables, the formulas that we work with will be of the following form:

A formula which does not contain any ordinal variables, i.e., a formula of the two-way modal $\mu $ -calculus, is called plain. The underlying plain formula of a formula $\varphi $ , denoted $\mathsf {u}(\varphi )$ , is the plain formula obtained from erasing all ordinal annotations and quantifiers from $\varphi $ :

$$ \begin{gather*} \begin{aligned} \mathsf{u}(x) &= x & \mathsf{u}(\varphi \wedge \psi ) &= \mathsf{u}(\varphi ) \wedge \mathsf{u}(\psi) & \mathsf{u}( [a] \varphi ) &= [a] \mathsf{u}(\varphi ), \\ \mathsf{u}(p) &= p & \mathsf{u}(\varphi \vee \psi ) &= \mathsf{u}(\varphi ) \vee \mathsf{u}(\psi) & \mathsf{u}( {\langle{a}\rangle} \varphi ) &= {\langle{a}\rangle} \mathsf{u}(\varphi ), \end{aligned} \\ \begin{aligned} \mathsf{u}( \eta x^{\kappa} \varphi ) &= \eta x \, \mathsf{u}(\varphi ) & \mathsf{u}( \forall \lambda < \kappa \, \varphi ) &= \mathsf{u}(\varphi ), \\ \mathsf{u}( \eta x \varphi ) &= \eta x \, \mathsf{u}(\varphi ) & \mathsf{u}( \exists \lambda < \kappa \, \varphi ) &= \mathsf{u}(\varphi ). \end{aligned} \end{gather*} $$

The semantics of this language can be defined as follows. If $f \colon \mathcal {P} W \rightarrow \mathcal {P} W$ is a monotone function on the powerset of W we identify two ways of iterating f along ordinals: $f^{\kappa }_{\top } \in \mathcal {P} W$ denotes the result of iterating $f \ \kappa $ -many times on the starting from W, and $f^{\kappa } _{\bot } \in \mathcal {P} W$ the $\kappa $ -th iterant of f starting from $\emptyset $ :

$$\begin{align*}f^{\kappa} _{\top} = \bigcap_{\xi < \kappa } f( f^{\xi}_{\top} ) \qquad\qquad f^{\kappa} _{\bot} = \bigcup_{\xi < \kappa } f( f^{\xi}_{\bot} ). \end{align*}$$

Note that $f^0_{\top } = W$ and $f^0_{\bot } = \emptyset $ . Given a model $M = (W,R,V)$ , an ordinal assignment is a map o assigning an ordinal $o(\kappa )$ to each ordinal variable $\kappa $ . Then the meaning $[\![\varphi ]\!]^o_M$ of a formula $\varphi $ in this model and under this assignment is inductively defined as follows. We write $[\![\lambda x. \varphi ]\!]$ to express the monotone map $Z \mapsto [\![\varphi ]\!]^o_{M[x\mapsto Z]}$ on $\mathcal {P} W$ .

• • For a propositional variable p, $[\![p]\!]^o_M = V(p)$ .

• • Standard clauses for Booleans and modalities.

• • $[\![\mu x^{\kappa }.\varphi ]\!]^o_M $ is the $o(\kappa )$ -th iterant of $[\![\lambda x. \varphi ]\!]$ on $\emptyset $ , i.e., $[\![\mu x^{\kappa }.\varphi ]\!]^o_M = [\![\lambda x. \varphi ]\!]_{\bot }^{o(\kappa )}$ .

• • $[\![\nu x.\varphi ^{\kappa }]\!]^o_M $ is the $o(\kappa )$ -th iterant of $[\![\lambda x. \varphi ]\!]$ on W, i.e., $[\![\nu x^{\kappa }.\varphi ]\!]^o_M = [\![\lambda x. \varphi ]\!]_{\top }^{o(\kappa )}$ .

• • $[\![\mu x.\varphi ]\!]^o_M$ is the least fixpoint $[\![\lambda x. \varphi ]\!]$ , namely $ [\![\mu x.\varphi ]\!]^o_M = \bigcup _{\xi } [\![ \lambda x. \varphi ]\!]^{\xi }_{\bot }$ .

• • $[\![\nu x.\varphi ]\!]^o_M$ is the greatest fixpoint of $[\![\lambda x. \varphi ]\!]$ , namely $ [\![\nu x.\varphi ]\!]^o_M = \bigcap _{\xi } [\![ \lambda x. \varphi ]\!]^{\xi }_{\top }$ .

• • $[\![\exists \lambda < \kappa .\varphi ]\!]^o_M = \{u \in W \mid \exists \xi < o(\kappa ) : u \in [\![\varphi ]\!]^{o[\lambda \mapsto \xi ]} _M \}$ .

• • $[\![\forall \lambda < \kappa .\varphi ]\!]^o_M = \{u \in W \mid \forall \xi < o(\kappa ) : u \in [\![\varphi ]\!]^{o[\lambda \mapsto \xi ]} _M \}$ .

We write $M,u \vDash _o \varphi $ if $u \in [\![\varphi ]\!]^o_M$ . If $\varphi $ is a plain formula we may write simply $M,u\vDash \varphi $ .

We think of negation as an operation on sentences, extending the involution on proposition letters, and determined by connective duality. Inductively we define the operation $\varphi \mapsto \overline {\varphi }$ for all formulas:

$$ \begin{align*} \overline{x} &= x & \overline{\varphi \wedge \psi} &= \overline{\varphi } \lor \overline{\psi} & \overline{[a] \varphi } &= {\langle{a}\rangle} \overline{\varphi } & \overline{\mu x^{\kappa} \varphi } &= \nu x^{\kappa} \, \overline{\varphi } & \overline{\forall \lambda < \kappa \, \varphi } &= \exists \lambda < \kappa \, \overline{\varphi } \\ & & \overline{\varphi \lor \psi} &= \overline{\varphi } \land \overline{\psi} & \overline{{\langle{a}\rangle} \varphi } &= [a] \overline{\varphi } & \overline{\nu x^{\kappa} \varphi } &= \mu x^{\kappa} \, \overline{\varphi } & \overline{\exists \lambda < \kappa \, \varphi } &= \forall \lambda < \kappa \, \overline{\varphi }. \end{align*} $$

It is routine to show that on the set of sentences this operation indeed behaves as classical negation. Furthermore, observe that this operation is an involution on the set of formulas, and that the negation of a plain formula is plain.

2.2 Subsumption, well-annotated formulas, and active variables

In this subsection we define some notions that are not needed in the definition of the proof systems but play a key role in our reasoning about the properties of the proof system.

The subsumption order $<_{\rho }$ associated with a formula $\rho $ is defined as the smallest preorder on $\mathrm {Var}(\rho )$ such that $x <_{\rho } y$ if $\rho $ has a subformula $\sigma y \psi $ of which x is a free variable. Observe that the subsumption order of a fixpoint formula is identical to that of its unfolding. By taking, if needed, alphabetic variants (i.e., renaming the bound variables in $\rho $ ) we may always assume that the subsumption order of a given formula is a strict partial order. It may occasionally be convenient to make the following assumption which is possible without loss of generality.

Convention 2.1. In some parts of this paper we will restrict attention to a fixed finite set $\Gamma _0$ of plain formulas in which distinct occurrences of fixed point quantifiers are associated with distinct variables, and its closure. We then may assume a strict partial order $<$ on the set of fixpoint variables occurring in $\Gamma _0$ which is such that $\mathord {<} \supseteq \mathord {<_{\varphi }} \cap (\mathrm {Var}(\varphi ) \times \mathrm {Var}(\varphi ))$ , for all $\varphi \in \mathrm {Clos}(\Gamma _0)$ . The order $<$ will be referred to as the subsumption order. If $x < y$ we refer to x as being higher ranked than y.

Definition 2.2. An annotation is a partial function from fixed point variables to ordinal variables. Let $x_0 , x_1 , \dotsc $ enumerate the fixed point variables in decreasing order with respect to subsumption. Given an annotation o and $n \in \omega $ , $o \upharpoonright n$ is the restriction of o to the domain $\{ x_i \mid i < n \}$ . Given a plain formula $\varphi $ and annotation $o \colon \mathrm {FV} \to \mathrm {OV}$ define a (nonplain) formula $\varphi ^o$ as follows:

$$ \begin{gather*} \begin{aligned} x^o &= x &\qquad ( \psi \wedge \theta )^o &= \psi^o \wedge \theta^o &\qquad ([a] \varphi )^o &= [a] \varphi ^o, \\ p^o &= p & ( \psi \vee \theta )^o &= \psi^o \vee \theta^o & ( {\langle{a}\rangle} \varphi )^o &= {\langle{a}\rangle} \varphi ^o, \end{aligned} \\ ( \eta x_i \psi )^o = \begin{cases} \eta x_i^{o(x_i)} \psi^{o \upharpoonright i }, & \text{if } x_i \in \mathop{dom} o, \\ \eta x_i \psi^{o \upharpoonright i }, & \text{otherwise.} \end{cases} \end{gather*} $$

Definition 2.3. A formula $ \varphi $ is well-annotated if there exists an annotation o such that $ \varphi = \mathsf {u}(\varphi )^{o}$ . The annotation o satisfying this equation with smallest domain is named $\mathsf {o}_{\varphi } $ . $\varphi $ is positively annotated if it is well-annotated and $\mathop {dom} ( \mathsf {o}_{\varphi } )$ consists only of $\nu $ -fixed point variables of $\varphi $ . The negation of a positively annotated formula is said to be negatively annotated.

Note that plain formulas are positively annotated, and that well-annotated formulas do not contain quantifiers.

Definition 2.4. Given a set of formulas $\Gamma $ , we say that an ordinal variable $ \kappa $ is active in $\Gamma $ if $\kappa $ occurs free in some positively annotated formula in $ \Gamma $ . The set of active variables in $\Gamma $ is denoted by $\mathrm {Act}(\Gamma )$ .

2.3 Game semantics

In this section we briefly review the game-theoretic semantics for the two-way $\mu $ -calculus; this will prove to be a useful approach in the completeness argument further on.

The evaluation game $\mathcal {E}(M,\varphi )$ of a formula $\varphi $ on a model $M = (W,R,V)$ is an infinite board game, the players of which we shall call Verifier and Falsifier. The positions of the game are all pairs of the form $(w,\psi )$ , where $w \in W$ and $\psi \in \mathrm {Clos}(\varphi )$ . The player to move at a given position and the moves at his or her disposal are listed in Table 1.

Table 1 The evaluation game $\mathcal {E}(M,\varphi )$ .

Any match or play of this game consists of a (finite or infinite) sequence $(w_n,\varphi _n)_{n<\kappa }$ of positions (with $\kappa \leq \omega $ ). A finite match, i.e., with $\kappa < \omega $ , is won by a player if it is their opponent who is supposed to move at the last position $(w_{\kappa -1}, \varphi _{\kappa -1})$ , while there is no move available.

To determine the winner of an infinite match $(w_n,\varphi _n)_{n<\omega }$ we observe that the induced sequence $(\varphi _n)_{n<\omega }$ of formulas is an infinite trace, that is: for every $i<\omega $ , either $\varphi _i$ is a fixpoint formula and $\varphi _{i+1}$ is its unfolding, or else $\varphi _{i+1}$ is a direct (modal or Boolean) subformula of $\varphi _i$ . It is well known that for every infinite trace $\tau = (\varphi _n)_{n<\omega }$ there is a unique formula that occurs infinitely often on $\tau $ and is a subformula of $\varphi _n$ for cofinitely many n. We will call this formula, which must be a fixpoint formula, the most significant formula of $\tau $ , and we declare Verifier (Falsifier) to be the winner of an infinite match $(w_n,\varphi _n)_{n<\omega }$ if the most significant formula of the induced trace $(\varphi _n)_{n<\omega }$ is a $\nu $ -formula (a $\mu $ -formula, respectively). It is well known that this winning condition can be formulated as a parity condition and that consequently the game $\mathcal {E}(M,\varphi )$ has positional determinacy.

Theorem 2.5 (Adequacy of evaluation games).

For any plain formula $\varphi $ , model M, and world w, we have $M,w \vDash \varphi $ if and only if the position $(w,\varphi )$ is winning for Verifier in $\mathcal {E}(M,\varphi )$ .

For a proof of the theorem see, e.g., [6].

3 Proof systems

In this section we first define the finitary, cyclic proof system that is the subject of this paper and then discuss infinitary, non-wellfounded proofs that are needed for our completeness argument.

3.1 Sequents and constraints

The sequents in our proof system contain a constraint that describes the relative size of ordinal variables and keeps track of the order in which they are introduced.

Definition 3.1. A constraint is a tuple $\mathcal {O} = ( O , < , \triangleleft )$ where:

1. 1. O is a finite set of ordinal variable symbols, called the domain,

2. 2. $<$ is an irreflexive, transitive and upwards linear ordering $< $ (so $(O ,> )$ is a finite forest), called the descendant relation,

3. 3. $\triangleleft $ is a total linear order on $\mathcal {O}$ , called the age relation, consistent with the ancestor relation: $\kappa < \lambda $ implies $ \lambda \triangleleft \kappa $ for all $\kappa , \lambda \in O$ .

Given a constraint $\mathcal {O} = ( O , <_{\mathcal {O}} , \triangleleft _{\mathcal {O}} )$ , we write $\mathrm {OV}(\mathcal {O})$ for O, the set of ordinal variables appearing in $\mathcal {O}$ . When there is no risk of confusion, we identify the constraint $\mathcal {O}$ with the set $\mathrm {OV}(\mathcal {O})$ , writing $\kappa \in \mathcal {O}$ rather than the formally precise $\kappa \in \mathrm {OV}(\mathcal {O})$ . The reflexive closure of $<_{\mathcal {O}}$ is denoted $\le _{\mathcal {O}}$ .

Definition 3.2. A sequent is an expression $\mathcal {O} : \Gamma $ where $\mathcal {O}$ is a constraint and $\Gamma $ is a finite set of formulas whose free ordinal variables are elements of $\mathcal {O}$ . We sometimes write a sequent $\mathcal {O} : \Gamma $ as just $ \Gamma $ , denoting $\mathcal {O}$ by $\mathcal {O}( \Gamma )$ .

Given a constraint $\mathcal {O}$ and $\kappa \in \mathcal {O}$ , a descendant of $\kappa $ is any $\lambda \in \mathcal {O}$ such that $\lambda <_{\mathcal {O}} \kappa $ , in which case $\kappa $ is called an ancestor of $\lambda $ (in $\mathcal {O}$ ). We say $\lambda $ is a child of $\kappa $ , or that $\kappa $ is the parent of $\lambda $ , if $\lambda <_{\mathcal {O}} \kappa $ and there is no $\rho \in \mathcal {O}$ such that $\lambda <_{\mathcal {O}} \rho $ and $\rho <_{\mathcal {O}} \kappa $ . Every $\kappa \in \mathcal {O}$ has at most one parent, but may have multiple children. If $\kappa \triangleleft _{\mathcal {O}} \lambda $ we say that $\kappa $ is older than $\lambda $ (relative to $\mathcal {O}$ ).

A substitution on ordinal variables is simply a map $\sigma : \mathrm {OV} \to \mathrm {OV}$ . With respect to a constraint $\mathcal {O}$ we call a substitution $\sigma $ increasing if $\lambda \le _{\mathcal {O}} \sigma (\lambda )$ for all $\lambda $ , and decreasing if $\sigma (\lambda ) \le _{\mathcal {O}} \lambda $ for all $\lambda $ .

For later use we introduce two auxiliary relations on a constraint $\mathcal {O}$ . First of all, we say that $\lambda $ is to the left of $\rho $ if $\lambda $ and $\rho $ are incomparable with respect to $\leq _{\mathcal {O}}$ and $\lambda ' \triangleleft _{\mathcal {O}} \rho '$ , where $\lambda '$ is the $<$ -greatest ancestor of $ \lambda $ that is not an ancestor of $ \rho $ and $ \rho ' $ is the $<$ -greatest ancestor of $ \rho $ that is not an ancestor of $ \lambda $ . We then define $\lambda \prec _{\mathcal {O}} \rho $ if $\lambda <_{\mathcal {O}} \rho $ or $ \lambda $ is to the left of $ \rho $ , and we sometimes denote $\lambda \prec _{\mathcal {O}} \rho $ as $\lambda \prec _{\mathcal {O}} \rho $ . As we will see later, $\prec _{\mathcal {O}}$ is in fact a strict linear order.

Here is an example to illustrate the different orders on ordinal variables and how they are related. Consider a constraint $\mathcal {O}$ containing seven ordinal variables , where $\kappa _0 \triangleleft _{\mathcal {O}} \dotsm \triangleleft _{\mathcal {O}} \kappa _{6}$ and $<_{\mathcal {O}}$ is the transitive closure of

$$\begin{align*}\{(\kappa_3,\kappa_1),(\kappa_4,\kappa_1),(\kappa_5,\kappa_2),(\kappa_6,\kappa_2),(\kappa_1,\kappa_0),(\kappa_2,\kappa_0)\}.\end{align*}$$

Represented as a tree the $<_{\mathcal {O}}$ -relation is shown in Figure 1. The figure is drawn so that, with the age relation as specified, the “left-of” relation between ${<_{\mathcal {O}}}$ -incomparable variables can be read off directly from the diagram. So $\kappa _3$ is to the left of $\kappa _2,\kappa _4,\kappa _5,\kappa _6$ , while $\kappa _1$ is to the left of $\kappa _2,\kappa _5,\kappa _6$ , etc. The $\prec _{\mathcal {O}}$ relation is thus the strict linear order given by

$$\begin{align*}\kappa_3 \prec_{\mathcal{O}} \kappa_4 \prec_{\mathcal{O}} \kappa_1 \prec_{\mathcal{O}} \kappa_5 \prec_{\mathcal{O}} \kappa_6 \prec_{\mathcal{O}} \kappa_2 \prec_{\mathcal{O}} \kappa_0.\end{align*}$$

To simplify notation we introduce a special symbol $\star $ and write $o(x) = \star $ for an annotation o if $x \notin \mathop {dom} (o)$ . Given an ordinal constraint $\mathcal {O}$ , we extend the order $<_{\mathcal {O}}$ to $\mathcal {O} \cup \{\star \}$ by setting $\kappa <_{\mathcal {O}} \star $ for every ordinal variable $\kappa $ in $\mathcal {O}$ . Note that $\prec _{\mathcal {O}}$ , with its definition extended to incorporate $\star $ , is still a linear order over $\mathcal {O} \cup \{\star \}$ and $\kappa \prec _{\mathcal {O}} \star $ for every ordinal variable $\kappa $ in $\mathcal {O}$ .

Figure 1 A sample constraint.

The semantics of sequents is given as follows.

Definition 3.3. Let $M = (W,R,V)$ be a model. A sequent $\mathcal {O} : \Gamma $ holds in M if for all ordinal assignments o such that $o(\kappa ) < o(\lambda )$ whenever $\kappa <_{\mathcal {O}} \lambda $ we have that $\bigcup \{[\![\varphi ]\!]^o_M \mid \varphi \in \Gamma \} = W$ . We say that an ordinal assignment o refutes $\mathcal {O} : \Gamma $ in M if $o(\kappa ) < o(\lambda )$ whenever $\kappa <_{\mathcal {O}} \lambda $ , but $\bigcup \{[\![\varphi ]\!]^o_M \mid \varphi \in \Gamma \} \neq W$ .

3.2 Rules and derivations

The sequent calculus we introduce makes use of three operations on constraints: The operation denoted $ \mathcal {O} + \lambda $ extends $\mathcal {O}$ by a fresh variable $ \lambda $ as the youngest element and makes no change to the descendant relation. As a variation, in $ \mathcal {O}+_{\kappa } \lambda $ the variable $ \lambda $ is also added as a child of $\kappa $ . That is, for $\mathcal {O} = ( O , < , \triangleleft )$ , $\lambda \in O$ and $\kappa \in O$ :

$$ \begin{align*} \mathcal{O} + \lambda &= ( O \cup \{ \lambda \} , \mathord< , \mathord \triangleleft \cup \{ ( \rho , \lambda ) \mid \rho \in O \} ), \\ \mathcal{O} +_{\kappa} \lambda &= ( O \cup \{ \lambda \} , \mathord< \cup \{ ( \lambda , \kappa ' ) \mid \kappa \leq \kappa' \} , \mathord \triangleleft \cup \{ ( \rho , \lambda ) \mid \rho \in O \} ). \end{align*} $$

In both the above constructions it is a requirement that $\lambda $ does not occur already in $\mathcal {O}$ .

The third construction is the restriction of a constraint to a set of ordinal variables. Given $\mathcal {O}$ as above and $V \subseteq O$ , we define $\mathcal {O} \setminus V$ to be the constraint

$$\begin{align*}\mathcal{O} \setminus V = ( O' , \mathord < \cap ( O' \times O' ) , \mathord \triangleleft \cap ( O' \times O ') ) \qquad\text{where } O' = O \setminus V. \end{align*}$$

Using these operations we can define the inference rules of our sequent calculus. These are presented in Table 2, where we use the expression $\mathcal {O}(\lambda < \kappa )$ to refer to a constraint $\mathcal {O}$ such that $\lambda <_{\mathcal {O}} \kappa $ . A tree constructed by applications of these rules, and labelled with sequents and names of the rules applied, will be called a derivation. We shall reserve the term proof for derivations satisfying one of several syntactic criteria guaranteeing validity, defined in the following sections. Given a derivation $\Pi $ and a vertex m in $\Pi $ , the sequent labelling m is denoted $\Pi (m)$ .

Table 2 Rules of sequent calculus.

Note that these rules feature no side conditions, besides the obvious constraint that all sequents involved in a rule instance must be bona fide sequents. This means that the $\forall $ -rule satisfies the usual eigenvariable condition: the variable $\lambda $ appearing in the premise cannot occur in the conclusion. If it had occurred in some formula, then by definition of a sequent it should also appear in the constraint, meaning that the constraint $\mathcal {O}+_{\kappa } \lambda $ appearing in the premise would not be well-defined. A similar eigenvariable constraint holds for the rule $\nu (\kappa )$ , and for the same reason. In the same vein, observe that in an application of $\mathsf {lw}$ , for the premise to be a well-formed sequent, no ordinal variable in the set V may occur free in $\Gamma $ .

The reader may have noticed that the cut rule also has a hidden restriction due to the definition of a sequent: the cut formula will never contain an ordinal variable that does not occur in the conclusion. This is not as restrictive as it may at first seem. Cuts can still be used to introduce new ordinal variables in proof search, since the cut formulas may contain quantifiers which can then be instantiated, such as in the following:

The calculus does not feature a rule for introducing an unapproximated least fixed point from an approximant, for instance,

Although sound, the above rule is not necessary for a complete sequent calculus. Without such a rule, derivations have the property that explicitly approximated least fixed points only arise from premises of the cut rule.

Proposition 3.4. Let R be an instance of any of the derivation rules except cut, with conclusion $\mathcal {O}:\Gamma $ . If every formula in $\Gamma $ is well-annotated, then every formula appearing in a premise of R is well-annotated.

Proof By inspection of the proof rules.

Further on we shall frequently need to employ the following minimisation rule:

This rule is easily derived via a cut:

Intuitively, we can view the minimisation rule as expressing a case distinction for how we may construct a counter-model to $\Gamma $ , in particular when $\Gamma $ contains the formula $\varphi [\nu x^{\kappa }\psi /z]$ : either we decide that $\kappa $ is the smallest ordinal approximant of the fixpoint $\nu x \psi $ for which the formula fails to hold, or we introduce a name $\kappa _0$ for smaller ordinal approximant such that $\varphi [\nu x^{\kappa _0}\psi /z]$ fails to hold. In the sequel we shall assume that the minimisation rule is a rule of our proof systems.

3.3 Cyclic proofs

We now present our main notion of a valid proof, which is based on “cyclic” derivations, which can be seen as finite representations of infinite but regular, non-wellfounded proof trees. It is straightforward to show that having no restrictions on allowed cycles trivialises the calculus, allowing any sequent to be derived by a cyclic proof. The notion of cyclic proof therefore comes equipped with a condition on cycles, called the correctness criterion, ensuring only valid sequents are derivable. First, we define more precisely what is meant by a “cycle.”

Definition 3.5. A derivation with back-edges is a pair $( \Pi , c )$ where $\Pi $ is a derivation and c is a partial function from the leaves of $\Pi $ to inner nodes of $\Pi $ , called the companion function, such that for every leaf $l \in \mathop {dom} c$ ,

• • l and $c(l)$ are labelled by the same sequent, i.e., $\Pi (l) = \Pi (c(l))$ , and

• • l is an ancestor of $c(l)$ .

We call $c(l)$ the companion of l.

Note that our requirement that a leaf l is labelled by the same sequent as its companion $c(l)$ entails more than just the same formulas occurring in the leaf and companion. It also implies that the constraints are identical, which means in particular that the relative ages of ordinal variables in leaf and companion are the same. This plays a dual role. On one hand, it facilitates proof search, and will be used extensively in our completeness argument. For this purpose, however, it is not clear that the age ordering needs to be incorporated directly into the definition of a valid proof. We shall see that, in fact, the age ordering also plays a crucial role in ensuring that the proof system is sound. It is for this reason that it is explicitly part of the proof system, rather than just an auxiliary technical device used to prove completeness.

It remains to formulate a criterion for distinguishing valid cyclic proofs from invalid derivations. For our purposes, the correctness criterion can be formulated as a particular instance of the structural rule $\mathsf {lw}$ occurring on the path between companion and leaf. We thus begin with isolating these special instances of weakening, henceforth called resets.

Definition 3.6. The reset rule is any instance of constraint weakening of the form

such that:

1. 1. $\kappa \in \mathcal {O}$ and $\kappa $ does not occur in $\Gamma $ .

2. 2. K is the set of children of $\kappa $ in $\mathcal {O}$ .

Note that, since derivations are assumed to be well formed, the children of $\kappa $ , namely the variables in K above, do not occur in $\Gamma $ .

Definition 3.7. Let $( \Pi , c )$ be a derivation with back-edges and let $l \in \mathop {dom} c$ be labelled by a sequent $\mathcal {O} : \Gamma $ . An ordinal variable $\kappa \in \mathcal {O}$ is a reset variable for l if::

1. 1. $\kappa $ occurs in the constraint at every vertex on the path from $c(l)$ to l.

2. 2. An instance of $\mathsf {reset}(\kappa )$ occurs on this path.

A leaf of $\Pi $ is successful if some variable is a reset variable for the leaf.

We can now stipulate the correctness criterion for cyclic proofs.

Definition 3.8. A cyclic proof is a finite derivation with back-edges $( \Pi , c )$ such that $\mathop {dom} c$ contains all non-axiomatic leaves of $\Pi $ and every leaf in $\mathop {dom} c$ is successful. We write $\vdash \mathcal {O} : \Gamma $ to express the existence of a cyclic proof with root labelled by $\mathcal {O} : \Gamma $ .

Given a plain formula $\rho $ , a cyclic proof of $\rho $ is a cyclic proof with end sequent $\emptyset : \rho $ , where $\emptyset $ denotes the empty constraint, i.e., the unique constraint in which the underlying set of ordinal variables is empty. We write $\vdash \rho $ to say there exists a cyclic proof of $\rho $ .

Examples of cyclic proofs are given in Figures 2 and 3. The former presents a simple case of excluded middle for the formula $\mu y.\, p \vee {\langle {a}\rangle } y$ . The proof involves a single non-axiomatic leaf, denoted by $\ast $ . Along the path from this leaf to its companion (also marked $\ast $ ), the variable $\kappa $ appears in every constraint and is reset. Hence, this path is successful. A cyclic proof of the formula $p \rightarrow \nu x.\, [\breve {a}] x \wedge \mu y.\, p \vee {\langle {a}\rangle } y$ is given in Figure 3. This formula expresses the property that for every $\breve {a}$ -path there is a “returning” a-path. The proof in Figure 3 also displays a single non-axiomatic leaf whose companion is the inner sequent marked as †, though each of the five omitted subproofs of $\overline Y , Y$ also involves an internal leaf-companion pair as per Figure 2. As the variable $\kappa $ occurs in the constraint of every sequent along the connecting path, this leaf is successful. Note that in both examples, the repeating cycles require two applications of the reset rule. The reason for this is that we require leaves and companions to be identical as sequents. This is just a technical convenience; one could instead formulate a weaker condition on leaf-companion pairs, requiring identity only up to a renaming of ordinal variables. Some care is needed to ensure soundness however; the precise formulation of such a condition was worked out in [1].

Figure 2 Cyclic proof of the sequent $\overline {\mu y.\, p \vee {\langle {a}\rangle } y} , \mu y.\, p \vee {\langle {a}\rangle } y$ . The relation of non-axiomatic leaves to companions is denoted by $\ast $ . The proof employs the following abbreviations: Y and $Y^{\kappa }$ denote the formulas $\mu y.\, p \vee {\langle {a}\rangle } y$ and $\mu y^{\kappa }.\, p \vee {\langle {a}\rangle } y$ respectively; constraints are abbreviated to $\kappa $ for $( \{ \kappa \} , \emptyset , \emptyset )$ , $\kappa \kappa '$ for $\kappa +_{\kappa } \kappa '$ and $\kappa \kappa ' \kappa "$ for $(\kappa \kappa ') +_{\kappa '} \kappa "$ .

Figure 3 Cyclic proof of the formula $\overline p \vee \nu x.\, [\breve {a}] x \wedge \mu y.\, p \vee {\langle {a}\rangle } y$ . Subproofs of the sequent $\emptyset : \overline Y , Y$ are as in Figure 2 and omitted. The relation of non-axiomatic leaves to companions is denoted by †. The proof employs the same abbreviations as Figure 2 with, in addition, X and $X^{\kappa }$ denoting formulas $\nu x.\, [\breve {a}] x \wedge Y$ and $\nu x^{\kappa }.\, [\breve {a}] x \wedge Y$ respectively.

For certain proofs in the following, it will be convenient to consider a conditional notion of cyclic proof, i.e., cyclic proofs from assumptions. For this notion of proof it is important to restrict the application of structural rules on paths from the conclusion to assumptions.

Definition 3.9. Let $\mathcal S \cup \{ \mathcal {O} : \Gamma \}$ be a set of sequents. A (cyclic) proof of $\mathcal {O} : \Gamma $ from assumptions $\mathcal S$ is a finite derivation with back-edges $( \Pi , c )$ such that every leaf $l \in \mathop {dom} c$ is successful and every leaf $l \in \mathop {dom} c$ is either an axiom, or else (i) it is labelled by a sequent in $\mathcal S$ , and (ii) there is no application of $\mathsf {lw}$ (including reset rules) on the path from the root of $\Pi $ to l.

We are now ready to state our main result:

Theorem 3.10 (Soundness and completeness).

Let $\rho $ be any plain formula of the two-way $\mu $ -calculus. Then $\rho $ is valid if, and only if, it has a cyclic proof.

The remainder of the paper is devoted to proving Theorem 3.10. Section 4 culminates in the proof of soundness. Completeness is the subject of Sections 5 and 6.

The proof of completeness of the cyclic proof system relies on completeness of non-wellfounded proofs, where the correctness condition on infinite branches is stipulated in terms of infinite descending chains of ordinal variables in the controls of sequents along infinite paths. In their most general formulation, completeness for such proofs is easy to prove, but not very helpful towards proving the main theorem since non-wellfounded proofs can be highly non-regular without any bound on the size of sequents in a proof tree.

Therefore, we isolate a sub-class of non-wellfounded proofs, called slim proofs, which, although not finitely presentable in general, are in an important sense closer to the finitary notion of provability: in slim proofs, the number of formulas that can appear in sequents is bounded. Constraints, however, can grow without bound. Finitising the constraints is the second step towards obtaining a cyclic proof for a valid sequent. Completeness with respect to slim proofs is established via a two-player game that we call the mosaic game, in which one player (Prover) tries to construct a proof of the root formula, and the opposing player (Refuter) attempts to build a counter-model by selecting certain “saturated” sequents called tiles.

With completeness of slim proofs in place, the next step is to insert uses of the reset rule in order to bound the size of constraints. This transformation alters the correctness condition on infinite paths from an infinite descent condition to an infinitary version of the reset condition from cyclic proofs: every infinite branch features some ordinal variable that is reset infinitely often. The final step of the completeness argument is to show that any non-wellfounded slim derivation satisfying the infinite reset condition can be pruned to a finite, cyclic proof.

3.4 Non-wellfounded proofs

In the proof of completeness for cyclic derivations we will make extensive use of an intermediate notion of proof based on infinite, or non-wellfounded, derivations. In analogy with the case of cyclic proofs, an infinite derivation will be considered a proof provided every infinite path in the derivation fulfils a syntactic criterion. Later we will consider infinite proofs where correctness is based on an (infinitary) notion of reset variable. For now we introduce the concept of an infinite descent proof where the requirement on infinite paths is that the sequence of constraints in the path induces an infinite descending sequence of ordinal variables.

Definition 3.11. Let $P =( \mathcal {O}_i )_{ i < \omega }$ be an infinite sequence of constraints.

We say that P has an infinite $<$ -descending chain of ordinals if there are an infinite sequence $(\kappa _i)_{i < \omega }$ of ordinal variables and an increasing function $\sigma : \omega \to \omega $ such that for every i it holds that $\kappa _{i + 1} <_{\mathcal {O}_{\sigma (i)}} \kappa _i$ and $\kappa _{i + 1} \in \mathrm {OV}(\mathcal {O}_l)$ for all $l \in \{\sigma (i),\sigma (i) + 1,\dots ,\sigma (i + 1)\}$ . An infinite $\prec $ -descending chain of ordinals is defined analogously.

An infinite derivation is said to be an infinite descent proof if every leaf is an axiom, and every infinite path is such that the sequence of constraints through this path has an infinite $<$ -descending chain of ordinal variables.

Definition 3.12. A finite proof tree is said to be a wellfounded proof if every leaf is labelled by a sequent of the form $\mathcal {O} : \varphi , \overline {\varphi }$ .

4 Soundness

In this section we show how to prove soundness for the cyclic and non-wellfounded variants of the proof system that is defined in the previous section. We start with the soundness proof for the cyclic proof system.

Definition 4.1. A strongly connected component, abbreviated SCC, in a cyclic proof tree is a set X of nodes which is connected, seen as a subgraph of the proof tree, where the (directed) edge relation is given as the union of the parent–child and the back-edge relation.

It is clear that every strongly connected component X of a cyclic proof tree has a lowest element, i.e., a unique element with the shortest path to the root of the proof tree, which must be the companion node of some leaf. We call this the root of X. (Note that we imagine trees as growing upwards, with the root at the bottom, in line with the way that we depict proof trees.)

The following characterization of cyclic proofs will be useful:

Proposition 4.2. Let $\Pi $ be a cyclic proof tree. Then $\Pi $ is a valid cyclic proof if, and only if, for every SCC X of $\Pi $ there is some ordinal variable $\kappa _X$ that appears in the constraint of each sequent in X, and is reset in at least one vertex of X.

Proof For right to left, it suffices to note that for every leaf l, the path from the companion of l to l is a strongly connected component of $\Pi $ .

For left to right, let $\Pi $ be a valid cyclic proof.

Claim 1. Let X be any SCC of $\Pi $ . Then there exists an ordinal variable $\kappa _X$ that belongs to the constraint of every vertex in X, and is equal to the variable $\kappa _l$ associated with some leaf l.

Proof of Claim

We prove this by induction on the number of non-axiom leaves in X. The base case consists of the case where X is a single cycle (comprising all nodes on the path to a leaf l from its companion), and in this case we just take $\kappa _X = \kappa _l$ .

Now, suppose that X has more than one non-axiom leaf. Consider the set S of vertices in X that are ancestors of all non-axiom leaves in X. It is clear that any two vertices in this set are comparable with respect to the descendant relation, so we can pick the maximum element s of the set, i.e., $s \in S$ and s is a descendant of every member of S. We call s the splitting point of X. Because all proof rules have at most two premises it follows that s has exactly two children, a left child and a right child. Every non-axiom leaf is a descendant of either the left child of s or the right child of s. In the first case we speak of a left leaf and in the second case a right leaf. Note that some leaf of X must have the root of X as companion, and this leaf must be either a left or right leaf. We may assume without loss of generality that it is a left leaf, the other case is symmetrical. Note that some right leaf must have a companion that is an ancestor of s, since X is strongly connected. Let c denote the lowest ancestor of s (closest to the root of X) that is the companion of some right leaf. Let $X_0$ be the set of vertices that lie on a path from the root of X to some left leaf, and let $X_1$ be the set of vertices that lie on a path from c to some right leaf. Then $X_0 \cup X_1 = X$ , and both $X_0$ and $X_1$ are SCCs with fewer non-axiom leaves than X (note that c is the root of $X_1$ ). So by the induction hypothesis, there are variables $\lambda _0,\lambda _1$ such that $\lambda _0$ appears in the constraint of every vertex in $X_0$ and $\lambda _1$ appears in the constraint of every vertex in $X_1$ . In particular, since $c \in X_0\cap X_1$ , both $\lambda _0$ and $\lambda _1$ appear in the constraint of c. We now consider two cases.

Case 1: $\lambda _0$ is older than $\lambda _1$ in the constraint of c. By assumption $\lambda _0$ appears in the constraint of every vertex in $X_0$ . We define the depth of a right leaf l as the number of leaves passed on the shortest path from the leaf to c. More precisely, if the companion of l is c then l has depth $0$ . Otherwise the depth of l is the smallest number $k+1$ such that the companion of l belongs to the path from the companion of $l'$ to $l'$ , where $l'$ is some right leaf of depth k. We prove by induction on the depth of a leaf l that $\lambda _0$ belongs to the constraint of every vertex on the path from the companion of l to l, and furthermore is older than $\lambda _1$ in every such constraint.

For depth $= 0$ , suppose l has c as companion. If there is some u on the path from c to l in which $\lambda _0$ does not appear in the constraint, then it has to be re-introduced later since the label of l is equal to that of c. But since $\lambda _1$ is on the constraint of every vertex on the path from c to l, $\lambda _0$ can only be re-introduced as a younger variable than $\lambda _1$ , and remain so. So the label of l cannot equal that of c after all, contradiction.

For depth $= k + 1$ , suppose l has companion v that is on the path from the companion of $l'$ to $l'$ , where $l'$ has depth k. Then again, $\lambda _0$ is introduced as a younger variable than $\lambda _1$ in the companion v, and we can repeat the same argument.

Case 2: $\lambda _1$ is older than $\lambda _0$ in c. Then in fact, $\lambda _1$ must appear in the constraint of the root of X, since $\lambda _0$ belongs to the constraint of every vertex on the path from the root of X to c, and so if $\lambda _1$ were introduced on this path it would have to be younger than $\lambda _0$ . With this observation in place we can repeat the whole argument from the previous case, but with the root of X in place of c.

To finish the proof, take any connected component X of $\Pi $ , and let $\kappa _X$ be the variable provided by the Claim. Then $\kappa _X = \kappa _l$ for some leaf l. By definition of a valid cyclic proof, $\kappa _l$ is reset at least once on the path from the companion of l to l. But this path is contained in X, so $\kappa _X = \kappa _l$ is reset in some vertex in X.

Proposition 4.3. If $\rho $ has a cyclic proof then $\rho $ is valid.

Proof Let $\Pi $ be a cyclic proof of $\rho $ .

Assume for a contradiction that there are some model M, a world w in M, and an ordinal assignment o such that $M, w \nvDash _o \rho $ . Our strategy is to find an infinite walk through the cyclic proof $\Pi $ , inducing a series of ordinal assignments, from which we can read off an infinitely descending sequence of ordinals. This contradiction then gives the proposition. We construct the walk by induction as follows. We define a vertex $v_n$ of $\Pi $ , an element $w_n$ of W, and an ordinal assignment $o_n$ by induction on n. We shall maintain the invariant that for each n, $o_n$ refutes the label of $v_n$ (henceforth denoted $\Gamma _n$ ) at $w_n$ . Note that this means that we never reach a leaf labelled by an axiom. For the base case, we define $v_0$ to be the root of the proof tree labelled $\vdash \rho $ , set $w_0 = w$ , and set $o_0 = o$ . Note that o can be taken to be the empty assignment if $\rho $ does not contain any ordinal variables. The assignment $o_0$ refutes the sequent $\vdash \rho $ at $w_0$ by the assumption that $M,w\nvDash _o \rho $ . The inductive step is by case distinction depending on the rule applied at the vertex $v_n$ . We distinguish between applications of the left weakening rule that correspond to the reset of a variable from other applications of left weakening. These need to be treated separately as they allow us to build the decreasing chain of ordinals.

Case $v_n$ is the conclusion of an application of $\kappa : x$ . Here, $\kappa $ is a fresh variable and the principal formula of the rule is of the form $\nu x\,\varphi $ , which is replaced by $ \nu x^{\kappa }\varphi $ . We define $o_{n+1}$ to be the extension of $o_n$ obtained by mapping $\kappa $ to the closure ordinal of the map $\varphi ^{o_n}_M$ , and set $v_{n+1}$ to be the premise of $v_n$ and $w_{n+1} = w_n$ .

Case $v_n$ is the conclusion of an application of the modal rule. Let the principal formula be $[a] \varphi $ . Since $o_n$ refutes the label of $\Gamma _n$ at $w_n$ , it is clear that there is some ${a}$ -successor $w'$ at which $o_n$ refutes the premise. So we set $w_{n+1} = w'$ , $v_{n+1}$ to be the premise of the rule application and $o_{n+1} = o_{n}$ .

Case $v_n$ is the conclusion of an application of the cut rule. Since $o_n$ refutes $\Gamma _n$ at $w_n$ , it has to refute one of the premises at $w_n$ also. We pick $v_{n+1}$ to be this premise, and set $w_{n+1} = w_n$ , $o_{n+1} = o_n$ .

Case $v_n$ is the conclusion of an application of the $\wedge $ -rule. Since $o_n$ refutes $\Gamma _n$ at $w_n$ , it has to refute one of the premises at $w_n$ also. We pick $v_{n+1}$ to be this premise, and set $w_{n+1} = w_n$ , $o_{n+1} = o_n$ .

Case $v_n$ is the conclusion of an application of the $\vee $ -rule, $\eta $ -rule, or $\exists $ -rule. We set $v_{n+1}$ to be the premise, and set $w_{n + 1} = w_n$ and $o_{n+1} = o_n$ . The invariant is easily seen to be maintained.

Case $v_n$ is the conclusion of an application of $\mu (\kappa )$ . We define $w_{n + 1} = w_n$ and $o_{n + 1} = o_n$ . By assumption we have that $w_n \notin [\![\mu x^{\kappa } \varphi ]\!]^{o_n} = f^{o_n(\kappa )}(\emptyset )$ , where f is the monotone map with $f(Z) = [\![\varphi ]\!]^{o_n}_{M[x \mapsto Z]}$ . If we now consider any $\lambda $ such that $o_n(\lambda ) < o_n(\kappa )$ we have that $f^{o_n(\lambda ) + 1}(\emptyset ) \subseteq f^{o_n(\kappa )}(\emptyset )$ , because $o_n(\lambda ) + 1 \leq o_n(\kappa )$ . Thus it follows that $w_{n + 1} = w_n \notin f^{o_n(\lambda ) + 1}(\emptyset ) = f(f^{o_n(\lambda )}(\emptyset )) = [\![\varphi [\mu x^{\lambda }. \varphi / x]]\!]^{o_n}$ . Thus the invariant is maintained.

Case $v_n$ is the conclusion of an application of the $\forall $ -rule. Let $\lambda < \kappa $ be the fresh variable introduced. Since $o_n$ refutes $\Gamma _n$ at $w_n$ there must be some $\xi < o_n(\kappa )$ such that $o_n[\lambda \mapsto \xi ]$ refutes the premise at $w_n$ . So we set $v_{n+1}$ to be the premise of $v_n$ , $w_{n+1} = w_n$ , and $o_{n+1} = o_n[\lambda \mapsto \xi ]$ .

Case $v_n$ is the conclusion of an application of the $\nu (\kappa )$ -rule. Let $\lambda < \kappa $ be the fresh variable introduced. Since $o_n$ refutes $\Gamma _n$ at $w_n$ we have that $w_n \notin [\![\nu x^{\kappa }. \varphi ]\!]^{o_n}$ . If we write f for the monotone map with $f(Z) = [\![\varphi ]\!]^{o_n}_{M[x \mapsto Z]}$ this means that $w_n \notin f^{o_n(\kappa )}(W)$ . By the definition of $f^{o_n(\kappa )}$ we have that

$$\begin{align*}f^{o_n(\kappa)}(W) = \bigcap_{\zeta < \kappa} f(f^{o_n(\zeta)}(W)).\end{align*}$$

Thus there exists some ordinal $\zeta < o_n(\kappa )$ such that $w_n \notin f(f^{\zeta }(W))$ . We set $w_{n + 1} = w_n$ and $o_{n + 1} = o_n[\lambda \mapsto \zeta ]$ . This refutes the premise because $w_{n + 1} = w_n \notin f(f^{\zeta }(W)) = [\![\varphi [\nu x^{\lambda }. \varphi / x]]\!]^{o_{n + 1}}$ .

Case $v_n$ is a leaf with companion $v'$ . We set $o_{n + 1} = o_n$ , and set $w_{n+1} = w_{n}$ and $v_{n+1} = v'$ . The invariant is obviously maintained.

Case $v_n$ is the conclusion of an application of left weakening in which the variable $\kappa $ is reset. This means that neither $\kappa $ nor any of its children appear on the right-hand side of $\Gamma _n$ , and all children of $\kappa $ are removed. List the children of $\kappa $ as $\lambda _1,...,\lambda _m$ . We define the new assignment $o_{n+1}$ by setting

$$ \begin{align*}o_{n+1}(\kappa) = \mathsf{max}(o_n(\lambda_1),...,o_n(\lambda_m)), \end{align*} $$

and $o_{n+1}(\lambda ) = o_{n}(\lambda )$ for $\lambda \neq \kappa $ . We set $w_{n+1} = w_n$ and we set $v_{n+1}$ to be the premise of the rule application. We need to check that the new assignment $o_{n+1}$ refutes $\Gamma _{n+1}$ at $w_{n+1}$ . Since none of the variables $\kappa ,\lambda _1,...,\lambda _m$ appear on the right-hand side of $\Gamma _n$ or $\Gamma _{n+1}$ , it suffices to show that the new assignment is consistent with the constraint $\mathcal {O}_{n+1}$ of $\Gamma _{n+1}$ .

First, note that $o_{n+1}(\kappa ) < o_{n}(\kappa )$ , since we have $o_n(\lambda _i) < o_{n}(\kappa )$ for each $i \in \{1,...,m\}$ and since $o_{n+1}(\kappa )$ was defined as $\mathsf {max}(o_n(\lambda _1),...,o_n(\lambda _m))$ (this observation will be important later!). Hence if $\kappa '$ is the parent of $\kappa $ in $\mathcal {O}_{n+1}$ then

$$ \begin{align*}o_{n+1}(\kappa) < o_{n}(\kappa) < o_{n}(\kappa') = o_{n+1}(\kappa'),\end{align*} $$

as required. Now, suppose $\xi $ is a child of $\kappa $ in $\mathcal {O}_{n+1}$ . Then there must be some $\lambda _i$ , $i \in \{1,...,m\}$ , such that $\xi $ was a descendant of $\lambda _i$ in the constraint of $\Gamma _n$ . Hence we get

$$ \begin{align*} o_{n+1}(\xi) & = o_{n}(\xi) \\ & < o_n(\lambda_i) \\ & \leq \mathsf{max}(o_n(\lambda_1),...,o_n(\lambda_m)) \\ & = o_{n+1}(\kappa), \end{align*} $$

so $o_{n+1}(\xi ) < o_{n+1}(\kappa )$ as required.

Other cases. The other cases of left or right weakening are trivial.

With this construction in place, consider the infinite walk $v_0v_1v_2\ldots $ through $\Pi $ that we obtain in the limit. Let X be the set of all vertices that are visited infinitely many times on $\Pi $ . This is obviously a strongly connected component, so since $\Pi $ was a valid cyclic proof, by Proposition 4.2 there is some $\kappa $ that appears in the constraint of every vertex in X, and is reset on the path from the root of X to one of its leaves. Hence, it is clear that the value assigned to $\kappa $ by the ordinal assignments $o_i$ never increases, and decreases every time the walk passes through the vertex at which $\kappa $ is reset. So the successive values that these ordinal assignments give to $\kappa $ produce an infinite descending series of ordinals, which is impossible. This contradiction concludes the proof.

We now briefly sketch to adapt the soundness proof for the cyclic system to non-wellfounded proofs.

Proposition 4.4. If $\rho $ has a non-wellfounded proof then $\rho $ is valid.

Proof sketch

The argument is similar to the proof of Proposition 4.3: Let $\Pi $ be a non-wellfounded proof of $\rho $ . We assume for contradiction that there are some model M, world w in M, and an ordinal assignment o such that $M,w \not \models _o \rho $ . We find an infinite path $v_0,v_1$ through $\Pi $ and ordinal assignments $o_0,o_1,\dots $ such that $o_i$ refutes $\mathcal {O}_i : \Gamma _i$ , where $\mathcal {O}_i : \Gamma _i$ is the sequent at $v_i$ . The construction of this infinite path is similar as in the proof of Proposition 4.3. We can omit the case for leafs with companions and treat all instances of left weakening as left weakenings that do not correspond to a reset. In the end a contradiction arises from an infinite descending chain of ordinals that can be read of from the sequence $o_1,o_2,\dots $ using the condition from Definition 3.11.

5 Completeness for infinite proofs

In this section we will prove completeness for infinite non-wellfounded proofs, as the first step towards our main result, i.e., completeness for cyclic proofs. More precisely, we introduce a special class of non-wellfounded proofs that we call slim proofs and prove that any valid formula has a slim proof. Slim proofs are genuinely infinite (non-regular), and can contain infinitely many different sequents. However, they do have the property that there is a fixed bound on the number of formulas occurring in any sequent, although the constraints can grow without bound. This property will be important later when we transform slim proofs into finite, cyclic proofs.

5.1 Slim proofs

We start by defining the notion of a slim proof.

Definition 5.1. Let $\mathcal {O} : \Gamma $ be any sequent and let $o_0$ and $o_1$ be any annotations that have their range is in $\mathrm {OV}(\mathcal {O})$ . We write $o_0 \prec ^x_{\mathcal {O}} o_1$ if $o_0(x) \prec _{\mathcal {O}} o_1(x)$ while, for all y higher ranking than x, we have $o_0(y) = o_1(y)$ . We write $o_0 \prec _{\mathcal {O}} o_1$ if there is some ordinal variable x such that $o_0 \prec ^x_{\mathcal {O}} o_1$ .

Definition 5.2. Let $\mathcal {O} : \Gamma $ be any sequent, and let $ \varphi , \psi \in \Gamma $ be positively annotated formulas. We write $ \varphi \prec _{\mathcal {O}} \psi $ , or just $ \varphi \prec \psi $ when $\mathcal {O}$ is clear from context, if $\mathsf {u}( \varphi ) = \mathsf {u}( \psi )$ and, $\mathsf {o}_{\varphi } \prec \mathsf {o}_{\psi }$ .

We write $\preceq _{\mathcal {O}}$ as shorthand for “ $\prec _{\mathcal {O}}$ or $=$ .” A positively annotated formula $\varphi $ is minimal with respect to a constraint $\mathcal {O}$ if there is no formula $\psi $ such that $\psi \prec _{\mathcal {O}} \varphi $ . A sequent $\mathcal {O} : \Gamma $ is said to be minimal if every positively annotated formula occurring in $\Gamma $ is minimal with respect to $\mathcal {O}$ .

Definition 5.3. Let $\Gamma $ be a set of plain formulas. The set $OC(\Gamma )$ consists of all positively or negatively annotated formulas $\varphi $ such that $\mathsf {u}(\varphi ) \in \mathrm {Clos}(\Gamma )$ . The set $QC(\Gamma )$ consists of $OC(\Gamma )$ , together with all formulas of the form $Q\kappa < \lambda : \varphi $ , where $Q \in \{ \forall , \exists \}$ and $\varphi \in OC(\Gamma )$ . The extended closure $EC(\Gamma )$ of $\Gamma $ consists of $QC(\Gamma )$ , together with all formulas of the form $[a]\bigvee \Delta $ or $\bigvee \Delta $ , where $\Delta $ is a subset of $QC(\Gamma )$ .

A proof tree $\Pi $ is said to be slim if:

1. 1. All formulas in $\Pi $ belong to the extended closure of the root formula.

2. 2. For any formula $\varphi $ that occurs in some sequent $\Gamma $ in $\Pi $ , all free ordinal variables of $\varphi $ are active in $\Gamma $ . Equivalently, for any sequent $\Gamma $ in $\Pi $ , any ordinal variable that occurs freely in some formula in $\Gamma $ also occurs freely in some positively annotated formula in $\Gamma $ .

3. 3. Any sequent in $ \Pi $ which is not minimal with respect to its constraint is the conclusion of an application of right weakening.

4. 4. There is no application of left weakening in $\Pi $ .

5. 5. In any application of the cut rule, $\mu (\kappa )$ or $\exists $ , all ordinal variables occurring free in the cut formula or minor formula of the rule application are active variables in the conclusion.

Observe that because infinite branches in slim proofs do not contain applications of $\mathsf {lw}$ the set of ordinal variables in the constraint only grows as we move along the branch. We can thus define the following notion of the limit constraint of a branch:

Definition 5.4. Fix an infinite branch $\beta = v_0,v_1,\dots $ of a slim proof and let $\mathcal {O}_i = (O_i,<_i,\triangleleft _i)$ be the constraint at $v_i$ for all $i \in \omega $ . Define the infinite set $O_{\beta } = \bigcup _{i \in \omega } O_i$ , and the orders $<_{\beta }$ , $\triangleleft _{\beta }$ , and $\prec _{\beta }$ over $O_i$ such that ${\ll _{\beta }} = \bigcup _i {\ll _i}$ for ${\ll } \in \{ <, \le , \triangleleft \}$ .

It is clear that in slim proofs an infinite $<$ -descending chain of ordinals in a branch $\beta $ , according to Definition 3.11 is the same as an infinite descending chain in the order $<_{\beta }$ , according to the usual definition of an infinite descending chain in some order. The same holds for infinite $\prec $ -descending chains.

Proposition 5.5. If $\beta = v_0,v_1,\dots $ is an infinite branch in a slim proof, then:

1. 1. $<_{\beta }$ is irreflexive, transitive, and upwards linear.

2. 2. $\triangleleft _{\beta }$ is a linear order.

3. 3. $\prec _{\beta }$ is a linear order.

4. 4. $<_{\beta }$ is conversely well-founded and $\triangleleft _{\beta }$ is well-founded.

5. 5. $\lambda \prec _{\beta } \kappa $ iff $\lambda <_{\beta } \kappa $ or $\lambda $ is to the left of $\kappa $ with respect to the orders $<_{\beta }$ and $\triangleleft _{\beta }$ .

Proof First observe that left weakening is never applied on $\beta $ because by assumption it is a branch in a slim proof. It follows then from an inspection of the proof rules that for all $i \in \omega $ it holds that either $\mathcal {O}_{i + 1} = \mathcal {O}_i$ , $\mathcal {O}_{i + 1} = \mathcal {O}_i + \lambda $ , or $\mathcal {O}_{i + 1} = \mathcal {O}_i +_{\kappa } \lambda $ , for some ordinal variable $\lambda $ . Thus, in every step there is at most one variable $\lambda $ added; this $\lambda $ is made maximal in $\triangleleft _{i + 1}$ , and it is either a new leaf in $<_{i + 1}$ or $<_{i + 1}$ -incomparable to all existing variables. Using this observation it is relatively straightforward to verify items 1–4.

For item 5 first recall that $\lambda $ is to the left of $\kappa $ with respect to the orders $<_{\beta }$ and $\triangleleft _{\beta }$ if $\lambda $ and $\kappa $ are $<_{\beta }$ -incomparable and $\lambda ' \triangleleft _{\beta } \kappa '$ holds, where $\lambda '$ is the $<_{\beta }$ -greatest $<_{\beta }$ -ancestor of $\lambda $ that is not a $<_{\beta }$ -ancestor of $\kappa $ and $\kappa '$ is the $<_{\beta }$ -greatest $<_{\beta }$ -ancestor of $\kappa $ that is not a $<_{\beta }$ -ancestor of $\lambda $ . Note that the $<_{\beta }$ -greatest node with some property is well-defined because $<_{\beta }$ is conversely well-founded.

The details of the proof of item 5 are left to the reader. The crucial step in the argument is to show that the following are equivalent:

1. 1. $\lambda '$ is the $<_{\beta }$ -greatest $<_{\beta }$ -ancestor of $\lambda $ that is not a $<_{\beta }$ -ancestor of $\kappa $ .

2. 2. For some i, $\lambda ', \lambda , \kappa $ exist and $\lambda '$ is the $<_i$ -greatest $<_i$ -ancestor of $\lambda $ that is not a $<_i$ -ancestor of $\kappa $ .

The proof of this equivalence relies on the observation that when moving from $\mathcal {O}_i$ to $\mathcal {O}_{i + 1}$ only new leafs or new roots are added to the order $<_{i + 1}$ . Thus, variables that are comparable at stage i stay comparable at stage $i + 1$ , and variables that exist in $\mathcal {O}_i$ and are incomparable stay incomparable.

Proposition 5.6. Let $\beta $ be an infinite branch of a slim proof tree $\Pi $ . Then it contains an infinite $\prec $ -descending chain of ordinal variables if, and only if, it contains an infinite $<$ -descending chain of ordinal variables.

Proof It is clear that it suffices to prove this result for the orders $\prec _{\beta }$ and $<_{\beta }$ from Definition 5.4. We write $\mathcal {O}, \prec , <$ , and $\triangleleft $ for $\mathcal {O}_{\beta }, \prec _{\beta }, <_{\beta }$ , and $\triangleleft _{\beta }$ , respectively. The direction from right to left follows directly from the definitions of $<_{\beta }$ and $\prec _{\beta }$ and the relation between $<_i$ and $\prec _i$ at any finite $i \in \omega $ .

For the direction from left to right assume that we have an infinite descending chain $\kappa _0 \succ \kappa _1 \succ \cdots $ of ordinal variables in $\mathcal {O}$ . The aim is to use König’s lemma to prove that there is an infinite descending chain in $<_{\mathcal {O}_{\beta }}$ .

Consider the following set of variables from $\mathcal {O}$ :

$$\begin{align*}F = \{ \lambda \in \mathcal{O} \mid \lambda \geq \kappa_i \mbox{ for some } i \in \omega\}. \end{align*}$$

Because by Proposition 5.5 $<$ is upwards linear and conversely well-founded we can consider F to be a forest under the order $<$ . The set F is infinite because it contains the infinitely many distinct $\kappa _i$ for $i \in \omega $ . We first show that there is an infinite subset $T \subseteq F$ that is a tree under $<$ .

Claim 2. There are only finitely many $<$ -maximal elements in F.

Proof of Claim 2

First, note that because F is upwards closed in $<$ the concepts of being $<$ -maximal and of being $<$ -maximal in F coincide. Assume then for a contradiction that there are infinitely many $<$ -maximal elements in F. Because $\triangleleft $ is a linear order and it is well-founded this means that we can build an infinite chain $\delta _0 \triangleleft \delta _1 \triangleleft \cdots $ of $<$ -maximal elements in F. By definition of F we have for each $i \in \omega $ some $k_i \in \omega $ such that $\kappa _{k_i} \leq \delta _i$ . It follows by item 5 of Proposition 5.5 that there is an infinite ascending $\kappa _{k_0} \prec \kappa _{k_1} \prec \cdots $ . But because of the infinite descending chain $\kappa _0 \succ \kappa _1 \succ \cdots $ , this contradicts the fact that $\prec $ is a partial order.

It follows by the pigeonhole principle that there must be one $<$ -maximal element r below which there are infinitely many elements from F. We define the set $T \subseteq F$ to be all those elements from F that are $<$ -smaller than r. The set T is an infinite tree under the order $<$ . The claim of the proposition then follows by König’s lemma if we can show that this tree T is finitely branching. This is shown in the following claim:

Claim 3. Every variable $\lambda \in T$ has only finitely many $<$ -children in T.

Proof of Claim 3

Assume for a contradiction that some $\lambda \in T$ has infinitely many $<$ -children in T. Because $\triangleleft $ is a linear order and it is well-founded this means that we can build an infinite chain $\delta _0 \triangleleft \delta _1 \triangleleft \cdots $ of $<$ -children of $\lambda $ with $\delta _i \in T$ for all i. By the definition of T we can find, for every $i \in \omega $ , some $k_i \in \omega $ such that $\kappa _{k_i} \leq \delta _i$ . It follows by item 5 of Proposition 5.5 that $\kappa _{k_0} \prec \kappa _{k_1} \prec \cdots $ , because as the $\delta _i$ are $<$ -siblings they must be $<$ -greatest ancestors of the $\kappa _{k_i}$ without being each other’s ancestors. But this contradicts the fact that $\prec $ is a partial order and the assumption that $\kappa _0 \succ \kappa _1 \succ \cdots $ .

This finishes the proof of Proposition 5.6.

A basic property of slim proofs that will be useful is the provability of the following generalized version of excluded middle:

Proposition 5.7. Let $\varphi $ be a positively annotated formula, and let $\sigma $ be an increasing substitution. Then there is slim proof for any sequent $\mathcal {O}: \varphi , \overline {\varphi [\sigma ]}$ .

Proof The proposition is proved by a formula induction, which we illustrate by considering the case where $\varphi = \nu x^{\kappa _0} \psi $ .

By the inductive hypothesis there is a slim proof $\Pi $ for any sequent $\mathcal {O}': \psi ', \overline {\psi '[\sigma ]}$ , where $\psi '$ is the formula $\psi [p/x]$ , for some fresh proposition letter p. Let $\Pi '$ be the derivation we obtain from $\Pi $ by replacing every occurrence of p with the formula $\nu x^{\kappa _1} \psi $ , and every occurrence of $\overline {p}$ with the formula $\mu x^{\kappa _0} \overline {\psi [\sigma ]}$ . Now consider the following derivation $\Pi _1$ (where we write $\lambda $ for $\sigma (\kappa _0)$ ):

Note that $\Pi _1$ need not be a proof, since there may be leaves in $\Pi _1$ , that were labeled in $\Pi '$ by an axiom $\mathcal {O}': p, \overline {p}$ , but in $\pi _1$ are labeled with the sequent $\mathcal {O}': \nu x^{\kappa _1} \psi , \mu x^{\kappa _0} \psi [\sigma ]$ . However, to any such leaf we may apply the same construction that we just described, with $\sigma [\kappa _0/\kappa _1]$ taking the role of $\sigma $ . Iterating this procedure we arrive at a slim proof in which any newly created infinite branch carries an infinitely descending sequence of variables $\cdots < \kappa _2 < \kappa _1 < \kappa _0$ .

The following is an immediate corollary of Proposition 5.7.

Proposition 5.8 (Excluded middle).

Let $\varphi $ be a positively annotated formula. Then there is slim proof for any sequent $\mathcal {O}: \varphi , \overline {\varphi }$ .

The remainder of this section is devoted to proving completeness for slim proofs (Theorem 5.28). The proof is carried out in several steps, so a high-level sketch may be helpful:

The first step is to define a particular kind of sequents, called tiles, that will be used as building blocks from which we construct a counter-model to a given formula that is not provable. Tiles are saturated sequents of a bounded size, where the saturation conditions are intended to mimic the conditions under which all formulas in the sequent are false; for example if a disjunction is present in the sequent, both disjuncts should be false, and if a formula $\forall \lambda < \kappa \varphi (\lambda )$ is present in the sequent then there should be some witness $\xi $ for which $\varphi (\xi )$ is false. However, adding such saturation conditions naïvely—e.g., if the sequent contains $\forall \lambda < \kappa \varphi (\lambda )$ then it contains $\varphi (\xi )$ for some $\xi < \kappa $ —would quickly destroy any hopes of maintaining a bound on the number of formulas appearing in a sequent. The appropriate saturation conditions have to be formulated carefully; the precise definition is Definition 5.13.

Completeness is proved in Section 5.4. A determined two-player game called the mosaic game is defined, in which “Prover” tries to produce a slim proof of a given formula, and the opposing player “Refuter” tries to construct a counter-model from tiles. The most difficult part of the completeness proof is to show that a winning strategy for Refuter actually provides a counter-model. To get some intuition about what the difficulty is, and how it is handled, consider a formula $[{a}]\nu x^{\kappa } \langle \breve {a}\rangle \varphi (x)$ , and say that Refuter is trying to construct a counter-model for some tile $\Gamma $ containing this formula. In the mosaic game, Prover can “attack” the box $[{a}]$ and ask Refuter to present some tile $\Psi $ which is to be ${a}$ -accessible from $\Gamma $ , and contains $\nu x^{\kappa } \langle \breve {a}\rangle \varphi (x)$ . In order to falsify $\nu x^{\kappa } \langle \breve {a}\rangle \varphi (x)$ at $\Psi $ , Refuter has to saturate by adding some child $\lambda $ of the variable $\kappa $ to the constraint of $\Psi $ , along with the formula $\langle \breve {a} \rangle \varphi (\nu x^{\lambda } \langle \breve {a} \rangle \varphi (x))$ . So here, the variable $\kappa $ has progressed to the “smaller” $\lambda $ . But if $\Psi $ was to be ${a}$ -accessible from $\Gamma $ , this means that Refuter has to make sure that the formula $\nu x^{\lambda } \langle \breve {a} \rangle \varphi (x)$ is false at $\Gamma $ . In other words, already when the tile $\Gamma $ was constructed, Refuter has to anticipate that the variable $\kappa $ will progress due to later steps in the counter-model construction.

The solution to handling this sort of back-and-forth behaviour is to make sure that $\Gamma $ already contains some formula which is “as good as” the formula $\nu x^{\lambda } \langle \breve {a} \rangle \varphi (x)$ , in some sense. It is quite tricky to formulate an appropriate saturation condition corresponding to this intuition. The notion of a minimality assumption introduced in Definition 5.9 will be the key concept used to handle this, with the saturation condition given in Definition 5.13. Definition 5.17 defines a notion of ${a}$ -successor of a tile, which is intended to capture the coherence conditions we require of the ${a}$ -accessibility relation in the counter-model construction used in the completeness proof. The key technical result that is used to handle the difficulty sketched above is Proposition 5.24, which captures the sense in which a tile anticipates progressions of ordinal variables that may occur in its ${a}$ -successors.

5.2 Pre-tiles and tiles

Our completeness proof for slim proofs will build a counter-model for an unprovable formula out of building blocks that we call tiles, which are essentially “small” but saturated sequents. The precise notion of “saturated” that we will use is quite technical, since a naïve concept of saturation would be incompatible with maintaining a bound on the number of formulas appearing in a sequent. It will be convenient to first define the notion of a “pre-tile” to capture the general structure of the sequents that we will be working with, and then define a tile as a pre-tile that satisfies appropriate saturation conditions.

Definition 5.9. A $\rho $ -pre-tile is a sequent $\mathcal {O} : \Gamma $ where $\Gamma $ admits a partition into three disjoint subsets $ \Gamma ^+$ , $\Gamma ^-$ , $\Gamma ^{\mu } $ such that:

• • Every formula $\varphi \in \Gamma ^+$ is positively annotated and $\mathsf {u}(\varphi )$ belongs to the closure of $\rho $ .

• • Every formula $\varphi \in \Gamma ^-$ is the negation of a positively annotated formula $\psi $ such that $\mathsf {u}(\psi )$ belongs to the closure of $\rho $ , and every ordinal variable that occurs freely in $\psi $ is active in $\Gamma ^+$ .

• • Every formula $\varphi \in \Gamma ^{\mu }$ is of the form $\exists \lambda < \kappa :\overline {\psi }[\lambda /\kappa ]$ where $\psi \in \Gamma ^+$ and $\kappa $ appears in $\psi $ .

The sets $\Gamma ^+,\Gamma ^-,\Gamma ^{\mu }$ are called the positive part, the negative part, and the minimality assumptions of $\Gamma $ respectively. The $\rho $ -pre-tile is said to be small if every formula in $\Gamma ^+$ is minimal with respect to $\mathcal {O}$ .

Observe that, for every plain formula $ \varphi $ , adding the empty constraint yields an example of a pre-tile, viz., $\emptyset : \varphi $ . Note that this pre-tile is of a special shape: the negative part and the set of minimality assumptions are empty. In general we can think of the partition of pre-tiles into these three parts—positive, negative, and minimality assumptions—as keeping track of the different roles that formulas play in the completeness proof. The positive part of a pre-tile is the “main” part in a sense; our goal from the start is to construct a counter-model to the positive part of a pre-tile of the form $\emptyset : \varphi $ . Along the way, assumptions may be introduced via cuts. In a two-sided sequent notation we can think of pre-tiles as sequents of the shape:

$$\begin{align*}\mathcal{O} : \Gamma, \Delta \Rightarrow \Theta,\end{align*}$$

where $\Delta , \Theta $ consist of positively annotated formulas, and $\Gamma $ consists of formulas of the form $\forall \lambda < \kappa \;\psi $ where $\psi \in \Theta $ . The function of the sets $\Gamma ,\Delta $ is essentially to constrain what formulas can belong to the positive part ( $\Theta $ ) without making the sequent provable. A formula $\psi \in \Delta $ belonging to the negative part ensures that $\psi $ cannot belong to the positive part, or “on the right-hand side” of the sequent, since that would result in a trivially provable sequent. Similarly, a minimality assumption $\forall \lambda < \kappa \;\psi (\lambda ) \in \Gamma $ ensures that $\Theta $ cannot contain the formula $\psi (\xi )$ for any $\xi <_{\mathcal {O}} \kappa $ , since that would also make the sequent provable.

Proposition 5.10. For every constraint $\mathcal {O} = (O,<_{\mathcal {O}},\triangleleft _{\mathcal {O}})$ the order $\prec _{\mathcal {O}}$ is a strict linear order over ordinal variables.

Proof It is obvious from the definition that $\prec _{\mathcal {O}}$ is irreflexive.

To show that $\prec _{\mathcal {O}}$ is transitive assume that $\kappa \prec _{\mathcal {O}} \lambda $ and $\lambda \prec _{\mathcal {O}} \delta $ . Because of the disjunctive definition of $\prec _{\mathcal {O}}$ one has to distinguish four cases. We only consider the case where $\kappa $ is to the left of $\lambda $ and $\lambda $ is to the left of $\delta $ . Let $\kappa '$ be the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\kappa $ that is not a $<_{\mathcal {O}}$ -ancestor of $\lambda $ , $\alpha $ the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\lambda $ that is not a $<_{\mathcal {O}}$ -ancestor of $\kappa $ , $\beta $ the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\lambda $ that is not a $<_{\mathcal {O}}$ -ancestor of $\delta $ , and $\delta '$ the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\delta $ that is not a $<_{\mathcal {O}}$ -ancestor of $\lambda $ . From the assumption we have that $\kappa ' \triangleleft _{\mathcal {O}} \alpha $ and $\beta \triangleleft _{\mathcal {O}} \delta '$ . Moreover, we have that $\kappa '$ and $\alpha $ either have the same parent in $<_{\mathcal {O}}$ or they are both $<$ -maximal and similarly for $\beta $ and $\delta '$ . Because $<_{\mathcal {O}}$ is upwards-linear we have that either $\alpha = \beta $ , $\alpha <_{\mathcal {O}} \beta $ or $\beta <_{\mathcal {O}} \alpha $ . We consider all these cases.

If $\alpha = \beta $ then it follows that either $\kappa '$ and $\delta '$ have the same parent in $<_{\mathcal {O}}$ or that they are both $<_{\mathcal {O}}$ -maximal. It follows that $\kappa '$ is also the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\kappa $ that is not a $<_{\mathcal {O}}$ -ancestor of $\delta $ and similarly $\delta '$ is also the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\delta $ that is not a $<_{\mathcal {O}}$ -ancestor of $\kappa $ . Moreover, by the transitivity of $\triangleleft _{\mathcal {O}}$ we also get that $\kappa ' \triangleleft _{\mathcal {O}} \lambda '$ . Hence, $\kappa $ is to the left of $\lambda $ and $\kappa \prec _{\mathcal {O}} \lambda $ follows by the definition of $\prec _{\mathcal {O}}$

If $\alpha <_{\mathcal {O}} \beta $ then $\beta $ is a $<_{\mathcal {O}}$ -ancestor of $\kappa $ because $\alpha $ was the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\lambda $ that is not a $<_{\mathcal {O}}$ -ancestor of $\kappa $ . It follows that either the common parent of $\beta $ and $\delta '$ is a $<_{\mathcal {O}}$ -ancestor of both $\kappa $ and $\delta $ , or that $\beta $ and $\delta '$ are both $<_{\mathcal {O}}$ -maximal. Because we already know that $\beta $ and $\delta '$ have the same parent or are both $<_{\mathcal {O}}$ -maximal it follows that $\beta $ is the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\kappa $ that is not a $<_{\mathcal {O}}$ -ancestor of $\delta $ , and $\delta '$ is the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\delta $ that is not a $<_{\mathcal {O}}$ -ancestor of $\kappa $ . Hence we get $\kappa \prec _{\mathcal {O}} \delta $ because $\beta \triangleleft _{\mathcal {O}} \delta '$ .

If $\beta <_{\mathcal {O}} \alpha $ then $\alpha $ is a $<_{\mathcal {O}}$ -ancestor of $\delta $ because $\beta $ was the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\lambda $ that is not a $<_{\mathcal {O}}$ -ancestor of $\delta $ . It follows that either the common parent of $\kappa '$ and $\alpha $ is a $<_{\mathcal {O}}$ -ancestor of both $\kappa $ and $\delta $ , or that $\kappa '$ and $\beta $ are both $<_{\mathcal {O}}$ -maximal. Because we already know that $\kappa '$ and $\alpha $ have the same parent or are both $<_{\mathcal {O}}$ -maximal it follows that $\kappa '$ is the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\kappa $ that is not a $<_{\mathcal {O}}$ -ancestor of $\delta $ , and $\alpha $ is the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor of $\delta $ that is not a $<_{\mathcal {O}}$ -ancestor of $\kappa $ . Hence we get $\kappa \prec _{\mathcal {O}} \delta $ because $\kappa ' \triangleleft _{\mathcal {O}} \beta $ .

To show that $\prec _{\mathcal {O}}$ is linear consider any $\kappa \neq \lambda $ . We need to show that either $\kappa \prec _{\mathcal {O}} \lambda $ or $\lambda \prec _{\mathcal {O}} \kappa $ . First, distinguish cases depending on whether $\kappa $ and $\lambda $ are comparable in the strict partial order $<_{\mathcal {O}}$ . If they are comparable then we have either $\kappa <_{\mathcal {O}} \lambda $ or $\lambda <_{\mathcal {O}} \kappa $ . It thus follows immediately from the definition of $\prec _{\mathcal {O}}$ that then $\kappa \prec _{\mathcal {O}} \lambda $ or $\lambda \prec _{\mathcal {O}} \kappa $ . In the other case $\kappa $ and $\lambda $ are $<_{\mathcal {O}}$ -incomparable it follows also that they are $\leq _{\mathcal {O}}$ -incomparable since we assume $\kappa \neq \lambda $ . There then must exists the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor $\kappa '$ of $\kappa $ that is not a $<_{\mathcal {O}}$ -ancestor of $\lambda $ and, similarly, there exists the $<_{\mathcal {O}}$ -maximal $<_{\mathcal {O}}$ -ancestor $\lambda '$ of $\lambda $ that is not a $<_{\mathcal {O}}$ -ancestor of $\kappa $ . It is clear that $\lambda '$ and $\kappa '$ must be distinct. Because $\triangleleft _{\mathcal {O}}$ is a strict linear order it follows that either $\kappa \triangleleft _{\mathcal {O}} \lambda $ or $\lambda \triangleleft _{\mathcal {O}} \kappa $ . In the former case we get that $\kappa \prec _{\mathcal {O}} \lambda $ and in the latter that $\lambda \prec _{\mathcal {O}} \kappa $ .

Proposition 5.11. Let $\mathcal {O} : \Gamma $ be any pre-tile and $\varphi $ any propositional formula. Then $\prec _{\mathcal {O}}$ is a strict linear order over the set $\{\psi \in \Gamma ^+ \mid \mathsf {u}(\psi ) = \varphi \}$ .

Proof Fix $\varphi $ and restrict $\prec _{\mathcal {O}}$ to the set $\{\psi \in \Gamma ^+ \mid \mathsf {u}(\psi ) = \varphi \}$ .

Observe that if $\psi , \chi \in \Gamma ^+$ with $\mathsf {u}(\psi ) = \mathsf {u}(\chi )$ then the domains of $\mathsf {o}_{\psi }$ and $\mathsf {o}_{\chi }$ must be the same. This is the case because by Definition 5.9 $\psi ,\chi \in \Gamma ^+$ entails that both $\psi $ and $\chi $ are positively annotated, which by Definition 2.3 means that all greatest fixpoint variables are annotated, and both formulas contain the same greatest fixpoint variables because $\mathsf {u}(\psi ) = \mathsf {u}(\chi )$ .

It follows from this observation that the restriction of the order $\prec _{\mathcal {O}}$ from Definition 5.2 to formulas from $\{\psi \in \Gamma ^+ \mid \mathsf {u}(\psi ) = \varphi \}$ is just the lexicographic extension of the order $\prec _{\mathcal {O}}$ over ordinal variables to finite sequences, where each position in the sequence corresponds to one greatest fixpoint variable in $\varphi $ . It is clear that this yields a strict linear order, because as shown in Proposition 5.10 $\prec _{\mathcal {O}}$ is a strict linear order of ordinal variables.

We can now prove that small $\rho $ -pre-tiles are indeed small in the sense that there is a bound on the number of formulas that they contain.

Proposition 5.12. Let $\rho $ be any formula. Then there is a bound n such that, for any small $\rho $ -pre-tile $\mathcal {O}\vdash \Gamma $ , there are at most n distinct formulas in $\Gamma $ (up to renaming of bound ordinal variables).

Proof Because the $\rho $ -pre-tile $\Gamma $ is small, $\Gamma ^+$ contains only positively annotated formulas that are minimal with respect to the order $\prec _{\mathcal {O}}$ . From Proposition 5.11 we know that $\prec _{\mathcal {O}}$ is a strict linear order over any set $\Psi $ of annotated formulas with the same underlying plain formula, i.e., such that $\mathsf {u}(\varphi ) = \mathsf {u}(\psi )$ whenever $\varphi ,\psi \in \Psi $ . It follows that $\Gamma ^+$ contains at most one annotated formula $\varphi $ for every underlying plain formula $\mathsf {u}(\varphi )$ , equal to $\mathsf {u}(\varphi )^o$ for some annotation o. This means that $\Gamma ^+$ is bounded by the size m of the closure of $\rho $ . This also means that the number of active ordinal variables in $\Gamma $ has a fixed upper bound, since every annotated formula $\theta ^o$ in $\Gamma ^+$ can at most have one ordinal variable assigned to each fixpoint variable by the annotation o. Since every formula in $\Gamma ^-$ is the negation of some annotated formula, whose underlying plain formula is in the closure of $\rho $ , it follows that the number of formulas in $\Gamma ^-$ is bounded by $m\cdot k^{\lvert \mathrm {Var}(\rho ) \rvert }$ , where k is the fixed upper bound on the number of active ordinal variables. (Note that $k^{\lvert \mathrm {Var}(\rho ) \rvert }$ bounds the number of annotations of fixpoint variables in $\rho $ by active ordinal variables in $\Gamma $ .) For $\Gamma ^{\mu }$ , since each of the formulas in $\Gamma ^{\mu }$ is of the form $\exists \lambda < \kappa : \overline {\varphi [\lambda /\kappa ]}$ where $\varphi \in \Gamma ^+$ , the number of distinct such formulas up to renaming of bound variables is bounded by $m \cdot k$ . Since the formula part of $\Gamma $ is $\Gamma ^+ \cup \Gamma ^- \cup \Gamma ^{\mu }$ , the result follows.

Note that essentially the same proof with some minor modifications can be used to show that, for any slim proof $\Pi $ , there is a bound on the number of formulas that can occur in any sequent in $\Pi $ up to renaming of bound ordinal variables. We sometimes abuse notation by writing just $\Gamma $ instead of $\mathcal {O} : \Gamma $ . In such cases we let $\mathcal {O}(\Gamma )$ denote $\mathcal {O}$ . From now on, without further mention we will equate formulas that differ only by a renaming of bound variables, and similarly we count two pre-tiles as the same if they are equal up to renaming of bound ordinal variables.

Definition 5.13. Let $\mathcal {O} : \Gamma $ be a (small) $\rho $ -pre-tile. We say that this pre-tile is propositionally saturated if it satisfies the following condition:

1. 1. If $\varphi $ is positively annotated, $\mathsf {u}(\varphi )$ is in the closure of $\rho $ and all ordinal variables appearing in $\varphi $ are active in $\Gamma ^+$ , then either $\overline {\varphi } \in \Gamma ^-$ or $\varphi ' \in \Gamma ^+$ for some $\varphi ' \preceq _{\mathcal {O}} \varphi $ .

If, in addition, $\mathcal {O} : \Gamma $ satisfies the conditions below, we call it a (small) $\rho $ -tile:

1. 2. $\nu x\, \varphi \notin \Gamma ^+$ for all formulas of the form $\nu x \varphi $ (outermost $\nu $ -fixpoints must be annotated).

2. 3. If $\nu x^{\kappa } \varphi \in \Gamma ^+$ then for some $\kappa _0$ with $\kappa _0 <_{\mathcal {O}} \kappa $ and for some $\varphi ' \preceq _{\mathcal {O}} \varphi (\nu x^{\kappa _0} \varphi )$ , we have $\varphi ' \in \Gamma ^+$ .

3. 4. If all variables in $\varphi (\nu x^{\kappa } \psi )$ are active in $\Gamma $ and the underlying plain formula is in the closure of $\rho $ , and $\theta \in \Gamma ^+$ for some $\theta \preceq _{\mathcal {O}(\Gamma )} \varphi (\nu x^{\kappa } \psi )$ , then either $\exists \lambda < \kappa : \overline {\varphi }(\mu x^{\lambda } \overline {\psi }) \in \Gamma ^{\mu }$ , or for some $\kappa _0$ with $\kappa _0 <_{\mathcal {O}} \kappa $ and some $\theta ' \preceq _{\mathcal {O}} \varphi (\nu x^{\kappa _0}\psi )$ we have $\theta ' \in \Gamma ^+$ .

The collection of small $\rho $ -tiles is denoted by $T_{\rho }$ .

The last condition in Definition 5.13 expresses a saturation condition corresponding to the minimisation rule. We can understand it semantically as follows: suppose we wish to construct a counter-model for the unprovable sequent $\mathcal {O}: \Gamma $ , where $\varphi (\nu x^{\kappa }\psi ) \in \Gamma $ (or some $\preceq $ -smaller formula belongs to $\Gamma $ ). By the minimisation rule, either $\mathcal {O} : \Gamma , \exists \lambda < \kappa : \overline {\varphi }(\mu x^{\lambda } \overline {\psi })$ is unprovable, or $\mathcal {O}+_{\kappa } \kappa _0 : \Gamma , \varphi (\nu x^{\kappa _0}\psi )$ is unprovable. In either of these two sequents, we have more information about how the ordinal variable $\kappa $ must be evaluated in a refuting model. In any counter-model for $\mathcal {O} : \Gamma , \exists \lambda < \kappa : \overline {\varphi }(\mu x^{\lambda } \overline {\psi })$ , we know that $\kappa $ has to be evaluated as the smallest ordinal that refutes $\varphi (\nu x^{\kappa } \psi )$ . Otherwise it would not be a counter-model, as the formula $\exists \lambda < \kappa : \overline {\varphi }(\mu x^{\lambda } \overline {\psi })$ would be true. In a counter-model for the sequent $\mathcal {O}+_{\kappa } \kappa _0 : \Gamma , \varphi (\nu x^{\kappa _0}\psi )$ , the opposite holds: there is some ordinal smaller than the value of $\kappa $ that refutes the formula $\varphi (\nu x^{\kappa } \psi )$ , and we have introduced a fresh name $\kappa _0$ for this ordinal.

In the next subsection we will show how an unprovable pre-tile can be “saturated” to an unprovable tile. For technical reasons it will be necessary to be careful with how this saturation is carried out, so that a given pre-tile stands in a suitable relationship to the corresponding tiles. This relationship $\preceq $ is spelled out in the following definition; intuitively, we can read $\Psi \preceq \Gamma $ as “ $\Psi $ is at least as saturated as $\Gamma $ .”

Definition 5.14. Let $\Gamma ,\Psi $ be pre-tiles, and let L be a set of ordinal variables. We write $\Psi \preceq _L \Gamma $ if the following conditions hold:

1. 1. $\mathrm {OV}(\mathcal {O}(\Psi )) = \mathrm {OV}(\mathcal {O}(\Gamma )) \uplus L$ .

2. 2. For all $\lambda , \lambda ' \in \mathrm {OV}(\mathcal {O}(\Gamma ))$ it holds that $\lambda <_{\mathcal {O}(\Psi )} \lambda '$ iff $\lambda <_{\mathcal {O}(\Gamma )} \lambda '$ , and that $\lambda \triangleleft _{\mathcal {O}(\Psi )} \lambda '$ iff $\lambda \triangleleft _{\mathcal {O}(\Gamma )} \lambda '$ .

3. 3. $\mathrm {Act}(\Psi ) \subseteq \mathrm {Act}(\Gamma ) \uplus L$ .

4. 4. $\kappa \triangleleft _{\mathcal {O}(\Psi )} \lambda $ for all $\kappa \in \mathrm {OV}(\mathcal {O}(\Gamma ))$ and $\lambda \in L$ .

5. 5. No variable in L is a $<_{\mathcal {O}(\Gamma )}$ -ancestor of any variable in $\mathcal {O}(\Gamma )$ .

6. 6. If $\lambda \in L$ , $\kappa \in \mathcal {O}(\Gamma )$ , and $\lambda <_{\mathcal {O}(\Psi )} \kappa $ , then there is some $\kappa ' \in \mathrm {Act}(\Gamma )$ such that $\lambda <_{\mathcal {O}(\Psi )} \kappa ' \leq _{\mathcal {O}(\Psi )} \kappa $ .

7. 7. For every formula $\varphi \in \Gamma ^+$ there is some formula $\varphi ' \in \Psi ^+$ such that $\varphi ' \preceq _{\mathcal {O}(\Psi )} \varphi $ .

We write $\Psi \preceq \Gamma $ if there is some L such that $\Psi \preceq _L \Gamma $ .

Proposition 5.15. The relation $\preceq $ over tiles is a pre-order.

Proof Reflexivity is trivial ( $\Gamma \preceq _{\emptyset } \Gamma $ ), so we check transitivity. Let $\Gamma _2 \preceq _{L_1} \Gamma _1 \preceq _{L_0} \Gamma _0$ . We show that $\Gamma _2 \preceq _{L_0 \uplus L_1} \Gamma _0$ , checking each condition individually.

1. We have

$$ \begin{align*} \mathrm{OV}(\mathcal{O}(\Gamma_2)) & = \mathrm{OV}(\mathcal{O}(\Gamma_1)) \uplus L_1 \\ & = \mathrm{OV}(\mathcal{O}(\Gamma_0)) \uplus L_0 \uplus L_1. \end{align*} $$

2. Straightforward.

3. We have

$$ \begin{align*} \mathrm{Act}(\Gamma_2) & \subseteq \mathrm{Act}(\Gamma_1) \uplus L_1 \\ & \subseteq \mathrm{Act}(\Gamma_0) \uplus L_0 \uplus L_1. \end{align*} $$

4. No variable in $L_0$ is older than any variable in $\mathcal {O}(\Gamma _0)$ , and no variable in $L_1$ is older than any variable in $\mathcal {O}(\Gamma _1)$ . But $\mathcal {O}(\Gamma _1) = \mathcal {O}(\Gamma _0) \uplus L_0$ , so this means that no variable in $L_1$ is older than any variable in $\mathcal {O}(\Gamma _0)$ . Hence no variable in $L_0 \uplus L_1$ is older than any variable in $\mathcal {O}(\Gamma _0)$ .

5. No variable in $L_0$ is an ancestor of any variable in $\mathcal {O}(\Gamma _0)$ , and no variable in $L_1$ is an ancestor of any variable in $\mathcal {O}(\Gamma _1)$ . But $\mathcal {O}(\Gamma _1) = \mathcal {O}(\Gamma _0) \uplus L_0$ , so this means that no variable in $L_1$ is an ancestor of any variable in $\mathcal {O}(\Gamma _0)$ . Hence no variable in $L_0 \uplus L_1$ is an ancestor of any variable in $\mathcal {O}(\Gamma _0)$ .

6. Suppose $\kappa \in \mathcal {O}(\Gamma _0)$ and $\lambda \in L_0 \uplus L_1$ , where $\lambda <_{\mathcal {O}(\Gamma _2)} \kappa $ . If $\lambda \in L_0$ then since $\Gamma _1 \preceq _{L_0} \Gamma _0$ it follows that there is some $\lambda ' \in \mathrm {Act}(\Gamma _0)$ such that $\lambda <_{\mathcal {O}(\Gamma _1)} \lambda ' \leq _{\mathcal {O}(\Gamma _1)} \kappa $ . But then $\lambda <_{\mathcal {O}(\Gamma _2)} \lambda ' \leq _{\mathcal {O}(\Gamma _2)} \kappa $ as well. If $\lambda \in L_1$ , then since $\kappa \in \mathcal {O}(\Gamma _1)$ and $\Gamma _2 \preceq _{L_1} \Gamma _1$ , there is some $\lambda ' \in \mathrm {Act}(\Gamma _1)$ such that $\lambda <_{\mathcal {O}(\Gamma _2)} \lambda ' \leq \kappa $ . But $\mathrm {Act}(\Gamma _1) \subseteq \mathrm {Act}(\Gamma _0) \uplus L_0$ . If $\lambda ' \in \mathrm {Act}(\Gamma _0)$ then we are done. If $\lambda ' \in L_0$ , then $\lambda ' <_{\mathcal {O}(\Gamma _1)} \kappa $ and so since $\Gamma _1 \preceq _{L_0} \Gamma _0$ there is some $\lambda " \in \mathrm {Act}(\Gamma _0)$ such that $\lambda ' <_{\mathcal {O}(\Gamma _1)} \lambda " \leq _{\mathcal {O}(\Gamma _1)} \kappa $ . But then we have

$$ \begin{align*}\lambda <_{\mathcal{O}(\Gamma_1)} \lambda' <_{\mathcal{O}(\Gamma_1)} \lambda" \leq_{\mathcal{O}(\Gamma_1)} \kappa\end{align*} $$

and so we are done.

7. Let $\varphi \in \Gamma _0^+$ . Since $\Gamma _1 \preceq \Gamma _0$ there is some formula $\varphi ' \in \Gamma _1^+$ such that $\varphi ' \preceq _{\mathcal {O}(\Gamma _1)} \varphi $ . Since $\Gamma _2 \preceq \Gamma _1$ there is some formula $\varphi " \in \Gamma _2^+$ such that $\varphi " \preceq _{\mathcal {O}(\Gamma _2)} \varphi '$ . But clearly $\varphi ' \preceq _{\mathcal {O}(\Gamma _1)} \varphi $ entails $\varphi ' \preceq _{\mathcal {O}(\Gamma _2)} \varphi $ , so transitivity of $\preceq _{\mathcal {O}(\Gamma _2)}$ we get $\varphi " \preceq _{\mathcal {O}(\Gamma _2)} \varphi $ .

Proposition 5.16. Suppose $\Psi \preceq _L \Gamma $ . If $\lambda \in L$ and $\kappa \in \mathrm {Act}(\Gamma )$ are such that $\lambda $ is to the left of $\kappa $ in $\mathcal {O}(\Psi )$ , then there is an ordinal variable $\lambda ' \in \mathrm {Act}(\Gamma )$ such that $\lambda <_{\mathcal {O}(\Psi )} \lambda '$ and $\lambda '$ is also to the left of $\kappa $ in $\mathcal {O}(\Psi )$ .

Proof Suppose $\lambda \in L$ and $\kappa \in \mathrm {Act}(\Gamma )$ , and $\lambda $ is to the left of $\kappa $ in $\mathcal {O}(\Psi )$ . Then there are ancestors $\kappa _0,\lambda _0$ of $\kappa ,\lambda $ respectively such that $\lambda _0 \triangleleft _{\mathcal {O}(\Psi )} \kappa _0$ . Since $\kappa \in \mathcal {O}(\Gamma )$ , we have $\kappa _0 \in \mathcal {O}(\Gamma )$ since $\mathcal {O}(\Psi ) = \mathcal {O}(\Gamma )\uplus L$ and no variable in L is an ancestor of any variable in $\mathcal {O}(\Gamma )$ . Since $\lambda _0 \triangleleft _{\mathcal {O}(\Psi )} \kappa _0$ we have $\lambda _0 \in \mathcal {O}(\Gamma )$ since $\mathcal {O}(\Psi ) = \mathcal {O}(\Gamma )\uplus L$ and no variable in L is older than any variable in $\mathcal {O}(\Gamma )$ . It follows that $\lambda <_{\mathcal {O}(\Psi )} \lambda _0$ since $\lambda \in L$ , $\lambda _0 \in \mathcal {O}(\Gamma )$ and $\lambda _0$ was an ancestor of $\lambda $ . Since $\Psi \preceq _L \Gamma $ , there is some $\lambda ' \in \mathrm {Act}(\Gamma )$ with $\lambda <_{\mathcal {O}(\Psi )} \lambda ' \leq _{\mathcal {O}(\Psi )} \lambda _0$ . It follows that $\lambda '$ is to the left of $\kappa $ , and so we are done.

Definition 5.17. Let $\Gamma $ be a $\rho $ -tile. A $\rho $ -tile $\Psi $ is said to be an $({a},\varphi ,L)$ -successor of $\Gamma $ if $[a] \varphi \in \Gamma ^+$ and

$$\begin{align*}\Psi \preceq_L ( \mathcal{O}(\Gamma):\{\varphi\} \cup \{\psi \mid {\langle{a}\rangle} \psi \in \Gamma^+\} ). \end{align*}$$

We say that $\Psi $ is an ${a}$ -successor of $\Gamma $ if it is an $({a},\varphi ,L)$ -successor of $\Gamma $ for some $\varphi $ and L. An ${a}$ -successor $\Psi $ of $\Gamma $ is said to be a non-trivial ${a}$ -successor if the sequent $\mathcal {O}(\Psi ) : [\breve {a}] \bigvee \Gamma , \Psi $ is not provable by a slim proof.

Similarly, we say that $\Psi $ is an ${a}$ -successor of $\Gamma $ , relative to some formula $\varphi $ , and we write $\Gamma \to _{{a},\varphi } \Psi $ , if $\Psi $ is an $({a},\varphi ,L)$ -successor of $\Gamma $ for some L.

Proposition 5.18. Suppose $\Psi $ is an $({a},\varphi ,L)$ -successor of $\Gamma $ . If $\lambda \in L$ and $\kappa \in \mathrm {Act}(\Gamma )$ are such that $\lambda $ is to the left of $\kappa $ in $\mathcal {O}(\Psi )$ , then there is an ordinal variable $\lambda ' \in \mathrm {Act}(\Gamma )$ such that $\lambda < \lambda '$ and $\lambda '$ is also to the left of $\kappa $ in $\mathcal {O}(\Psi )$ .

Proof Immediate from Proposition 5.16.

5.3 Technical results on tiles and pre-tiles

In this subsection we will prove several observations on the relations between tiles and pre-tiles that will be relevant to the mosaic game that we introduce later as the main tool for our completeness proof.

The following proposition shows that provability of a given pre-tile can be reduced to provability of a (finite) set of tiles. From the dual perspective, any non-provable pre-tile can be saturated to some non-provable tile. Intuitively, the idea behind the proof is to step by step construct a tree representing a non-deterministic procedure to saturate a given pre-tile, in such a way that in each step of the procedure some of the ordinal variables progress. For example, we may add a child $\xi $ of $\kappa $ together with the formula $\varphi (\xi )$ to a pre-tile that contains the formula $\forall \lambda < \kappa \;\varphi (\lambda )$ in order to meet the saturation condition associated with such formulas, which results in a progression of the variable $\kappa $ . The result of this is that if a particular run of the procedure does not terminate but goes on forever, then it produces an infinitely descending chain of ordinal variables. The tree representing all possible runs of this non-deterministic procedure can then be viewed as a slim proof tree that derives the given pre-tile from a finite set of tiles as assumptions.

Proposition 5.19. Let $\mathcal {O} : \Gamma $ be any small $\rho $ -pre-tile, and let $\Delta $ be any finite set of formulas. Then there is a (possibly infinite) slim proof tree $\Pi $ with root labelled $\mathcal {O} : \Gamma ,\Delta $ , in which every non-axiom leaf is of the form $\mathcal {O}' : \Psi ,\Delta $ for some small $\rho $ -tile $\mathcal {O}' : \Psi $ with $\Psi \preceq \Gamma $ , and every infinite branch in $\Pi $ has an infinite descending $<$ -chain of ordinal variables.

Proof Throughout the proof we assume $\Delta = \emptyset $ , for notational convenience. The proof for the general case is not different in any significant respect.

We construct the proof tree $\Pi $ in a step-by-step manner, as the limit of a series of approximations $(\Pi _i)_{i < \omega }$ , where each leaf in each approximant $\Pi _i$ is propositionally saturated. Let $\Pi _0$ be the finite proof tree having $\Gamma $ as its root sequent, followed by enough applications of the cut rule to ensure that all the leaves of $\Pi _0$ are propositionally saturated.

Given that the proof tree $\Pi _i$ has been constructed, consider a leaf of $\Pi _i$ labelled by the sequent $\Psi $ . We say that $\chi $ in the closure of $\rho $ is a defect of $\Psi $ if one of the following conditions holds:

• • $\chi $ is of the form $\nu x\varphi $ .

• • $\chi $ belongs to $\Psi ^+$ , is of the form $\nu x^{\kappa } \varphi $ , and there are no $\kappa _0$ and $\varphi \in \Psi ^+$ such that $\kappa _0 <_{\mathcal {O}(\Psi )} \kappa $ and $\varphi ' \preceq _{\mathcal {O}(\Gamma )} \varphi (\nu x^{\kappa _0} \varphi )$ .

• • $\chi $ is of the form $\varphi (\nu x^{\kappa } \psi )$ , all free ordinal variables of $\chi $ are active in $\Gamma $ , the formula $\exists \lambda < \kappa : \overline {\varphi }(\mu x^{\lambda } \overline {\psi })$ does not belong to $\Psi ^{\mu }$ , and there are no $\kappa _0$ and $\varphi ' \in \Psi ^+$ with $\kappa _0 <_{\mathcal {O}(\Psi )} \kappa $ and $\varphi ' \preceq _{\mathcal {O}(\Gamma )} \varphi (\nu x^{\kappa _0} \psi )$ .

Clearly, a leaf of $\Pi _i$ is a tile if it is propositionally saturated and has no defects. If every leaf in $\Pi _i$ is a tile then we stop the process and set $\Pi = \Pi _i$ . Otherwise, we pick a leaf l in $\Pi _i$ and a defect of its label $\Psi $ , and extend $\Pi _i$ to $\Pi _{i+1}$ according to the following steps:

1. 1. Apply the appropriate rule (the minimisation rule, the rule $x : \kappa $ adding the formula $\nu x^{\kappa }\varphi \prec _{\mathcal {O}(\Pi _i)+\kappa } \varphi $ , or the $\nu (\kappa )$ -rule) depending on the type of defect, adding one or two children for l in which the chosen formula is no longer a defect.

2. 2. Use right weakening to remove all non-minimal formulas in the positive part of each new leaf. Note that this step removes any formula of the form $\nu x.\varphi $ that was the principal formula of the rule $x : \kappa $ applied in the first step.

3. 3. Finally, apply cuts until all leaves above l are propositionally saturated.

To be precise, the choice of which defect to deal with in each step of the construction has to follow a fair scheduling procedure to ensure that each defect is eventually taken care of, but this is rather trivial since there are only finitely many defects to choose from at each stage. Given that we implement fair scheduling, we ensure that each leaf in the proof tree $\Pi $ that we produce as the limit of the sequence $(\Pi _i)_{i < \omega }$ is a tile, so it remains only to show that every infinite branch in $\Pi $ has an infinite descending chain of ordinal variables.

So let $\beta $ be an infinite branch of $\Pi $ . For each $i < \omega $ , let $\beta \vert \Pi _i$ denote the initial segment of $\beta $ that is a branch from the root to a leaf of $\Pi _i$ , and let $\Gamma _i$ denote the last sequent on $\beta \vert \Pi _i$ . For each $i<\omega $ we write $\mathcal {O}_i$ for $\mathcal {O}(\Gamma _i)$ . Since $\beta $ is infinite there are infinitely many i such that $\beta \vert \Pi _i$ is a proper initial segment of $\beta \vert \Pi _{i+1}$ ; we say that such an index i is a growth point for $\beta $ .

The following claim shows that the procedure maintains the invariant that, if $\Psi '$ is a descendant of $\Psi $ in $\Pi _i$ , then $\Psi ' \preceq \Psi $ .

Claim 4. Let $L = \mathcal {O}(\Gamma _{i+1})\setminus \mathcal {O}(\Gamma _i)$ . Then,

1. 1. $\mathcal {O}(\Gamma _{i + 1}) = \mathcal {O}(\Gamma _i) \uplus L$ .

2. 2. $\mathrm {Act}(\Gamma _{i+1}) \subseteq \mathrm {Act}(\Gamma _i) \uplus L$ .

3. 3. No variable in L is older than any variable in $\mathrm {OV}(\mathcal {O}(\Gamma _i))$ , and every variable in L is a root (has no ancestors) or a child of some variable in $\mathrm {Act}(\Gamma _i)$ .

4. 4. If $\varphi \in \Gamma _i^+$ , then there is some formula $\varphi ' \in \Gamma _{i+1}^+$ with $\varphi ' \preceq _{\mathcal {O}_{i+1}} \varphi $ .

Proof of Claim 4

The proof of items (1) and (2) are trivial since the construction never removes variables from the constraint and never makes pre-existing non-active variables active. For the proof of item (3), we just need to inspect the construction of $\Gamma _{i+1}$ : it is obvious that no variable in $\mathcal {O}(\Gamma _{i+1})\setminus \mathcal {O}(\Gamma _i)$ is older than any variable in $\mathcal {O}(\Gamma _i)$ , by inspection of the rules applied. Furthermore, we note that any variable in L must have been added either as a new root or as a child of some active variable of $\Gamma _i$ ; the rule $x : \kappa $ adds $\kappa $ as a new root, the minimisation rule is only applied to formulas all of whose variables are active, and the $\nu (\kappa )$ -rule is only applied to formulas that actually appear in $\Gamma _i^+$ , which certainly means all variables of that formula are active. Applications of right weakening or cuts do not introduce any new ordinal variables at all.

The proof of item (4) is easy, since the only steps in the construction of $\Gamma _{i+1}$ that removes formulas in $\Gamma _i$ are applications of weakening where we pick the minimal formulas.

Given an index i let $\mathsf {u}(\Gamma )_i$ denote the set $\{\mathsf {u}(\varphi ) \mid \varphi \in \Gamma _i^+\}$ . It is clear from Claim 4 that $\mathsf {u}(\Gamma )_i \subseteq \mathsf {u}(\Gamma )_j$ whenever $i \leq j$ . So since the set of underlying plain formulas in $\Gamma _i^+$ is bounded by the size of the closure of the root formula $\rho $ , there is some index i with $\mathsf {u}(\Gamma )_i = \mathsf {u}(\Gamma )_j$ for all $j \geq i$ . We may as well assume $i = 0$ since otherwise we can just consider a final segment of $\beta $ suitably re-indexed. With this assumption in place we can now prove:

Claim 5. For every growth point i of $\beta $ , either there is some formula $\varphi \in \Gamma _i^+$ and some formula $\varphi '$ in $\Gamma _{i + 1}^+\setminus \Gamma _i^+$ with $\varphi ' \prec _{\mathcal {O}_{i+1}} \varphi $ , or $\Gamma _{i + 1}$ has strictly fewer defects than $\Gamma _i$ .

Proof of Claim 5

Let i be a growth point. We make a case distinction according to how $\Gamma _{i+1}$ follows a fix of some defect. There are the following possible cases to consider:

Case $\Gamma _i$ is the conclusion of an application of the $x: \kappa $ -rule in which the principal formula $\nu x\varphi $ is a defect. Then $\Gamma _{i+1}^+$ contains the formula $\nu x^{\kappa }\varphi \prec _{\mathcal {O}(\Gamma _{i+1})} \nu x\varphi $ . Furthermore, $\nu x^{\kappa }\varphi $ cannot be in $\Gamma _i^+$ because then $\nu x\varphi $ would not be minimal.

Case $\Gamma _i$ is the conclusion of an application of the $\nu (\kappa )$ -rule in which the principal formula $\nu x^{\kappa } \varphi $ is a defect. The premise of this rule application then contains $\varphi [\nu x^{\kappa '} \varphi /x]$ where $\kappa ' <_{\mathcal {O}_{i+1}} \kappa $ . Let $\psi $ be the unique formula in $\Gamma _i$ such that $\mathsf {u}(\psi ) = \mathsf {u}(\varphi [\nu x^{\kappa '} \varphi /x])$ . We cannot have $\psi \preceq _{\mathcal {O}_{i+1}} \varphi [\nu x^{\kappa '}\varphi /x]$ , since then $\nu x^{\kappa } \varphi $ was not a defect of $\Gamma _i$ . So $\varphi [\nu x^{\kappa '}\varphi /x] \prec _{\mathcal {O}_{i+1}} \psi $ , and since $\psi \in \Gamma _i^+$ we are done.

Case $\Gamma _i$ is the conclusion of an application of the minimisation rule, and $\Gamma _{i+1}$ is a descendant of the left premise. Since no formulas in $\Gamma _i^+$ or $\Gamma _i^-$ are removed in the left premise, and no new active variables are introduced, we see that the left premise is already a propositionally saturated small pre-tile and therefore equal to $\Gamma _{i + 1}$ . So in this case the defect is fixed and no new defects are introduced, meaning that $\Gamma _{i+1}$ has strictly fewer defects than $\Gamma _i$ .

Case $\Gamma _i$ is the conclusion of an application of the minimisation rule, and $\Gamma _{i+1}$ is a descendant of the right premise. The defect that is to be fixed is of the form $\varphi (\nu x^{\kappa }\psi )$ , where all variables of this formula are active in $\Gamma _i$ , $\theta \in \Gamma _i^+$ for some $\theta \preceq _{\mathcal {O}_i} \varphi (\nu x^{\kappa } \psi )$ , and the right premise contains $\varphi (\nu x^{\kappa '}\psi )$ for some $\kappa '$ with $\kappa ' <_{\mathcal {O}_{i+1}} \kappa $ . Either $\varphi (\nu x^{\kappa '}\psi ) \in \Gamma _{i+1}^+$ , or it is replaced by some $\prec _{\mathcal {O}_{i+1}}$ -smaller formula $\theta ' \in \Gamma _{i+1}^+$ . Note that in the latter case we cannot have $\theta \prec _{\mathcal {O}_{i+1}} \theta '$ , since then $\theta '$ would not be minimal. By linearity of $\preceq _{\mathcal {O}_{i+1}}$ we get $\theta '\preceq _{\mathcal {O}_{i+1}} \theta $ . If $\theta ' = \theta $ then clearly $\Gamma _{i+1}$ contains strictly fewer defects than $\Gamma _i$ since no new formulas were introduced, and in the other case we have $\theta ' \prec _{\mathcal {O}_{i+1}} \theta $ as required.

This concludes the proof of the claim.

Let $\varphi $ be the underlying plain formula of some formula in $\Gamma _0^+$ . Say that $\varphi $ is improved at index i if, for $\varphi '$ denoting the unique formula in $\Gamma _i^+$ with $\mathsf {u}(\varphi ') = \varphi $ and $\varphi "$ denoting the unique formula in $\Gamma _{i+1}^+$ with $\mathsf {u}(\varphi ") = \varphi $ , we have $\varphi " \prec _{\mathcal {O}_{i+1}} \varphi '$ .

From Claim 5 and the pigeonhole principle (there is only a fixed finite number of underlying plain formulas), it follows that some formula is improved at infinitely many indices. This gives us an infinite $\prec $ -descending chain of formulas on $\beta $ and therefore, by considering the highest ranking variable in $\varphi $ whose annotation changes infinitely many times, an infinite $\prec $ -descending chain of ordinal variables. By Proposition 5.6, this ensures that we find an infinite $<$ -descending chain of ordinal variables on $\beta $ .

Finally, from Claim 4 it clearly follows that $\Gamma _{i+1} \preceq \Gamma _i$ for all i. Together with Proposition 5.15, it follows that $\Psi \preceq \Gamma $ for any leaf $\Psi $ in the proof tree $\Pi $ that we have constructed.

As a corollary we obtain:

Proposition 5.20. Let $\mathcal {O} : \Gamma $ be any small $\rho $ -tile and suppose $[a] \varphi \in \Gamma $ . Then there is a (possibly infinite) slim proof tree $\Pi $ , in which every leaf $\Psi $ is a non-trivial small ${a}$ -successor of $\Gamma $ containing $\varphi '$ for some $\varphi ' \prec _{\mathcal {O}(\Psi )}\varphi $ , and every infinite branch has an infinite $<$ -descending chain of ordinal variables.

Proof We first note that, where $\{[a] \varphi \} \cup \{ {\langle {a}\rangle } \psi \mid \psi \in \Psi \} \subseteq \Gamma $ , the following is an instance of the modal rule:

Now, apply Proposition 5.19 to the sequent $\mathcal {O} : [\breve {a}]\bigvee \Gamma , \varphi , \Psi $ , producing a slim proof tree in which every leaf is labelled by some sequent of the form $\mathcal {O}' : [\breve {a}] \bigvee \Gamma , \Theta $ where $\mathcal {O}' : \Theta $ is an ${a}$ -successor of $\Gamma $ . Finally, for each such leaf labelled $\mathcal {O}' : [\breve {a}] \bigvee \Gamma , \Theta $ , if the ${a}$ -successor $\mathcal {O}' : \Theta $ is non-trivial then extend it by an application of weakening, leaving $\mathcal {O}' : \Theta $ as the label of the new leaf, and otherwise, plug in a wellfounded proof of $\mathcal {O}' : [\breve {a}] \bigvee \Gamma , \Theta $ . The resulting proof tree now has the properties required by the proposition.

Next we draw some consequences of the saturation conditions of a tile. The following proposition shows that an unprovable tile behaves in accordance with the local conditions for a counter-model.

Proposition 5.21. Let $\Gamma $ be a small tile which does not have a slim proof. The following properties hold.

1. 1. If $\varphi \wedge \psi \in \Gamma ^+$ then $\varphi ' \in \Gamma ^+$ for some $\varphi '\preceq _{\mathcal {O}(\Gamma )} \varphi $ or $\psi ' \in \Gamma ^+$ for some $\psi ' \preceq _{\mathcal {O}(\Gamma )} \psi $ .

2. 2. If $\varphi \vee \psi \in \Gamma $ then $\varphi ' \in \Gamma ^+$ for some $\varphi '\preceq _{\mathcal {O}(\Gamma )} \varphi $ and $\psi ' \in \Gamma ^+$ for some $\psi ' \preceq _{\mathcal {O}(\Gamma )} \psi $ .

3. 3. If $\mu x\, \varphi \in \Gamma $ then $\theta \in \Gamma ^+$ for some $\theta \preceq _{\mathcal {O}(\Gamma )}\varphi [\mu x\, \varphi /x]$ .

Proof For item $(1)$ , suppose that $\varphi \wedge \psi \in \Gamma ^+$ but there is no $\varphi ' \preceq _{\mathcal {O}(\Gamma )} \varphi $ with $\varphi ' \in \Gamma ^+$ and no $\psi ' \preceq _{\mathcal {O}(\Gamma )} \psi $ with $\psi ' \in \Gamma $ . Then since all ordinal variables in both $\varphi $ and $\psi $ are active in $\Gamma $ , we get $\overline {\varphi } \in \Gamma $ and $\overline {\psi } \in \Gamma $ . Thus we can provide a slim proof of $\Gamma $ as follows:

The proofs of items $(2)$ and $(3)$ are similar.

Next, we prove two crucial propositions about ${a}$ -successors of a tile, both involving the “backwards modalities” for the converse action $\breve {a}$ .

Proposition 5.22. Let $\Gamma $ be a small $\rho $ -tile and let $\Psi $ be a non-trivial small ${a}$ -successor of $\Gamma $ . Suppose ${\langle {\breve {a}}\rangle } \psi \in \Psi ^+$ , and suppose every ordinal variable in $\psi $ is active in $\Gamma $ . Then $\psi ' \in \Gamma ^+$ for some $\psi ' \preceq _{\mathcal {O}(\Gamma )} \psi $ .

Proof Since ${\langle {\breve {a}}\rangle } \psi \in \Psi ^+$ the underlying plain formula of $\psi $ belongs to the closure of $\rho $ , and by assumption all its ordinal variables are active in $\Gamma $ . Hence, since $\Gamma $ is a tile, either $\psi ' \in \Gamma ^+$ for some $\psi ' \preceq _{\mathcal {O}(\Gamma )} \psi $ or $\overline {\psi } \in \Gamma ^-$ . But in the latter case, we can easily construct a wellfounded proof of the sequent $\mathcal {O}(\Psi ) : [\breve {a}] \bigvee \Gamma ,\Psi $ :

This contradicts the assumption that $\Psi $ was a non-trivial ${a}$ -successor.

The next proposition is more subtle, and will play a key role in our completeness proof for slim proofs. First a definition:

Definition 5.23. Let $\Gamma $ be a small $\rho $ -tile and let $\Psi $ be a non-trivial small ${a}$ -successor of $\Gamma $ . Suppose ${\langle {\breve {a}}\rangle } \psi \in \Psi ^+$ and suppose x is the highest ranking $\nu $ -variable of $\psi $ such that $\lambda = \mathsf {o}_{\psi }(x)$ is not active in $\Gamma $ , assuming such a variable exists. Let $\kappa $ be an active variable of $\Gamma $ such that $\lambda \prec _{\mathcal {O}(\Psi )} \kappa $ . Let $\sigma : \mathrm {Act}(\Psi ) \to \mathrm {Act}(\Gamma )$ be some substitution on ordinal variables such that:

1. 1. $\sigma (\xi ) = \xi $ for each $\xi $ that is active in $\Gamma $ ,

2. 2. $\sigma (\lambda ) \prec _{\mathcal {O}(\Gamma )} \kappa $ ,

3. 3. $\psi ' \in \Gamma ^+$ for some $\psi ' \preceq _{\mathcal {O}(\Gamma )} \psi [\sigma ]$ .

Then we say that the substitution $\sigma $ preserves progression from $\kappa $ to ${\langle {\breve {a}}\rangle }\psi $ (relative to $\Gamma $ and $\Psi $ ). If $\varphi $ is a formula in $\Gamma ^+$ and $\sigma $ preserves progression from $\mathsf {o}_{\varphi }(x)$ to ${\langle {\breve {a}}\rangle }\psi $ , then we say the substitution $\sigma $ preserves progression from $\varphi $ to ${\langle {\breve {a}}\rangle }\psi $ .

Proposition 5.24. Let $\Gamma $ be a small $\rho $ -tile and let $\Psi $ be a non-trivial small ${a}$ -successor of $\Gamma $ . Suppose ${\langle {\breve {a}}\rangle } \psi \in \Psi ^+$ . Let o be any annotation whose range is contained in $\mathrm {Act}(\Gamma )$ and suppose x is a fixpoint variable such that $\mathsf{o}_{\psi } \prec ^x_{\mathcal {O}(\Psi )} o$ and $\mathsf{o}_{\psi }(y) \in \mathrm {Act}(\Gamma )$ for all y higher ranking or equal to x. Then there is a formula $\theta $ such that:

• • $\theta \in \Gamma ^+$ ,

• • $\mathsf {u}(\theta ) = \mathsf {u}(\psi )$ , and

• • $\mathsf{o}_{\theta } \prec ^y_{\mathcal {O}(\Gamma )} o$ for some y higher ranking or equal to x.

Proof We first define a substitution $\tau : \mathrm {Act}(\Psi ) \to \mathrm {Act}(\Gamma )$ as follows: for each variable $\lambda \in \mathrm {Act}(\Psi )$ , $\tau $ maps $\lambda $ to its $<_{\mathcal {O}(\Psi )}$ -smallest ancestor in $\mathrm {Act}(\Gamma )$ . Note that this is well-defined by definition of an ${a}$ -successor, and note that $\tau (\kappa ) = \kappa $ for $\kappa \in \mathrm {Act}(\Gamma ) \cap \mathrm {Act}(\Psi )$ , and therefore $\tau (\mathsf{o}_{\psi }(y)) = \mathsf{o}_{\psi }(y) = o(y)$ for all y higher ranking or equal to x.

Claim 6. There is some formula $\theta \in \Gamma ^+$ such that $\theta \preceq _{\mathcal {O}(\Gamma )} \psi [\tau ]$ .

Proof of Claim 6

Otherwise we have $\overline {\psi [\tau ]} \in \Gamma ^-$ , and we can derive $\mathcal {O}(\Psi ) : \Psi , [\breve {a}] \bigvee \Gamma $ as follows.

Since $\mathsf{o}_{\psi }(x) \prec _{\mathcal {O}(\Psi )} o(x)$ we have two different cases to consider.

Case 1: $\mathsf{o}_{\psi }(x)$ is to the left of $o(x)$ . Since $\Psi $ was an ${a}$ -successor, we have $\mathsf{o}_{\psi }(x) \in L$ for some L such that $\mathcal {O}(\Psi ) = \mathcal {O}(\Gamma ) \uplus L$ . By Proposition 5.18 there is some variable $\kappa \in \mathrm {Act}(\Gamma )$ such that $\mathsf{o}_{\psi }(x) <_{\mathcal {O}(\Psi )} \kappa $ and $\kappa $ is to the left of $o(x)$ in $\mathcal {O}(\Psi )$ (equivalently in $\mathcal {O}(\Gamma )$ ). By definition of $\tau $ it follows that $\tau (\mathsf{o}_{\psi }(x))$ is also to the left of $o(x)$ in $\mathcal {O}(\Gamma )$ . Hence $\tau (\mathsf{o}_{\psi }(x)) \prec _{\mathcal {O}(\Gamma )} o(x)$ . By Claim 6 there is some formula $\theta \in \Gamma ^+$ such that $\theta \preceq _{\mathcal {O}(\Gamma )} \psi [\tau ]$ . It easily follows that $\mathsf{o}_{\theta } \prec ^y_{\mathcal {O}(\Gamma )} o$ for some y higher ranking or equal to x.

Case 2: $\mathsf{o}_{\psi }(x) <_{\mathcal {O}(\Psi )} o(x)$ . Let us write $\psi $ as $\alpha (\nu x^{\mathsf{o}_{\psi }(x)} \beta )$ so that $\psi [\tau ]$ is $\alpha [\tau ](\nu x^{\tau (\mathsf{o}_{\psi }(x))} \beta [\tau ])$ .

Claim 7. $\exists \xi < o(x):\overline {\alpha [\tau ]}(\mu x^{\xi } \overline {\beta [\tau ]}) \notin \Gamma ^{\mu }$ .

Proof of Claim 7

By assumption we have $\mathsf{o}_{\psi }(x) <_{\mathcal {O}(\Psi )} o(x)$ , so if the displayed formula were in $\Gamma ^{\mu }$ then we could prove $\mathcal {O}(\Psi ): \Psi , [\breve {a}] \bigvee \Gamma $ as follows:

Since $\theta \in \Gamma ^+$ and $\theta \preceq _{\mathcal {O}(\Psi )} \psi [\tau ]$ , the saturation condition of a tile with respect to the minimisation rule ensures that there are some $\lambda <_{\mathcal {O}(\Gamma )} o(x)$ and some formula $\theta '\in \Gamma ^+$ such that $\theta ' \preceq _{\mathcal {O}(\Gamma )} \alpha [\tau ](\nu x^{\lambda } \beta [\tau ])$ . Let $o'$ be the annotation of the formula $\alpha [\tau ](\nu x^{\lambda } \beta [\tau ])$ , so that $o'(x) = \lambda <_{\mathcal {O}(\Gamma )} o(x)$ , hence $o'(x) \prec _{\mathcal {O}(\Gamma )} o(x)$ . Furthermore, for all y ranking higher than or equal to x we have

$$ \begin{align*} o'(y) & = \mathsf{o}_{\psi[\tau]}(y) \\ & = \tau(\mathsf{o}_{\psi}(y)) \\ & = o(y), \end{align*} $$

where the last inequality is due to $\mathsf{o}_{\psi }(y)$ being active in $\Gamma $ (since x was the highest ranking variable with $\mathsf{o}_{\psi }(x)$ non-active in $\Gamma $ ). Now let $o"$ be the annotation of $\theta '$ . Since $\theta ' \preceq _{\mathcal {O}(\Gamma )} \alpha [\tau ](\nu x^{\lambda } \beta [\tau ])$ it follows by definition that $o" \prec ^y_{\mathcal {O}(\Gamma )} o'$ for some y. Either y is higher ranking than or equal to x in which case $o"(y) \prec _{\mathcal {O}(\Gamma )} o'(y) \preceq _{\mathcal {O}(\Gamma )} o(y)$ , or y is lower ranking than x in which case $o"(x) = o'(x) \prec _{\mathcal {O}(\Gamma )} o(x)$ . In either case the desired conclusion follows.

5.4 Completeness of slim proofs

The goal of this section is to show that every valid formula $\rho $ has a slim proof. We will do so using a two-player game that we call the mosaic game, played between two players called “Prover” and “Refuter.” Our strategy is as follows: We first prove the determinacy of the mosaic game, that is, the fact that either Prover or Refuter has a winning strategy. It then suffices to show that Refuter cannot have a winning strategy if $\rho $ is valid, and $\rho $ has a slim proof if the mosaic game is a win for Prover.

We now define the mosaic game for the given formula $\rho $ . The two players in the mosaic game are called Prover and Refuter. There are three kinds of positions in this game: the fixed formula $\rho $ , used as the starting position, $\rho $ -tiles and pairs $( \Gamma , [a] \varphi )$ where $\Gamma $ is a $\rho $ -tile and $[a] \varphi \in \Gamma ^+$ . Ownership of positions and legal moves of the game are specified in Table 3, where we recall that $T_{\rho }$ denotes the set of $\rho $ -tiles, and we write $\Gamma \to _{{a},\varphi } \Psi $ if $\Psi $ is an ${a}$ -successor of $\Gamma $ , relative to $\varphi $ (cf. Definition 5.17). In words, the mosaic game for $\rho $ starts at the formula $\rho $ itself, which is a position for Refuter. After Refuter’s initial move, which consists of a $\rho $ -tile containing the formula $\rho $ , the two players take turns. At a $\rho $ -tile $\Gamma $ , Prover has to select a formula $[a] \varphi \in \Gamma ^+$ , and at a position of the form $(\Gamma ,[a] \varphi )$ , Refuter has to pick a witness in the form of an ${a}$ -successor of $\Gamma $ , relative to $\varphi $ .

Table 3 Moves in the mosaic game.

Prover wins an infinite play if the play contains an infinite descending $\prec $ -chain of ordinal variables, otherwise Refuter wins the play. More formally, if $( \mathcal {O}_i : \Gamma _i )_{i < \omega }$ enumerates the $\rho $ - tiles occurring in an infinite play, then this play is won by Prover iff there exist $k < \omega $ and an infinite sequence of ordinal variables $(\kappa _i)_{i<\omega }$ such that $\kappa _{i+1} \preceq _{\mathcal {O}_{k+i}} \kappa _i$ for all i, and $\kappa _{i+1} \prec _{\mathcal {O}_{k+i}} \kappa _i$ for infinitely many i. (Note that if $\Gamma _0,\Gamma _1$ are tiles such that $\Gamma _1$ is reachable from $\Gamma _0$ via some partial play in the mosaic game, then the constraint of $\Gamma _1$ contains that of $\Gamma _0$ . This is a direct consequence of the definition of an ${a}$ -successor and the relation $\preceq _L$ over pre-tiles.) Finite plays are lost by the player who got stuck.

Proposition 5.25. The mosaic game is determined.

Proof Fix a formula $\rho $ and an injection of the set of positions into the natural numbers, so that every play in the mosaic game for $\rho $ corresponds to a unique function from $\mathbb N$ to $\mathbb N$ , i.e., an element of the Baire space $\mathbb N^{\mathbb N}$ . Let $P \subseteq \mathbb N^{\mathbb N}$ be the set of sequences in which Refuter makes an illegal move and (moreover) the first illegal move. Furthermore, let $W \subseteq \mathbb N^{\mathbb N}$ describe the set of infinite plays in the mosaic game for $\rho $ that are winning for Prover.

Recall that Prover and Refuter take alternating turns in the mosaic game; it is then not hard to see that Prover has a winning strategy in the mosaic game for $\rho $ iff Player I (i.e., the player that plays first) has a winning strategy in the Gale–Stewart game on the Baire space with winning set $P \cup W$ . We claim that this winning set is Borel, whence determinacy of the mosaic game is a consequence of Martin’s Borel Determinacy Theorem [14]. Being a union of open sets, P is clearly Borel. We show that W is also Borel.

Given a play $\pi $ , say that an ordinal variable $\kappa $ is covered in $\pi $ if it has some active descendant in every constraint in $\pi $ in which $\kappa $ occurs. Note that for each ordinal variable $\kappa $ , the set of plays in which $\kappa $ is covered is Borel. Let be a sequence of n tiles from a given play $\pi $ in the mosaic game, with constraints , such that $\Gamma _{n-1} \preceq \cdots \preceq \Gamma _0$ . We call this sequence a stable progression of length n if there are variables each of which is covered in $\pi $ , such that:

• • $\kappa _i \in \mathrm {Act}(\mathcal {O}_i)$ for each $i < n$ ,

• • $\kappa _j <_{\mathcal {O}_j} \kappa _i$ for $0 \leq i < j < n$ .

Let $W_n$ be the set of infinite plays that contain a stable progression of length n. Clearly each set $W_n$ is Borel, so the set $\bigcap _{n \in \omega } W_n$ is Borel. We claim that $W = \bigcap _{n \in \omega } W_n$ .

For the left-to-right inclusion: if $\pi \in W$ then it has an infinite $\prec $ -descending chain. Repeating the proof of Proposition 5.6, we can show that $\pi $ in fact has an infinite $<$ -descending chain. Since as a sequence of tiles the play $\pi $ is decreasing with respect to the order $\preceq $ , by definition of the relation $\preceq $ on tiles (Definition 5.14), it is not hard to see that every ordinal variable in this infinite $<$ -descending chain has to be covered. Hence $\pi $ contains stable progressions of arbitrary length.

For right-to-left, suppose $\pi $ has a progression of length n, for all $n \in \omega $ . We define a tree consisting of all the ordinal variables that are covered in $\pi $ , where $\lambda $ is a child of $\kappa $ if this holds with respect to some constraint appearing in $\pi $ . Note that this is a finite set of finitely branching rooted trees: since we never add $<$ -ancestors to pre-existing variables (by Definition 5.14), the set of children of a variable is increasing along $\pi $ , and since the number of active variables in a tile is bounded this means there is also a bound on the size of $<$ -anti-chains of covered variables in any constraint in $\pi $ . We can view the structure as a single finitely branching tree by appending a new root. The resulting tree is infinite since $\pi $ contains stable progressions of arbitrary length, and so by König’s lemma it contains an infinite branch. This infinite branch is an infinite $<$ -descending chain of ordinal variables in $\pi $ , and therefore also an infinite $\prec $ -descending chain.

With Proposition 5.25 in place, we want to prove that a winning strategy for Prover yields a slim proof, and on the other hand, a winning strategy for Refuter yields a counter-model. We begin with the first statement.

Proposition 5.26. If Prover has a winning strategy in the mosaic game for $\rho $ , then the formula $\rho $ has a slim proof.

Proof Let $\sigma $ be a winning strategy for Prover in the mosaic game for $\rho $ . We show how to construct a slim proof for an arbitrary small $\rho $ -tile $\Gamma \preceq \{ \rho \}$ as Proposition 5.19 ensures this is sufficient to establish that $\rho $ admits a slim proof. Consider the tree of maximal plays consistent with $\sigma $ starting from $\Gamma $ . By assumption, all such plays are winning for Prover. We now let $\Pi $ be the tree of positions owned by Prover in these plays. These positions are precisely the small $\rho $ -tiles in the $\sigma $ -plays starting from $\Gamma $ . We can thus view $\Pi $ as a derivation with root $\Gamma $ in the calculus consisting only of rules

where $\rightarrow _{a,\varphi }$ is the relation of a-successor relative to $\varphi $ from Definition 5.17. Moreover, as $\sigma $ is winning, every infinite path through the derivation contains an infinite $ \prec $ -decreasing chain of ordinal variables through the sequence of constraints on the path. All that remains is to replace each of above rules by the corresponding slim derivation guaranteed by Proposition 5.20 and Proposition 5.6: The restriction on applications of $\mathsf {lw} $ in slim derivations guarantees that the induced expansion of $\Pi $ is a slim proof.

We now come to the key technical result of the paper, showing that winning strategies for Refuter indeed correspond to counter-models.

Proposition 5.27. Suppose Refuter has a winning strategy in the mosaic game for $\rho $ . Then $\rho $ is not valid.

Proof Fix a winning strategy $\sigma $ for Refuter, and let $\Gamma $ be the tile containing $\rho $ chosen by the first move of Refuter according to $\sigma $ . We construct a counter-model $M^{\sigma } = (W^{\sigma },R^{\sigma },V^{\sigma })$ as follows: $W^{\sigma }$ is the set of $\sigma $ -guided partial plays whose last position belong to Prover, i.e., the last position is a small tile. In the sequel we may write $\pi \sqsubseteq \pi '$ ( $\pi \sqsubset \pi '$ ) if $\pi $ is an initial segment of $\pi '$ (a proper initial segment of $\pi '$ , respectively). Given an action label ${a}$ , and plays $\pi _0,\pi _1 \in W^{\sigma }$ , we set $(\pi _0,\pi _1) \in R^{\sigma }_{{a}}$ if and only if either

1. 1. $\pi _1$ extends $\pi _0$ with a choice of a formula $[a] \varphi $ by Prover, followed by a choice of a non-trivial ${a}$ -successor $\Psi $ of the last position on $\pi _0$ containing some $\varphi ' \prec _{\mathcal {O}(\Psi )} \varphi $ , according to the strategy $\sigma $ of Refuter, or

2. 2. $\pi _0$ extends $\pi _1$ with a choice of a formula $[\breve {a}] \varphi $ by Prover, followed by a choice of a non-trivial $\breve {a}$ -successor $\Psi $ of the last position on $\pi _1$ containing some $\varphi ' \prec _{\mathcal {O}(\Psi )} \varphi $ , according to the strategy $\sigma $ of Refuter.

Note that $\pi _0 R^{\sigma }_{{a}} \pi _1$ iff $\pi _1 R^{\sigma }_{\breve {a}} \pi _0$ . For the valuation $V^{\sigma }$ , we set $\pi \in V^{\sigma }(p)$ if and only if $\overline {p} \in \Theta $ , where $\Theta $ is the last position of $\pi $ .

Note that $(\Gamma , \rho )$ is a position in the evaluation game for $\rho $ in $M^{\sigma }$ , since $\Gamma \in W^{\sigma }$ (more precisely, the partial play consisting only of the position $\Gamma $ is in $W^{\sigma }$ ). We shall provide a winning strategy $\sigma '$ for Falsifier in the evaluation game at this position. While constructing the strategy $\sigma '$ we shall inductively maintain the condition that for any $\sigma '$ -guided partial play $(\pi _0,\varphi _0)...(\pi _n,\varphi _n)$ , the partial plays $\pi _0,...,\pi _n$ are $\sigma $ -guided, and furthermore there is a sequence of positively annotated formulas $(\varphi _0^{\prime },...,\varphi _n^{\prime })$ such that, if we denote the last sequent on each play $\pi _i$ as $\Theta _i$ and its constraint set as $\mathcal {O}_i$ , then:

1. 1. $\varphi _i^{\prime } \in \Theta _i^+$ .

2. 2. $\mathsf {u}(\varphi _i^{\prime }) = \varphi _i$ .

3. 3. If $i < n$ , $\varphi _i = \psi _0 \vee \psi _1$ and $\varphi _{i+1} = \psi _j$ where $j \in \{0,1\}$ , then $\pi _{i} = \pi _{i + 1}$ , $\varphi _i^{\prime }$ is of the form $\psi _0^{\prime }\vee \psi _1^{\prime }$ and $\varphi _{i + 1}^{\prime } \preceq _{\mathcal {O}_i} \psi _j^{\prime }$ .

4. 4. If $i < n$ , $\varphi _i = \psi _0 \wedge \psi _1$ and $\varphi _{i+1} = \psi _j$ where $j \in \{0,1\}$ , then $\pi _{i} = \pi _{i + 1}$ , $\varphi _i^{\prime }$ is of the form $\psi _0^{\prime }\wedge \psi _1^{\prime }$ and $\varphi _{i + 1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \psi _j^{\prime }$ .

5. 5. If $i < n$ , $\varphi _i = \mu x. \psi $ and $\varphi _{i + 1} = \psi [\mu x. \psi /x]$ , then $\pi _{i} = \pi _{i + 1}$ , $\varphi _i^{\prime }$ is of the form $\mu x. \psi '$ and $\varphi _{i + 1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \psi '[\mu x. \psi '/x]$ .

6. 6. If $i < n$ , $\varphi _i = \nu x. \psi $ and $\varphi _{i + 1} = \psi [\nu x. \psi /x]$ , then $\pi _{i} = \pi _{i + 1}$ , $\varphi _i^{\prime }$ is of the form $\nu x^{\kappa } \theta $ and $\varphi _{i + 1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \theta [\nu x^{\kappa _0} \theta /x]$ for some $\kappa _0$ such that $\kappa _0 <_{\mathcal {O}_{i+1}} \kappa $ .

7. 7. If $i < n$ , $\varphi _{i} = [a] \psi $ and $\varphi _{i + 1} = \psi $ , then $\pi _i \sqsubset \pi _{i + 1}$ , $(\pi _{i},\pi _{i+1}) \in R^{\sigma }_{a}$ , and $\varphi _i^{\prime }$ is of the form $[a]\psi '$ where $\varphi _{i + 1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \psi '$ .

8. 8. If $i < n$ , $\varphi _{i} = {\langle {a}\rangle }\psi $ , $\varphi _{i + 1} = \psi $ , then $(\pi _{i},\pi _{i+1}) \in R^{\sigma }_{a}$ , $\varphi _i^{\prime }$ is of the form ${\langle {a}\rangle }\psi '$ and either

   1. (a) $\pi _{i}\sqsubset \pi _{i + 1}$ and $\varphi _{i + 1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \psi '$ , or

   2. (b) $\pi _{i + 1} \sqsubset \pi _i$ , and letting k be the greatest index less than $i+1$ with $\pi _k = \pi _{i+1}$ , we have, either:

      1. i. all ordinal variables in $\psi '$ are active in $\Theta _{i+1}$ , and $\varphi _{i+1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \psi '$ , or

      2. ii. some ordinal variable in $\psi '$ is not active in $\Theta _{i+1}$ , for the highest ranking fixpoint variable x with $\mathsf{o}_{\psi '}(x) \notin \mathrm {Act}(\Theta _{i+1})$ it does not hold that $\mathsf{o}_{\psi '} \prec ^x_{\mathcal {O}_{i}} \mathsf{o}_{\varphi _k^{\prime }}$ , and $\varphi _{i+1}^{\prime } \preceq _{\mathcal {O}_{i+1}} \psi '[\tau ]$ for some substitution $\tau $ with $\tau (\kappa ) = \kappa $ for all $\kappa \in \mathrm {Act}(\Theta _{i+1})$ , or

      3. iii. some ordinal variable in $\psi '$ is not active in $\Theta _{i+1}$ , for the highest ranking fixpoint variable x with $\mathsf{o}_{\psi '}(x) \notin \mathrm {Act}(\Theta _{i+1})$ it holds that $\mathsf{o}_{\psi '} \prec ^x_{\mathcal {O}_i} \mathsf{o}_{\varphi _k^{\prime }}$ where x is the highest ranking, and for some y higher ranking or equal to x we have $\mathsf{o}_{\varphi _{i+1}} \prec ^y_{\mathcal {O}_{i+1}} \mathsf{o}_{\psi ^{\prime }}$ .

Suppose the strategy $\sigma '$ has been defined on all partial plays of length $< n$ , and let $(\pi _0,\varphi _0)\cdots(\pi _n,\varphi _n)$ be a play of length n. We show how to define the strategy $\sigma '$ on this play, if the last position belongs to Falsifier, and we show how to maintain the inductive invariant for each $\sigma '$ -guided play of length $n + 1$ extending $(\pi _0,\varphi _0)\cdots(\pi _n,\varphi _n)$ . The construction is carried out on a case-by-case basis depending on the shape of the last position.

Case $\varphi _n$ is of the form p or $\overline {p}$ for some propositional variable p. Then there are no available moves, so we need not define the strategy $\sigma '$ here and the inductive invariant is trivially maintained for all extensions of the play.

Case $\varphi _n$ is of the form $\alpha \wedge \beta $ . This position belongs to Falsifier. By the induction hypothesis $\varphi _n^{\prime } \in \Theta _n^+$ , and $\mathsf {u}(\varphi _n^{\prime }) = \alpha \wedge \beta $ . Hence $\varphi _n^{\prime }$ is of the form $\alpha ' \wedge \beta '$ where $\mathsf {u}(\alpha ') = \alpha $ and $\mathsf {u}(\beta ') = \beta $ . By Proposition 5.21, $\alpha " \in \Theta _n^+$ for some $\alpha " \preceq _{\mathcal {O}_n} \alpha '$ or $\beta " \in \Theta _n^+$ for some $\beta " \preceq _{\mathcal {O}_n} \beta '$ (or both). In the first case we define $\sigma '$ so that Falsifier chooses $(\pi _n,\alpha )$ and set $\varphi _{n + 1}^{\prime } = \alpha "$ , and in the second case we define $\sigma '$ so that Falsifier chooses $(\pi _n,\beta )$ and set $\varphi _{n + 1}^{\prime } = \beta "$ (and if both cases hold the choice can be defined arbitrarily). The inductive invariant is clearly maintained.

Case $\varphi _n$ is of the form $\alpha \vee \beta $ . This position belongs to Verifier. By the induction hypothesis $\varphi _n^{\prime } \in \Theta _n^+$ , and $\mathsf {u}(\varphi _n^{\prime }) = \alpha \vee \beta $ . Hence $\varphi _n^{\prime }$ is of the form $\alpha ' \vee \beta '$ where $\mathsf {u}(\alpha ') = \alpha $ and $\mathsf {u}(\beta ') = \beta $ . By Proposition 5.21, $\alpha " \in \Theta _n^+$ for some $\alpha " \preceq _{\mathcal {O}_n} \alpha '$ and $\beta " \in \Theta _n^+$ for some $\beta " \preceq _{\mathcal {O}_n} \beta '$ . So clearly, given any extension of the play $(\pi _0,\varphi _0)...(\pi _n,\varphi _n)$ in which Verifier chooses $(\pi _n,\gamma )$ with $\gamma \in \{\alpha , \beta \}$ , we can choose $\gamma '$ so that the inductive invariant is maintained.

Case $\varphi _n$ is of the form $[a] \alpha $ . This position belongs to Falsifier. The shadow formula $\varphi _n^{\prime }$ is of the form $[a] \alpha '$ where $\mathsf {u}(\alpha ') = \alpha $ , and we have $[a] \alpha ' \in \Theta _n^+$ by the induction hypothesis. Let Prover play the formula $[a] \alpha '$ , and let $\Psi $ be the non-trivial small ${a}$ -successor of $\Theta _n$ chosen by Refuter in response to this move according to the strategy $\sigma $ . By definition of an admissible move for Refuter there is some $\alpha " \in \Psi ^+$ such that $\alpha " \preceq _{\mathcal {O}(\Psi )} \alpha '$ . We set $\sigma '$ so that Falsifier chooses $(\pi _n \cdot \Psi ,\alpha )$ . Since $\alpha " \in \Psi $ and $\mathsf {u}(\alpha ") = \mathsf {u}(\alpha ') = \alpha $ , the inductive invariant is maintained.

Case $\varphi _n$ is of the form ${\langle {a}\rangle } \alpha $ . This position belongs to Verifier, and we have to show that the inductive invariant is maintained for every possible move of Verifier. Every choice of Verifier at this position is of the form $(\pi ',\alpha )$ where one of the following two cases holds: $(i) \ \pi '$ is of the form $(\pi _n \cdot \Psi )$ where $\Psi $ is a non-trivial ${a}$ -successor of $\Theta _n$ , or $(ii) \ \pi _n$ is of the form $\pi ' \cdot \Theta _n$ where $\Theta _n$ is a non-trivial $\breve {a}$ -successor of the last tile on $\pi '$ . In either case, $\varphi _n'$ is of the form ${\langle {a}\rangle } \beta $ where $\mathsf {u}(\beta ) = \alpha $ . In case $(i)$ , we must have some $\alpha ' \in \Psi ^+$ with $\alpha ' \preceq _{\mathcal {O}(\Psi )} \beta $ by definition of an ${a}$ -successor, and the inductive invariant is maintained. In case $(ii)$ , denote the last tile on $\pi '$ by $\Theta '$ . Clearly, this means that there must be some index $k < n$ for which $\pi _k = \pi '$ , so let k be the largest such index. If all ordinal variables of $\beta $ are active in $\Theta '$ then pick $\alpha '$ to be some formula in $(\Theta ')^+$ with $\alpha ' \preceq _{\mathcal {O}(\Theta ')} \beta $ , which exists by Proposition 5.22. If some ordinal variable of $\beta $ is non-active in $\Theta '$ then let x be the highest ranking variable with $\mathsf{o}_{\beta }(x) \notin \mathrm {Act}(\Theta ')$ . If it does not hold that $\mathsf{o}_{\beta } \prec ^x_{\mathcal {O}(\Theta _n)} \mathsf{o}_{\varphi _k^{\prime }}$ then let the substitution $\tau $ be as in the proof of Proposition 5.24. Then we pick $\varphi _{n+1}^{\prime }$ so that $\varphi _{n+1}^{\prime } \preceq _{\mathcal {O}(\Theta _n)} \beta [\tau ]$ as provided in the same proof. Finally, if it holds that $\mathsf{o}_{\beta } \prec ^x_{\mathcal {O}(\Theta _n)} \mathsf{o}_{\varphi _k^{\prime }}$ then pick $\varphi _{n+1}^{\prime }$ so that $\mathsf{o}_{\varphi _{n+1}^{\prime }} \prec ^y_{\mathcal {O}(\Theta ')} \mathsf{o}_{\varphi _k^{\prime }}$ for some y higher ranking or equal to x, as provided by Proposition 5.24.

Case $\varphi _n$ is of the form $\nu x \alpha $ . Then the unique next position in any extension of this play is $(\pi _n,\alpha [\nu x\alpha /x])$ . The formula $\varphi _n^{\prime } \in \Theta _n^+$ is $\nu x^{\kappa }\beta $ for some $\kappa $ and some $\beta $ with $\mathsf {u}(\beta ) = \alpha $ . By the definition of a tile there is some $\kappa _0$ such that $\kappa _0 <_{\mathcal {O}(\Theta _n)} \kappa $ and there is some formula $\gamma \in \Theta _n^+$ such that $\gamma \preceq _{\mathcal {O}(\Theta _n)} \beta [\nu x^{\kappa _0}\beta /x]$ . Since clearly $\mathsf {u}(\gamma ) = \mathsf {u}(\beta [\nu x^{\kappa _0}\beta /x]) = \alpha [\nu x.\alpha /x]$ , the invariant is maintained.

Case $\varphi _n$ is of the form $\mu x \alpha $ . Then the unique next position in any extension of this play is $(\pi _n,\alpha [\mu x\alpha /x])$ . The formula $\varphi _n^{\prime } \in \Theta _n$ is $\mu x\beta $ for some $\beta $ with $\mathsf {u}(\beta ) = \alpha $ . By the definition of a tile we have $\gamma \preceq _{\mathcal {O}_n} \beta [\mu x \beta /x]$ for some $\gamma \in \Theta _n$ . Since clearly $\mathsf {u}(\gamma ) = \mathsf {u}(\beta [\mu x \beta /x]) = \alpha [\mu x\alpha /x]$ , the invariant is maintained.

We now show that $\sigma '$ is indeed a winning strategy for Falsifier. First we show that every full finite $\sigma '$ -guided play is won by Falsifier. The last position of such a play must take one of the following forms: $(i) \ (\pi ,p)$ for some propositional variable p with $\pi \in V^{\sigma }(p)$ , $(ii) \ (\pi ,\overline {p})$ for some propositional variable p with $\pi \notin V^{\sigma }(p)$ , or $(iii) \ (\pi ,[{a}] \varphi )$ with $\pi $ not having an ${a}$ -successor.

Now the latter case cannot occur—this is a more or less direct consequence of our construction of the relation $R^{\sigma }_{a}$ , based on Refuter’s winning strategy $\sigma $ in the mosaic game. In the other two cases we reason as follows, denoting the last tile on $\pi $ by $\Theta $ . If the last position of the play is $(\pi ,p)$ and $\pi \in V^{\sigma }(p)$ then $\overline {p} \in \Theta $ by definition of $V^{\sigma }$ . But $p \in \Theta $ by the invariant of $\sigma '$ -guided plays, so we get an instance of excluded middle which contradicts the definition of a non-trivial tile. On the other hand, if the last position is $(\pi ,\overline {p})$ and $\pi \notin V^{\sigma }(p)$ then $\overline {p} \notin \Theta $ by definition. This contradicts the invariant of $\sigma '$ -guided plays, which says that $\overline {p} \in \Theta $ . So in each case the assumption that the finite full play is lost by Falsifier leads to a contradiction, and we have established that Falsifier wins every full finite $\sigma $ -guided play.

In the remainder of the proof we will argue that every infinite $\sigma '$ -guided play is won by Falsifier as well. Let $(\pi _i,\varphi _i)_{i < \omega }$ be an infinite $\sigma '$ -guided play, and assume for a contradiction that this play is lost by Falsifier. As an immediate consequence of the following claim (cf. our discussion of the evaluation game in Section 2.3), this means that the highest ranking variable that is unfolded infinitely many times in the play is a $\nu $ -variable.

Claim 8. Let $(\varphi _i)_{i<\omega }$ be an infinite trace starting from $\varphi _0 = \rho $ , and let $\eta x\, \psi $ be its most significant formula. Then for any other formula $\lambda z\, \chi $ that occurs infinitely often on this trace, we have $x<_{\rho } z$ , i.e., x ranks higher than z in the subsumption order of $\rho $ .

Proof of Claim (sketch)

While the statement of the claim is rather intuitive, the details of its proof are quite tedious. Define the relation $\sqsubseteq _C$ on the fixpoint formulas in the set $\mathrm {Clos}(\rho )$ by putting $\alpha \sqsubseteq _C \beta $ if there is a finite trace from $\alpha $ to $\beta $ such that $\alpha $ is a subformula of every formula on the trace. It then follows from the assumptions of the claim that the formula $\eta x\, \psi $ is $\sqsubseteq _C$ -minimal among all fixpoint formulas appearing on the trace $(\varphi _i)_{i<\omega }$ . Now consider Kozen’s expansion map $\texttt {exp}$ from $\mathit {Sfor}(\rho )$ to $\mathrm {Clos}(\rho )$ [13]; the key observation is that for any two bound variables $x,y \in \mathrm {Var}(\rho )$ we have that $x <_{\rho } y$ iff $\texttt {exp}(x) \sqsubset _C \texttt {exp}(y)$ .

To contradict the assumption that $\sigma $ was a winning strategy for Refuter, we shall now construct an infinite $\sigma $ -guided play containing an infinite progressing chain of ordinal variables, which is therefore won by Prover.

We denote the last sequent on each partial play $\pi _i$ by $\Theta _i$ , and we denote $\mathcal {O}(\Theta _i)$ by $\mathcal {O}_i$ . Consider the infinite sequence of “shadow formulas” $(\varphi _i^{\prime })_{i<\omega }$ . Given a fixpoint variable x, say that the index i is a progress point for x if $\pi _i$ is an initial segment of $\pi _{i+1}$ and $\mathsf {o}_{\varphi _{i+1}^{\prime }}(x) \neq \mathsf {o}_{\varphi _{i}^{\prime }}(x)$ . We refer to the highest ranking $\nu $ -variable that has infinitely many progress points on $(\varphi _i^{\prime })_{i<\omega }$ as the dominant variable of the sequence and denote it by Z. Note that at least one $\nu $ -variable has infinitely many progress points, since by clause (6) in the construction of the shadow formulas $\varphi _i^{\prime }$ , every index at which a $\nu $ -variable is unfolded on the play $(\pi _i,\varphi _i)_{i < \omega }$ must be a progress point either for that variable or some higher ranking variable, and since there is a $\nu $ -variable unfolded infinitely many times in the play $(\pi _i,\varphi _i)_{i < \omega }$ .

Claim 9. There is an index $k < \omega $ such that:

• • $\pi _k$ is an initial segment of $\pi _m$ for all $m> k$ ,

• • no higher ranking $\nu $ -variable than Z has any progress point after k,

• • no higher ranking variable than Z is unfolded at any point after k.

Proof of Claim

Let $k_0$ be some index for which no higher ranking $\nu $ -variable than Z has any progress points after $k_0$ , and no higher ranking fixpoint variable than Z is unfolded after $k_0$ . Such an index exists by definition of Z (and since Z must be higher ranking or equal to the highest ranking variable that is unfolded infinitely many times on $(\pi _i,\varphi _i)_{i < \omega }$ , since that variable is a $\nu $ -variable by assumption and has infinitely many progress points). Now consider the set of $\sigma $ -guided partial plays of the form $\pi _m$ with $m \geq k_0$ . It is clear that this set is downwards directed with respect to the initial segment order, so we find a shortest $\sigma $ -guided play $\pi '$ belonging to this set. We set k to be the smallest index $\geq k_0$ for which $\pi _k = \pi '$ .

We assume that $k = 0$ in the previous claim, since otherwise we can just re-index the play $(\pi _i,\varphi _i)_{i < \omega }$ . For each index i we let $\xi _i$ denote the ordinal variable $\mathsf {o}_{\varphi _i^{\prime }}(Z)$ .

Claim 10. Suppose that $i \leq j < \omega $ are indices such that $\pi _i = \pi _k = \pi _j$ for all $i \leq k \leq j$ . If Z has a progress point k with $i \leq k < j$ then $\xi _j \prec _{\mathcal {O}_j} \xi _i$ , and otherwise $\xi _j = \xi _i$ .

Proof of Claim

This is proved by induction on the difference $j - i$ , the case for $j - i = 0$ being trivial. For the induction step, supposing that the induction hypothesis holds for $j - i$ , consider the index $j + 1$ . It suffices to prove that $\xi _{j+1} \preceq _{\mathcal {O}_j} \xi _j$ ; it then follows that $\xi _{j+1} \prec _{\mathcal {O}_j} \xi _j$ if j is a progress point. We have to consider several cases for the shape of $\varphi _j$ and $\varphi _{j+1}$ . Note that by our assumption that $\pi _i = \pi _j = \pi _{j+1}$ , $\varphi _j$ cannot be of the form $[a] \psi $ or ${\langle {a}\rangle } \psi $ .

Case $\varphi _j$ is of the form $\alpha \wedge \beta $ and $\varphi _{j+1}$ is either $\alpha $ or $\beta $ . Say $\varphi _{j+1} = \alpha $ . Then the shadow formula $\varphi _j^{\prime }$ is of the form $\alpha ' \wedge \beta '$ where $\mathsf {u}(\alpha ') = \alpha $ and $\mathsf {u}(\beta ') = \beta $ , and $\varphi _{j+1}^{\prime } \preceq _{\mathcal {O}_j} \alpha '$ . By assumption no variable ranking higher than Z has a progress point at j, so we get

$$ \begin{align*} \mathsf{o}_{\varphi_{j+1}^{\prime}}(Z) & \preceq_{\mathcal{O}_{j+1}} \mathsf{o}_{\alpha'}(Z) \\ & = \mathsf{o}_{\alpha' \wedge \beta'}(Z) \\ & = \mathsf{o}_{\varphi_{j}^{\prime}}(Z). \end{align*} $$

Hence $\xi _{j+1} \preceq _{\mathcal {O}_{j+1}} \xi _j$ as required.

Case $\varphi _j$ is of the form $\alpha \vee \beta $ . This is similar to the previous case.

Case $\varphi _n$ is of the form $\nu x \alpha $ . Then the formula $\varphi _j^{\prime }$ is $\nu x^{\kappa }\beta $ for some $\kappa $ and some $\beta $ with $\mathsf {u}(\beta ) = \alpha $ . Then there is some $\kappa _0$ such that $\varphi _{j+1}^{\prime } \preceq _{\mathcal {O}_j} \beta [\nu x^{\kappa _0}\beta /x]$ . Since no variable ranking higher than Z has a progress point at j, we get

$$ \begin{align*} \mathsf{o}_{\varphi_{j+1}^{\prime}}(Z) & \preceq_{\mathcal{O}_{j+1}} \mathsf{o}_{\beta[\nu x^{\kappa_0} \beta/x]}(Z) \\ & \preceq_{\mathcal{O}_{j+1}} \mathsf{o}_{\nu x^{\kappa} \beta}(Z) \\ & = \mathsf{o}_{\varphi_{j}^{\prime}}(Z). \end{align*} $$

Hence $\xi _{j+1} \preceq _{\mathcal {O}_{j+1}} \xi _j$ as required.

Case $\varphi _n$ is of the form $\mu x \alpha $ . This is similar to the previous case.

Claim 11. Suppose that $i \leq j < \omega $ are indices such that for all $i \leq k < j$ , $\pi _k$ is an initial segment of $\pi _{k + 1}$ . If Z has a progress point k with $i \leq k < j$ then $\xi _j \prec _{\mathcal {O}_j} \xi _i$ , and otherwise $\xi _j = \xi _i$ .

Proof of Claim

This is proved by induction on the difference $j - i$ , in the same manner as Claim 10. The case for $j - i = 0$ is trivial, and for the induction step we show that $\xi _{j+1} \preceq _{\mathcal {O}_j} \xi _j$ . The only difference is that we now have to consider the cases where $\varphi _j$ is of the form $[a]\psi $ or ${\langle {a}\rangle } \psi $ . We focus on the latter case since they are treated in the same way: if $\varphi _j = {\langle {a}\rangle } \psi $ then $\varphi _j^{\prime }$ is of the form ${\langle {a}\rangle }\psi '$ where $\mathsf {u}(\psi ') = \psi $ . Furthermore, since we assumed that $\pi _j$ is an initial segment of $\pi _{j+1}$ , the last tile on $\pi _{j+1}$ must be an ${a}$ -successor of the last tile on $\pi _j$ , and $\varphi _{j+1}^{\prime } \preceq _{\mathcal {O}_{j+1}} \psi '$ . Hence we get

$$ \begin{align*} \mathsf{o}_{\varphi_{j+1}^{\prime}}(Z) & \preceq_{\mathcal{O}_{j+1}} \mathsf{o}_{\psi'}(Z) \\ & = \mathsf{o}_{{\langle{a}\rangle}\psi'}(Z) \\ & = \mathsf{o}_{\varphi_{j}^{\prime}}(Z). \end{align*} $$

So $\xi _{j+1} \preceq _{\mathcal {O}_{j+1}} \xi _j$ as required.

Claim 12. Suppose that $i \leq j < \omega $ are indices such that $\pi _i = \pi _j$ and $\pi _i$ is an initial segment of $\pi _k$ for all $i < k < j$ . If Z has a progress point k with $i \leq k < j$ then $\xi _j \prec _{\mathcal {O}_j} \xi _i$ , and otherwise $\xi _j \preceq _{\mathcal {O}_j} \xi _i$ .

Proof of Claim

We prove this by induction on the difference $j - i$ . If $j - i = 0$ then $i = j$ and so $\xi _i = \xi _j$ . Now suppose $j - i> 0$ , and suppose the statement holds for all $i' \leq j'$ with $j' - i' < j - i$ . If $\pi _i = \pi _k$ for all $i \leq k \leq j$ then the statement follows directly from Claim 10. Otherwise, it is clear that we can find indices $i',j'$ such that $i < i' \leq j' < j$ , $\pi _{i'} = \pi _{j'}$ , $\pi _i = \pi _{i'-1}$ , $\pi _j = \pi _{j'+1}$ , $\Theta _{i'} = \Theta _{j'}$ is a non-trivial ${a}$ -successor of $\Theta _i$ for some ${a}$ , and the partial play $(\pi _i,\varphi _i)\cdots(\pi _j,\varphi _j)$ has the shape

$$ \begin{align*}(\pi,\varphi_i)\cdots(\pi,\varphi_{i'-1}) (\pi\cdot \Theta,\varphi_{i'})\cdots(\pi\cdot \Theta,\varphi_{j'})(\pi,\varphi_{j'+1})\cdots(\pi,\varphi_j), \end{align*} $$

where $\pi = \pi _i = \pi _{i'-1} = \pi _{j' + 1} = \pi _j$ , and $\Theta = \Theta _{i'} = \Theta _{j'}$ .

We shall prove the following statements:

1. 1. If Z has a progress point m with $i \leq m < i'-1$ then $\xi _{i'-1} \prec _{\mathcal {O}_{i'-1}} \xi _i$ and otherwise $\xi _{i' -1} \preceq _{\mathcal {O}_{i'-1}} \xi _i$ .

2. 2. If Z has a progress point m with $j'+1 \leq m < j$ then $\xi _{j} \prec _{\mathcal {O}_{j}} \xi _{j'+1}$ and otherwise $\xi _{j} \preceq _{\mathcal {O}_{j}} \xi _{j'+1}$

3. 3. If Z has a progress point m with $i' \leq m < j'$ then $\xi _{j'} \prec _{\mathcal {O}_{j'}} \xi _{i'}$ and otherwise $\xi _{j'} \preceq _{\mathcal {O}_{j'}} \xi _{i'}$ .

4. 4. If $i'-1$ is a progress point for Z then $\xi _{i'} \prec _{\mathcal {O}_{i'}} \xi _{i' - 1}$ , and otherwise $\xi _{i'} \preceq _{\mathcal {O}_{i'}} \xi _{i' - 1}$ .

5. 5. If $\xi _{j'} \prec _{\mathcal {O}_{j'}} \xi _{i'-1}$ then $\xi _{j'+1} \prec _{\mathcal {O}_{j'+1}} \xi _{i'-1}$ .

6. 6. If $\xi _{j'} \preceq _{\mathcal {O}_{j'}} \xi _{i'-1}$ then $\xi _{j'+1} \preceq _{\mathcal {O}_{j'+1}} \xi _{i'-1}$ .

Items (1)–(3) are immediate from the induction hypothesis.

For the proof of item (4), first suppose that $i'-1$ is a progress point for Z; then $\xi _{i'} \prec _{\mathcal {O}_{i'}} \xi _{i' - 1}$ by Claim 11 applied to the indices $i'-1,i'$ , so that we are done. On the other hand, if $i'-1$ is not a progress point for Z, we reason as follows. First note that $\varphi _{i'-1}^{\prime }$ must be of the form $[a] \psi $ or ${\langle {a}\rangle } \psi $ for some formula $\psi $ such that either $\varphi _{i'}^{\prime } = \psi $ or $\varphi _{i'}^{\prime } \prec _{\mathcal {O}_{i'}} \psi $ . If $\psi = \varphi _{i'}^{\prime }$ then (with $\bigcirc \in \{[a] ,{\langle {a}\rangle }\}$ ):

$$\begin{align*}\xi_{i'} = \mathsf{o}_{\varphi_{i'}^{\prime}}(Z) = \mathsf{o}_{\psi}(Z) = \mathsf{o}_{\bigcirc \psi}(Z) = \mathsf{o}_{\varphi_{i'-1}^{\prime}}(Z) = \xi_{i'-1}. \end{align*}$$

Finally, if $\varphi _{i'}^{\prime } \prec _{\mathcal {O}_{i'}} \psi $ , then there is some fixpoint variable y such that $\mathsf {o}_{\varphi _{i'}^{\prime }}(y) \prec _{\mathcal {O}_{i'}} \mathsf {o}_{\psi }(y)$ and $\mathsf {o}_{\varphi _{i'}^{\prime }}(z) = \mathsf {o}_{\psi }(z)$ for all z ranking higher than y. But then $i'-1$ is a progress point for y; hence, by our choice of Z, the variable Z is higher ranking than y. Hence $\mathsf {o}_{\varphi _{i'}^{\prime }}(Z) = \mathsf {o}_{\psi }(Z)$ , and by the same reasoning as above we can show that $\mathsf {o}_{\psi }(Z) = \mathsf {o}_{\varphi _{i'-1}^{\prime }}(Z)$ . Hence $\mathsf {o}_{\varphi _{i'}^{\prime }}(Z) = \mathsf {o}_{\varphi _{i'-1}^{\prime }}(Z)$ as required.

For the proof of item (5), suppose $\xi _{j'} \prec _{\mathcal {O}_{j'}} \xi _{i'-1}$ . We recall that $\Theta _{j'+1} = \Theta _{i'-1}$ , so $\xi _{i'-1}$ is an active variable of $\Theta _{j'+1}$ , and $\Theta _{j'}$ is a non-trivial ${a}$ -successor of $\Theta _{j'+1}$ . By our assumption on Z being the highest ranking fixpoint variable with any progress points, this means that $\mathsf{o}_{\varphi _{j'}^{\prime }} \prec ^Z_{\mathcal {O}_{j'}} \mathsf{o}_{\varphi _{i'-1}^{\prime }}$ ; hence, $\mathsf{o}_{\varphi _{j'+1}^{\prime }} \prec ^{y}_{\mathcal {O}_{j'}} \mathsf{o}_{\varphi _{i'-1}^{\prime }}$ for some y higher ranking or equal to Z. But then $y = Z$ , again by our assumption that Z is the highest ranking variable with any progress points. In other words we have $\mathsf{o}_{\varphi _{j'+1}^{\prime }}(Z) \prec _{\mathcal {O}_{j'+1}} \mathsf{o}_{\varphi _{i'-1}^{\prime }}(Z)$ , i.e., $\xi _{j'+1} \prec _{\mathcal {O}_{j'+1}} \xi _{i'-1},$ as required.

For the proof of item (6) suppose $\xi _{j'} = \xi _{i'-1}$ . Then $\xi _{j'}$ is an active variable of $\Theta _{i'-1} = \Theta _{j'+1}$ . Write $\varphi _{j'}^{\prime } = {\langle {a}\rangle }\psi '$ . If all variables in $\psi ' $ are active in $\Theta _{j'+1}$ then $\varphi _{j'+1}^{\prime } \preceq _{\mathcal {O}_{j'+1}} \psi '$ , and since Z was the highest ranking variable with any progress point it follows that

$$ \begin{align*} \xi_{j'+1} & = \mathsf{o}_{\varphi_{j'+1}^{\prime}}(Z) \\ & \preceq_{\mathcal{O}_{j'+1}} \mathsf{o}_{\psi'}(Z) \\ & = \xi_{j'} \\ & = \xi_{i'-1} \end{align*} $$

as required. On the other hand if some variable $\mathsf{o}_{\psi '}(y)$ of $\psi '$ is not active in $\Theta _{j'+1} = \Theta _{i'-1}$ then either $\varphi _{j'+1}^{\prime } \preceq _{\mathcal {O}_{j'+1}} \psi '[\tau ]$ for some substitution $\tau $ that is the identity on all active variables of $\Theta _{j'+1}$ , including $\xi _{i'-1}$ , or $\mathsf{o}_{\varphi _{j'+1}^{\prime }} \prec ^y_{\mathcal {O}_{j'+1}} \mathsf{o}_{\varphi _{i'-1}^{\prime }}$ for some fixpoint variable y. Since Z was the highest ranking variable with any progress point, in either case we get $\mathsf{o}_{\varphi _{j'+1}^{\prime }}(Z) \preceq _{\mathcal {O}_{j'+1}} \mathsf{o}_{\psi '}(Z)$ and therefore $\xi _{j'+1} \preceq _{\mathcal {O}_{j'+1}} \xi _{i'-1}$ as before.

We now proceed to finish the proof of the claim using items (1)–(6). If Z has a progress point m with $i'-1 \leq m < j'$ then either $m = i'-1$ or $i' \leq m < j$ . So combining items (3) and (4):

1. 7. If Z has a progress point m with $i'-1 \leq m < j'$ , then $\xi _{j'} \prec _{\mathcal {O}_{j'}} \xi _{i'-1}$ , and otherwise $\xi _{j'} \preceq _{\mathcal {O}_{j'}} \xi _{i'-1}$ .

Combining items (5)–(7), we immediately obtain:

1. 8. If Z has a progress point m with $i'-1 \leq m < j'$ , then $\xi _{j'+1} \prec _{\mathcal {O}_{j'+1}} \xi _{i'-1}$ , and otherwise $\xi _{j'+1} \preceq _{\mathcal {O}_{j'+1}} \xi _{i'-1}$ .

The index $j'$ cannot be a progress point for Z since $\pi _j^{\prime }$ is not an initial segment of $\pi _{j'+1}$ . So if Z has a progress point m with $i' -1 \leq m < j$ , then either $i'-1 \leq m < j'$ or $j'+1 \leq m < j$ . So combining items (8) and (2):

1. 9. If Z has a progress point m with $i'-1 \leq m < j$ , then $\xi _{j} \prec _{\mathcal {O}_{j}} \xi _{i'-1}$ , and otherwise $\xi _{j} \preceq _{\mathcal {O}_{j}} \xi _{i'-1}$ .

Finally, if Z has a progress point m with $i \leq m < j$ , then either $i \leq m < i'-1$ or $i'-1 \leq m < j$ . So combining items (9) and (1), we have:

1. 10. If Z has a progress point m with $i \leq m < j$ , then $\xi _{j} \prec _{\mathcal {O}_{j}} \xi _{i}$ , and otherwise $\xi _{j} \preceq _{\mathcal {O}_{j}} \xi _{i}$ .

But item (10) is the conclusion we aimed to prove, so the proof is finished.

Claim 13. Let $N \subseteq \omega $ be a set of indices such that $\pi _i = \pi _j$ for all $i \in N$ . Then N is finite.

Proof of Claim

Say that a play $\pi '$ of the mosaic game is visited infinitely many times if the set $N = \{i < \omega \mid \pi _i = \pi '\}$ is infinite. We want to show that no $\pi '$ is visited infinitely many times.

It is easy to see that the set of plays $\pi '$ of the mosaic game that are visited infinitely many times is downwards directed with respect to the initial segment ordering. Assume for contradiction that this set is non-empty then it contains some $\pi '$ that is visited infinitely many times, and for any $\pi "$ that is visited infinitely many times, $\pi '$ is an initial segment of $\pi "$ . Hence for some $k < \omega $ , $\pi '$ is an initial segment of $\pi _m$ for all $m \geq k$ . Furthermore, by the pigeonhole principle there is a formula $\psi $ such that $(\pi _m,\varphi _m) = (\pi ',\psi )$ for infinitely many $m < \omega $ . Consequently there must be infinitely many $k_0,k_1,k_2, ... < \omega $ for which $(\pi _{k_i},\varphi _{k_i}) = (\pi ',\psi )$ , $\pi '$ is an initial segment of $\pi _m$ for $k_i \leq m \leq k_{i+1}$ , and Z has a progress point m with $k_i \leq m < k_{i+1}$ . But then, it follows immediately from Claim 12 that for each $k_i$ , we have $\xi _{k_{i+1}} \prec _{\mathcal {O}} \xi _{k_i}$ , where $\mathcal {O}$ is the constraint of the last sequent on $\pi '$ . Hence we find an infinite set of distinct ordinal variables in the same tile, which is impossible since the constraint of a sequent is always finite.

Claim 14. There is a (unique) infinite $\sigma $ -guided play $\pi _{\infty }$ and a sequence $S = (l_i,r_i)_{i < K}$ of pairs of indices (where $K \leq \omega $ ), such that the following conditions hold for each $i< K$ :

• • $l_i < r_i$ , and $r_i < l_{i + 1}$ (if $i+1 < K$ ).

• • $\pi _{l_i} = \pi _{r_i} \sqsubseteq \pi _{\infty }$ .

• • $\pi _{l_i} \sqsubseteq \pi _m$ for each m with $l_i \leq m \leq r_i$ .

• • $\pi _m \sqsubseteq \pi _{m + 1}$ , for all m with $r_i \leq m < l_{i + 1}$ (if $i+1 < K$ ).

Furthermore, if $K < \omega $ then

• • $\pi _m \sqsubseteq \pi _{m + 1}$ and $\pi _m \sqsubset \pi _{\infty }$ , for all $m \geq r_{K-1}$ .

We can view the play $\pi _{\infty }$ as a limit of the partial plays $(\pi _i)_{i < \omega }$ in the mosaic game appearing in the infinite play $(\pi _i,\varphi _i)_{i < \omega }$ in the evaluation game, not in the sense that $\pi _i \sqsubseteq \pi _{\infty }$ for all $i < \omega $ , but for infinitely many $i<\omega $ . Intuitively, Claim 14 says that the infinite play $(\pi _i,\varphi _i)_{i < \omega }$ looks as displayed in Figure 4. The dotted arrow shows how the play $(\pi _i,\varphi _i)_{i < \omega }$ traverses the tree of $\sigma $ -guided plays, and the shaded branch to the left shows the infinite $\sigma $ -guided play $\pi _{\infty }$ .

Figure 4 The play $\pi _{\infty }$ of Claim 14.

Proof of Claim

We begin by showing that there is an infinite $\sigma $ -guided play $\pi _{\infty }$ such that every finite initial segment of $\pi _{\infty }$ is equal to $\pi _i$ for some $i < \omega $ . Consider the set $\Pi $ of partial $\sigma $ -guided plays $\pi '$ such that every finite initial segment of $\pi '$ is equal to $\pi _i$ for some $i < \omega $ . This set is clearly downwards closed under the initial segment order, so it forms a finitely branching tree in which $\pi "$ is considered as a child of $\pi '$ iff it is a minimal partial play in $\Pi $ of which $\pi '$ is a proper initial segment. Thus, by König’s lemma it suffices to prove that this tree is infinite. But clearly, $\pi _i$ belongs to $\Pi $ for every $i < \omega $ . So if the set $\Pi $ were finite, by the pigeonhole principle it would have to contain some member $\pi '$ which is equal to $\pi _i$ for infinitely many $i < \omega $ , and this contradicts Claim 13.

We now show that the play $\pi _{\infty }$ must satisfy the constraints listed in the claim. We define, by induction on the length of an initial segment $\pi '$ of $\pi _{\infty }$ , a set $S(\pi ')$ of pairs of indices as follows. Suppose that $\pi '$ is an initial segment of $\pi _{\infty }$ and that $S(\pi ")$ has been defined for all proper initial segments $\pi "$ of $\pi '$ . Let $S'$ be the union of all $S'(\pi ")$ for $\pi "$ a proper initial segment of $\pi '$ . We define $S(\pi ')$ by a case distinction. If there are no two distinct indices $i < j < \omega $ for which $\pi ' = \pi _i = \pi _j$ , then we set $S(\pi ') = S'$ . Otherwise, let l be the smallest index such that $\pi ' = \pi _l$ , and let r be the greatest index for which $\pi ' = \pi _r$ . The latter must exist by Claim 13. Then $l < r$ . We set $S(\pi ) = S' \cup \{(l,r)\}$ .

With this construction in place, we set S to be the union of all $S(\pi ')$ where $\pi '$ is an initial segment of $\pi _{\infty }$ . It is not hard to see that the constraints of the claim are met with this definition of S.

We now show that the $\sigma $ -guided play $\pi _{\infty }$ is lost by Refuter, which gives a contradiction. As a consequence of Claim 12, for every $i < K$ we have $\xi _{r_i} \prec _{\mathcal {O}_{r_i}} \xi _{l_i}$ if Z has a progress point m with $l_i \leq m < r_i$ , and $\xi _{r_i} = \xi _{l_i}$ otherwise. Furthermore, by Claim 11, it follows that for each i with $i + 1 < K$ we have $\xi _{l_{i+1}} \prec _{\mathcal {O}_{l_{i+1}}} \xi _{r_i}$ if Z has a progress point m with $r_i \leq m < l_{i+1}$ , and $\xi _{l_{i+1}} = \xi _{r_i}$ otherwise. Also by Claim 11, if K is finite then for each m with $m \geq r_{K-1}$ , if m is a progress point for Z then $\xi _{m+1} \prec _{\mathcal {O}_{m+1}} \xi _m$ , and $\xi _{m+1} = \xi _m$ otherwise.

Putting these observations together, since Z has infinitely many progress points by assumption, there must be a strictly increasing sequence of indices $i_0,i_1,i_2, ...$ such that $\pi _{i_j} \sqsubseteq \pi _{\infty }$ and $\xi _{i_{j+1}} \prec _{\mathcal {O}_{i_{j+1}}} \xi _{i_j}$ for each $j < \omega $ . Hence $\pi _{\infty }$ is lost by Refuter, contradicting the assumption that $\sigma $ was a winning strategy for Refuter. We can now conclude that Falsifier wins every $\sigma '$ -guided infinite play.

Theorem 5.28. If $\rho $ is valid then it has a slim proof.

Proof If $\rho $ is valid, then by Proposition 5.27, Refuter does not have a winning strategy in the mosaic game for $\rho $ , so that by Proposition 5.25, it is Prover who has a winning strategy. It then follows by Proposition 5.26 that $\rho $ is provable.

6 From slim proofs to cyclic proofs

With completeness for slim proofs in place, we proceed to show that the existence of a slim proof for root formula $\rho $ implies that there also exists a (finite) cyclic proof of that formula. In other words, we want a procedure to transform a given slim proof into a cyclic proof. It will be convenient to split this transformation into two steps, first introducing an infinitary analogue of cyclic proofs that will be called infinitely reset proofs, and then showing how such an infinite proof can be pruned into a finite proof tree which, with suitable back edges added, forms a cyclic proof.

6.1 Infinitely reset proofs

We first define the notion of an infinitely reset proof.

Definition 6.1. An infinite proof tree $\Pi $ for root formula $\rho $ is said to be infinitely reset if, for every infinite branch $\beta $ on $\Pi $ , there is some ordinal variable $\kappa $ that appears non-active in every sequent in some final segment of $\beta $ , and is reset infinitely many times on $\beta $ .

We want to show that a slim proof can be transformed into an infinitely reset proof containing only finitely many sequents. In order to do that, we have to tame the growth of constraints in the proof tree using the constraint weakening rule, and inserting instances of the reset rule when possible. In order for this to work we have to keep track of which ordinal variables we want to keep in order to possibly be reset later, and which ones we want to simply throw away. The following definition captures this distinction:

Definition 6.2. Let $\mathcal {O} : \Gamma $ be a sequent and $\kappa $ an ordinal variable in $\mathcal {O}$ . Then $\kappa $ is said to be redundant if it is non-active and all of its descendants are non-active.

We are now ready to state and prove the result.

Proposition 6.3. If $\rho $ has a slim proof then it has an infinitely reset proof in which only finitely many distinct sequents appear.

Proof Let $\Pi $ be a slim proof of $\rho $ . We construct an infinite proof tree $\Pi '$ together with a map $f : \Pi ' \to \Pi $ as the union of finite approximants $\Pi ^{\prime }_i$ and $f_i$ , for $i < \omega $ , defined as follows. First, we set $\Pi ^{\prime }_0$ to consist of a single vertex, labelled with the end sequent of $\Pi $ , and we let $f_0$ map this single vertex to the root of $\Pi $ . Now suppose the approximants $\Pi ^{\prime }_i$ and $f_i$ have been defined, so that for every vertex v of $\Pi ^{\prime }_i$ labelled $\mathcal {O}_v : \Gamma _v$ , the label of $f_i(v)$ is of the form $\mathcal {O}_{f_i(v)} : \Gamma _{f_i(v)}$ where $\Gamma _v = \Gamma _{f_i(v)}$ and $\mathcal {O}_{v} = \mathcal {O}_{f_i(v)}\setminus V$ for some set V of non-active variables of $\mathcal {O}_{f_i(v)}$ . We construct $\Pi ^{\prime }_{i+1}$ and $f_{i+1}$ by doing the following for each non-axiom leaf v of $\Pi ^{\prime }_i$ :

• • If the constraint of v contains redundant ordinal variables, make v the conclusion to an application of left weakening that removes all these redundant variables and let $f_{i+1}$ map the new premiss to $f_i(v)$ .

• • If the constraint of v contains no redundant ordinal variables but there is an instance of the reset rule with conclusion matching v, make v the conclusion to such an instance of reset and let $f_{i+1}$ map the new premiss to $f_i(v)$ .

• • If neither of the two previous cases apply, then make v the conclusion of the same rule instance as $f_i(v)$ and let $f_{i+1}$ map each new premiss w to the corresponding premiss of $f_i(v)$ .

Note that the last case of this construction can be carried out thanks to the assumption that $\Pi $ was a slim proof. In particular, we are relying here on the restriction on the cut rule, $\mu (\kappa )$ or $\exists $ , that all ordinal variables occurring free in the cut formula or minor formula of the rule application are active variables in the conclusion. For example, suppose $f_i(v)$ is the conclusion to an instance of the $\exists $ -rule of the form:

By assumption the constraint of v is of the form $\mathcal {O}\setminus V$ for some set of non-active variables V of $\mathcal {O}$ . The constraint on applications of the $\exists $ -rule in slim proofs ensures that $\lambda $ is active in $\Gamma _v$ and thus cannot belong to V. Hence $\lambda $ belongs to $\mathcal {O}\setminus V$ and we can safely make v the conclusion to the corresponding rule instance:

We claim that the limit $\Pi '$ obtained from this construction is an infinitely reset proof.

Claim 15. Let $\mathcal {O} : \Gamma $ be a sequent such that $\mathcal {O}$ contains at most n active variables, and suppose $\mathcal {O}$ contains a chain $\kappa _0,...,\kappa _{2n+1}$ of $2n+2$ different ordinal variables such that $\kappa _{2n+1} <_{\mathcal {O}} \cdots <_{\mathcal {O}} \kappa _0$ . Then there is an instance of the reset rule with conclusion $\mathcal {O} : \Gamma $ in which one of the variables $\kappa _0,...,\kappa _{2n+1}$ is reset.

Proof of Claim 15

Since the length of the chain is $2n+2$ it contains a chain of $n+2$ different non-active variables. Clearly, as these variables are all part of a chain, at least $n+1$ of these non-active variables have a non-empty set of children. Finally, as the sets of children of two different variables are disjoint, at most n of these variables can have an active child. So the chain must contain at least one non-active variable $\kappa $ with a non-empty set of children, all of which are non-active. This variable can be reset.

Claim 16. Let $\beta = \Gamma _0\Gamma _1\Gamma _2\cdots$ be an infinite branch of $\Pi '$ with corresponding sequence of constraints $\mathcal {O}_0\mathcal {O}_1\mathcal {O}_2\cdots$ and let $f[\beta ]$ be the corresponding branch of $\Pi $ . If $f[\beta ]$ has an infinite descending chain $\kappa _0,\kappa _1,\kappa _2...$ of ordinal variables, then there is an index $k < \omega $ and variable $\lambda $ in $\mathcal {O}_k$ such that:

1. 1. $\lambda $ belongs to $\mathcal {O}_i$ for all $i \geq k$ , and

2. 2. $\lambda $ is reset infinitely many times on $\beta $ .

Proof of Claim 16

We write $f[\beta ] = \Gamma _0^f\Gamma _1^f\Gamma _2^f\cdots$ and let $\mathcal {O}_0^f\mathcal {O}_1^f\mathcal {O}_2^f\cdots$ denote the corresponding sequence of constraints. We assume that $\kappa _0$ occurs in $\mathcal {O}^f_0$ since otherwise we can just drop the prefix of the sequence before the first occurrence of $\kappa _0$ and re-index. For each $i < \omega $ we denote by $g(i)$ the highest index such that $\kappa _{g(i)}$ appears in $\mathcal {O}_i^f$ . Note that $\kappa _{g(i)}$ must be active in $\Gamma ^f_i$ , since there must be some descendant $\Gamma ^f_j$ with $j> i$ that is the conclusion to either a $\nu $ -rule or $\forall $ -rule in which $\kappa _{g(i)}$ occurs in the principal formula. So $\kappa _{g(i)}$ is active in $\Gamma ^f_j$ and hence, because $\Pi $ is a slim proof, in $\Gamma ^f_i$ . Note that g is monotone in the sense that $i \leq j$ implies $g(i) \leq g(j)$ , since there are no applications of left weakening in $\Pi $ .

For each $i < \omega $ we denote by $S_i$ the set of variables $\lambda $ in $\mathcal {O}_i$ that fulfil the following two properties.

Stability: No proper ancestor of $\lambda $ is reset in any constraint $\mathcal {O}_j$ with $j \geq i$ .

Ancestry: $\kappa _{g(i)} <_{\mathcal {O}_i} \lambda $ .

We note that $S_i$ is non-empty for all sufficiently large i, since eventually $\kappa _{g(i)}$ must have at least one proper ancestor, and the $<_{\mathcal {O}_i}$ -largest ancestor of $\kappa _{g(i)}$ must satisfy Stability since it has no proper ancestors. Note that if $\lambda \in S_i$ then the Ancestor condition entails that $\kappa _{g(j)} <_{\mathcal {O}_j} \lambda $ for all $j \geq i$ such that $\lambda $ belongs to $\mathcal {O}_j$ . Together with the Stability condition this entails that $\lambda \in S_i$ belongs to $\mathcal {O}_j$ for all $j \geq i$ , since an ancestor of $\kappa _{g(j)}$ is never redundant and hence can only be removed by resetting its parent.

Now pick an index $i_0$ for which $S_{i_0}$ is non-empty, and pick $\lambda _0 \in S_{i_0}$ . Since, by Stability, $\lambda _0$ belongs to $\mathcal {O}_j$ for all $j \geq i_0$ , we are done if $\lambda _0$ is reset infinitely many times. Otherwise, there is some $k> i_0$ such that $\lambda _0$ is never reset in any constraint $\mathcal {O}_j$ for $j \geq k$ . Let $i_1$ be the first index after k such that $\lambda _0$ has a child in $\mathcal {O}_{i_1}$ which is an ancestor of $\kappa _{g(i_1)}$ ; such an index obviously exists since $\kappa _0\kappa _1\kappa _2\cdots$ is an infinite descending chain. We let $\lambda _1$ denote this child of $\lambda _0$ in $\mathcal {O}_{i_1}$ . Since $\lambda _0$ is never reset after $i_1$ , $\lambda _1$ satisfies the Stability and Ancestor conditions with respect to the index $i_1$ . Now repeat the same argument; eventually, we must find a variable that belongs to $\mathcal {O}_j$ for all sufficiently large j and is reset infinitely many times. For, suppose not; then, let m be the maximum number of active variables that can appear in any constraint in $\Pi '$ . By repeating the previous argument sufficiently many times we eventually find a chain of $2m+2$ variables $\lambda _{2m+1},...,\lambda _0$ such that $\lambda _{2m+1} <_{\mathcal {O}_{i_{2m+1}}} \dots <_{\mathcal {O}_{i_{2m+1}}} \lambda _0$ , none of which can be reset. This contradicts Claim 15, so the proof is done.

It follows immediately from Claim 16 that the proof tree $\Pi '$ has the desired property, that on every infinite branch there is some variable that eventually appears in every constraint and is reset infinitely many times. Furthermore, whenever the number of non-active variables in the constraint exceeds a certain bound, then since the number of active variables is bounded either there are redundant variables (that are immediately removed by left weakening) or there is a sufficiently long chain of variables so that the reset rule can be applied (by Claim 15). It follows that the proof tree $\Pi '$ has only finitely many sequents up to renaming of ordinal variables. So by suitably renaming ordinal variables, we can produce an infinitely reset proof $\Pi "$ in which only finitely many sequents appear.

6.2 Completeness of cyclic proofs

We are now ready for the final step of the completeness proof, showing that any infinitely reset proof containing finitely many sequents can be folded to a cyclic proof. We recall that a cyclic proof tree is a finite proof tree together with a back edge for each non-axiom leaf l, the target of which is called the companion of the leaf, such that the label of each non-axiom leaf l is identical with the label of its companion. Furthermore, such a cyclic proof tree is a valid cyclic proof if for every non-axiom leaf l there is some ordinal variable $\kappa _l$ such that $\kappa _l$ belongs to the constraint of every vertex on the path from the companion of l to l, and is reset at least once on this path.

Proposition 6.4. Let $\Pi $ be an infinite reset proof for the formula $\rho $ , and assume that only finitely many distinct sequents appear in $\Pi $ . Then $\rho $ has a cyclic proof.

Proof Let $\Pi $ and $\rho $ be as in the formulation of the proposition.

Consider an arbitrary infinite branch $\beta $ of $\Pi $ . Since $\Pi $ is an infinite reset proof, we may associate an ordinal variable $\kappa _{\beta }$ with $\beta $ which appears non-active in every sequent in some final segment of $\beta $ and is reset infinitely often in $\beta $ . But then by the pigeonhole principle it follows from the additional assumption on $\Pi $ that $\beta $ contains two nodes, $c_{\beta }$ and $l_{\beta }$ , labelled with the same sequent, and such that $l_{\beta }$ is a (proper) descendant of $c_{\beta }$ , the variable $\kappa _{\beta }$ is a non-active element of the constraint of every sequent on the path from $c_{\beta }$ to $l_{\beta }$ , and $\kappa _{\beta }$ is reset at least once on this path.

Now we prune the underlying tree of $\Pi $ as follows. Let L be the set of first repeats of $\Pi $ , that is, those nodes of the form $l_{\beta }$ for some infinite branch $\beta $ that do not have a proper ancestor of the form $l_{\alpha }$ for some other infinite branch $\alpha $ . Define $\Pi _L$ as the proof tree we obtain by pruning all descendants of nodes in L; in other words, the leaves of $\Pi _L$ are either axiomatic or elements of L.

The key observation is that $\Pi _L$ is finite. To see this, suppose otherwise, then by König’s lemma $\Pi _L$ contains an infinite branch $\beta $ . By construction $\beta $ must be an infinite branch of $\Pi $ as well, so that we may consider the node $l_{\beta }$ . Since $l_{\beta }$ belongs to $\Pi _L$ , it cannot have a proper ancestor in L. It follows that $l_{\beta }$ itself must be a first repeat and thus belongs to L. But then $\Pi _L$ cannot contain any descendant of $l_{\beta }$ , which contradicts the assumption that $\beta $ is an infinite branch in $\Pi _L$ .

We claim that in fact $\Pi _L$ is a cyclic proof for $\rho $ . For this purpose we need to define a companion map on $\Pi _L$ , so consider an arbitrary non-axiomatic leaf l of $\Pi _L$ . By construction we may fix some infinite branch $\beta $ of $\Pi $ such that $l = l_{\beta }$ . Now define the companion of l to be the node $c_{\beta }$ . It is then straightforward to verify that with this companion map, $\Pi _L$ is indeed a cyclic proof for $\rho $ .

Putting our results together, we now obtain:

Proposition 6.5. If a plain formula $\rho $ is valid, then it has a cyclic proof.

Proof Let $\rho $ be valid, then it has a slim proof by Theorem 5.28. As a direct consequence of Proposition 6.3 and Proposition 6.4 we may conclude that $\rho $ has a cyclic proof as well.

Finally, Theorem 3.10 now follows immediately from Proposition 4.3 and Proposition 6.5.

7 Conclusion

We have presented a sound and complete cyclic proof system for the two-way $\mu $ -calculus. The defining feature of the system is the use of ordinal variables for detecting successful branches and ordinal quantifiers for handling the effect of two-way traces. The sequent calculus builds on two strong and successful formalisms for modal $\mu $ -calculus: explicit ordinal approximants [5, 17, 18] and name signatures [12, 19].

The proof system we introduced is suitable for effective proof search, as our completeness proof shows that cuts can be restricted to a small set of formulas. However, our completeness proof relies on saturation techniques that make it difficult to calculate a bound on the size of proofs for valid formulas. We leave open whether the proof system can be used to obtain an optimal decision procedure for the two-way $\mu $ -calculus, matching the exponential time bound obtained by Vardi [21].

One can view the move from modal $\mu $ -calculus to two-way $\mu $ -calculus as a first step towards finitary proof systems for guarded fragments of first-order fixed point logic [3, 4, 9]. The cyclic calculus of the present paper is subsumed in the cyclic proof system for the first-order $\mu $ -calculus of [1]. Looking forward, we thus hope that insights from the present work can yield complete systems for larger (guarded) fragments of the first-order $\mu $ -calculus.

There is an apparent connection between two-way $\mu $ -calculus and model-checking infinite-state processes. It is well known that the two-way $\mu $ -calculus lacks the finite model property, although any satisfiable formula has a model that can be represented as a regular tree [21]. But even a regular tree model is in general infinite-state from the perspective of the two-way $\mu $ -calculus, as the appropriate notion of bisimulation will distinguish infinitely many states, all satisfying different formulas in the language. A calculus for model-checking context-free infinite-state processes was proposed by Schöpp and Simpson [16] which is similar to our own in the way it builds on [5]. As an example of an infinite-state process, Schöpp and Simpson consider a context-free system that represents a transition system with two actions converse to each other.

To date, there is no known complete Hilbert-style axiomatisation of the two-way $\mu $ -calculus. Indeed, the only sound and complete proof systems are the $\omega $ -branching well-founded proofs of [2] and the cyclic proofs of this article. An obvious question is whether either system sheds light on a Hilbert axiomatisation. One can also ask how the two proof systems are related. Aside from the difference in language (ordinals are external to the logical language in [2]), the crucial use of cut in the present work is a non-trivial hurdle in any comparison. As noted, we leave open whether our calculi are complete in the absence of cut.