Proof. Standard induction on the structure of A. □

Proof. Consider an example of $\infty $ -proof for the sequent $\Box (\Box (p \rightarrow \Box p) \rightarrow p) \Rightarrow p$ given above. We transform this example into an $\infty $ -proof for $\Box (\Box (A \rightarrow \Box A) \rightarrow A) \Rightarrow A$ by replacing p with A and adding required $\infty $ -proofs instead of initial sequents using Lemma 3.3. □

Proof. Standard induction on the structure (local height) of a proof of $\Gamma \Rightarrow \Delta $ . □

Proof. Assume $\pi $ is a proof of $\Gamma \Rightarrow \Delta $ in $\mathsf {Grz}_{\mathsf {Seq}}+\mathsf {cut}$ . By induction on the size of $\pi $ we prove $\mathsf {Grz}_{\infty }+\mathsf {cut}\vdash \Gamma \Rightarrow \Delta $ .

If $\Gamma \Rightarrow \Delta $ is an initial sequent of $\mathsf {Grz}_{\mathsf {Seq}}+\mathsf {cut}$ , then it is either an initial sequent of $\mathsf {Grz}_{\infty }+\mathsf {cut}$ , or is provable in $\mathsf {Grz}_{\infty }+\mathsf {cut}$ by Lemma 3.3. Otherwise, consider the last application of an inference rule in $\pi $ .

The only nontrivial case is when the proof $\pi $ has the form

where $\Sigma ,\Box \Pi = \Gamma $ and $\Box A, \Lambda = \Delta $ . By the induction hypothesis there is an $\infty $ -proof $\xi $ of $\Box \Pi ,\Box (A\to \Box A)\Rightarrow A$ in $\mathsf {Grz}_{\infty }+\mathsf {cut}$ .

We have the following $\infty $ -proof $\lambda $ of $\Box \Pi \Rightarrow A$ in $\mathsf {Grz}_{\infty }+\mathsf {cut} $ :

where $G= \Box (A \rightarrow \Box A) \rightarrow A$ , $\xi ^{\prime }$ is an $\infty $ -proof of $\Box \Pi ,\Box (A\to \Box A)\Rightarrow A,A$ obtained from $\xi $ by Lemma 3.5, and $\theta $ is an $\infty $ -proof of $\Box \Pi ,\Box G \Rightarrow A$ , which exists by Lemma  3.4 and Lemma 3.5.

The required $\infty $ -proof for $\Sigma ,\Box \Pi \Rightarrow \Box A, \Lambda $ has the form

where $\lambda '$ is an $\infty $ -proof of the sequent $\Sigma ,\Box \Pi \Rightarrow A,\Lambda $ obtained from the $\infty $ -proof $\lambda $ by Lemma 3.5.

The cases of other inference rules being last in $\pi $ are straightforward, so we omit them. □

Proof. First we will prove a more general statement: if $\mathsf {Grz}_{\infty }\vdash \Gamma \Rightarrow \Delta $ , then $\mathsf {Grz}_{\mathsf {Seq}} \vdash \Lambda ^\ast ,\Gamma \Rightarrow \Delta $ for any finite set of formulas $\Lambda $ . The statement of the theorem immediately follows by assuming the set $\Lambda $ to be empty.

Assume $\pi $ is an $\infty $ -proof of the sequent $\Gamma \Rightarrow \Delta $ in $\mathsf {Grz}_\infty $ and $\Lambda $ is a finite set of formulas. By induction on the number of elements in the finite set $Sub(\Gamma \Rightarrow \Delta )\backslash \Lambda $ with a subinduction on $\lvert \pi \rvert $ , we prove $\mathsf {Grz}_{\mathsf {Seq}} \vdash \Lambda ^\ast ,\Gamma \Rightarrow \Delta $ .

If $\lvert \pi \rvert =0$ , then $\Gamma \Rightarrow \Delta $ is an initial sequent. We see that the sequent $\Lambda ^\ast ,\Gamma \Rightarrow \Delta $ is an initial sequent and it is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ . Otherwise, consider the last application of an inference rule in $\pi $ .

Case 1. Suppose that $\pi $ has the form

where $A\to B,\Sigma = \Delta $ . Notice that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . By the induction hypothesis for $\pi ^\prime $ and $\Lambda $ , the sequent $\Lambda ^\ast ,\Gamma ,A\Rightarrow B,\Sigma $ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ . Applying the rule ( $\to _{\mathsf {R}}$ ) to it, we obtain that the sequent $\Lambda ^\ast ,\Gamma \Rightarrow \Delta $ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ .

Case 2. Suppose that $\pi $ has the form

where $\Sigma , A\to B = \Gamma $ . We see that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . By the induction hypothesis for $\pi ^\prime $ and $\Lambda $ , the sequent $\Lambda ^\ast ,\Sigma , B\Rightarrow \Delta $ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ . Analogously, we have $\mathsf {Grz}_{\mathsf {Seq}} \vdash \Lambda ^\ast ,\Sigma \Rightarrow A,\Delta $ . Applying the rule ( $\to _{\mathsf {L}}$ ), we obtain that the sequent $\Lambda ^\ast ,\Sigma , A\to B \Rightarrow \Delta $ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ .

Case 3. Suppose that $\pi $ has the form

where $\Sigma , \Box A = \Gamma $ . We see that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . By the induction hypothesis for $\pi ^\prime $ and $\Lambda $ , the sequent $\Lambda ^\ast ,\Sigma , A, \Box A\Rightarrow \Delta $ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ . Applying the rule ( $\mathsf {refl}$ ), we obtain $\mathsf {Grz}_{\mathsf {Seq}} \vdash \Lambda ^\ast ,\Sigma , \Box A\Rightarrow \Delta $ .

Case 4. Suppose that $\pi $ has the form

where $\Phi , \Box \Pi = \Gamma $ and $\Box A, \Sigma =\Delta $ .

Subcase 4.1: the formula A belongs to $\Lambda $ . We see that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . By the induction hypothesis for $\pi ^\prime $ and $\Lambda $ , the sequent $\Lambda ^\ast ,\Phi , \Box \Pi \Rightarrow A, \Sigma $ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ . Then we see

where the rule ( $\mathsf {weak}$ ) is admissible by Lemma 3.5.

Subcase 4.2: the formula A doesn’t belong to $\Lambda $ . We have that the number of elements in $Sub(\Box \Pi \Rightarrow A)\backslash (\Lambda \cup \{A\})$ is strictly less than the number of elements in $Sub(\Phi , \Box \Pi \Rightarrow \Box A, \Sigma )\backslash \Lambda $ . Therefore, by the induction hypothesis for $\pi ^{\prime \prime }$ and $\Lambda \cup \{A\}$ , the sequent $\Lambda ^\ast ,\Box (A\to \Box A),\Box \Pi \Rightarrow A$ is provable in $\mathsf {Grz}_{\mathsf {Seq}}$ . Then we have

□

Proof. Assume, in the given space, we a have descending sequence of closed balls

$$ \begin{align*}B_{r_0}(\pi_0) \supset B_{r_1}(\pi_1) \supset B_{r_2}(\pi_2) \supset \cdots \end{align*} $$

with radii tending to $0$ . Consider a subsequence of this sequence

$$ \begin{align*}B_{r^\prime_0}(\pi^\prime_0) \supset B_{r^\prime_1}(\pi^\prime_1) \supset B_{r^\prime_2}(\pi^\prime_2) \supset \cdots \end{align*} $$

such that $r^\prime _i \leqslant 2^{-i}$ for all $i \in \mathbb {N}$ . Trivially, we have $\bigcap \limits ^\infty _{i=0} B_{r_i} (\pi _i) = \bigcap \limits ^\infty _{i=0} B_{r^\prime _i} (\pi ^\prime _i)$ . Note also that

$$ \begin{align*}\pi^\prime_0 \sim_0 \pi^\prime_1 \sim_1 \pi^\prime_2 \sim_2 \cdots.\end{align*} $$

Consequently there exists an $\infty $ -proof $\pi $ of the system $\mathsf {Grz}_{\infty } +\mathsf {cut} $ such that $\pi \sim _i \pi ^\prime _i$ for any $i \in \mathbb {N}$ . We shall check that $\pi \in B_{r^\prime _i} (\pi ^\prime _i )$ . For any $i,k\in \mathbb {N}$ , we have

$$ \begin{align*}d_{\mathcal P} (\pi^\prime_i, \pi) \leqslant \max \{ d_{\mathcal P} (\pi^\prime_i, \pi^\prime_{i+k}), d_{\mathcal P} (\pi^\prime_{i+k}, \pi)\}\leqslant \max \{ r^\prime_i, d_{\mathcal P} (\pi^\prime_{i+k}, \pi)\} .\end{align*} $$

Since $\lim \limits _{n\to \infty } d_{\mathcal P} (\pi ^\prime _n, \pi ) =0$ , we obtain $d_{\mathcal P} (\pi ^\prime _i, \pi ) \leqslant r^\prime _i$ for any $i \in \mathbb {N}$ . It follows that $\pi \in \bigcap \limits ^\infty _{i=0} B_{r^\prime _i} (\pi ^\prime _i) = \bigcap \limits ^\infty _{i=0} B_{r_i} (\pi _i)$ .□

Proof of Proposition 4.10

Since the set $\mathcal F_m$ is nonempty, there is a nonexpansive function $\mathsf {a}\in \mathcal F_m$ . For any ordinal $\alpha < \omega ^2$ , we recursively define a function $\mathsf {a}_\alpha \colon \mathcal P^m\to \mathcal P$ in the following way. We put $\mathsf {a}_0= \mathsf {a}$ and $\mathsf {a}_{\alpha +1}= \mathsf {U} (\mathsf {a}_\alpha )$ . Additionally, in the limit case, we set $\mathsf {a}_{\omega \cdot (n+1)}(\vec {\pi }) = \mathsf {a}_{\omega \cdot n+(\sum _{s=1}^m\lvert \pi _s\rvert ) +1}(\vec {\pi })$ for any $\vec {\pi } \in \mathcal P^m$ and any $n \in \mathbb {N}$ .

Now we check by transfinite induction up to the ordinal $\omega ^2$ that all functions $\mathsf {a}_\alpha $ are nonexpansive. The function $\mathsf {a}_0= \mathsf {a}$ is nonexpansive. The successor case is trivial. It remains to check the limit case. Consider a function $\mathsf {a}_{\omega \cdot (n+1)}$ . For all tuples $\vec \pi $ and $\vec \pi '$ we have $\mathsf a_{\omega \cdot (n+1)}(\vec \pi )\sim _0 \mathsf a_{\omega \cdot (n+1)}(\vec \pi ')$ by definition. If for tuples $\vec \pi $ and $\vec \pi '$ and some $h\geqslant 1$ we have $\pi _1\sim _h\pi ^{\prime }_1,\ldots ,\pi _m\sim _h\pi ^{\prime }_m$ , then $\sum _{s=1}^m\lvert \pi _s\rvert =\sum _{s=1}^m\lvert \pi _s'\rvert =t$ and $\mathsf {a}_{\omega \cdot (n+1)}(\vec {\pi }) = \mathsf {a}_{\omega \cdot n+t +1}(\vec {\pi }) \sim _h \mathsf {a}_{\omega \cdot n+t +1}(\vec \pi ')=\mathsf {a}_{\omega \cdot (n+1)}(\vec \pi ')$ , because the function $\mathsf {a}_{\omega \cdot n+t +1}$ is nonexpansive by the induction hypothesis. Therefore all functions $\mathsf {a}_\alpha $ are nonexpansive.

In this proof we will write $\mathsf { c}\simeq _\alpha \mathsf {d}$ if $\mathsf { c}\sim _{n,k} \mathsf {d}$ and $\alpha = \omega \cdot n +k$ . We claim that for any ordinal $\alpha < \omega ^2$ and any ordinal $\beta < \alpha $ we have $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\alpha $ . We check this claim by transfinite induction on $\alpha $ . The case $\alpha =0$ is trivial.

Suppose $\alpha = \gamma +1$ . By the induction hypothesis, we have $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\gamma $ for any ordinal $\beta < \gamma $ . If $\gamma =0$ , then $\mathsf {a}_0 \simeq _0 \mathsf {a}_1$ and the statement holds. If $\gamma = \gamma ^\prime +1$ , then we have $\mathsf {a}_{\gamma ^\prime } \simeq _{\gamma ^\prime }\mathsf {a}_{\gamma }$ by the induction hypothesis. Since $\mathsf {U}$ is a contractive mapping, we have $\mathsf {a}_\gamma = \mathsf {U}(\mathsf {a}_{\gamma ^\prime } ) \simeq _{\gamma ^\prime +1} \mathsf {U}(\mathsf {a}_{\gamma } ) = \mathsf {a}_\alpha $ . In addition, for any $\beta <\gamma $ we see $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\gamma \simeq _\gamma \mathsf {a}_\alpha $ . Hence $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\alpha $ and the statement holds. If $\gamma = \omega \cdot (n+1)$ , then $\mathsf {a}_{\omega \cdot n+k} \simeq _{\omega \cdot n + k} \mathsf {a}_{\omega \cdot (n+1)}$ for any $k \in \mathbb {N}$ . We see $\mathsf {a}_{\omega \cdot n+k+1} = \mathsf {U}(\mathsf {a}_{\omega \cdot n+k}) \simeq _{\omega \cdot n + k+1} \mathsf {U}(\mathsf {a}_{\omega \cdot (n+1)})=\mathsf {a}_\alpha $ for any $k \in \mathbb {N}$ . Thus $\mathsf {a}_{\omega \cdot (n+1)}(\vec {\pi }) = \mathsf {a}_{\omega \cdot n+\sum _{s=1}^m\lvert \pi _s\rvert +1}(\vec {\pi }) \sim _{n+1} \mathsf {a}_\alpha (\vec {\pi })$ for any tuple $\vec {\pi } \in \mathcal P^m$ . Consequently $\mathsf {a}_{\omega \cdot (n+1)} \simeq _{\omega \cdot (n + 1)} \mathsf {a}_\alpha $ . For any $\beta <\gamma $ we have $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\gamma \simeq _\gamma \mathsf {a}_\alpha $ . Hence $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\alpha $ and the statement holds.

Now suppose $\alpha = \omega \cdot (n+1)$ for some $n \in \mathbb {N}$ . From the induction hypothesis, we have $\mathsf {a}_{\omega \cdot n} \simeq _{\omega \cdot n} \mathsf {a}_{\omega \cdot n+k}$ for any $k \in \mathbb {N}$ . Hence $\mathsf {a}_{\omega \cdot (n+1)}(\vec {\pi }) = \mathsf {a}_{\omega \cdot n+\sum _{s=1}^m\lvert \pi _s\rvert +1}(\vec {\pi }) \sim _n \mathsf {a}_{\omega \cdot n}(\vec {\pi })$ for any tuple $\vec {\pi } \in \mathcal P^m$ and $\mathsf {a}_{\omega \cdot n} \simeq _{\omega \cdot n} \mathsf {a}_\alpha $ . Now consider any $\beta < \alpha $ . If $\beta < \omega \cdot n$ , then $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_{\omega \cdot n}$ by the induction hypothesis. We see $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_{\omega \cdot n} \simeq _{\omega \cdot n} \mathsf {a}_\alpha $ and $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\alpha $ . Otherwise, $\beta = \omega \cdot n+k$ for some $k \in \mathbb {N}$ . It remains to check that $\mathsf {a}_{\omega \cdot n+k} \simeq _{\omega \cdot n+k} \mathsf {a}_\alpha $ . Consider any tuple $\vec {\tau } \in \mathcal P^m$ . We see $\mathsf {a}_{\omega \cdot (n+1)}(\vec {\tau }) = \mathsf {a}_{\omega \cdot n+\sum _{s=1}^m\lvert \tau _s\rvert +1}(\vec {\tau })\sim _n \mathsf {a}_{\omega \cdot n}(\vec {\tau }) \sim _n \mathsf {a}_{\omega \cdot n+k}(\vec {\tau })$ . If $\sum \limits _{s=1}^m\lvert \tau _s\rvert <~k$ , then $\mathsf {a}_{\omega \cdot n+\sum _{s=1}^m\lvert \tau _s\rvert +1} \simeq _{\omega \cdot n+\sum _{s=1}^m\lvert \tau _s\rvert +1} \mathsf {a}_{\omega \cdot n+k}$ and $\mathsf {a}_{\omega \cdot (n+1)}(\vec {\tau }) = \mathsf {a}_{\omega \cdot n+\sum _{s=1}^m\lvert \tau _s\rvert +1}(\vec {\tau }) \sim _{n+1} \mathsf {a}_{\omega \cdot n+k}(\vec {\tau })$ . We have checked that for any ordinal $\alpha < \omega ^2$ and any ordinal $\beta < \alpha $ we have $\mathsf {a}_\beta \simeq _\beta \mathsf {a}_\alpha $ .

Now we define the required fixed-point $\mathsf {a}_{\omega ^2}$ . We see that for any tuple $\vec {\pi } \in \mathcal P^m$

$$ \begin{align*}\mathsf{a}_0(\vec{\pi}) \sim_0 \mathsf{a}_\omega(\vec{\pi}) \sim_1 \mathsf{a}_{\omega \cdot 2}(\vec{\pi}) \sim_2\mathsf{a}_{\omega \cdot 3}(\vec{\pi}) \sim_3 \cdots .\end{align*} $$

In other words, we have a descending sequence of closed balls

$$ \begin{align*}B_{1}(\mathsf{a}_0(\vec{\pi})) \supset B_{\frac{1}{2}}(\mathsf{a}_\omega(\vec{\pi})) \supset B_{\frac{1}{4}}(\mathsf{a}_{\omega \cdot 2}(\vec{\pi})) \supset B_{\frac{1}{8}}(\mathsf{a}_{\omega \cdot 3}(\vec{\pi})) \supset \cdots \end{align*} $$

with radii tending to $0$ . By Proposition 4.9, there is an $\infty $ -proof $\kappa $ such that $ \kappa \in \bigcap \limits ^\infty _{i=0} B_{2^{-i}}(\mathsf {a}_{\omega \cdot i}(\vec {\pi }))$ , i.e., $\kappa \sim _{i} \mathsf a_{\omega \cdot i} (\vec {\pi })$ for all $i\in \mathbb N$ . This $\infty $ -proof is unique since radii of the balls tend to $0$ . We define $\mathsf a_{\omega ^2} (\vec {\pi }) = \kappa $ . Let us check that the mapping $\mathsf a_{\omega ^2}$ is nonexpansive. If for tuples $\vec \pi $ and $\vec \pi '$ we have $\pi _1\sim _h\pi ^{\prime }_1,\ldots ,\pi _m\sim _h\pi ^{\prime }_m$ for some $h\in \mathbb N$ , then we can choose i such that $i>h$ . We have $\mathsf a_{\omega ^2}(\vec \pi )\sim _h \mathsf a_{\omega \cdot i}(\vec \pi )\sim _h\mathsf a_{\omega \cdot i}(\vec \pi ')\sim _h \mathsf a_{\omega ^2}(\vec \pi ')$ . Therefore $\mathsf a_{\omega ^2}(\vec \pi )\sim _h \mathsf a_{\omega ^2}(\vec \pi ')$ and the mapping $\mathsf a_{\omega ^2}$ is nonexpansive.

Now we claim that $ \mathsf {a}_{\omega ^2} =\mathsf {U}(\mathsf a_{\omega ^2})$ . It is sufficient to show that $\mathsf a_{\omega ^2} \simeq _{\omega \cdot i} \mathsf {U}(\mathsf a_{\omega ^2})$ for any $i\in \mathbb {N}$ . By the definition of $\mathsf a_{\omega ^2}$ , we see $\mathsf a_{\omega ^2} \simeq _{\omega \cdot i} \mathsf {a}_{\omega \cdot i} $ for any $i\in \mathbb {N}$ . It follows that $\mathsf a_{\omega ^2} \simeq _{\omega \cdot i} \mathsf {a}_{\omega \cdot i} \simeq _{\omega \cdot i} \mathsf {a}_{\omega \cdot i+1 }= \mathsf {U}(\mathsf a_{\omega \cdot i}) \simeq _{\omega \cdot i+1} \mathsf {U}(\mathsf a_{\omega ^2})$ . Hence $\mathsf a_{\omega ^2} \simeq _{\omega \cdot i} \mathsf {U}(\mathsf a_{\omega ^2})$ for any $i\in \mathbb {N}$ and $ \mathsf {a}_{\omega ^2} =\mathsf {U}(\mathsf a_{\omega ^2})$ . □

Proof of Lemma 5.12

We define the required nonexpansive adequate mapping only for the last inference rule of Lemma 5.12 and omit other cases. Assume we have a formula A and an $\infty $ -proof $\pi $ of a sequent $\Sigma \Rightarrow \Upsilon $ . If $\Box A \notin \Upsilon $ , then we put $\mathsf {li}_{\:\Box A}(\pi ) =\pi $ . Otherwise, we define $\mathsf {li}_{\:\Box A}(\pi )$ by induction on $\lvert \pi \rvert $ .

If $\lvert \pi \rvert =0$ , then $\Sigma \Rightarrow \Upsilon $ is an initial sequent. We see that $\Sigma \Rightarrow A, \Upsilon \backslash \{\Box A \}$ is also an initial sequent and define $\mathsf {li}_{\:\Box A}(\pi )$ as the $\infty $ -proof consisting only of this sequent.

Suppose $\lvert \pi \rvert>0$ . We define $\mathsf {li}_{\:\Box A}(\pi )$ according to the last application of an inference rule in $\pi $ :

In these cases $\infty $ -proofs $\mathsf {li}_{\:\Box A}(\pi _0)$ (and $\mathsf {li}_{\:\Box A}(\pi _1)$ ) are defined since $\lvert \pi _0 \rvert < \lvert \pi \rvert $ (and $\lvert \pi _1 \rvert < \lvert \pi \rvert $ ).

Suppose the last inference in $\pi $ is an application of the rule $(\Box )$ with the principle formula being not $\Box A$ . Then we define $\mathsf {li}_{\:\Box A}(\pi )$ as follows:

It remains to consider the case when the last inference in $\pi $ has the form:

In this case we put $\mathsf {li}_{\:\Box A}(\pi )=\pi _0$ . The mapping $\mathsf {li}_{\:\Box A}$ is well-defined.

Now we claim that $\mathsf {li}_{\:\Box A}$ is nonexpansive. We shall check that for any $\infty $ -proofs $\pi $ and $\pi ^\prime $ , and any $n\in \mathbb N$ , we have

$$ \begin{align*}\pi\sim_n\pi'\Rightarrow \mathsf{li}_{\:\Box A}(\pi)\sim_n \mathsf{li}_{\:\Box A}(\pi^\prime).\end{align*} $$

Assume we have two $\infty $ -proofs $\pi $ and $\pi ^\prime $ such that $\pi \sim _n\pi '$ . If $n=0$ , then trivially $\mathsf {li}_{\:\Box A}(\pi )\sim _n \mathsf {li}_{\:\Box A}(\pi ^\prime )$ . If $n>0$ , then the main fragments of $\pi $ and $\pi ^\prime $ are identical. Suppose the root of $\pi $ is marked by a sequent $\Sigma \Rightarrow \Upsilon $ , where $\Box A \notin \Upsilon $ . Then the same condition holds for the $\infty $ -proof $\pi ^\prime $ . In this case, we have

$$ \begin{align*} \mathsf{li}_{\:\Box A}(\pi) = \pi \sim_n \pi^\prime = \mathsf{li}_{\:\Box A}(\pi^\prime).\end{align*} $$

Otherwise, the statement $\mathsf {li}_{\:\Box A}(\pi )\sim _n \mathsf {li}_{\:\Box A}(\pi ^\prime )$ is proved by induction on $\lvert \pi \rvert = \lvert \pi ^\prime \rvert $ with the case analysis according to the definition of $\mathsf {li}_{\:\Box A}$ . If $\lvert \pi \rvert =\lvert \pi ^\prime \rvert =0$ , then $\pi =\pi ^\prime $ and $\mathsf {li}_{\:\Box A}(\pi )\sim _n\mathsf {li}_{\:\Box A}(\pi ^\prime )$ .

If the last inference in $\pi $ is an application of the rule $(\to _{\mathsf {R}})$ , then $\pi $ and $\pi ^\prime $ have the following forms

where $\pi _0 \sim _n \pi ^\prime _0$ . By the induction hypothesis for $\lvert \pi _0\rvert = \lvert \pi ^\prime _0\rvert $ , we have $\mathsf {li}_{\:\Box A}(\pi _0)\sim _n \mathsf {li}_{\:\Box A}(\pi ^\prime _0)$ . From the definition of the mapping $\mathsf {li}_{\:\Box A}$ , we obtain $\mathsf {li}_{\:\Box A}(\pi )\sim _n \mathsf {li}_{\:\Box A}(\pi ^\prime )$ .

Consider the case when the last inference in $\pi $ is an application of the rule $({\Box })$ with the principle formula $\Box A$ . We have that $\pi $ and $\pi ^\prime $ have the following forms

where $\pi _0 \sim _n \pi ^\prime _0$ and $\pi _1 \sim _{n-1} \pi ^\prime _1$ . From the definition of the mapping $\mathsf {li}_{\:\Box A}$ , we obtain $\mathsf {li}_{\:\Box A}(\pi )=\pi _0 \sim _n \pi ^\prime _0 = \mathsf {li}_{\:\Box A}(\pi ^\prime )$ .

All the other cases are treated similarly, so we omit them. We have that the mapping $\mathsf {li}_{\:\Box A}$ is nonexpansive. Now we check that $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert \leqslant \lvert \pi \rvert $ for any $\pi \in \mathcal {P}$ .

Assume we have an $\infty $ -proof $\pi $ . Suppose the root of $\pi $ is marked by a sequent $\Sigma \Rightarrow \Upsilon $ , where $\Box A \notin \Upsilon $ . In this case, we have $\mathsf {li}_{\:\Box A}(\pi ) = \pi $ and $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert \leqslant \lvert \pi \rvert $ .

Otherwise, the assertion $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert \leqslant \lvert \pi \rvert $ is proved by induction on $\lvert \pi \rvert $ with the case analysis according to the definition of $\mathsf {li}_{\:\Box A}$ . If $\lvert \pi \rvert =0$ , then $\Sigma \Rightarrow \Upsilon $ is an initial sequent. We see that $\Sigma \Rightarrow A, \Upsilon \backslash \{\Box A \}$ is also an initial sequent and $\mathsf {li}_{\:\Box A}(\pi )$ was defined as the $\infty $ -proof consisting only of this sequent. We have $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert =0$ and $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert \leqslant \lvert \pi \rvert $ .

If the last inference in $\pi $ is an application of the rule $(\to _{\mathsf {R}})$ , then $\pi $ has the form

By the induction hypothesis for $\lvert \pi _0\rvert $ , we have $\lvert \mathsf {li}_{\:\Box A}(\pi _0)\rvert \leqslant \lvert \pi _0 \rvert $ . From the definition of the mapping $\mathsf {li}_{\:\Box A}$ , we see $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert =\lvert \mathsf {li}_{\:\Box A}(\pi _0)\rvert +1 \leqslant \lvert \pi _0 \rvert +1 =\lvert \pi \rvert $ .

Consider the case when the last inference in $\pi $ is an application of the rule $({\Box })$ with the principle formula $\Box A$ . We see that $\pi $ has the form

From the definition of the mapping $\mathsf {li}_{\:\Box A}$ , we obtain $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert =\lvert \pi _0 \rvert \leqslant \lvert \pi \rvert $ .

Cases of other inferences are treated similarly, so we omit them. We have that $\lvert \mathsf {li}_{\:\Box A}(\pi )\rvert \leqslant \lvert \pi \rvert $ for any $\pi \in \mathcal {P}$ . It remains to check that the mapping $ \mathsf {li}_{\:\Box A}$ is adequate.

Assume we have an $\infty $ -proof $\pi $ such that $\pi \in \mathcal {P}_n$ . We claim that $\mathsf {li}_{\:\Box A}(\pi )\in \mathcal {P}_n$ . If $n=0$ , then trivially $ \mathsf {li}_{\:\Box A}(\pi ) \in \mathcal {P}_0=\mathcal {P}$ . Suppose the root of $\pi $ is marked by a sequent $\Sigma \Rightarrow \Upsilon $ , where $\Box A \notin \Upsilon $ . Then we have $ \mathsf {li}_{\:\Box A}(\pi ) = \pi \in \mathcal {P}_n$ .

Otherwise, the assertion $\mathsf {li}_{\:\Box A}(\pi )\in \mathcal {P}_n$ is proved by induction on $\lvert \pi \rvert $ with the case analysis according to the definition of $\mathsf {li}_{\:\Box A}$ . If $\lvert \pi \rvert =0$ , then $\Sigma \Rightarrow \Upsilon $ is an initial sequent. We see that $\Sigma \Rightarrow A, \Upsilon \backslash \{\Box A \}$ is also an initial sequent and $\mathsf {li}_{\:\Box A}(\pi )$ was defined as the $\infty $ -proof consisting only of this sequent. We have $ \mathsf {li}_{\:\Box A}(\pi ) \in \mathcal {P}_n$ .

If the last inference in $\pi $ is an application of the rule $(\to _{\mathsf {R}})$ , then $\pi $ has the form

where $\pi _0\in \mathcal {P}_n$ . By the induction hypothesis for $\lvert \pi _0\rvert $ , we have $\mathsf {li}_{\:\Box A}(\pi _0)\in \mathcal {P}_n$ . From the definition of the mapping $\mathsf {li}_{\:\Box A}$ , we see $\mathsf {li}_{\:\Box A}(\pi )\in \mathcal {P}_n$ .

Consider the case when the last inference in $\pi $ is an application of the rule $({\Box })$ with the principle formula $\Box A$ . We see that $\pi $ has the form

where $\pi _0 \in \mathcal {P}_n$ and $\pi _1 \in \mathcal {P}_{n-1}$ . From the definition of the mapping $\mathsf {li}_{\:\Box A}$ , we obtain $\mathsf {li}_{\:\Box A}(\pi )=\pi _0 \in \mathcal {P}_n$ .

Notice that the last inference in $\pi $ differs from an application of the rule $(\mathsf {cut})$ . The remaining cases of other inferences are treated in a similar way to the case of $(\to _{\mathsf {R}})$ , so we omit them. □

Proof. Let us check that the set $\mathcal R_A$ is nonempty. Consider the mapping $\mathsf u_{cut}:\mathcal P^2\to \mathcal P$ that is defined as follows. For a cut pair $(\pi ,\tau )$ with the cut formula A, it joins the $\infty $ -proofs $\pi $ and $\tau $ with an appropriate instance of the rule $(\mathsf {cut})$ . For all other pairs, the mapping $\mathsf u_{cut}$ returns the first argument. Clearly, $\mathsf u_{cut}$ is nonexpansive and therefore lies in $\mathcal R_A$ .

The rest of the proof is completely analogous to the proof of Proposition 4.10 □

Proof. Given a cut pair with the cut formula p, consider the $\infty $ -proof obtained by applying the corresponding instance of the cut rule. This instance of cut can be eliminated by “moving” it upwards within the main fragment of the $\infty $ -proof. Therefore we can define the required p-removing mapping $\mathsf {re}_p$ following the standard cut reductions for cuts with atomic cut formulas.

Assume we have two $\infty $ -proofs $\pi $ and $\tau $ . If the pair $(\pi ,\tau )$ is not a cut pair or is a cut pair with the cut formula being not p, then we put $\mathsf {re}_{p}(\pi ,\tau )=\pi $ . Otherwise, we define $\mathsf {re}_{p}(\pi ,\tau )$ by induction on $\lvert \pi \rvert $ . Let the cut result of the pair $(\pi ,\tau )$ be $\Gamma \Rightarrow \Delta $ .

If $\lvert \pi \rvert =0$ , then $\Gamma \Rightarrow \Delta , p$ is an initial sequent. Suppose that $\Gamma \Rightarrow \Delta $ is also an initial sequent. Then $\mathsf {re}_{p}(\pi ,\tau )$ is defined as the $\infty $ -proof consisting only of the sequent $\Gamma \Rightarrow \Delta $ . If $\Gamma \Rightarrow \Delta $ is not an initial sequent, then $\Gamma $ has the form $p,\Phi $ , and $\tau $ is an $\infty $ -proof of the sequent $p,p,\Phi \Rightarrow \Delta $ . Applying the nonexpansive adequate mapping $\mathsf {acl}_p$ from Lemma 5.13, we put $\mathsf {re}_{p}(\pi ,\tau ) := \mathsf {acl}_p (\tau )$ .

Now suppose that $\lvert \pi \rvert>0$ . We define $\mathsf {re}_{p}(\pi ,\tau )$ according to the last application of an inference rule in $\pi $ :

In these cases $\infty $ -proofs $\mathsf {re}_p(\pi _0, \cdot )$ (and $\mathsf {re}_p(\pi _1, \cdot )$ ) are defined since $\lvert \pi _0 \rvert < \lvert \pi \rvert $ (and $\lvert \pi _1 \rvert < \lvert \pi \rvert $ ). Consider the last case when the last inference in $\pi $ is an application of the rule $(\Box )$ . We set

where $\mathsf {re}_p(\pi _0, \mathsf {li}_{\: \Box B}(\tau ))$ is defined since $\lvert \pi _0 \rvert < \lvert \pi \rvert $ . The mapping $\mathsf {re}_p$ is well-defined.

Now we claim that $\mathsf {re}_p$ is nonexpansive. It sufficient to check that for any pairs $(\pi ,\tau )$ and $(\pi ^\prime ,\tau ^\prime )$ , and any $n\in \mathbb N$ we have

$$ \begin{align*}\pi\sim_n\pi',\; \tau\sim_n\tau'\Rightarrow \mathsf{re}_p(\pi,\tau)\sim_n \mathsf{re}_p(\pi^\prime,\tau^\prime).\end{align*} $$

Assume we have two pairs of $\infty $ -proofs $(\pi ,\tau )$ and $(\pi ^\prime ,\tau ^\prime )$ such that $\pi \sim _n\pi '$ , $\tau \sim _n\tau '$ . If $n=0$ , then trivially $ \mathsf {re}_p(\pi ,\tau )\sim _n \mathsf {re}_p(\pi ^\prime ,\tau ^\prime )$ . If $n>0$ , then the main fragments of $\pi $ and $\pi ^\prime $ ( $\tau $ and $\tau ^\prime $ ) are identical. Suppose that $(\pi ,\tau )$ is not a cut pair or is a cut pair with the cut formula not being p. Then the same condition holds for the pair $(\pi ^\prime ,\tau ^\prime )$ . In this case, we have

$$ \begin{align*} \mathsf{re}_p(\pi,\tau) = \pi \sim_n \pi^\prime = \mathsf{re}_p(\pi^\prime,\tau^\prime).\end{align*} $$

Otherwise, $(\pi ,\tau )$ and $(\pi ^\prime ,\tau ^\prime )$ are cut pairs with the cut formula p. Now the statement $\mathsf {re}_p(\pi ,\tau )\sim _n \mathsf {re}_p(\pi ^\prime ,\tau ^\prime )$ is proved by induction on $\lvert \pi \rvert = \lvert \pi ^\prime \rvert $ with the case analysis according to the definition of $\mathsf {re}_p$ . Let the cut result of the pair $(\pi ,\tau )$ (and $(\pi ^\prime ,\tau ^\prime )$ ) be $\Gamma \Rightarrow \Delta $ .

If $\lvert \pi \rvert = \lvert \pi ^\prime \rvert =0$ , then $\Gamma \Rightarrow \Delta , p$ is an initial sequent. Suppose that $\Gamma \Rightarrow \Delta $ is an initial sequent. Then $\mathsf {re}_{p}(\pi ,\tau ) = \mathsf {re}_{p}(\pi ^\prime ,\tau ^\prime )$ . If $\Gamma \Rightarrow \Delta $ is not an initial sequent, then $\mathsf {re}_{p}(\pi ,\tau ) = \mathsf {acl}_p (\tau ) \sim _n \mathsf {acl}_p (\tau ^\prime ) = \mathsf {re}_{p}(\pi ^\prime ,\tau ^\prime )$ since the mapping $\mathsf {acl}_p $ is nonexpansive.

If the last inference in $\pi $ is an application of the rule $(\to _{\mathsf {R}})$ , then $\pi $ and $\pi ^\prime $ have the following forms

where $\pi _0 \sim _n \pi ^\prime _0$ . Since $\mathsf {i}_{B \to C}$ is nonexpansive, we have $\mathsf {i}_{B \to C}(\tau ) \sim _n \mathsf {i}_{B \to C}(\tau ^\prime )$ . Consequently, by the induction hypothesis for pairs $(\pi _0, \mathsf {i}_{B \to C}(\tau ))$ and $(\pi ^\prime _0, \mathsf {i}_{B \to C}(\tau ^\prime ))$ , we have $\mathsf {re}_p(\pi _0, \mathsf {i}_{B \to C}(\tau )) \sim _n \mathsf {re}_p(\pi ^\prime _0, \mathsf {i}_{B \to C}(\tau ^\prime ))$ . Thus we obtain $\mathsf {re}_p(\pi ,\tau )\sim _n \mathsf {re}_p(\pi ^\prime ,\tau ^\prime )$ .

Consider the case when the last inference in $\pi $ is an application of the rule $({\Box })$ . We have that $\pi $ and $\pi ^\prime $ have the following forms

where $\pi _0 \sim _n \pi ^\prime _0$ and $\pi _1 \sim _{n-1} \pi ^\prime _1$ . Since $\mathsf {li}_{\: \Box B}$ is nonexpansive, we have $\mathsf {li}_{\: \Box B}(\tau ) \sim _n \mathsf {li}_{\: \Box B}(\tau ^\prime )$ . Consequently, by the induction hypothesis for pairs $(\pi _0, \mathsf {li}_{\: \Box B}(\tau ))$ and $(\pi ^\prime _0, \mathsf {li}_{\: \Box B}(\tau ^\prime ))$ , we have $\mathsf {re}_p(\pi _0, \mathsf {li}_{\: \Box B}(\tau )) \sim _n \mathsf {re}_p(\pi ^\prime _0, \mathsf {li}_{\: \Box B}(\tau ^\prime ))$ . Thus we obtain $\mathsf {re}_p(\pi ,\tau )\sim _n \mathsf {re}_p(\pi ^\prime ,\tau ^\prime )$ .

All the other cases are treated similarly, so we omit them. We have that the mapping $\mathsf {re}_p$ is nonexpansive. It remains to check that the mapping $\mathsf {re}_p$ is adequate.

Assume we have a pair of $\infty $ -proofs $(\pi ,\tau )$ such that $\pi \in \mathcal {P}_n$ and $\tau \in \mathcal {P}_n $ . We claim that $\mathsf {re}_p(\pi ,\tau ) \in \mathcal {P}_n$ . If $n=0$ , then trivially $ \mathsf {re}_p(\pi ,\tau ) \in \mathcal {P}_0=\mathcal {P}$ . If the pair $(\pi ,\tau )$ is not a cut pair or is a cut pair with the cut formula being not p, then we have $ \mathsf {re}_p(\pi ,\tau ) = \pi \in \mathcal {P}_n$ .

Now suppose $(\pi ,\tau )$ is a cut pair with the cut formula p and $n>0$ . We proceed by induction on $\lvert \pi \rvert $ with the case analysis according to the definition of $\mathsf {re}_p$ . Let the cut result of the pair $(\pi ,\tau )$ be $\Gamma \Rightarrow \Delta $ .

If $\lvert \pi \rvert = 0$ , then $\Gamma \Rightarrow \Delta , p$ is an initial sequent. Suppose that $\Gamma \Rightarrow \Delta $ is an initial sequent. Then $\mathsf {re}_{p}(\pi ,\tau ) \in \mathcal {P}_n$ by the definition of $\mathsf {re}_{p}$ . If $\Gamma \Rightarrow \Delta $ is not an initial sequent, then $\mathsf {re}_{p}(\pi ,\tau ) = \mathsf {acl}_p (\tau )\in \mathcal {P}_n$ since the mapping $\mathsf {acl}_p $ is adequate.

Now let us consider the cases of inference rules $(\to _{\mathsf {L}})$ and $({\Box })$ . If the last inference in $\pi $ is an application of the rule $(\to _{\mathsf {L}})$ , then $\pi $ has the following form

where $\pi _0, \pi _1 \in \mathcal {P}_n$ . Since $\mathsf {li}_{B \to C}$ and $\mathsf {ri}_{B \to C}$ are adequate, we have $\mathsf {li}_{B \to C}(\tau )\in \mathcal {P}_n$ and $\mathsf {ri}_{B \to C}(\tau ) \in \mathcal {P}_n$ . Consequently, by the induction hypothesis for the pairs $(\pi _0, \mathsf {li}_{B \to C}(\tau ))$ and $(\pi _1, \mathsf {ri}_{B \to C}(\tau ))$ , we have $\mathsf {re}_p(\pi _0, \mathsf {li}_{B \to C}(\tau ))\in \mathcal {P}_n$ and $\mathsf {re}_p(\pi _1, \mathsf {ri}_{B \to C}(\tau ))\in \mathcal {P}_n$ . Thus we obtain $\mathsf {re}_p(\pi ,\tau )\in \mathcal {P}_n$ .

Consider the case when the last inference in $\pi $ is an application of the rule $({\Box })$ . Then $\pi $ has the form

where $\pi _0 \in \mathcal {P}_n$ and $\pi _1 \in \mathcal {P}_{n-1}$ . Since $\mathsf {li}_{\: \Box B}$ is adequate, we have $\mathsf {li}_{\: \Box B}(\tau ) \in \mathcal {P}_n$ . Consequently, by the induction hypothesis for the pair $(\pi _0, \mathsf {li}_{\: \Box B}(\tau ))$ , we have $\mathsf {re}_p(\pi _0, \mathsf {li}_{\: \Box B}(\tau )) \in \mathcal {P}_n$ . Thus we obtain $\mathsf {re}_p(\pi ,\tau )\in \mathcal {P}_n$ .

Notice that the last inference in $\pi $ differs from an application of the rule $(\mathsf {cut})$ . The remaining cases of inference rules $(\to _{\mathsf {R}})$ and $(\mathsf {refl})$ are treated in a similar way to the case of $(\to _{\mathsf {L}})$ , so we omit them. □

Proof. Given a cut pair with the cut formula $\Box B$ , consider the $\infty $ -proof obtained by applying the corresponding instance of the cut rule. By ordinary cut reductions we can “move” it upwards within the $\infty $ -proof arbitrarily high through the fragments. The desired result of applying the $\Box B$ -removing operator can be viewed as the limit of this procedure. To do it accurately we define the mapping $\mathsf {re}_{\Box B}$ as the fixed-point of a contractive operator $\mathsf G_{\Box B} \colon \mathcal R_{\Box B} \to \mathcal R_{\Box B}$ .

For a mapping $\mathsf u\in \mathcal R_{\Box B}$ and a pair of $\infty $ -proofs $(\pi ,\tau )$ , the $\infty $ -proof $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )$ is defined as follows. If $(\pi ,\tau )$ is not a cut pair or a cut pair with the cut formula being not $\Box B$ , then we put $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )=\pi $ .

Now let $(\pi ,\tau )$ be a cut pair with the cut formula $\Box B$ and the cut result $\Gamma \Rightarrow \Delta $ . If $\lvert \pi \rvert =0$ or $\lvert \tau \rvert =0$ , then $\Gamma \Rightarrow \Delta $ is an initial sequent. In this case, we define $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )$ as the $\infty $ -proof consisting only of the sequent $\Gamma \Rightarrow \Delta $ .

Suppose that $\lvert \pi \rvert>0$ and $\lvert \tau \rvert>0$ . We define $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )$ according to the last application of an inference rule in $\pi $ :

Consider the case when $\pi $ has the form

We define $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )$ according to the last application of an inference rule in $\tau $ . If the last inference is an application of the rule $\mathsf {(refl)}$ with the principal formula being not $\Box B$ or is an application of the rule ${(\Box )}$ without the formula $\Box B$ in the right premise, then $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )$ is defined similarly to the previous cases of $\mathsf {(refl)}$ and $({\Box })$ . Cases of inference rules $(\to _{\mathsf {L}})$ , $(\to _{\mathsf {R}})$ , and $\mathsf {(cut)}$ are also completely similar to the previous cases of $(\to _{\mathsf {L}})$ , $(\to _{\mathsf {R}})$ , and $\mathsf {(cut)}$ .

If the last application of an inference rule in $\tau $ is an application of the rule $\mathsf {(refl)}$ with the principal formula $\Box B$ , then we put

It remains to consider the crucial case when $\tau $ has the form

We define $\mathsf G_{\Box B}(\mathsf u)(\pi , \tau )$ as

where $\pi '$ equals

Notice that $\Phi ^\prime , \Box \Pi ^\prime =\Phi ,\Box \Pi $ and $\Box C, \Sigma ^\prime =\Sigma $ , and $\Box \Pi ^\prime \backslash \Box \Pi ,\Box \Pi =\Box \Pi \backslash \Box \Pi ^\prime ,\Box \Pi ^\prime $ .

Now the operator $\mathsf G_{\Box B}$ is well-defined. By the case analysis according to the definition of $\mathsf G_{\Box B}$ , we see that $\mathsf G_{\Box B} (\mathsf u) $ is nonexpansive and belongs to $\mathcal R_{\Box B}$ whenever $\mathsf u \in \mathcal R_{\Box B}$ .

We claim that $\mathsf G_{\Box B}$ is contractive. It sufficient to check that for any $\mathsf u, \mathsf v\in \mathcal R_{\Box B}$ and any $n,k\in \mathbb N$ we have

$$ \begin{align*}\mathsf u\sim_{n,k}\mathsf v \Rightarrow \mathsf G_{\Box B}(\mathsf u)\sim_{n,k+1}\mathsf G_{\Box B}(\mathsf v).\end{align*} $$

Assume there are two $\Box B$ -removing mappings $\mathsf u$ and $\mathsf v$ such that $\mathsf u\sim _{n,k}\mathsf v$ . Consider an arbitrary pair of $\infty $ -proofs $(\pi ,\tau )$ . By the case analysis according to the definition of $\mathsf G_{\Box B}$ , we prove that $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\sim _{n}\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ . In addition, we check that if $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ , then $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\sim _{n+1}\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ .

If the pair $(\pi ,\tau )$ is not a cut pair or is a cut pair with the cut formula being not $\Box B$ , then we have $ \mathsf G_{\Box B}(\mathsf u)(\pi ,\tau ) = \pi =\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ . Otherwise, consider last inferences in $\pi $ and $\tau $ .

Suppose that the $\infty $ -proof $\pi $ has the form

Then we have $\mathsf {u}(\pi _0, \mathsf {wk}_{ C; \emptyset } (\tau ))\sim _n \mathsf {v}(\pi _0, \mathsf {wk}_{ C; \emptyset } (\tau ))$ . Hence, $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\sim _{n}\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ .

In addition, if $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ , then $\lvert \pi _0\rvert +\lvert \mathsf {wk}_{ C; \emptyset } (\tau )\lvert <k$ . Thus, $\mathsf {u}(\pi _0, \mathsf {wk}_{ C; \emptyset } (\tau ))\sim _{n+1} \mathsf {v}(\pi _0, \mathsf {wk}_{ C; \emptyset } (\tau ))$ . We obtain that $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\sim _{n+1}\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ .

Now let us consider the case when $\pi $ and $\tau $ have the forms

We see that $\mathsf {u}(\mathsf {wk}_{B;\emptyset }(\pi ),\tau _0) \sim _n \mathsf {v}(\mathsf {wk}_{B;\emptyset }(\pi ),\tau _0)$ . Since the mapping $\mathsf {re}_{B}$ is nonexpansive, we have

$$ \begin{align*}\mathsf G_{\Box B}(\mathsf u)(\pi,\tau) = \mathsf{re}_{B}(\pi_0,\mathsf{u}(\mathsf{wk}_{B;\emptyset}(\pi),\tau_0)) \sim_n \mathsf{re}_{B}(\pi_0,\mathsf{v}(\mathsf{wk}_{B;\emptyset}(\pi),\tau_0)) = \mathsf G_{\Box B}(\mathsf v)(\pi,\tau).\end{align*} $$

In addition, if $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ , then $\lvert \mathsf {wk}_{B;\emptyset }(\pi )\rvert +\lvert \tau _0\lvert <k$ . Consequently, $\mathsf {u}(\mathsf {wk}_{B;\emptyset }(\pi ),\tau _0) \sim _{n+1} \mathsf {v}(\mathsf {wk}_{B;\emptyset }(\pi ),\tau _0)$ . Thus, we have

$$ \begin{align*}\mathsf G_{\Box B}(\mathsf u)(\pi,\tau) = \mathsf{re}_{B}(\pi_0,\mathsf{u}(\mathsf{wk}_{B;\emptyset}(\pi),\tau_0)) \sim_{n+1} \mathsf{re}_{B}(\pi_0,\mathsf{v}(\mathsf{wk}_{B;\emptyset}(\pi),\tau_0)) = \mathsf G_{\Box B}(\mathsf v)(\pi,\tau).\end{align*} $$

Let us consider the main case when $\pi $ and $\tau $ have the forms

We have $\mathsf {u}\left (\pi ',\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1)\right )\sim _n\mathsf {v}\left (\pi ',\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1)\right )$ , and $\mathsf {u}(\mathsf {li}_{\Box C}(\pi ),\tau _0)\sim _{n}\mathsf {v}(\mathsf {li}_{\Box C}(\pi ),\tau _0)$ . Hence, $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\sim _{n}\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ .

If $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ , then $\mathsf {u}\left (\pi ',\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1)\right )\sim _n\mathsf {v}\left (\pi ',\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1)\right )$ and $\mathsf {u}(\mathsf {li}_{\Box C}(\pi ),\tau _0)\sim _{n+1}\mathsf {v}(\mathsf {li}_{\Box C}(\pi ),\tau _0)$ , because $\lvert \mathsf {li}_{\Box C}(\pi )\rvert +\lvert \tau _0\rvert < k$ . We obtain $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\sim _{n+1}\mathsf G_{\Box B}(\mathsf v)(\pi ,\tau )$ .

All the other cases of lowermost inferences in $\pi $ and $\tau $ are treated similarly, so we omit them. We have that the operator $\mathsf {G}_{\Box \mathsf {B}}$ is contractive.

Now we define the required $\Box B$ -removing mapping $\mathsf {re}_{\Box B}$ as the fixed-point of the the operator $\mathsf G_{\Box B} \colon \mathcal R_{\Box B} \to \mathcal R_{\Box B}$ , which exists by Lemma 6.14

It remains to check that the mapping $\mathsf {re}_{\Box B}$ is adequate. For any $n,k\in \mathbb N$ , let us call a mapping $\mathsf u\in \mathcal R_{\Box B} (n,k)$ -adequate if it satisfies the following two conditions: $\mathsf u(\pi ,\tau )\in \mathcal P_i$ for any $i\leqslant n$ and any $\pi , \tau \in \mathcal P_i$ ; $\mathsf u(\pi ,\tau )\in \mathcal P_{n+1}$ whenever $\pi , \tau \in \mathcal P_{n+1}$ and $\lvert \pi \rvert + \lvert \tau \rvert <k$ .

We claim that $\mathsf G_{\Box B}(\mathsf u)$ is $(n,k+1)$ -adequate whenever $\mathsf {u}$ is a $(n,k)$ -adequate mapping from $\mathcal R_{\Box B}$ . Consider an arbitrary pair of $\infty $ -proofs $(\pi ,\tau )$ and an $(n,k)$ -adequate mapping $\mathsf u\in \mathcal R_{\Box B}$ . By the case analysis according to the definition of $\mathsf {G}_{\Box \mathsf {B}}$ , we prove that $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal {P}_i$ if $i\leqslant n$ and $\pi , \tau \in \mathcal P_i$ . In addition, we check that $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal P_{n+1}$ if $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ and $\pi , \tau \in \mathcal P_{n+1}$ .

If the pair $(\pi ,\tau )$ is not a cut pair or is a cut pair with the cut formula being not $\Box B$ , then we have $ \mathsf G_{\Box B}(\mathsf u)(\pi ,\tau ) = \pi $ . In this case, the required statements trivially hold. Otherwise, consider last inferences in $\pi $ and $\tau $ .

Suppose that the $\infty $ -proof $\pi $ has the form

Since the mapping $\mathsf {i}_{ C\to D}$ is adequate, we have $\mathsf {u}(\pi _0, \mathsf {i}_{ C\to D} (\tau ))\in \mathcal {P}_i$ whenever $i\leqslant n$ and $\pi , \tau \in \mathcal P_i$ . In this case, we see that $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal P_{i}$ .

If $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ , then $\lvert \pi _0\rvert +\lvert \mathsf {i}_{ C\to D}(\tau )\lvert <k$ . Thus, $\mathsf {u}(\pi _0, \mathsf {i}_{ C\to D} (\tau ))\in \mathcal P_{n+1}$ whenever $\pi , \tau \in \mathcal P_{n+1}$ . We obtain that $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal P_{n+1}$ .

Suppose that $\pi $ and $\tau $ have the forms

Trivially, $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal P_{0} = \mathcal {P}$ . Thus consider the case when $\pi , \tau \in \mathcal {P}_i$ for some $0<i \leqslant n$ . Then we see that $\pi _0, \tau _0 \in \mathcal {P}_i$ and $\pi _1, \tau _1 \in \mathcal {P}_{i-1}$ . Since the mapping $\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }$ and $\mathsf {li}_{\Box C}$ are adequate, we have $\mathsf {u}(\mathsf {li}_{\Box C}(\pi ),\tau _0)\in \mathcal {P}_i$ and $\mathsf {u}\left (\pi ',\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1)\right )\in \mathcal {P}_{i-1}$ . Hence, $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal {P}_i$ .

If $\lvert \pi \rvert +\lvert \tau \lvert <k+1$ and $\pi ,\tau \in \mathcal {P}_{n+1}$ , then $\lvert \mathsf {li}_{\Box C}(\pi ) \rvert + \lvert \tau _0 \rvert <k$ and $\mathsf {u}(\mathsf {li}_{\Box C}(\pi ),\tau _0)\in \mathcal {P}_{n+1}$ . Also, we see that $\pi '\in \mathcal {P}_n$ and $\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1) \in \mathcal {P}_n$ . Hence, $\mathsf {u}\left (\pi ',\mathsf {wk}_{\Box \Pi \backslash \Box \Pi ^\prime ;\emptyset }(\tau _1)\right )\in \mathcal {P}_{n}$ . We obtain $\mathsf G_{\Box B}(\mathsf u)(\pi ,\tau )\in \mathcal {P}_{n+1}$ .

We omit other cases of lowermost inferences in $\pi $ and $\tau $ , because they are treated similarly.

We established that $\mathsf G_{\Box B}(\mathsf u)$ is $(n,k+1)$ -adequate for any $(n,k)$ -adequate $\mathsf u\in \mathcal R_{\Box B}$ . Notice that if a mapping $\mathsf {u} $ is $(n,k)$ -adequate for all $k\in \mathbb N$ , then it is also $(n+1,0)$ -adequate. Now by induction on n with a subinduction on k, we immediately obtain that the mapping $\mathsf {re}_{\Box B}$ , which is a fixed-point of $\mathsf G_{\Box B}$ , is $(n,k)$ -adequate for all $n,k\in \mathbb N$ . Therefore the mapping $\mathsf {re}_{\Box B}$ is adequate. □

Proof. We define $\mathsf {re}_A$ by induction on the structure of the formula $A $ .

Case 1: A has the form p. In this case, $\mathsf {re}_{p} $ is defined by Lemma 6.15.

Case 2: A has the form $\bot $ . Then we put $\mathsf {re}_{\bot }(\pi ,\tau ):= \mathsf {i}_\bot (\pi )$ , where $\mathsf {i}_\bot $ is the nonexpansive adequate mapping from Lemma 5.12.

Case 3: A has the form $B\to C$ . Then we put

$$ \begin{align*}\mathsf{re}_{B \to C}(\pi,\tau):=\mathsf{re}_C(\mathsf{re}_B(\mathsf{wk}_{\emptyset; C}(\mathsf{ri}_{B\to C}(\tau)),\mathsf{i}_{B\to C}(\pi)),\mathsf{li}_{B\to C}(\tau)),\end{align*} $$

where $\mathsf {ri}_{B \to C}$ , $\mathsf {i}_{B \to C}$ , $\mathsf {li}_{B \to C}$ are the nonexpansive adequate mappings from Lemma 5.12 and $\mathsf {wk}_{\emptyset ; C}$ is the nonexpansive adequate mapping from Lemma 5.11.

Case 4: A has the form $\Box B$ . By the induction hypothesis, there is an adequate B-removing mapping $\mathsf {re}_B$ . The required $\Box B$ -removing mapping $\mathsf {re}_{\Box B}$ exists by Lemma 6.16. □

Proof. The space is obviously nonempty, since the identity function lies in $\mathcal T$ . The proof is analogous to the proof of Proposition 4.10 □

Proof. We construct the required cut-elimination mapping $\mathsf {ce}$ so it commutes with every application of inference rules except $\mathsf {(cut)}$ and satisfies the following condition:

In order to do this, we define a contractive operator $\mathsf F \colon \mathcal T \to \mathcal T$ and obtain the mapping $\mathsf {ce}$ as the fixed-point of $\mathsf F$ .

For a mapping $\mathsf u\in \mathcal T$ and an $\infty $ -proof $\pi $ , the $\infty $ -proof $\mathsf F(\mathsf u)(\pi )$ is defined as follows. If $\lvert \pi \rvert =0$ , then we define $\mathsf F(\mathsf u)(\pi )$ to be $\pi $ .

Otherwise, we define $\mathsf F(\mathsf u)(\pi )$ according to the last application of an inference rule in $\pi $ :

Now the operator $\mathsf F$ is well-defined. By the case analysis according to the definition of $\mathsf F$ , we see that $\mathsf F (\mathsf u) $ is nonexpansive and belongs to $\mathcal T$ whenever $\mathsf u \in \mathcal T$ .

We claim that $\mathsf {F}$ is contractive. It sufficient to check that for any $\mathsf u, \mathsf v\in \mathcal T$ and any $n,k\in \mathbb N$ we have

$$ \begin{align*}\mathsf u\sim_{n,k}\mathsf v \Rightarrow \mathsf {F(u)}\sim_{n,k+1}\mathsf{F(v)}.\end{align*} $$

Assume there are mappings $\mathsf u$ and $\mathsf v$ from $\mathcal {T}$ such that $\mathsf u\sim _{n,k}\mathsf v$ . Consider an arbitrary $\infty $ -proof $\pi $ . By the case analysis according to the definition of $\mathsf {F}$ , we prove that $\mathsf F(\mathsf u)(\pi )\sim _{n}\mathsf F(\mathsf v)(\pi )$ . In addition, we check that if $\lvert \pi \rvert <k+1$ , then $\mathsf F(\mathsf u)(\pi )\sim _{n+1}\mathsf F(\mathsf v)(\pi )$ .

Let us consider the case when $\pi $ has the form

We have $\mathsf u(\pi _0) \sim _n \mathsf v(\pi _0)$ and $\mathsf u(\pi _1) \sim _n \mathsf v(\pi _1)$ . Thus, $F(\mathsf u)(\pi ) \sim _n F(\mathsf v)(\pi )$ .

If $\lvert \pi \rvert <k+1$ , then $\lvert \pi _0\rvert <k$ . We have $\mathsf u(\pi _0) \sim _{n+1} \mathsf v(\pi _0)$ and $\mathsf u(\pi _1) \sim _n \mathsf v(\pi _1)$ . Hence, $F(\mathsf u)(\pi ) \sim _{n+1} F(\mathsf v)(\pi )$ .

Now consider the case when $\pi $ has the form

We have $\mathsf u(\pi _0) \sim _n \mathsf v(\pi _0)$ and $\mathsf u(\pi _1) \sim _n \mathsf v(\pi _1)$ . Since the mapping $\mathsf {re}_A$ is nonexpansive, we see that

$$ \begin{align*}F(\mathsf u)(\pi) = \mathsf {re}_A(\mathsf u(\pi_0),\mathsf u(\pi_1)) \sim_n \mathsf {re}_A(\mathsf v(\pi_0),\mathsf v(\pi_1))= F(\mathsf v)(\pi).\end{align*} $$

Moreover, if $\lvert \pi \rvert <k+1$ , then $\lvert \pi _0\rvert <k$ and $\lvert \pi _1\rvert <k$ . From the assumption $\mathsf u\sim _{n,k}\mathsf v$ , we obtain $\mathsf u(\pi _0) \sim _{n+1} \mathsf v(\pi _0)$ and $\mathsf u(\pi _1) \sim _{n+1} \mathsf v(\pi _1)$ . Hence,

$$ \begin{align*}F(\mathsf u)(\pi) = \mathsf {re}_A(\mathsf u(\pi_0),\mathsf u(\pi_1)) \sim_{n+1} \mathsf {re}_A(\mathsf v(\pi_0),\mathsf v(\pi_1))= F(\mathsf v)(\pi).\end{align*} $$

Other cases are straightforward, so we omit them. We have that the operator $\mathsf {F}$ is contractive.

Now we define the required cut-elimination mapping $\mathsf {ce}$ as the fixed-point of the the operator $\mathsf F \colon \mathcal T \to \mathcal T$ , which exists by Lemma 6.18

For any $n,k\in \mathbb N$ , let us call a mapping $\mathsf u\in \mathcal T (n,k)$ -free if it satisfies the following two conditions: $\mathsf u(\pi )\in \mathcal P_n$ for any $\pi \in \mathcal P$ ; $\mathsf u(\pi )\in \mathcal P_{n+1}$ whenever $\lvert \pi \rvert <k$ .

We claim that $F(\mathsf u)$ is $(n,k+1)$ -free whenever $\mathsf {u}$ is an $(n,k)$ -free mapping from $\mathcal T$ . Consider an arbitrary $\infty $ -proof $\pi $ and an $(n,k)$ -free mapping $\mathsf u\in \mathcal T$ . By the case analysis according to the definition of $\mathsf {F}$ , we prove that $F(\mathsf u)(\pi )\in \mathcal {P}_n$ . In addition, we check that $\mathsf F(\mathsf u)(\pi )\in \mathcal P_{n+1}$ if $\lvert \pi \rvert <k+1$ .

Let us consider the case when $\pi $ has the form

We have $\mathsf u(\pi _0) ,\mathsf u(\pi _1) \in \mathcal {P}_n$ . Hence, $F(\mathsf u)(\pi ) \in \mathcal {P}_n$ .

If $\lvert \pi \rvert <k+1$ , then $\lvert \pi _0\rvert <k$ . We have $\mathsf u(\pi _0) \in \mathcal {P}_{n+1}$ and $\mathsf u(\pi _1) \in \mathcal {P}_n$ . Hence, $F(\mathsf u)(\pi ) \in \mathcal {P}_{n+1}$ .

Now we consider the case when $\pi $ has the form

We have $\mathsf u(\pi _0) ,\mathsf u(\pi _1) \in \mathcal {P}_n$ . Since the mapping $\mathsf {re}_A$ is adequate, we see that $F(\mathsf u)(\pi ) = \mathsf {re}_A(\mathsf u(\pi _0),\mathsf u(\pi _1)) \in \mathcal {P}_n$ .

If $\lvert \pi \rvert <k+1$ , then $\lvert \pi _0\rvert <k$ and $\lvert \pi _1\rvert <k$ . We obtain $\mathsf u(\pi _0), \mathsf {u}(\pi _1) \in \mathcal {P}_{n+1}$ . Hence, $F(\mathsf u)(\pi ) = \mathsf {re}_A(\mathsf u(\pi _0),\mathsf u(\pi _1))\in \mathcal {P}_{n+1}$ .

We omit the other cases of the lowermost inferences in $\pi $ , because they are trivial.

We established that $\mathsf F(\mathsf u)$ is $(n,k+1)$ -free for any $(n,k)$ -free $\mathsf u\in \mathcal T$ . Notice that if a mapping $\mathsf {u} $ is $(n,k)$ -free for all $k\in \mathbb N$ , then it is also $(n+1,0)$ -free. Now by induction on n with a subinduction on k, we immediately obtain that the mapping $\mathsf {ce}$ , which is a fixed-point of $\mathsf F$ , is $(n,k)$ -free for all $n,k\in \mathbb N$ . Therefore, for any $\infty $ -proof $\pi $ , the $\infty $ -proof $\mathsf {ce}(\pi )$ does not contain instances of the rule $\mathsf {(cut)}$ .

Now assume $\mathsf {Grz}_{\infty } +\mathsf {cut}\vdash \Gamma \Rightarrow \Delta $ . Take an $\infty $ -proof of the sequent $\Gamma \Rightarrow \Delta $ in the system $\mathsf {Grz}_{\infty } +\mathsf {cut}$ and apply the mapping $\mathsf {ce}$ to it. We obtain an $\infty $ -proof of the same sequent in the system $\mathsf {Grz}_{\infty }$ .□

Proof. Assume $\pi $ is an $\infty $ -proof of the sequent $\Gamma _1,\Gamma _2\Rightarrow \Delta _1,\Delta _2$ in $\mathsf {Grz}_\infty $ and $\Lambda _1$ , $\Lambda _2$ are finite sets of formulas. We prove the statement of the lemma by induction on the sum of cardinalities $\mathit {card}(Sub(\Gamma _1\Rightarrow \Delta _1)\backslash \Lambda _1 )+\mathit {card}( Sub(\Gamma _2\Rightarrow \Delta _2)\backslash \Lambda _2)$ with a subinduction on $\lvert \pi \rvert $ .

Suppose $\lvert \pi \rvert =0$ . Then $\Gamma _1,\Gamma _2\Rightarrow \Delta _1,\Delta _2$ is an initial sequent. If $\Gamma _1\Rightarrow \Delta _1$ ( $\Gamma _2\Rightarrow \Delta _2$ ) is an initial sequent, then we put $I:= \bot $ ( $I:= \top $ ). Otherwise, we have an atomic proposition p such that $p \in \Gamma _1$ and $p\in \Delta _2$ ( $p \in \Gamma _2$ and $p\in \Delta _1$ ). In this case, we put $I:= p$ ( $I:= \neg p$ ).

Now consider the last application of an inference rule in $\pi $ .

Case 1. Suppose that $\pi $ has the form

where $A\to B,\Sigma = \Delta _1, \Delta _2$ . Notice that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . If $A \to B \in \Delta _1$ ( $A \to B \in \Delta _2$ ), then we put $\Gamma ^\prime _1:= \Gamma _1 \cup \{A\}$ ; $\Delta ^\prime _1:= (\Delta _1\backslash \{A\to B\})\cup \{B\}$ ; $\Gamma ^\prime _2:=\Gamma _2$ ; $\Delta ^\prime _2:=\Delta _2$ ( $\Gamma ^\prime _2:= \Gamma _2 \cup \{A\}$ ; $\Delta ^\prime _2:= (\Delta _2\backslash \{A\to B\})\cup \{B\}$ ; $\Gamma ^\prime _1:=\Gamma _1$ ; $\Delta ^\prime _1:=\Delta _1$ ). We see that $\pi ^\prime $ is an $\infty $ -proof of the sequent $\Gamma ^\prime _1,\Gamma ^\prime _2\Rightarrow \Delta ^\prime _1,\Delta ^\prime _2$ in $\mathsf {Grz}_\infty $ . By the induction hypothesis for $\pi ^\prime $ , $\Lambda _1$ and $\Lambda _2$ , there is a corresponding interpolant $I^\prime $ . We set $I:=I^\prime $ .

Case 2. Suppose that $\pi $ has the form

where $\Sigma , A\to B = \Gamma _1,\Gamma _2$ . We see that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . If $A \to B \in \Gamma _1$ ( $A \to B \in \Gamma _2$ ), then we put $\Gamma ^\prime _1:= (\Gamma _1 \backslash \{A\to B\})\cup \{B\}$ ; $\Gamma ^{\prime \prime }_1:= \Gamma _1 \backslash \{A\to B\}$ ; $\Delta ^\prime _1:= \Delta _1 $ ; $\Delta ^{\prime \prime }_1:= \Delta _1 \cup \{A\}$ ; $\Gamma ^\prime _2:=\Gamma _2$ ; $\Gamma ^{\prime \prime }_2:=\Gamma _2$ ; $\Delta ^\prime _2:=\Delta _2$ ; $\Delta ^{\prime \prime }_2:=\Delta _2$ ( $\Gamma ^\prime _2:= (\Gamma _2 \backslash \{A\to B\})\cup \{B\}$ ; $\Gamma ^{\prime \prime }_2:= \Gamma _2 \backslash \{A\to B\}$ ; $\Delta ^\prime _2:= \Delta _2 $ ; $\Delta ^{\prime \prime }_2:= \Delta _2 \cup \{A\}$ ; $\Gamma ^\prime _1:=\Gamma _1$ ; $\Gamma ^{\prime \prime }_1:=\Gamma _1$ ; $\Delta ^\prime _1:=\Delta _1$ ; $\Delta ^{\prime \prime }_1:=\Delta _1$ ). We see that $\pi ^\prime $ and $\pi ^{\prime \prime }$ are $\infty $ -proofs of $\Gamma ^\prime _1,\Gamma ^\prime _2\Rightarrow \Delta ^\prime _1,\Delta ^\prime _2$ and $\Gamma ^{\prime \prime }_1,\Gamma ^{\prime \prime }_2\Rightarrow \Delta ^{\prime \prime }_1,\Delta ^{\prime \prime }_2$ in $\mathsf {Grz}_\infty $ . By the induction hypothesis for $\pi ^\prime $ , $\Lambda _1$ and $\Lambda _2$ , there is an interpolant $I^\prime $ . Analogously, by the induction hypothesis for $\pi ^{\prime \prime }$ , $\Lambda _1$ and $\Lambda _2$ , there is an interpolant $I^{\prime \prime }$ . If $A \to B \in \Gamma _1$ , then we set $I:=I^\prime \vee I^{\prime \prime }$ . Otherwise, when $A \to B \in \Gamma _2$ , we set $I:=I^\prime \wedge I^{\prime \prime }$ .

Case 3. Suppose that $\pi $ has the form

where $\Sigma , \Box A = \Gamma _1,\Gamma _2$ . If $\Box A \in \Gamma _1$ ( $\Box A \in \Gamma _2$ ), then we put $\Gamma ^\prime _1:= \Gamma _1 \cup \{A\}$ ; $\Delta ^\prime _1:= \Delta _1$ ; $\Gamma ^\prime _2:=\Gamma _2$ ; $\Delta ^\prime _2:=\Delta _2$ ( $\Gamma ^\prime _2:= \Gamma _2 \cup \{A\}$ ; $\Delta ^\prime _2:= \Delta _2$ ; $\Gamma ^\prime _1:=\Gamma _1$ ; $\Delta ^\prime _1:=\Delta _1$ ). We see that $\pi ^\prime $ is an $\infty $ -proof of the sequent $\Gamma ^\prime _1,\Gamma ^\prime _2\Rightarrow \Delta ^\prime _1,\Delta ^\prime _2$ in $\mathsf {Grz}_\infty $ . By the induction hypothesis for $\pi ^\prime $ , $\Lambda _1$ and $\Lambda _2$ , there is a corresponding interpolant $I^\prime $ . We set $I:=I^\prime $ .

Case 4. Suppose that $\pi $ has the form

where $\Phi , \Box \Pi = \Gamma _1, \Gamma _2$ and $\Box A, \Sigma =\Delta _1, \Delta _2$ .

Subcase 4.1: the formula $\Box A \in \Delta _1$ and $A \in \Lambda _1 $ ( $\Box A \in \Delta _2$ and $A \in \Lambda _2$ ). We see that $\lvert \pi ^\prime \rvert < \lvert \pi \rvert $ . We put $\Gamma ^\prime _1:= \Gamma _1 $ ; $\Delta ^\prime _1:= (\Delta _1 \backslash \{\Box A\}) \cup \{A\} $ ; $\Gamma ^\prime _2:=\Gamma _2$ ; $\Delta ^\prime _2:=\Delta _2$ ( $\Gamma ^\prime _2:= \Gamma _2 $ ; $\Delta ^\prime _2:= (\Delta _2 \backslash \{\Box A\}) \cup \{A\} $ ; $\Gamma ^\prime _1:=\Gamma _1$ ; $\Delta ^\prime _1:=\Delta _1$ ). We see that $\pi ^\prime $ is an $\infty $ -proof of the sequent $\Gamma ^\prime _1,\Gamma ^\prime _2\Rightarrow \Delta ^\prime _1,\Delta ^\prime _2$ in $\mathsf {Grz}_\infty $ . By the induction hypothesis for $\pi ^\prime $ , $\Lambda _1$ and $\Lambda _2$ , there is a corresponding interpolant $I^\prime $ such that

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_1^\ast \cup\Gamma^\prime_1\rightarrow\bigvee\Delta^\prime_1 \cup \{ I^\prime\} \quad \text{and} \quad\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup\{ I^\prime\} \cup \Gamma^\prime_2\rightarrow\bigvee\Delta^\prime_2\:.\end{align*}$$

If $\Box A \in \Delta _1$ and $A \in \Lambda _1 $ , then $\Box (A \to \Box A) \in \Lambda _1^\ast $ . Thus we have $\mathsf {Grz} \vdash \bigwedge \Lambda _1^\ast \rightarrow (A \to \Box A)$ . It follows that we can replace the formula A in $\Delta ^\prime _1$ by $\Box A$ and obtain

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_1^\ast \cup\Gamma^\prime_1\rightarrow\bigvee\Delta_1 \cup \{ I^\prime \} \:.\end{align*}$$

Note also that $\Gamma ^\prime _1:= \Gamma _1 $ , $\Gamma ^\prime _2:=\Gamma _2$ , $\Delta ^\prime _2:=\Delta _2$ . Hence,

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_1^\ast \cup\Gamma_1\rightarrow\bigvee\Delta_1 \cup \{ I^\prime \}\quad \text{and} \quad\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup\{ I^\prime\} \cup \Gamma_2\rightarrow\bigvee\Delta_2\:.\end{align*}$$

We set $I:=I^\prime $ . The case $\Box A \in \Delta _2$ and $A \in \Lambda _2 $ is analogous.

Subcase 4.2: the formula $\Box A \in \Delta _2$ and $A \notin \Lambda _2$ ( $\Box A \in \Delta _1$ and $A \notin \Lambda _1$ ). We have that $\Gamma _1, \Gamma _2 = \Phi , \Box \Pi $ and $\Delta _1, \Delta _2 = \Box A, \Sigma $ . We split $\Box \Pi $ into two multisets $\Box \Pi _1 \subset \Gamma _1$ and $\Box \Pi _2 \subset \Gamma _2$ such that $\Box \Pi = \Box \Pi _1, \Box \Pi _2$ . Put $\Gamma ^{\prime \prime }_1:= \Box \Pi _1 $ ; $\Delta ^{\prime \prime }_1:= \emptyset $ ; $\Gamma ^{\prime \prime }_2:=\Box \Pi _2$ ; $\Delta ^{\prime \prime }_2:=\{A\}$ ( $\Gamma ^{\prime \prime }_1:= \Box \Pi _1 $ ; $\Delta ^{\prime \prime }_1:= \{A\} $ ; $\Gamma ^{\prime \prime }_2:=\Box \Pi _2$ ; $\Delta ^{\prime \prime }_2:=\emptyset $ ). We see that $\pi ^{\prime \prime }$ is an $\infty $ -proof of the sequent $\Gamma ^{\prime \prime }_1,\Gamma ^{\prime \prime }_2\Rightarrow \Delta ^{\prime \prime }_1,\Delta ^{\prime \prime }_2$ in $\mathsf {Grz}_\infty $ .

If $\Box A \in \Delta _2$ and $A \notin \Lambda _2 $ , then $\mathit {card}(Sub(\Box \Pi _1\Rightarrow )\backslash \Lambda _1 )+\mathit {card}( Sub(\Box \Pi _2\Rightarrow A)\backslash (\Lambda _2\cup \{A\})$ is strictly less than $\mathit {card}(Sub(\Gamma _1\Rightarrow \Delta _1)\backslash \Lambda _1 )+\mathit {card}( Sub(\Gamma _2\Rightarrow \Delta _2)\backslash \Lambda _2)$ . Hence by the induction hypothesis for $\pi ^{\prime \prime }$ , $\Lambda _1$ and $\Lambda _2\cup \{A\}$ there exists an interpolant $I^{\prime \prime }$ such that

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_1^\ast \cup\Box \Pi_1\rightarrow I^{\prime\prime} \quad \text{and} \quad\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup \{\Box (A \to \Box A)\}\cup\{ I^{\prime\prime}\} \cup \Box \Pi_2\rightarrow A\:.\end{align*}$$

Since $\mathsf {Grz}\vdash \Box C \rightarrow \Box \Box C$ for any formula C, from the left condition we obtain

$$ \begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_1^\ast \cup\Box \Pi_1\rightarrow \Box I^{\prime\prime} \:.\end{align*} $$

Hence,

$$ \begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_1^\ast \cup\Gamma_1\rightarrow \bigvee\Delta_1 \cup\{\Box I^{\prime\prime} \}\:.\end{align*} $$

From the right condition we see

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup\{ I^{\prime\prime}\} \cup \Box \Pi_2\rightarrow (\Box (A \to \Box A) \to A)\:.\end{align*}$$

Thus,

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup\{ \Box I^{\prime\prime}\} \cup \Box \Pi_2\rightarrow \Box (\Box (A \to \Box A) \to A)\:.\end{align*}$$

Applying the axiom (v) of $\mathsf {Grz} $ we see that

$$\begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup\{ \Box I^{\prime\prime}\} \cup \Box \Pi_2\rightarrow \Box A\:.\end{align*}$$

Therefore,

$$ \begin{align*}\mathsf{Grz} \vdash \bigwedge \Lambda_2^\ast \cup\{ \Box I^{\prime\prime}\} \cup \Gamma_2\rightarrow \bigvee\Delta_2 \:.\end{align*} $$

Now we can set $I:=\Box I^{\prime \prime }$ . In the case $\Box A \in \Delta _1$ , $A \notin \Lambda _1$ we can analogously set $I:=\Diamond I^{\prime \prime }$ . □

Proof. Assume $\mathsf {Grz} \vdash A \rightarrow B$ . By Lemma 2.1, we have $\mathsf {Grz}_{\mathsf {Seq}} + \mathsf {cut} \vdash A \Rightarrow B$ . Applying Theorem 3.6 and Theorem 6.19 we obtain $\mathsf {Grz}_\infty \vdash A \Rightarrow B$ . Applying the previous lemma with $\Lambda _1=\Lambda _2=\emptyset $ , $\Gamma _1= \{ A\}$ , $\Delta _2=\{ B\}$ , $\Gamma _2=\Delta _1=\emptyset $ , we find an interpolant for $A \to B$ .

□