Proof. We prove this by induction on the structure of a derivation. It suffices to verify that, the initial sequents are valid and the inference rules preserve validity. We only show some non-trivial cases.

\((\supset^\bullet_2)\)

We only show the case when \(F^\circ\in\Phi\) as the other cases are similar. Assume w.l.o.g. that \(\Omega\) is block-free and the output formula of the conclusion is in \(\Omega\). Then the rule is with conclusion \(\Omega^*,[\Phi, A\supset B^\bullet],F^\circ\) and two premises \(\Omega^*,[{\Phi}^\ast,A\supset B^\bullet,A^\circ]\) and \(\Omega^*,[\Phi, A\supset B^\bullet],F^\circ\). Assume by absurdity that this rule application does not preserve validity, then there exists a bi-relational model \(\mathcal{M}=(W,\leq,R,V)\) with \(x\in W\) such that \(x\nVdash\Omega^*,[\Phi, A\supset B^\bullet],F^\circ\). By definition, there is \(x'\in W\) such that \(x\leq x'\) and \(x'\Vdash\bigwedge\Omega\wedge \Diamond (\bigwedge \Phi\wedge (A\supset B))\) and \(x'\nVdash F\). It follows that there is \(y\in W\) such that \(y\Vdash (A\supset B)\wedge \bigwedge\Phi\). Since the left premise is valid, we have \(x'\Vdash \Omega^*,[{\Phi}^\ast,A\supset B^\bullet,A^\circ]\). Thus \(y\Vdash A\). Recall \(y\Vdash A\supset B\), so \(y\Vdash B\). Meanwhile, the right premise is also valid, so \(x'\Vdash \Omega^*,[\Phi,B^\bullet],F^\circ\), which implies \(x'\nVdash \Diamond (\bigwedge\Phi\wedge B)\). Since \(Rx'y\) and \(y\Vdash \bigwedge \Phi\), we have \(y\nVdash B\), a contradiction.

\((\Diamond^\bullet_2)\)

The rule is of one of the two forms: conclusion \(\Omega,[\Phi,\Diamond A^\bullet,F^\circ]\) and premise \(\Phi,[A^\bullet],F^\circ\); conclusion \(\Phi,[A^\bullet],\bot^\circ\) and premise \(\Omega,[\Phi,\Diamond A^\bullet]\). For the first case, assume this rule does not preserve validity, then there exists a bi-relational model \(\mathcal{M}=(W,\leq,R,V)\) with \(x\in W\) such that \(x\nVdash \Omega,[\Phi,\Diamond A^\bullet,F^\circ]\). By definition, this means there is \(x',y\in W\) such that \(x'\geq x, Rx'y\) and \(y\Vdash \bigwedge \Phi \wedge \Diamond A\) and \(y\nVdash F\). Meanwhile, since the premise is valid, we have \(y\Vdash \Phi,[A^\bullet],F^\circ\), which means \(y\Vdash \bigwedge \Phi\wedge {\Diamond A}\supset F\). Since \(y\leq y\), by \(y\Vdash \bigwedge \Phi \wedge \Diamond A\) it follows \(y\Vdash F\), a contradiction. For the second case, the output formula occurs in \(\Omega\). Assume this rule application does not preserve validity, then there exists a bi-relational model \(\mathcal{M}=(W,\leq,R,V)\) with \(x\in W\) such that \(x\nVdash \Omega,[\Phi,\Diamond A^\bullet]\). By definition, regardless of the exact location of the output formula, there exists \(x'\in W\) such that \(x'\geq x\) such that \(x'\Vdash \Diamond (\bigwedge \Phi \wedge \Diamond A)\). This further implies there is \(y\in W\) such that \(Rx'y\) and \(y\Vdash \bigwedge \Phi \wedge \Diamond A\). Meanwhile, since the premise is valid, we have \(y\Vdash \Phi,[A^\bullet],\bot^\circ\), which means \(y\nVdash \bigwedge \Phi\wedge {\Diamond A}\), a contradiction.

This completes the proof. ◻

Proof. We show that any instance of axioms of \(\mathcal{C}_\mathbf{FIK}\) can be proved in \(\mathsf{SC}_\mathbf{FIK}\) and that the rule of (mp) is simulated by \((\mathsf{cut})\) as usual. The proof of axiom (\(\mathsf{wCD}\)) is given in Figure 4 as an example. For rule (nec), we prove by induction on a derivation that for any formula \(A\) if \(A^\circ\) is provable in \(\mathsf{SC}_\mathbf{FIK}\)+\((\mathsf{cut})+(\mathsf{cut}^{[\cdot]})\), \([A^\circ]\) is also provable in the same system, and then we conclude by an application of \((\square^\circ_1)\). ◻

Proof. We carry on the proof by mutual induction on \(\mathsf{cut}(d_1,h_1)\) and \(\mathsf{cut}^{[\cdot]}(d_2,h_2)\), where

• \(\mathsf{cut}(d_1,h_1)\):= every application \((r)\) of \(\mathsf{cut}\) in a derivation has a rank strictly smaller than \((d_1,h_1)\)

• \(\mathsf{cut}^{[\cdot]}(d_2,h_2)\):= every application \((r)\) of \(\mathsf{cut}^{[\cdot]}\) in a derivation has a rank strictly smaller than \((d_2,h_2)\)

Therefore, the induction hypotheses we use are the following:

The two inductive hypotheses will take care of the two derivations of the following form, denoted as \(\mathcal{D}\) and \(\mathcal{E}\) respectively,

The structure of the proof is as follows. We consider different cases according to the role of the cut formula in the premises of \((\mathsf{cut})\) for the last step in \(\mathcal{D}_1\) and \(\mathcal{D}_2\), then similarly for the roles of the cut formula in the premises of \((\mathsf{cut}^{[\cdot]})\) for the last step in \(\mathcal{E}_1\) and \(\mathcal{E}_2\). Our goal is to push up each application of \((\mathsf{cut})\) and \((\mathsf{cut}^{[\cdot]})\) to some upper applications with strictly smaller ranks.

First, for \(\mathcal{D}\), let us denote the last rule applied in \(\mathcal{D}_1\) and \(\mathcal{D}_2\) as \((r_1),(r_2)\) respectively. If either \(A^\circ\) is weak in \((r_1)\) or \(A^\bullet\) is weak in \((r_2)\), we only need to apply the same rule with another context without that occurrence of \(A\). Otherwise, neither \(A^\circ\) nor \(A^\bullet\) is weak, then one of the following holds: (D1) one of the premises is an axiom namely the inductive base (\(\mathsf{cut}\) applied at height 0); and for inductive step, (D2) \(A\) is principal in both premises; (D3) \(A^\circ\) is principal in \((r_1)\) and \(A^\bullet\) is side in \((r_2)\); (D4) \(A^\circ\) is side in \((r_1)\).

Next, for \(\mathcal{E}\), similar to the first half of the proof, we discuss possible different roles of the cut formula in the premises of \((\mathsf{cut}^{[\cdot]})\) for the last step in \(\mathcal{E}_1\) and \(\mathcal{E}_2\). We denote the last rule applied in \(\mathcal{E}_1\) and \(\mathcal{E}_2\) as \((e_1),(e_2)\) respectively. In addition to the weak cases, we have: (E1) one of the premises is an axiom; (E2) cut formula \(A\) is principal in both premises; (E3) \(A^\circ\) is principal in \((e_1)\) and \(A^\bullet\) is side in \((e_2)\); (E4) \(A^\circ\) is side in \((e_1)\).

Let us consider all the cases of (D1)-(D4) and (E1)-(E4) in turn.

(D1) one of the premises is an axiom, which implies one of the following: (1) \({\Omega}^\ast\) or \(\Omega\) is an axiom, so is the sequent on the conclusion; (2) \(A=p\) and \(p^\bullet\in \Omega\), then we obtain \(\Omega\) just by contraction from the right premise \(A^\bullet,\Omega\); (3) \(A=p\) and \(p^\circ\in\Omega\), dual to the second case.

(D2) cut formula \(A\) is principal in both premises, we consider the following non-trivial sub-cases:

• If \(A= B\supset C\), we have

  max width=.92

  \(\vlderivation{ \vliin{}{(\mathsf{cut})}{\Omega}{ \vlin{}{(\supset^\circ)}{ {\Omega}^\ast,B\supset C^\circ }{ \vltr {\mathcal{D}_1'} { {\Omega}^\ast,B^\bullet,C^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } { \vliin{}{(\supset^\bullet)}{ B\supset C^\bullet,\Omega }{ \vltr {\mathcal{D}_2'} { B\supset C^\bullet, {\Omega}^\ast,B^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } { \vltr {\mathcal{D}_2''} { C^\bullet,\Omega }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

  \(\leadsto\)

• If \(A=\square B\), further assume \(\Omega=\Omega',[\Phi]\), then we have

  max width=.92

  \(\vlderivation{ \vliin{}{(\mathsf{cut})}{\Omega',[\Phi]}{ \vlin{}{(\square^\circ)}{ {\Omega}^\ast,\square B^\circ }{ \vltr {\mathcal{D}_1'} { \Omega^*,[B^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } { \vlin{}{(\square^\bullet)}{ \Omega',\square B^\bullet,[\Phi] }{ \vltr {\mathcal{D}_2'} { \Omega',\square B^\bullet,[B^\bullet,\Phi] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

  \(\leadsto\)

• If \(A=\Diamond B\), assume \(\Omega=\Omega',[\Phi]\) and the output formula of the conclusion is in \(\Phi\), then we have

  max width=.92

  \(\vlderivation{ \vliin{}{(\mathsf{cut})}{ \Omega',[\Phi] }{ \vlin{}{(\Diamond^\circ)}{ {\Omega'}^\ast,[{\Phi}^\ast],\Diamond B^\circ }{ \vltr {\mathcal{D}_1'} { {\Omega'}^\ast,[{\Phi}^\ast,B^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } { \vlin{}{(\Diamond^\bullet)}{ \Diamond B^\bullet,\Omega',[\Phi] }{ \vltr {\mathcal{D}_2'} { \Omega',[\Phi],[B^\bullet] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

  \(\leadsto\)

  The other case when the output formula is in \(\Omega'\) is similar.

(D3) \(A^\circ\) is principal in \((r_1)\) while \(A^\bullet\) is side in \((r_2)\). We have the following sub-cases:

1. \(r_2\) is one of the invertible rules except \(\square_1^\circ\).

   As an example, we show the case when \(r_2=\supset_1^\bullet\). Suppose \(\Omega=B\supset C^\bullet, \Omega'\), in this case, we have the following derivation unfolding \(\mathcal{D}\),

   \(\vlderivation{ \vliin{}{(\mathsf{cut})}{ B\supset C^\bullet, {\Omega'}^\ast }{ \vltr {\mathcal{D}_1'} { B\supset C^\bullet, {\Omega'}^\ast,A^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } { \vliin{}{(\supset_1^\bullet)}{ A^\bullet,B\supset C^\bullet, \Omega' }{ \vltr {\mathcal{D}_{21}'}{ A^\bullet,B\supset C^\bullet,{\Omega'}^\ast,B^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } { \vltr {\mathcal{D}_{22}'}{ A^\bullet,C^\bullet, {\Omega'} }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

   Then we transform the derivation into the following

   max width=.93

2. suppose \(r_2=\square_1^\circ\) and \(\Omega=\Omega',\square B^\circ\). Hence \({\Omega}^\ast=\Omega'\) and the right premise of cut is derived from \(A^\bullet, \Omega',[B^\circ]\). We have the following sub-cases according to the shape of \(A\),

   • \(A=C\vee D\) and \(r_1=\vee^\circ\), in this case, the left premise of \((\mathsf{cut})\) is \(\Omega_1,C\vee D^\circ\) and is derived from \(\Omega_1,C^\circ\), the right premise of \((\mathsf{cut})\) is \(C\vee D^\bullet,\Omega_2',\square B^\circ\). By Lemma [inver-lemma], both \(C^\bullet,\Omega_2',\square B^\circ\) and \(D^\bullet,\Omega_2',\square B^\circ\) are derivable at the same height. Then the proof proceeds in the same way as in (D2). \(A=C\wedge D\) is similar.

   • \(A=C\supset D\) and \(r_1=\supset_1^\circ\), we apply \((\mathsf{cut})\) to the premise of \((\square_1^\circ)\) and then apply \(\square_1^\circ\).

   • \(A=\square C\) and \(r_1=\square_1^\circ\), we have

     max width=.85

     \(\vlderivation{ \vliin{}{(\mathsf{cut})}{ \Omega',\square B^\circ }{ \vlin{(r_1)}{}{ \Omega',\square C^\circ }{ \vltr {\mathcal{D}_1'} { \Omega',[C^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } { \vlin{}{(\square_1^\circ)}{ \square C^\bullet,\Omega',\square B^\circ }{ \vltr {\mathcal{D}_2'} { \square C^\bullet,{\Omega'},[B^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

     \(\leadsto\)

   • \(A=\Diamond C, r_1=\Diamond_1^\circ\) and \(\Omega'=\Omega'',[\Phi]\), since \(\Omega=\Omega',\square B^\circ\), we have \({\Omega}^\ast=\Omega'',[\Phi]\).

     max width=.85

     \(\vlderivation{ \vliin{}{(\mathsf{cut})}{ \Omega'',[\Phi],\square B^\circ }{ \vlin{(r_1)}{}{ \Omega'',\Diamond C^\circ,[\Phi] }{ \vltr {\mathcal{D}_1'} { \Omega'',[\Phi,C^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } { \vlin{}{(\square_1^\circ)}{ \Diamond C^\bullet,\Omega'',[\Phi],\square B^\circ }{ \vltr {\mathcal{D}_2'} { \Diamond C^\bullet,{\Omega''},[\Phi],[B^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

     \(\leadsto\)

3. \(r_2\) is one of the non-invertible rules, according to the form of rules, we see \(r_2\in\{\Diamond^\circ,\vee_1^\circ,\vee_2^\circ\}\). Among all these three cases can be done by switching the order of \((e_2)\) and \((\mathsf{cut})\), we only show the case when \(r_2=\vee_2^\circ\) as an example. Assume \(\Omega=\Omega',[\Phi,B\vee C^\circ]\). We have

   max width=.95

   \(\vlderivation{ \vliin{}{(\mathsf{cut})}{ \Omega',[\Phi,B\vee C^\circ] }{ \vlin{(e_1)}{}{ \Omega',[\Phi],A^\circ }{ \vltr {\mathcal{E}_1'} { \vdots }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } { \vlin{}{(\vee_2^\circ)}{ A^\bullet, \Omega',[\Phi,B\vee C^\circ] }{ \vltr {\mathcal{E}_2'} { A^\bullet,\Omega',[\Phi,B^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

   \(\leadsto\)

(D4) cut formula \(A^\circ\) is side in the left premise. This further implies the last rule \((r_1)\) applied in \(\mathcal{D}_1\) is one of the invertible \(\bullet\)-rules since other rules do not have side \(\circ\)-formulas (outside a block) on the conclusion. The proof is the same as the side case (i) covered in (D3).

(E1) one of the premises is an axiom,

similar to the corresponding cases in (D1);

(E2) cut formula \(A\) is principal in both premises. Note that \(\Phi\) is a simple sequent, namely block-free, so \(A\) cannot be of the form \(\square B\) or \(\Diamond B\) under the assumption of (E2). \(A= B\vee C\) or \(B\wedge C\) is trivial, we only consider \(A= B\supset C\), we have

(E3) \(A^\circ\) is principal in \((e_1)\) while \(A^\bullet\) is side in \((e_2)\). Similar to (D3).

(E4) \(A^\circ\) is side in \((e_1)\). This implies the last rule \((e_1)\) applied in \(\mathcal{E}_1\) is one of the \(\bullet\)-invertible rules or is \((\Diamond_2^\bullet)\). For the invertible rules, the proof is similar to the side case (i) covered in (D3). Here we only show the case when \(e_1=\Diamond_2^\bullet\). In this case, \(\Phi=\Diamond B^\bullet, \Phi'\) and derivation \(\mathcal{E}\) is unfolded as

We discuss the role of \(A^\bullet\) in \((e_2)\) and the role of \(A^\circ\) in \((e_1')\). We have the following cases where neither \(A^\bullet\) nor \(A^\circ\) is weak:

1. both \(A^\bullet\) and \(A^\circ\) are principal, then according to the form of rules, \(A\) cannot be a \(\square\)-formula. Thus we have the following sub-cases:

   • \(A=C\wedge D\) or \(C\vee D\). We only show the first one. In this case, we have

     max width=.9

     \(\vlderivation{ \vliin{}{(\mathsf{cut}^{[\cdot]})}{ \Omega,[\Phi',\Diamond B^\bullet] }{ \vlin{(e_1)}{}{ {\Omega}^\ast,[{\Phi'}^\ast,\Diamond B^\bullet,C\wedge D^\circ] }{ \vliin{(e_1')}{}{ {\Phi'}^\ast,[B^\bullet],C\wedge D^\circ } { \vltr {\mathcal{E}_{11}'} { {\Phi'}^\ast,[B^\bullet],C^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } { \vltr {\mathcal{E}_{12}'} { {\Phi'}^\ast,[B^\bullet],D^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } } { \vlin{}{(e_2)}{ \Omega,[C\wedge D^\bullet,\Phi',\Diamond B^\bullet] }{ \vltr{\mathcal{E}_2'} { \Omega,[C^\bullet,D^\bullet,\Phi',\Diamond B^\bullet] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\) \(\leadsto\)

   • \(A=C\supset D\). In this case, derivation \(\mathcal{E}\) is unfolded as

     \(\vlderivation{ \vliin{}{(\mathsf{cut}^{[\cdot]})}{ \Omega,[\Phi',\Diamond B^\bullet] }{ \vlin{(e_1)}{}{ {\Omega}^\ast,[{\Phi'}^\ast,\Diamond B^\bullet,C\supset D^\circ] }{ \vlin{(e_1')}{}{ {\Phi'}^\ast,[B^\bullet],C\supset D^\circ } { \vltr {\mathcal{E}_{1}'} { {\Phi'}^\ast,[B^\bullet],C^\bullet,D^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } } { \vliin{}{(e_2)}{ \Omega,[C\supset D^\bullet,\Phi',\Diamond B^\bullet] }{ \vltr{\mathcal{E}_{21}'} { {\Omega}^\ast,[C\supset D^\bullet,{\Phi'}^\ast,\Diamond B^\bullet,C^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } { \vltr{\mathcal{E}_{22}'} { \Omega,[D^\bullet,\Phi',\Diamond B^\bullet] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

     and we transform it into

     max width=.85

   • \(A=\Diamond C\). In this case, we have

     max width=.85

     \(\vlderivation{ \vliin{}{(\mathsf{cut}^{[\cdot]})}{ \Omega,[\Phi',\Diamond B^\bullet] }{ \vlin{(e_1)}{}{ {\Omega}^\ast,[{\Phi'}^\ast,\Diamond B^\bullet,\Diamond C^\circ] }{ \vlin{(e_1')}{}{ {\Phi'}^\ast,[B^\bullet],\Diamond C^\circ } { \vltr {\mathcal{E}_{1}'} { {\Phi'}^\ast,[B^\bullet,C^\circ] }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } } { \vlin{}{(e_2)}{ \Omega,[\Diamond C^\bullet,\Phi',\Diamond B^\bullet] }{ \vltr{\mathcal{E}_{2}'} { [C^\bullet], {\Phi'}^+, \Diamond B^\bullet }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

     \(\leadsto\)

2. \(A^\bullet\) is side in \((e_2)\), then according to the form of rules, \(e_2\) can be any rule of the calculus.

   • if \(e_2\) is an invertible rule or \(\Diamond^\circ,\vee^\circ\), we switch the order of \((e_2)\) and \((\mathsf{cut}^{[\cdot]})\), that is, apply \((\mathsf{cut}^{[\cdot]})\) to the premise of \((e_2)\) and the conclusion of \((e_1')\) first, then apply \((e_2)\).

   • if \(e_2\in\{\supset_2^\circ,\square_2^\circ,\Diamond_2^\bullet\}\), the three cases are similar and we only show one here. Assume \(\Phi'=\Psi,C\supset D^\circ\), then \(\Omega^*=\Omega\), \({\Phi'}^\ast=\Psi\), and we have

     max width=.9

     \(\vlderivation{ \vliin{}{(\mathsf{cut}^{[\cdot]})}{ \Omega,[\Psi,\Diamond B^\bullet,C\supset D^\circ] }{ \vlin{(e_1)}{}{ \Omega,[\Psi,\Diamond B^\bullet,A^\circ] }{ \vlin{(e_1')}{}{\Psi,[B^\bullet],A^\circ} { \vltr {\mathcal{E}_1'} { \vdots }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } } { \vlin{}{(e_2)}{ \Omega,[A^\bullet,\Psi,\Diamond B^\bullet,C\supset D^\circ] }{ \vltr{\mathcal{E}_2'} { A^\bullet,\Psi,\Diamond B^\bullet,C^\bullet, D^\circ }{ \vlhy {\quad}} { \vlhy {}} { \vlhy {\quad}} } } }\)

     \(\leadsto\)

3. \(A^\circ\) is side in \((e_1')\) and \(A^\bullet\) is principal in \((e_2)\). Similar to (iii), \(A\) cannot be a \(\square\)-formula. For cases when \(A=C\wedge D\) or \(C\supset D\), the proof is the same to (iii), since the corresponding \(\circ\)-rules with respect to \(A^\circ\) are invertible. Thus we only have two cases remaining: \(A=\Diamond D\) or \(A=C\vee D\). We show the former case as the latter is similar.

   In this case, the derivation \(\mathcal{E}\) is unfolded as follows, where \(\Psi=\Phi'\),

   (a) If \(e_1'=\Diamond_2^\bullet\), the conclusion of \(\mathsf{cut}\) follows from the premise of \((e_1')\) by \((\Diamond_2^\bullet)\) twice.

   (b) If \(e_1'\) is one of the \(\bullet_1\)-rules except \(\Diamond_1^\bullet\), then from the premise of \((e_1')\), we apply \((e_1)\) first, then \((\mathsf{cut}^{[\cdot]})\) to the conclusion of \((e_1)\) with the conclusion of \((e_2)\), and the \(\bullet_2\)-counterpart of \((e_1')\) in the end.

   (c) If \(e_1'\) is \(\Diamond^\circ\), then \(\Psi,[B^\bullet,D^\circ]\) is derivable, we transform the whole derivation into

   (d) If \(e_1'\) is one of the \(\bullet_2\)-rules or \(\Diamond_1^\bullet\), let us consider the rules applied above \(e_1'\). Assume that before any \(\circ\)-rule is applied, there are no \(\bullet_1\)-rules applied above \(e_1'\), otherwise we return to case (a), switching the rule order and simulating the derivation with the \(\bullet_2\)-counterpart as above. Let us enumerate the branches of \(\mathcal{E}_1'\) as \(\mathcal{B}_1,\ldots,\mathcal{B}_k\) and for each \(\mathcal{B}_i\) further enumerate sequents contained in it as \(\Phi_{i_0},\ldots,\Phi_{i_j},\ldots,\Phi_{i_m}\) such that \(\Phi_{i_0}={\Phi'}^\ast,[B^\bullet],\Diamond D^\circ\) and \(\Phi_{i_m}\) is an axiom. Then for each \(\mathcal{B}_i\), it implies one of the following situations regarding the output formula:

   1. \(\Diamond D^\circ\) is in each \(\Phi_{i_j}\).

   2. there is some \(i_k\geq 1\) such that \(\Phi_{i_k}=\Theta,[\Lambda],\Diamond D^\circ\) for some \(\Theta,\Lambda\) and \(\Phi_{i_{k+1}}=\Theta,[\Lambda,D^\circ]\); meanwhile, for any \(i_j\leq i_k\), the output formula of \(\Phi_{i_j}\) is \(\Diamond D^\circ\).

   3. there is some \(i_k\geq 1\) such that \(\Phi_{i_k}=\Theta,[\Psi,P\supset Q^\bullet],\Diamond D^\circ\) for some \(\Theta,\Psi,P,Q\) and \(\Phi_{i_{k+1}}=\Theta,[\Psi,P\supset Q^\bullet,P^\circ]\); meanwhile, for any \(i_j\leq i_k\), the output formula of \(\Phi_{i_j}\) is \(\Diamond D^\circ\).

   We process each \(\mathcal{B}_i\) respectively and construct the corresponding \(\mathcal{B}_i'\) for it. If (h1) holds, this means \(\Diamond D^\circ\) is unused and hence side in the whole branch, so we can just replace each occurrence of \(D^\circ\) in \(\mathcal{B}_i\) with the output formula \(F^\circ\) of \(\Psi^+\) and then get \(\mathcal{B}_i'\). If (h2) holds, we reconstruct \(\mathcal{B}_i\) into \(\mathcal{B}_i'\) as follows. First we keep all the components \(\Phi_{i_j}\)’s for \(j>k+1\). Next, we remove \(\Phi_{i_k}\); and as in (b), cut \(\Phi_{i_{k+1}}\) with the premise of \((e_2)\) and obtain \(\Phi_{i_k}'\) as follows

   Then for all the \(\Phi_{i_j}\)’s with \(j<k\), let \(\Phi'_{i_j}=\Psi,\Diamond B^\bullet, {\Phi}^\ast_{i_j},F^\circ\).

   Lastly, if (h3) holds, to construct \(\mathcal{B}_i'\) from the current \(\mathcal{B}\), we keep all the components \(\Phi_{i_j}\)’s for \(j>k\) and for \(j\leq k\), we replace \(\Diamond D^\circ\) with \(F^\circ\), which is the output formula of the final conclusion of \((\mathsf{cut}^{[\cdot]})\). Thus, for instance, \(\Phi_{i_k}'=\Theta,[\Psi,P\supset Q^\bullet],F^\circ\). Note that the way we process each branch \(\mathcal{B}\) in fact eliminates the cut formula \(\Diamond D^\circ\) in the whole branch by substituting with the output formula at certain points, but this does not influence other rule applications in the derivation, thus we can connect each \(\mathcal{B}_i'\) and reconstruct the derivation with contraction ending with \(\Psi^+,\Diamond B^\bullet,[B^\bullet]\). Then by \((\Diamond_2^\bullet)\) and contraction, we conclude \(\Omega,[\Psi,\Diamond B^\bullet]\).

This completes the whole proof of cut-admissibility. ◻

Proof. Each set-sequent \(\Omega\) is a member of the set \(\mathcal{P}(\mathsf{Sub}{(A)})\times \mathcal{P}(\mathcal{P}(\mathsf{Sub}{(A)}))\) Let \(|A|=\mathcal{O}(n)\), we have \(|\mathsf{Sub}{(A)}|=\mathcal{O}(n)\), whence the size of \(\Omega\) is \(2^{\mathcal{O}(n)}\) and therefore the cardinality of the sets of such sequents is the cardinality of the set \(\mathcal{P}(\mathsf{Sub}{(A)})\times \mathcal{P}(\mathcal{P}(\mathsf{Sub}{(A)}))\) which is \(2^{2^{\mathcal{O}(n)}}\). ◻

Proof. Let \(\Sigma=\Omega,[\Phi_1],\ldots,[\Phi_k]\) and call sequents \(\Omega,[\Psi_1],\ldots,[\Psi_{l}]\) of the form in the proposition its sub-sequents. Assume \(\Sigma\) is provable in \(\mathsf{SC}_\mathbf{FIK}^\times\) with a proof \(\mathcal{D}\), we show that \(\mathcal{D}\) can be transformed into a clean proof for some subsequent \(\Sigma_1\). The idea is, we find the first application which produces non-tight sequents in the premise and then reconstruct the derivation. We do this iteratively until we get a clean proof of some \(\Sigma_1\). First if a tight sequent is an initial sequent in \(\mathsf{SC}_\mathbf{FIK}\), then itself is a clean proof. Otherwise, let us consider the first rule application \((r)\) that might produce non-tight sequents. We show the following cases and others are similar.

(1) \(r=\wedge_2^\bullet\) or \(r=\vee_2^\bullet\), we only show the case of conjunction. Consider an application with premise \(\Omega',[\Phi,A\wedge B^\bullet, A^\bullet,B^\bullet], [\Phi,A\wedge B^\bullet,A^\bullet,B^\bullet]\) and conclusion \(\Omega',[\Phi,A\wedge B^\bullet], [\Phi,A\wedge B^\bullet,A^\bullet,B^\bullet]\).

From the premise by contraction in \(\mathsf{SC}_\mathbf{FIK}^\times\), we obtain \(\Omega',[\Phi,A\wedge B^\bullet, A^\bullet,B^\bullet]\) which is a tight sequent. We remove this rule application in \(\mathcal{D}\) and reconstruct \(\mathcal{D}\) as follows: For rule applications above the original premise \(\Omega',[\Phi,A\wedge B^\bullet, A^\bullet,B^\bullet], [\Phi,A\wedge B^\bullet,A^\bullet,B^\bullet]\), if it happens only in \(\Omega'\), we keep as it is; if it involves any of the two blocks \([\Phi,A\wedge B^\bullet, A^\bullet,B^\bullet], [\Phi,A\wedge B^\bullet,A^\bullet,B^\bullet]\), we apply them only in the single one. For rule applications below the original conclusion \(\Omega',[\Phi,A\wedge B^\bullet], [\Phi,A\wedge B^\bullet,A^\bullet,B^\bullet]\), we remove them if it involves the block \([\Phi,A\wedge B^\bullet]\) and keep the rest.

(2) \(r=\Diamond^\circ\). Consider an application with premise \(\Omega',[\Phi,A^\circ], [\Phi,\Theta]\) and conclusion \(\Omega',[\Phi], [\Phi,\Theta],\Diamond A^\circ\).

In this case, the premise has a block with output formula but its input part is included in some other block, so it is not tight. Assume w.l.o.g there are no other blocks such that \(\Phi,\Theta\) is a subset of it. By Proposition [prop:tight-preserving], we have \(\Omega',[\Phi], [\Phi,\Theta, A^\circ]\), By contraction, we have \(\Omega',[\Phi,\Theta, A^\circ]\). We replace the application by another one with premise \(\Omega',[\Phi,\Theta, A^\circ]\) and conclusion \(\Omega', [\Phi,\Theta],\Diamond A^\circ\).

Similar to the previous case, we reconstruct \(\mathcal{D}\) as follows: For rule applications above the original premise \(\Omega',[\Phi,A^\circ], [\Phi,\Theta]\), if it happens only in \(\Omega'\), we keep as it is; if it involves any of the two blocks \([\Phi,A^\circ], [\Phi,\Theta]\), we apply them only in the single one \([\Phi,\Theta, A^\circ]\). For rule applications below the conclusion \(\Omega',[\Phi], [\Phi,\Theta],\Diamond A^\circ\), if it involves the block \([\Phi]\) we remove it as well as all the occurrences of \([\Phi]\) and keep the rest.

(3) \(r=\square^\bullet\). Consider the following three cases: \[\begin{align} \AXC{\Omega',\square A^\bullet, [\Phi,A^\bullet], [\Phi, A^\bullet,F^\circ]} \RightLabel{\square^\bullet} \UIC{\Omega',\square A^\bullet, [\Phi], [\Phi, A^\bullet,F^\circ]} \DP & \; & \AXC{\Omega',\square A^\bullet, [\Phi,A^\bullet], [\Phi, A^\bullet]} \RightLabel{\square^\bullet} \UIC{\Omega',\square A^\bullet, [\Phi], [\Phi, A^\bullet]} \DP & \;& \AXC{\Omega',\square A^\bullet, [\Phi,A^\bullet], [A^\bullet, \Phi, F^\circ]} \RightLabel{\square^\bullet} \UIC{\Omega',\square A^\bullet, [A^\bullet,\Phi], [\Phi, F^\circ]} \DP \end{align}\] For the first two cases we have the reconstruction as in (2) and (1) respectively. Lastly for (3), first by weakening and contraction we have \(\Omega',\square A^\bullet,[\Phi,A^\bullet,F^\circ]\). We replace the application above with another one with premise \(\Omega',\square A^\bullet, [A^\bullet,\Phi,F^\circ]\) and conclusion \(\Omega',\square A^\bullet, [\Phi,F^\circ]\)

and reconstruct the derivation as: For rule applications above the original premise \(\Omega',\square A^\bullet, [\Phi,A^\bullet], [A^\bullet, F^\circ]\), if it happens only in \(\Omega'\), we keep as it is; if it involves any of the two blocks \([\Phi,A^\bullet], [A^\bullet, \Phi, F^\circ]\), we apply them only in the single one \([\Phi,A^\bullet, F^\circ]\). For rule applications below the conclusion \(\Omega',\square A^\bullet, [A^\bullet, \Phi], [\Phi, F^\circ]\), we remove these applications as well as all the occurrences of \([A^\bullet,\Phi]\) if they involves the block \([A^\bullet, \Phi]\) and keep the rest.

Each time we encounter the situations in (1)-(3), we reconstruct the proof until there are no any ‘bad’ rule applications as above. In the end, we obtain a clean proof of some sub-sequent of \(\Sigma\). ◻

Proof. Let \(A\) be a formula of size \(n\), \(\mathcal{D}\) be a clean derivation of the tight sequent \(A^\circ\) and \(\mathcal{B}\) be an arbitrary branch in \(\mathcal{D}\). We divide \(\mathcal{B}\) into phases \(\mathcal{B}_1,\ldots,\mathcal{B}_k,\ldots\) where each \(\mathcal{B}_i=S_i^1,\ldots S_i^{m_i}\) such that \(S_1^1= A^\circ\) and each \(S_{i+1}^1\) is obtained from \(S_i^{m_i}\) by one of the rules \((\Diamond_2^\bullet), (\supset_2^\circ)\) and \((\square_2^\circ)\). This means the maximal index \(k\) equals to the maximal number of applications of \((\Diamond_2^\bullet), (\supset_2^\circ)\) and \((\square_2^\circ)\) that are applied within \(\mathcal{B}\). By Proposition [prop:md-decrease], \(k\leq\mathsf{md}{(A)}\), hence we can write \(\mathcal{B}=\mathcal{B}_1,\ldots,\mathcal{B}_k\) for some \(k\leq\mathsf{md}{(A)}\). Moreover, we claim for any \(i\in\{1,\ldots,k\}\), \(m_i\) as the length of \(\mathcal{B}_i\) is bounded by \(2^{O(n)}\).

Proof of claim: \(m_i\) as the length of \(\mathcal{B}_i\) is identical to the number of sequents that are produced by backward proof search. Since \(\mathcal{B}_i\) does not contain applications of \((\Diamond_2^\bullet), (\supset_2^\circ)\) and \((\square_2^\circ)\), by definition, any backward rule application of other rules in \(\mathsf{SC}_\mathbf{FIK}^\times\) does not decrease the size of the input part. Since each tight sequent is also a set-sequent, by Proposition [prop:max-block], there are at most \(\mathcal{O}(2^n)\) blocks contained in a tight sequent. Also, each block has size \(\mathcal{O}(n^2)\), as the input part is increasing within \(\mathcal{B}_i\), hence the number of different input parts for sequents in \(\mathcal{B}_i\) is \(\mathcal{O}(n^2\cdot 2^n)\). On the other hand, while keeping/increasing the set of input, the output formula might be replaced by \(\supset^\bullet\) or decomposed by other \(\circ\)-rules. The unique output formula can occur in any block and since there are \(\mathcal{O}(n)\) output formulas and \(2^{\mathcal{O}(n)}\) blocks, there are \(2^{\mathcal{O}(n)}\cdot \mathcal{O}(n)\) possible occurrences of the output formula which give \(\mathcal{O}(2^n\cdot n^2)\cdot \mathcal{O}(n\cdot 2^n)=2^{\mathcal{O}(n)}\) different sequents, which is the upper bound of \(m_i\). \(\dashv\)

To estimate the length of each branch in \(\mathcal{D}\), since \(\mathcal{B}=\mathcal{B}_1,\ldots,\mathcal{B}_k\) and \(k\leq \mathsf{md}{(A)}=\mathcal{O}(n)\), by the claim above, the length of \(\mathcal{B}\) is bounded by \(2^{\mathcal{O}(n)} \cdot \mathcal{O}(n) = 2^{\mathcal{O}(n)}\). Therefore, we conclude \(\mathcal{B}\) is of exponential length in terms of \(n\). ◻