Proof. The proof is by the same argument as Palka’s proof of cut elimination for $\mathbf {ACT}_{\omega }$ [Reference Palka26, Theorem 3.1]. (Thus, it is simpler than the argument from [Reference Kuznetsov and Speranski21, Theorem 4.2] for cut elimination in ${!} \mathbf {ACT}_{\omega }$ , where a form of Mix rule was used; here it is unnecessary.)

In order to eliminate one cut (either $(\mathrm {Cut})_{\mathrm {d}1}$ or $(\mathrm {Cut})_{\mathrm {d}2}$ ), we suppose that its premises already have cut-free derivations and prove that then the conclusion also has one. (Once we know how to eliminate one cut, a standard transfinite induction argument shows that any derivable sequent is cut-free derivable.) We proceed by triple induction on the following parameters: (1) the complexity $|A|$ of the formula being cut (complexity is computed in the usual way, as the total number of variable, constant, and connective occurrences); (2) the rank of the right premise of cut; (3) the rank of the left premise of cut. In (2) and (3), ranks are computed w.r.t. the cut-free immediate derivability operator. As usual, we consider possible cases on the lowermost rules in the derivation of premises of cut.

The new interesting cases are those involving the rules $({!}L)_{\mathrm {d}}$ , $({!}R)_{\mathrm {d}}$ , and $(A)_{\mathrm {d}}$ . Other rules are considered exactly as in Palka’s proof [Reference Palka26, Theorem 3.1]. Moreover, the cases where one of these lowermost rules is non-principal, i.e., does not operate the formula A or B being cut, are also trivial: cut can be propagated upwards, reducing induction parameter (2) or (3). Notice that such propagation is possible for both $(\mathrm {Cut})_{\mathrm {d}1}$ and $(\mathrm {Cut})_{\mathrm {d}2}$ . (The latter was not considered by Palka, but the proof transformations are exactly the same.)

Thus, the interesting cases are those where both lowermost rules are principal and are not covered in Palka’s proof. That is, we have the following two cases.

Case 1: The formula being cut is ${!}A$ , introduced by $({!}R)_{\mathrm {d}}$ on the left and $({!}L)_{\mathrm {d}}$ on the right. The cut rule in this case is $(\mathrm {Cut})_{\mathrm {d}1}$ .

This is transformed into an application of $(\mathrm {Cut})_{\mathrm {d}2}$ with a smaller parameter (1): A has less complexity than ${!}A$ .

Case 2: The left premise is derived by $({\mathbin {\backslash }}R)_{\mathrm {d}}$ introducing the formula $B = (b_1 \cdot \ldots \cdot b_n) \mathbin {\backslash } (c_1 \cdot \ldots \cdot c_m)$ , and the lowermost rule in the derivation of the right premise is $(A)_{\mathrm {d}}$ which uses ${!}B$ in the ${!}$ -zone. The cut rule here is $(\mathrm {Cut})_{\mathrm {d}2}$ , and this is the only principal case for this cut rule. (In all other cases it just gets propagated, as noticed above. For the axiom, the contents of the ${!}$ -zone does not matter, so $(\mathrm {Cut})_{\mathrm {d}2}$ which removes something from it can be just ignored.)

The derivation in Case 2 ends as follows (the interesting case is ${!}B \notin {!}\Xi $ ):

This gets reconstructed in the following way. Consider the following two derivations (recall that a double line means several applications of a rule):

(If $m = 0$ or $n = 0$ , we use rules for $1$ instead of the ones for product.)

In the first derivation, $(\mathrm {Cut})_{\mathrm {d}1}$ is applied to $b_1 \cdot \ldots \cdot b_n$ , which has strictly smaller complexity than B. Thus, parameter (1) got reduced, and by induction hypothesis ${!}\Xi; b_1, \ldots , b_n \Rightarrow c_1 \cdot \ldots \cdot c_m$ is cut-free derivable.

In the second derivation, $(\mathrm {Cut})_{\mathrm {d}2}$ is applied with the same parameter (1) and a smaller parameter (2): the rank of the right premise got decreased by 1. By induction hypothesis, ${!}\Xi; \Gamma , c_1, \ldots , c_m, \Delta \Rightarrow C$ is cut-free derivable, and therefore so is ${!}\Xi; \Gamma , c_1 \cdot \ldots \cdot c_m, \Delta \Rightarrow C$ .

Finally, we combine the two d-sequents using $(\mathrm {Cut})_{\mathrm {d}1}$ :

This instance of cut has a smaller parameter (1), and by induction hypothesis the goal d-sequent is cut-free derivable.

Proof. Let us take the derivation of ${!}\Xi; \Gamma \Rightarrow C$ and add ${!}\Xi '$ to the $!$ -zone of each sequent. This results in a valid derivation of ${!}\Xi \cup {!}\Xi '; \Gamma \Rightarrow C$ .

Proof. First, we show that the d-sequent $\{{!}A\}; {}\Rightarrow A$ is derivable for any formula A of the form $(b_1 \cdot \ldots \cdot b_n) \mathbin {\backslash } (c_1 \cdot \ldots \cdot c_m)$ :

(For $n=1$ or $m=1$ , the corresponding product rules get replaced with rules for 1.)

Now we derive ${!}\Xi \cup \{ {!}A \}; \Gamma , \Delta \Rightarrow C$ from ${!}\Xi; \Gamma , {!}A, \Delta \Rightarrow C$ :

The derivation can be made cut-free by Proposition 3.1.

Proof. For the “if” direction, we prove a stronger statement: if a d-sequent ${!}\Xi; \Pi \Rightarrow C$ is derivable in ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ , then the sequent ${!}\Xi , \Pi \Rightarrow C$ is derivable in ${!} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ . In the latter ${!}\Xi $ stands for the sequence of all formulae contained in ${!}\Xi $ , in an arbitrary order. The proof is straightforward transfinite induction on the derivation (we may suppose, due to cut elimination, that this derivation is cut-free). The interesting cases are, of course, $({!}L)_{\mathrm {d}}$ , $({!}R)_{\mathrm {d}}$ , and $(A)_{\mathrm {d}}$ . These are translated into ${!} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ as follows. For $({!}L)_{\mathrm {d}}$ we have

(putting ${!}A$ to some place inside ${!}\Xi $ ; here and further ${!}\Xi _1, {!}\Xi _2 = {!}\Xi $ ). The rule $({!}R)_{\mathrm {d}}$ translates exactly into $({!}R)$ .

Finally, for $(A)_{\mathrm {d}}$ with $B = ((b_1 \cdot \ldots \cdot b_n) \mathbin {\backslash } (c_1 \cdot \ldots \cdot c_m))$ we construct the following derivation (with 1 instead of product, if n or m is zero):

Other rules are translated straightforwardly, adding (where needed) permutation rules to move ${!}\Xi $ , and contraction rules to merge two or several copies of ${!}\Xi $ into one. For the axioms, if the ${!}$ -zone is non-empty, it is added using the weakening rule ${!}W$ .

The “only if” direction is also proved by transfinite induction on derivation. However, here we shall essentially use cut in the ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ derivation being constructed. Fortunately, we have cut elimination (Proposition 3.1), so in the end we can get rid of cuts.

Again, axioms and all rules not operating ${!}$ are translated “as is,” the ${!}$ -zones being empty. The interesting rules are $({!}L)$ , $({!}R)$ , $({!}P_{1,2})$ , $({!}C)$ , and $({!}W)$ . Modelling of these rules is quite straightforward, given the handy admissible rules $(W)_{\mathrm {d}}$ and $({!}L)_{\mathrm {d}}^{\mathrm {inv}}$ (admissibility established above).

For $({!}L)$ , we have

Derivability of $\{{!}A\}; \Rightarrow A$ was established in the proof of Lemma 3.3.

For $({!}R)$ , we have

For $({!}P_1)$ and $({!}P_2)$ , we have

Finally, for $({!}W)$ and $({!}C)$ we have the following:

In the derivation modelling $({!}C)$ , the upper instance of $({!}L)_{\mathrm {d}}^{\mathrm {inv}}$ is applied with ${!}\Xi = \varnothing $ and the lower one is applied with ${!}\Xi = \{ {!}A \}$ , having $\{ {!}A \} \cup \{ {!}A \} = \{ {!}A \}$ .

Proof. One can examine Definition 4.4 and verify that any rule of $\mathtt {S} = \mathtt {S}_{l,r,e}(\mathtt {M})$ applied to a string of the form $l w_1 a q w_2 r$ (where $q\ne q^{(a)}$ and $w_1,w_2 \in C^\ast $ ) corresponds to a computation step of $\mathtt {M}$ . Assume that one reaches an accepting configuration $l \lambda ^m q^{(a)} w \lambda ^n r$ (where $w \in B^\ast $ ). Then the only possible derivation ending by a string with the suffix e looks as follows:

$$ \begin{align*} &l \lambda^m q^{(a)} w \lambda^n r \ \Rightarrow^\ast_{\mathtt{S}} \ l q^{(a)} w \lambda^n r \ \Rightarrow_{\mathtt{S}}\ l l^\prime q^{(a)} w \lambda^n r \\ &\Rightarrow^\ast_{\mathtt{S}} \ l w l^\prime q^{(a)} \lambda^n r \ \Rightarrow^\ast_{\mathtt{S}}\ l w l^\prime q^{(a)} r \ \Rightarrow_{\mathtt{S}} \ l w e. \end{align*} $$

So, indeed, if a string of the form $ve$ is obtained from $luq^{(0)} r$ , then $v=lw$ where w is the output of $\mathtt {M}$ on the input u.

Proof. The “only if” direction is trivial because each rule of $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ is a particular case of some rule of ${!} \mathbf {ACT}_{\omega }$ or is a composition of those. For example, the rule $({\mathbin {\&}} L_i)_{\mathrm {bsc}}$ is a composition of the rules $({\mathbin {\&}} L_i)$ and $(\mathbin {\backslash } L)$ . The rule $(A)_{\mathrm {bsc}}$ maps exactly onto $(A)_{\mathrm {d}}$ .

To prove the “if” direction, first of all, let us switch from the calculus ${!} \mathbf {ACT}_{\omega }$ to the dyadic calculus ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ . By Proposition 3.4 and Lemma 3.3, if ${!}\Upsilon _{\mathcal {H}}, \Pi \Rightarrow C$ is derivable in ${!} \mathbf {ACT}_{\omega }$ , then ${!}\Upsilon _{\mathcal {H}}; \Pi \Rightarrow C$ is derivable in ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ . Take some derivation of ${!}\Upsilon _{\mathcal {H}}; \Pi \Rightarrow C$ in ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ ; we proceed with proving that then $\Pi \Rightarrow C$ is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ by transfinite induction on the size of the given derivation (which is defined standardly by transfinite recursion). As for the base case, if ${!}\Upsilon _{\mathcal {H}}; \Pi \Rightarrow C$ is an axiom of ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ , then $\Pi = C$ . It is straightforward to verify that the sequents $r \Rightarrow r$ , $r_1 \cdot r_2 \Rightarrow r_1 \cdot r_2$ , $r^* \Rightarrow r^*$ are derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ .

To prove the induction step, consider the last rule application in the derivation of ${!}\Upsilon _{\mathcal {H}}; \Pi \Rightarrow C$ in ${!} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ . Clearly, if it is that of $({\cdot } L)_{\mathrm {d}}$ , $({}^* L_\omega )_{\mathrm {d}}$ , or $(A)_{\mathrm {d}}$ , then one simply applies the induction hypothesis to its premises and then applies the corresponding rule of $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ thus obtaining a correct derivation in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . In particular, the rules $(A)_{\mathrm {d}}$ and $(A)_{\mathrm {bsc}}$ correspond to each other as they affect a sequent in the same way. Thus it is interesting to consider only the rules $({\mathbin {\backslash }} L)_{\mathrm {d}}$ , $({\cdot } R)_{\mathrm {d}}$ , $({\mathbin {\&}} L_i)_{\mathrm {d}}$ , and $({}^* R_n)_{\mathrm {d}}$ (any other rule of ${!}_{\mathrm {d}} \mathbf {ACT}_{\omega }^{\mathrm {m}}$ cannot be the last one in the derivation of ${!}\Upsilon _{\mathcal {H}}; \Pi \Rightarrow C$ because neither $\Pi $ nor C contains ${!}$ , $\mathbin {/}$ , $\oplus $ , $0$ , $1$ ).

Case $({\mathbin {\backslash }} L)_{\mathrm {d}}:$

If a formula of the form $A \mathbin {\backslash } B$ belongs to $\mathrm {SFm}$ , then either $A=p$ or $A = p^*$ where p is a variable (see Definition 4.8). In the first case, let us apply the induction hypothesis to the premises and conclude that $\Pi \Rightarrow p$ and $\Gamma , B, \Delta \Rightarrow C$ are derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ , i.e., $p \vdash _{\mathrm {bsc}} \Pi $ and $\Pi _0 \vdash _{\mathrm {bsc}} \Gamma , B, \Delta $ where $\Pi _0 \Rightarrow C$ is an axiom of $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . Therefore, $\Pi _0 \vdash _{\mathrm {bsc}} \Gamma , B, \Delta \vdash _{\mathrm {bsc}} \Gamma , p, p \mathbin {\backslash } B, \Delta \vdash _{\mathrm {bsc}} \Gamma , \Pi , p \mathbin {\backslash } B, \Delta $ ; thus $\Gamma , \Pi , p \mathbin {\backslash } B, \Delta \Rightarrow C$ is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ as desired. In the case $A = p^*$ , the reasonings are similar, the only difference is that $p^n \vdash _{\mathrm {bsc}} \Pi $ for some n.

Case $({\cdot } R)_{\mathrm {d}}:$

Similarly to the previous case, one applies the induction hypothesis to the premises and obtains that $r_1 \vdash _{\mathrm {bsc}} \Gamma $ , $r_2 \vdash _{\mathrm {bsc}} \Delta $ . Thus, $r_1, r_2 \vdash _{\mathrm {bsc}} \Gamma , r_2 \vdash _{\mathrm {bsc}} \Gamma , \Delta $ and hence $\Gamma , \Delta \Rightarrow r_1 \cdot r_2$ is derivable from the axiom $r_1,r_2 \Rightarrow r_1 \cdot r_2$ .

Case $({}^* R_n)_{\mathrm {d}}:$

The argument is similar; namely, using the induction hypothesis one concludes that $r \vdash _{\mathrm {bsc}} \Pi _i$ for $i=1,\ldots , n$ and hence $r^n \vdash _{\mathrm {bsc}} \Pi _1, r^{n-1} \vdash _{\mathrm {bsc}} \ldots \vdash _{\mathrm {bsc}} \Pi _1, \ldots , \Pi _n$ . Since $r^n \Rightarrow r^\ast $ is an axiom of $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ , the sequent $\Pi _1, \ldots , \Pi _n \Rightarrow r^\ast $ is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ .

Case $({\mathbin {\&}} L_i)_{\mathrm {d}}:$

(Note that any formula $B_1 \mathbin {\&} B_2 \in \mathrm {SFm}$ is of the form $\left ( r_1 \mathbin {\backslash } A_1 \right ) \mathbin {\&} \left ( r_2 \mathbin {\backslash } A_2 \right )$ for some variables $r_1,r_2$ .) By the induction hypothesis, there is a derivation of $\Gamma , r_i \mathbin {\backslash } A_i, \Delta \Rightarrow C$ in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . Then, one reasons as follows. Given some fixed derivation of $\Gamma , r_i \mathbin {\backslash } A_i, \Delta \Rightarrow C$ in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ , find all the occurrences of the formula $r_i \mathbin {\backslash } A_i$ and replace them by $\left ( r_1 \mathbin {\backslash } A_1 \right ) \mathbin {\&} \left ( r_2 \mathbin {\backslash } A_2 \right )$ . Then, each application of $({\mathbin {\backslash }} L)_{\mathrm {bsc}}$ that introduces $r_i \mathbin {\backslash } A_i$ turns into an application of $({\mathbin {\&}} L_i)_{\mathrm {bsc}}$ that introduces $\left ( r_1 \mathbin {\backslash } A_1 \right ) \mathbin {\&} \left ( r_2 \mathbin {\backslash } A_2 \right )$ . These arguments can be formalised easily by means of induction.

Proof. Let us prove the first statement. The “if” direction is straightforward because $\Gamma , p \mathbin {\backslash } A, \Delta \Rightarrow C$ can be obtained from $\Gamma ^\prime , A, \Delta \Rightarrow C$ by an application of $(\mathbin {\backslash } L)_{\mathrm {bsc}}$ followed by a series of applications of $(A)_{\mathrm {bsc}}$ that correspond to the derivation $\Gamma \Rightarrow _{\mathtt {S}}^\ast \Gamma ^\prime \, p$ .

The “only if” direction is proved by induction on the size of a derivation of $\Gamma , p \mathbin {\backslash } A, \Delta \Rightarrow C$ in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . The last rule applied in it is either $({\mathbin {\backslash }} L)_{\mathrm {bsc}}$ or $(A)_{\mathrm {bsc}}$ . In the first case, $\Gamma = \Gamma ^\prime , p$ , and the rule application looks as follows:

The statement of the corollary follows. In the second case, $\Gamma = \Gamma _1, b_1, \ldots , b_n, \Gamma _2$ and the rule looks as follows:

By the induction hypothesis, there is $\Gamma ^\prime $ such that $\Gamma _1, c_1, \ldots , c_m, \Gamma _2 \Rightarrow _{\mathtt {S}}^\ast \Gamma ^\prime \, p$ and $\Gamma ^\prime , A, \Delta \Rightarrow C$ is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . It remains to observe that $\Gamma = \Gamma _1,b_1,\ldots , b_n , \Gamma _2 \Rightarrow _{\mathtt {S}} \Gamma _1, c_1, \ldots , c_m, \Gamma _2 \Rightarrow _{\mathtt {S}}^\ast \Gamma ^\prime \, p$ .

The second statement is proved in the same way. Notice that no rewriting rule of $\mathtt {S}$ contains $\mathit {ok}$ , so $\mathit {ok}$ cannot appear to the left from $\mathrm {Ok} \mathbin {\&} (p \mathbin {\backslash } A)$ .

Proof. Recall that $\mathrm {Ok} = \mathit {ok} \mathbin {\backslash } \mathit {ok}$ . Then the sequent can be derived in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ from the axiom $\mathit {lt} , \mathit {ok} \Rightarrow \mathit {lt} \cdot \mathit {ok}$ by n applications of $({\mathbin {\&}} L_1)_{\mathrm {bsc}}$ .

Proof of Lemma 4.9.

The proof is by transfinite induction on $\gamma := \omega ^{k_1}+\cdots +\omega ^{k_M}$ (if $M=0$ , then $\gamma := 0$ ). According to Lemma 4.10, the sequent (1) is derivable in ${!} \mathbf {ACT}_{\omega }$ if and only if the following sequent is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ :

(2) $$ \begin{align} \mathit{lt}, p_{1}^{x}, p_{\mathsf{Q}}, \mathit{en}, \mathrm{En}(k_M), \ldots, \mathrm{En}(k_1), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok.} \end{align} $$

The base case: $\gamma = 0$ . Then, (2) is of the form $\mathit {lt}, p_{1}^{x}, p_{\mathsf {Q}}, \mathit {en}, \mathrm {Brk} \Rightarrow \mathit {lt} \cdot \mathit {ok}$ . This sequent is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ ; below, we present a derivation for $\mathsf {Q} = \exists $ :

This agrees with the statement of Lemma 4.9. Indeed, since it cannot be the case that $0 = \gamma> \alpha $ for any ordinal $\alpha $ , the first statement of the lemma holds trivially. The second one holds as well because the sequent is derivable independently of x.

The inductive step: assume that $\gamma> 0$ (or equivalently, that $M> 0$ ).

Case 1: $k_M> 0$ . Recall that $\mathrm {En}(k_M) := \mathrm {Ok} \mathbin {\&} \mathit {en} \mathbin {\backslash } (\mathit {en} \cdot \mathrm {En}(k_M-1)^\ast )$ . Then, any derivation of (2) in the calculus $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ must end as follows:

(3)

The fact that there are no other ways to derive (2) is verified straightforwardly by considering all possible ways to apply rules of $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . In particular, there is no way to apply the rule $(A)_{\mathrm {bsc}}$ at any of the above steps because this is possible only if there is a variable from $Q_0 \cup Q_1 \cup \{\mathit {ex}\}$ in the left-hand side of a sequent.

Now, we can apply the induction hypothesis to the sequent

(4) $$ \begin{align} \mathit{lt}, p_{1}^{x}, p_{\mathsf{Q}}, \mathit{en} , \mathrm{En}(k_M-1)^{l}, \mathrm{En}(k_{M-1}), \ldots, \mathrm{En}(k_1), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align} $$

for each l. Indeed, the parameter $\gamma _l := \omega ^{k_1}+\cdots +\omega ^{k_{M-1}}+\omega ^{k_M-1}\cdot l$ of this sequent is less than $\gamma $ . By the induction hypothesis, if (4) is derivable and $\gamma _l> \alpha $ , then $x \in \mathbf {T}$ , and, conversely, if $x \in \mathbf {T}$ , then (4) is derivable.

Given this, let us prove both statements of the lemma for the sequent (2). Assume that (2) is derivable and $\gamma> \alpha $ . Then (4) is derivable for each $l \in \omega $ (since this sequent occurs in the only possible derivation (3)). Since $\gamma> \alpha $ and $\gamma = \sup _{l \in \omega } \gamma _l$ , then $\gamma _l> \alpha $ for some $l \in \omega $ . Therefore, by the induction hypothesis, $x \in \mathbf {T}$ , as desired. Conversely, let $x \in \mathbf {T}$ . Then, (4) is derivable for each $l \in \omega $ and hence so is (2), as the derivation (3) shows.

Case 2: $k_M = 0$ . Recall that $\mathrm {En}(0) := \mathrm {Ok} \mathbin {\&} \mathit {en} \mathbin {\backslash } \left ( \left ( p_{\exists } \mathbin {\backslash } \mathrm {En}_{\exists } \right ) \mathbin {\&} \left ( p_{\forall } \mathbin {\backslash } \mathrm {En}_{\forall } \right ) \right )$ . Let us denote the sequence of formulae $\mathrm {En}(k_{M-1}), \ldots , \mathrm {En}(k_1), \mathrm {Brk}$ by $\Xi $ . Any derivation of (2) must end as follows:

Here $i=1$ if $\mathsf {Q}=\exists $ and $i=2$ if $\mathsf {Q} = \forall $ .

Case 2a: $\mathsf {Q} = \exists $ . Recall that $\mathrm {En}_{\exists } = \mathit {go} \cdot \mathrm {Cmp}\left (q^{(0)}_0,h_0\right ) \cdot \left (\mathrm {Ok} \mathbin {\&} \mathit {go} \mathbin {\backslash } \mathit {ex} \right ) \cdot \left (\mathrm {Ok} \mathbin {\&} \mathrm {Cmp}\left (q^{(0)}_1, h_{\exists }\right ) \right )$ . Then, by Corollary 2.5, $\mathit {lt}, p_{1}^{x}, \mathrm {En}_{\exists }, \Xi \Rightarrow \mathit {lt} \cdot \mathit {ok}$ is derivable if and only if so is

$$\begin{align*}\mathit{lt}, p_{1}^{x}, \mathit{go}, \mathrm{Cmp}\left(q^{(0)}_0,h_0\right), \mathrm{Ok} \mathbin{\&} \mathit{go} \mathbin{\backslash} \mathit{ex}, \mathrm{Ok} \mathbin{\&} \mathrm{Cmp}\left(q^{(0)}_1, h_{\exists}\right), \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok}. \end{align*}$$

Recall that $\mathrm {Cmp}\left (q^{(0)}_0,h_0\right ) = \mathit {go} \mathbin {\backslash } \left ( q^{(0)}_0 \cdot \mathit {rt} \cdot \mathit {fn} \mathbin {\backslash } \left ( \left ( p_{1} \mathbin {\backslash } h_0(p_{1}) \right ) \mathbin {\&} \left ( p_{2} \mathbin {\backslash } h_0(p_{2}) \right ) \right ) \right )$ . The only way to derive the latter sequent in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ is by means of the following application of $({\mathbin {\backslash }} L)_{\mathrm {bsc}}$ :

Again, by Corollary 2.5, the premise is equiderivable with the sequent

(5) $$ \begin{align} \mathit{lt}, p_{1}^{x}, q^{(0)}_0 , \mathit{rt} , \mathit{fn} \mathbin{\backslash} \left( p_{1} \mathbin{\backslash} h_0(p_{1}) \mathbin{\&} p_{2} \mathbin{\backslash} h_0(p_{2}) \right), \Xi^\prime \Rightarrow \mathit{lt} \cdot \mathit{ok}, \end{align} $$

where $\Xi ^\prime = \mathrm {Ok} \mathbin {\&} \mathit {go} \mathbin {\backslash } \mathit {ex}, \mathrm {Ok} \mathbin {\&} \mathrm {Cmp}\left (q^{(0)}_1, h_{\exists }\right ), \Xi $ . The sequent (5) cannot be obtained by any rule application except for that of $(A)_{\mathrm {bsc}}$ . By Corollary 4.11, it is derivable if and only if $\mathit {lt}\, p_{1}^{x}\, q^{(0)}_0 \, \mathit {rt} \Rightarrow _{\mathtt {S}}^\ast \Gamma ^\prime \, \mathit {fn}$ for $\Gamma ^\prime $ such that $\Gamma ^\prime , p_{1} \mathbin {\backslash } h_0(p_{1}) \mathbin {\&} p_{2} \mathbin {\backslash } h_0(p_{2}), \Xi ^\prime \Rightarrow \mathit {lt} \cdot \mathit {ok}$ is derivable. Note that, if $\mathit {lt}\, p_{1}^{x}\, q^{(0)}_0 \, \mathit {rt} \Rightarrow _{\mathtt {S}}^\ast \Gamma ^\prime \, \mathit {fn}$ , then $\mathit {lt}\, p_{1}^{x}\, q^{(0)}_0 \, \mathit {rt} \Rightarrow _{\mathtt {S}_0}^\ast \Gamma ^\prime \, \mathit {fn}$ because the initial string contains a state from $Q_0$ but it contains neither states from $Q_1$ nor $\mathit {ex}$ . This property is preserved by any rule application of $\mathtt {S}$ , so, in the derivation $\mathit {lt}\, p_{1}^{x}\, q^{(0)}_0 \, \mathit {rt} \Rightarrow _{\mathtt {S}}^\ast \Gamma ^\prime \, \mathit {fn}$ , only rules from $\mathtt {S}_0$ can be used. Now, it is time to recall some properties of $\mathtt {S}_0 = \mathtt {S}_{\mathit {lt},\mathit {rt},\mathit {fn}}\left (\mathtt {M}_0 \right )$ . By Proposition 4.5, $\mathit {lt}\, p_{1}^{x}\, q^{(0)}_0 \, \mathit {rt} \Rightarrow _{\mathtt {S}_0}^\ast \Gamma ^\prime \, \mathit {fn}$ holds if and only if $\Gamma ^\prime = \mathit {lt} \, \mathfrak {f}_{0}(p_{1}^{x})$ . Therefore, (5) is derivable if and only if so is

(6) $$ \begin{align} \mathit{lt} , \mathfrak{f}_{0}(p_{1}^{x}), p_{1} \mathbin{\backslash} h_0(p_{1}) \mathbin{\&} p_{2} \mathbin{\backslash} h_0(p_{2}), \Xi^\prime \Rightarrow \mathit{lt} \cdot \mathit{ok}. \end{align} $$

Note that $\mathfrak {f}_{0}\left (p_{1}^{x}\right )$ ends with either $p_{1}$ or $p_{2}$ ; let us write $\mathfrak {f}_{0}\left (p_{1}^{x}\right ) = \Delta \, p_i$ . The sequent (6) does not contain symbols from $Q_0 \cup Q_1 \cup \{\mathit {ex}\}$ , so it cannot be obtained by $(A)_{\mathrm {bsc}}$ ; hence it can only be obtained by $({\mathbin {\&}} L_i)_{\mathrm {bsc}}$ as follows:

Let us consider two subcases.

Subcase i. $\mathfrak {f}_{0}\left (p_{1}^{x}\right ) = p_{1}$ . This happens, according to Definition 4.6, if and only if $\alpha = 0$ (recall that $x = \langle \varepsilon , \sharp \alpha , e \rangle $ ) and $x \in \mathbf {T}$ . Since $h_0(p_1)=\mathit {ok}$ , the sequent $\mathit {lt} , \Delta , h_0(p_{1}), \Xi ^\prime \Rightarrow \mathit {lt} \cdot \mathit {ok}$ equals $\mathit {lt} , \mathit {ok}, \mathrm {Ok} \mathbin {\&} \mathit {go} \mathbin {\backslash } \mathit {ex}, \mathrm {Ok} \mathbin {\&} \mathrm {Cmp}\left (q^{(0)}_1, h_{\exists }\right ), \Xi \Rightarrow \mathit {lt} \cdot \mathit {ok}$ and is derivable by Lemma 4.12.

Subcase ii. $\mathfrak {f}_{0}\left (p_{1}^{x}\right ) = p_{1}^{x} p_{2}$ . This happens if and only if $\alpha> 0$ . The sequent $\mathit {lt} , \Delta , h_0(p_{2}), \Xi ^\prime \Rightarrow \mathit {lt} \cdot \mathit {ok}$ equals

(7) $$ \begin{align} \mathit{lt}, p_{1}^{x}, \mathit{go}, \mathrm{Ok} \mathbin{\&} \mathit{go} \mathbin{\backslash} \mathit{ex}, \mathrm{Ok} \mathbin{\&} \mathrm{Cmp}\left(q^{(0)}_1, h_{\exists}\right), \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok}. \end{align} $$

Concluding the arguments above, if $\alpha = 0$ , then the sequent (2) we started with is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ if and only if $x \in \mathbf {T}$ . If $\alpha> 0$ , then derivability of (2) is equivalent to that of (7). The latter one’s derivation in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ must end as follows:

The premise can be obtained only by means of the rule $(A)_{\mathrm {bsc}}$ , which can indeed be applied because there is an occurrence of $\mathit {ex}$ in the left-hand side. Recall that

$$\begin{align*}\mathrm{Cmp}\left(q^{(0)}_1,h_{\exists}\right) = \mathit{go} \mathbin{\backslash} \left( q^{(0)}_1 \cdot \mathit{rt} \cdot \mathit{fn} \mathbin{\backslash} \left( \left( p_{1} \mathbin{\backslash} h_{\exists}(p_{1}) \right) \mathbin{\&} \left( p_{2} \mathbin{\backslash} h_{\exists}(p_{2}) \right) \right) \right). \end{align*}$$

By Corollary 4.11, there exists $\Gamma ^{\prime \prime }$ such that $\mathit {lt} \, p_{1}^{x} \, \mathit {ex} \Rightarrow _{\mathtt {S}}^\ast \Gamma ^{\prime \prime } \, \mathit {go}$ and the sequent

(8) $$ \begin{align} \Gamma^{\prime\prime}, q^{(0)}_1 \cdot \mathit{rt} \cdot \mathit{fn} \mathbin{\backslash} \left( \left( p_{1} \mathbin{\backslash} h_{\exists}(p_{1}) \right) \mathbin{\&} \left( p_{2} \mathbin{\backslash} h_{\exists}(p_{2}) \right) \right), \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align} $$

is derivable. The string rewriting system $\mathtt {S}$ contains rules from $\mathtt {S}_0$ and $\mathtt {S}_1$ and also the rules $\mathit {ex} \to p_{2}\, \mathit {ex}, \mathit {ex} \to \mathit {go}$ ; note that each rule from $\mathtt {S}_0 \cup \mathtt {S}_1$ contains an element of $Q_0 \cup Q_1$ in left-hand sides. Since $\mathit {lt} \, p_{1}^{x} \, \mathit {ex}$ does not contain symbols from $Q_0 \cup Q_1$ , none of these rules can be applied in a derivation $\mathit {lt} \, p_{1}^{x} \, \mathit {ex} \Rightarrow _{\mathtt {S}}^\ast \Gamma ^{\prime \prime } \, \mathit {go}$ . Thus, $\Gamma ^{\prime \prime } \, \mathit {go}$ is obtained from $\mathit {lt} \, p_{1}^{x} \, \mathit {ex}$ by means of the rules $\mathit {ex} \to p_{2} \, \mathit {ex}$ , $\mathit {ex} \to \mathit {go}$ . Therefore, there is $y \in \omega $ such that $\Gamma ^{\prime \prime } = \mathit {lt} \, p_{1}^{x} \, p_{2}^{y}$ .

By Corollary 2.5, the sequent (8) is equiderivable with the following:

(9) $$ \begin{align} \mathit{lt}, p_{1}^{x}, p_{2}^{y}, q^{(0)}_1 , \mathit{rt} , \mathit{fn} \mathbin{\backslash} \left( \left( p_{1} \mathbin{\backslash} h_{\exists}(p_{1}) \right) \mathbin{\&} \left( p_{2} \mathbin{\backslash} h_{\exists}(p_{2}) \right) \right), \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok}. \end{align} $$

Derivability of this sequent is analysed in the same way as that of (5). Namely, (9) is derivable if and only if so is

(10) $$ \begin{align} \mathit{lt} , \Delta^\prime, h_{\exists}(p_i), \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align} $$

for $\Delta ^\prime \, p_i = \mathfrak {f}_{1}\left (p_{1}^{x} p_{2}^{y}\right )$ . Again, two subcases arise.

Subcase A. $\mathfrak {f}_{1}\left (p_{1}^{x} p_{2}^{y}\right ) = p_{1}^{k} p_{2}$ . This happens if and only if $y = \mathtt {c}\left ( k, t \right )$ such that $k = \langle \overline {\varepsilon }, \sharp \beta , e^\prime \rangle $ for some $\beta < \alpha $ and $e^\prime \in \omega $ and such that $\mathtt {U}\left ( e, k \right )$ converges in at most t steps. In this case, $\Delta ^\prime = p_{1}^{k}$ and the sequent (10) has the form $\mathit {lt} , p_{1}^{k}, p_\forall \cdot \mathit {en}, \mathrm {En}(k_{M-1}), \ldots , \mathrm {En}(k_1), \mathrm {Brk} \Rightarrow \mathit {lt} \cdot \mathit {ok}$ (recall that $h_\exists (p_2) = p_\forall \cdot \mathit {en}$ ). Its derivability is equivalent to that of

(11) $$ \begin{align} \mathit{lt} , p_{1}^{k}, p_\forall , \mathit{en}, \mathrm{En}(k_{M-1}), \ldots, \mathrm{En}(k_1), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok.} \end{align} $$

Subcase B. $\mathfrak {f}_{1}\left (p_{1}^{x} p_{2}^{y}\right ) = p_{1}$ . In this case, the sequent (10) has the form

$$\begin{align*}\mathit{lt} , fl, \mathrm{En}(k_{M-1}), \ldots, \mathrm{En}(k_1), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align*}$$

because $h_\exists (p_1) = fl$ . It is not derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ , as one cannot obtain this sequent by means of any rule of $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ . (Note that $fl$ is a special variable that does not occur elsewhere; its purpose is to indicate that the computation fails because of the invalid input $(x,y)$ .)

Let us summarize all the reasonings for Case 2a.

• • If (2) is derivable and $\gamma = \omega ^{k_1} + \cdots + \omega ^{k_M}> \alpha $ , then the sequent (11) is derivable for some $k = \langle \overline {\varepsilon }, \sharp \beta , e^\prime \rangle $ such that $\beta < \alpha $ and $\mathtt {U}\left ( e, k \right )$ converges. The parameter $\gamma ^\prime $ of the sequent (11) is $\omega ^{k_1}+\cdots +\omega ^{k_{M-1}}$ , and it is greater than $\beta $ . The induction hypothesis implies that $k \in \mathbf {T}$ . The latter implies that $x \in \mathbf {T}$ because x is an index of a disjunction of formulae such that one of the disjuncts has index k.

• • If x belongs to $\mathbf {T}$ , then there exists $k = \langle \overline {\varepsilon }, \sharp \beta , e^\prime \rangle \in \mathbf {T}$ such that $\beta < \alpha $ and $\mathtt {U}\left ( e, k \right )$ converges. Let t be the number of steps after which $\mathtt {U}\left ( e, k \right )$ converges. One can apply the induction hypothesis and conclude that (11) is derivable. Then, the sequent (9) is derivable for $y = \mathtt {c}\left ( e, t \right )$ , which implies the derivability of (2).

This concludes the proof of Case 2a.

Case 2b: $X = \Pi $ . This case is dealt with in the same manner as Case 2a because $\mathrm {En}_{\exists }$ and $\mathrm {En}_{\forall }$ have similar structure. Let us briefly outline the main stages of the argument. Recall that $\mathrm {En}_{\forall } = \mathit {go} \cdot \mathrm {Cmp}\left (q^{(0)}_0,h_0\right ) \cdot \left (\mathrm {Ok} \mathbin {\&} \mathit {go} \mathbin {\backslash } \left ( p_{2}^\ast \cdot \mathit {go} \right ) \right ) \cdot \left ( \mathrm {Ok} \mathbin {\&} \mathrm {Cmp}\left (q^{(0)}_1, h_{\forall } \right ) \right )$ . First, one shows that the sequent $\mathit {lt}, p_{1}^{x}, \mathrm {En}_{\forall }, \Xi \Rightarrow \mathit {lt} \cdot \mathit {ok}$ is derivable if and only if one of the following holds:

1. i. $\alpha =0$ and $x \in \mathbf {T}$ ;

2. ii. $\alpha>0$ and the following sequent is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ :

   (12) $$ \begin{align} \mathit{lt}, p_{1}^{x}, \mathit{go}, \mathrm{Ok} \mathbin{\&} \mathit{go} \mathbin{\backslash} \left( p_{2}^\ast \cdot \mathit{go} \right) , \mathrm{Ok} \mathbin{\&} \mathrm{Cmp}\left(q^{(0)}_1, h_{\forall} \right) , \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok}. \end{align} $$

   (Compare it with the sequent (7).)

Any derivation of the sequent (12) must end as follows:

It follows from Corollary 2.5 that the sequent

(13) $$ \begin{align} \mathit{lt}, p_{1}^{x}, p_{2}^\ast , \mathit{go} , \mathrm{Ok} \mathbin{\&} \mathrm{Cmp}\left(q^{(0)}_1, h_{\forall} \right) , \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align} $$

is derivable if and only if so is

(14) $$ \begin{align} \mathit{lt}, p_{1}^{x}, p_{2}^y , \mathit{go} , \mathrm{Ok} \mathbin{\&} \mathrm{Cmp}\left(q^{(0)}_1, h_{\forall} \right) , \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align} $$

for each $y \in \omega $ . The sequent (14) is equiderivable with

(15) $$ \begin{align} \mathit{lt}, p_{1}^{x}, p_{2}^{y}, q^{(0)}_1 , \mathit{rt} , \mathit{fn} \mathbin{\backslash} \left( \left( p_{1} \mathbin{\backslash} h_{\forall}(p_{1}) \right) \mathbin{\&} \left( p_{2} \mathbin{\backslash} h_{\forall}(p_{2}) \right) \right), \Xi \Rightarrow \mathit{lt} \cdot \mathit{ok}. \end{align} $$

This one is similar to (9), so again two subcases arise.

If $\mathfrak {f}_{1}(p_{1}^x p_{2}^y) = p_{1}^{k} p_{2}$ , then $y = \mathtt {c}\left ( k, t \right )$ , where $k = \langle \overline {\varepsilon }, \sharp \beta , e^\prime \rangle $ for $\beta < \alpha $ and $\mathtt {U}\left ( e, k \right )$ converges. Let t be an upper bound on the number of steps in which $\mathtt {U}\left ( e, k \right )$ converges. In this case, the sequent (15) is derivable if and only if so is

(16) $$ \begin{align} \mathit{lt} , p_{1}^{k}, p_\exists , \mathit{en}, \mathrm{En}(k_{M-1}), \ldots, \mathrm{En}(k_1), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok.} \end{align} $$

Otherwise, $\mathfrak {f}_{1}\left (p_{1}^{x} p_{2}^{y}\right ) = p_{1}$ . In this case, the sequent (15) is equiderivable with the sequent

$$\begin{align*}\mathit{lt} , \mathit{ok}, \mathrm{En}(k_{M-1}), \ldots, \mathrm{En}(k_1), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok} \end{align*}$$

(recall that $h_{\forall }(p_{1}) = \mathit {ok}$ ). It is derivable in $\mathbf {ACT}_{\omega }^{\mathrm {bsc}}(\mathtt {S})$ by Lemma 4.12.

Combining these arguments we obtain the following:

• • If (2) is derivable and $\omega ^{k_1}+\cdots +\omega ^{k_M}>\alpha $ , then the sequent (16) is derivable for each $k = \langle \overline {\varepsilon }, \sharp \beta , e^\prime \rangle $ such that $\beta < \alpha $ , $e^\prime \in \omega $ and $\mathtt {U}\left ( e, k \right )$ converges. By the induction hypothesis, this means that all such k’s are members of $\mathbf {T}$ . The latter implies that $x \in \mathbf {T}$ because x is an index of the conjunction of the formulae such that their indices k satisfy the above properties.

• • If x belongs to $\mathbf {T}$ , then, for each $k = \langle \overline {\varepsilon }, \sharp \beta , e^\prime \rangle $ such that $\beta < \alpha $ and such that $\mathtt {U}\left ( e, k \right )$ converges in at most t steps, it holds that $k \in \mathbf {T}$ . The induction hypothesis implies that (15) is derivable for $y = \mathtt {c}\left ( e, t \right )$ . If y is not of this form, then (15) is derivable too, hence (13) is derivable. The derivability of (2) follows.

Proof of Theorem 4.1.

The set $\mathbf {T}$ is many-one reducible to the set of sequents derivable from $\mathcal {H}$ in $\mathbf {ACT}_{\omega }$ by means of the function

$$\begin{align*}x\ \mapsto\ \left(\mathit{lt}, p_{1}^{x}, p_{\mathsf{Q}}, \mathit{en}, \mathrm{En}(k_M(x)), \ldots, \mathrm{En}(k_1(x)), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok} \right), \end{align*}$$

where $\omega ^{k_1(x)} + \cdots + \omega ^{k_M(x)} = \alpha +1$ if $x = \langle \varepsilon , \sharp \alpha , e \rangle $ . If x is not of this form, then the reduction maps it to some underivable sequent, say, to $p \Rightarrow q$ . Lemma 4.9 implies that $x \in \mathbf {T}$ if and only if the sequent

$$ \begin{align*}{!}\Upsilon_{\mathcal{H}}, \mathit{lt}, p_{1}^{x}, p_{\mathsf{Q}}, \mathit{en}, \mathrm{En}(k_M(x)), \ldots, \mathrm{En}(k_1(x)), \mathrm{Brk} \Rightarrow \mathit{lt} \cdot \mathit{ok}\end{align*} $$

is derivable in ${!} \mathbf {ACT}_{\omega }$ . By Theorem 2.6 this is equivalent to the derivability of $\mathit {lt}, p_{1}^{x}, p_{\mathsf {Q}}, \mathit {en}, \mathrm {En}(k_M(x)), \ldots , \mathrm {En}(k_1(x)), \mathrm {Brk} \Rightarrow \mathit {lt} \cdot \mathit {ok}$ from $\mathcal {H}$ in $\mathbf {ACT}_{\omega }$ , which proves correctness of the reduction.

Proof. It is easy to verify that for every sequent s derivable in ${!} \mathbf {ACT}_{\omega }^{\hspace{1pt}-}$ ,

$$\begin{align*}{\mathrm{rank}^{-} \left( s \right)}\ \leqslant\ {\omega \cdot \underline{\mathrm{rank}}^{-} \left( s \right)}. \end{align*}$$

Hence it suffices to prove that each $ \underline {\mathrm {rank}}^{-} \left ( s \right )$ , with s as above, is less than $\omega ^{\omega }$ . To this end, we define the following operations on $\mathscr {N}$ :

$$ \begin{align*} {\left( m_0, m_1, \ldots \right) \boxplus \left( n_0, n_1, \ldots \right)}\ &:=\ {\left( m_0 + n_0, m_1 + n_1, \ldots \right)} ;\\ {\left( m_0, m_1, \ldots \right) {\uparrow}}\ &:=\ {\left( 0, m_0, m_1, \ldots \right)}. \end{align*} $$

Next, let $\mu $ be the function from the set of all formulae (not containing $^\ast $ in the scope of $!$ ) to $\mathscr {N}$ given by:

$$ \begin{align*} {\mu \left( A \right)}\ &:=\ {\left( 0, 0, 0, \ldots \right)} \quad \text{if}\ A\ \text{does~not contain}\ {}^\ast ;\\ {\mu \left( A \circ B \right)}\ &:=\ {\mu \left( A \right) \boxplus \mu \left( B \right)} \quad \text{for each} \ \ {\circ \in \left\{ \mathbin{\backslash}, \mathbin{/}, \cdot, \mathbin{\&}, \oplus \right\}} ;\\ {\mu \left( A^{\ast} \right)}\ &:= {\left( \mu \left( A \right) {\uparrow} \right) \boxplus \left( 2, 0, 0, \ldots \right)}. \end{align*} $$

So in particular, if A begins with $!$ , then $\mu \left ( A \right ) = 0$ . We extend $\mu $ to sequents by taking

$$\begin{align*}{\mu \left( A_1, \ldots, A_m \Rightarrow B \right)}\ :=\ {\mu \left( A_1 \right) \boxplus \ldots \boxplus \mu \left( A_n \right) \boxplus \mu \left( B \right)}. \end{align*}$$

Denote $\mu \circ \nu $ by $\dot {\mu }$ (see Section 2.4 for the definition of $\nu $ ). We claim that for every sequent s derivable in ${!} \underline {\mathbf {ACT}}_{\omega }^{\hspace{1pt}-}$ ,

(†) $$ \begin{align} {\underline{\mathrm{rank}}^{-} \left( s \right)}\ \leqslant\ {\dot{\mu} \left( s \right)} , \end{align} $$

by induction on $\dot {\mu } \left ( s \right )$ . Evidently, if $\dot {\mu } \left ( s \right ) = 0$ , then ${}^\ast $ does not occur in s, and therefore s can be derived by one application of ( $\mathrm {Fin}$ ), which implies $ \underline {\mathrm {rank}}^{-} \left ( s \right ) = 0$ .Footnote ⁶ Assume that $\dot {\mu } \left ( s \right )> 0$ , and consider an arbitrary derivation $\mathfrak {T}$ of s in ${!} \underline {\mathbf {ACT}}_{\omega }^{\hspace{1pt}-}$ .

1. a. Suppose that $\mathfrak {T}$ ends with an application of the $\omega $ -rule, whose premises are $s_0$ , $s_1$ , …; so s is obtained from $s_0$ , $s_1$ , … at the last step of $\mathfrak {T}$ . Then

   $$ \begin{align*} {\underline{\mathrm{rank}}^{-} \left( s \right)}\ &\leqslant\ {\sup \left\{ \underline{\mathrm{rank}}^{-} \left( s_i \right) \mid i \in \omega \right\} + 1} \\ &\leqslant\ {\sup \left\{ \dot{\mu} \left( s_i \right) \mid i \in \omega \right\} + 1}\ <\ {\dot{\mu} \left( s \right)} , \end{align*} $$
   where the second inequality is guaranteed by the inductive hypothesis.

2. b. Suppose that $\mathfrak {T}$ ends with an application of ( $\mathrm {Fin}$ ). Then we can view $\mathfrak {T}$ as ending with a possibly broader application of ( $\mathrm {Fin}$ ) with premises $s_1$ , …, $s_m$ , each of which is either an axiom or derived by the $\omega $ -rule in $\mathfrak {T}$ . Observe that

   $$\begin{align*}{\max \left\{ {\dot{\mu} \left( s_1 \right)}, \ldots, {\dot{\mu} \left( s_m \right)} \right\}}\ \leqslant\ {\dot{\mu} \left( s \right)}. \end{align*}$$

   Further, using the argument for (a), one can obtain $ \underline {\mathrm {rank}}^{-} \left ( s_i \right ) < {\dot {\mu }} \left ( s_i \right )$ for each $i = 1, \ldots , m$ . Thus, since ( $\mathrm {Fin}$ ) contributes one more inference step, we have

   $$\begin{align*}{\underline{\mathrm{rank}}^{-} \left( s \right)}\ \leqslant\ {\max \left\{ {\underline{\mathrm{rank}}^{-} \left( s_1 \right)} , \ldots , {\underline{\mathrm{rank}}^{-} \left( s_m \right)} \right\} + 1}\ \leqslant\ {\dot{\mu} \left( s \right)} , \end{align*}$$
   as desired.