######  Lemma 7.6.

The rule $(ihd)$ is admissible in
$\mathsf{G3IntQC}^{*}-\\{(ref),(tra),(nd),(cd)\\}$.

######  Proof 7.7.

Similar to the proof of Lem. 6.6. ∎

######  Theorem 7.8.

The rules $(id_{q})$, $(\bot_{l})$, $(\supset_{l})$, $(ref)$, $(tra)$,
$(\exists_{r}),(\forall_{l})$, $(\forall_{r})$, $(nd)$, $(cd)$, and $(ihd)$
are admissible in the calculus $\mathsf{IntQCL}$.

######  Proof 7.9.

The admissibility of $\\{(ref),(tra)\\}$,
$\\{(id_{q}),(\exists_{r}),(\forall_{l})\\}$, $\\{(nd),(cd)\\}$, and $(ihd)$
follow from Lem. 7.1, Lem. 7.3, Lem. 7.4, and Lem. 7.6, respectively.
Admissibility of $(\supset_{l})$ and $(\bot_{l})$ is shown as stated in Thm.
6.8. Admissibility of $(\forall_{r})$ in the presence of $(\forall^{c}_{r})$
is shown below:

$\mathcal{R},w\leq v,\underline{a}\in D_{v},\Gamma\Rightarrow
v:A(\underline{a}/x),\Delta$ $(lsub)$ $\mathcal{R},w\leq w,\underline{a}\in
D_{w},\Gamma\Rightarrow w:A(\underline{a}/x),\Delta$ $(ref)$
$\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow
w:A(\underline{a}/x),\Delta$ $(\forall^{c}_{r})$
$\mathcal{R},\Gamma\Rightarrow w:\forall xA,\Delta$

∎

######  Theorem 7.10.

(i) The calculus $\mathsf{IntQCL}$ is complete relative to treelike
derivations with the fixed root property. (ii) Every derivation in
$\mathsf{IntQCL}$ of a treelike labelled sequent is a treelike derivation with
the fixed root property.

######  Proof 7.11.

Similar to Thm. 5.9. ∎

Although we relied on the notion of a nested form derivation (Def. 6.12) in
the previous section to translate proofs from the refined labelled calculus
$\mathsf{IntQL}$ into proofs in the nested calculus $\mathsf{NIntQ}$, we note
that this notion, or an analog thereof, is unnecessary to translate
derivations from $\mathsf{IntQCL}$ to $\mathsf{NIntQC}$. This follows from the
fact that side conditions are not imposed on $(\exists_{r})$ and
$(\forall_{l})$ in $\mathsf{NIntQC}$—contrary to what is the case in
$\mathsf{NIntQ}$. Hence, applications of $(\exists^{c}_{r})$ and
$(\forall^{c}_{l})$ in $\mathsf{IntQCL}$ need not satisfy certain condition in
order to be translated, thus simplifying the translation from labelled to
nested in the constant domain setting.

######  Theorem 7.12.

Every derivation in $\mathsf{IntQCL}$ of a nestedlike labelled sequent
$\Lambda$ is effectively translatable to a derivation of the nested sequent
$\mathfrak{N}(\Lambda)$ in $\mathsf{NIntQC}$.

######  Proof 7.13.

By Lem. 4.9, we know that $\Lambda$ is treelike, implying that the derivation
of $\Lambda$ is treelike by Thm. 7.10, and so, the translation function
$\mathfrak{N}$ is defined. When translating from labelled to nested, the
existential rules $(\exists^{c}_{r})$ and $(\exists^{ic}_{r})$, and the
universal rules $(\forall^{c}_{l})$ and $(\forall^{ic}_{l})$, translate to
instances of $(\exists_{r})$ and $(\forall_{l})$, respectively. All remaining
rules in $\mathsf{IntQCL}$ translate to their corresponding version in the
nested calculus. ∎

######  Theorem 7.14.

Every derivation in $\mathsf{NIntQC}$ of a nested sequent $\Sigma$ is
effectively translatable to a derivation of the labelled sequent
$\mathfrak{L}(\Sigma)$ in $\mathsf{IntQCL}$.

######  Proof 7.15.

We show how to translate an instance of $(\exists_{r})$; the remaining cases
are similar to those in the proof of Thm. 6.14. Suppose we aim to translate an
$(\exists_{r})$ inference occurring in our input derivation:

$\Sigma\\{X\rightarrow A(\underline{a}/x),\exists xA,Y\\}$ $(\exists_{r})$
$\Sigma\\{X\rightarrow\exists xA,Y\\}$

If the parameter $\underline{a}$ in the above inference is an eigenvariable,
then we translate the inference to an instance of $(\exists^{in}_{r})$ in
$\mathsf{IntQCL}$. However, if the parameter occurs in a side formula, then
the translation is non-trivial. Suppose then, that there exists some formula
$B(\underline{a})$ (different than the occurrence of $A(\underline{a}/x)$)
occurring in the premise of the $(\exists_{r})$ inference above. Suppose that
the translation $\mathfrak{L}$ assigns the label $u$ to all formulae in the
component where $B(\underline{a})$ occurs, and note that
$u:B(\underline{a})\in\Gamma,\Delta$ below. This, in conjunction with the
definition of $\mathfrak{L}$ (Def. 4.7), implies the existence of a domain
atom $\underline{a}\in D_{u}$ in the image of $\Sigma\\{X\rightarrow
A(\underline{a}/x),\exists xA,Y\\}$ under $\mathfrak{L}$ (which is explicitly
included in the derivation below). Since $\mathfrak{L}(\Sigma\\{X\rightarrow
A(\underline{a}/x),\exists xA,Y\\})$ is a treelike labelled sequent, there
must exist an undirected path $u\sim v_{1}$, $\ldots$, $v_{n}\sim w$ from $u$
to $w$ in $\mathcal{R}$, i.e. $u\sim^{\mathcal{R}}w$. (NB. If $u=w$, then the
translation is straightforward, so we omit consideration of that case.) If we
weaken in domain atoms of the form $\underline{a}\in D_{v_{i}}$ (with
$i\in\\{1,\ldots,n\\}$) along this undirected path, invoke the admissibility
of $(nd)$ and $(cd)$ (Thm. 7.8), and then apply $(\exists^{c}_{r})$, we obtain
the image of the conclusion of the $(\exists_{r})$ inference above under the
$\mathfrak{L}$ translation. This entire process is succinctly demonstrated in
the derivation below:

$\mathfrak{L}(\Sigma\\{X\rightarrow A(\underline{a}/x),\exists xA,Y\\})$ . =
$\mathcal{R},\underline{a}\in D_{u},\underline{a}\in D_{w},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(wk)$ $\mathcal{R},\underline{a}\in
D_{u},\underline{a}\in D_{v_{1}},\ldots,\underline{a}\in
D_{v_{n}},\underline{a}\in D_{w},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(nd)\times k_{1}+(cd)\times k_{2}$
$\mathcal{R},\underline{a}\in D_{u},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{c}_{r})$
$\mathcal{R},\underline{a}\in D_{u},\Gamma\Rightarrow w:\exists xA,\Delta$ . =
$\mathfrak{L}(\Sigma\\{X\rightarrow\exists xA,Y\\})$
---

Note that $k_{1}+k_{2}=n+1$, i.e. $k_{1}+k_{2}$ is the number of labels
occurring in the undirected path from $u$ to $w$ occurring after $u$ and
including $w$. ∎

##  8 Reverse Translations, Corollaries, and Inheritance

The previous three sections were dedicated to refining the labelled calculi
$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$ to obtain refined
labelled variants that were translatable into nested calculi. In this section,
we analyze and provide the reverse translations from $\mathsf{NInt}$,
$\mathsf{NIntQ}$, and $\mathsf{NIntQC}$ to $\mathsf{G3Int}$,
$\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$, respectively. These reverse
translations are interesting in that they demonstrate how to add further
syntactic structures and semantic information in order to obtain the more
complicated semantic systems from the more refined nested systems.
Additionally, these reverse translations can be leveraged to show that each
nested calculus inherits proof theoretic properties from each labelled
calculus, which we discuss in the second subsection.

###  8.1 Reverse Translations

When translating from labelled to nested, we discovered what new rules and
what strengthened versions of rules were needed in order to allow the
elimination of certain structural rules (e.g. $(ref)$ and $(nd)$) from a
derivation. Obtaining the reverse translation is much simpler, as we already
know what rules need to be shown admissible. Lem. 8.1–8.5 below show how to
effectively transform derivations from $\mathsf{IntL}$, $\mathsf{IntQL}$, and
$\mathsf{IntQCL}$ into $\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and
$\mathsf{G3IntQC}$, respectively. These transformations, coupled with the
translations from Thm. 5.11, 6.16, and 7.14, yield effective translations from
our nested calculi to the $\mathsf{G3}$-style labelled calculi.

######  Lemma 8.1 ([21]).

The rules $(id^{*})$, $(\supset_{l}^{*})$, and $(lift)$ are admissible in
$\mathsf{G3Int}$.

######  Proof 8.2.

The proof of the admissibility of each rule in $\mathsf{G3Int}$ is shown
below:

$(id)$ $\mathcal{R},w\leq w,\Gamma,w:p\Rightarrow w:p,\Delta$ $(ref)$
$\mathcal{R},\Gamma,w:p\Rightarrow w:p,\Delta$

$\mathcal{R},w:A\supset B,\Gamma\Rightarrow\Delta,w:A$ $(wk)$
$\mathcal{R},w\leq w,w:A\supset B,\Gamma\Rightarrow\Delta,w:A$
$\mathcal{R},w:A\supset B,w:B,\Gamma\Rightarrow\Delta$ $(wk)$
$\mathcal{R},w\leq w,w:A\supset B,w:B,\Gamma\Rightarrow\Delta$ $(\supset_{l})$
$\mathcal{R},w\leq w,w:A\supset B,\Gamma\Rightarrow\Delta$ $(ref)$
$\mathcal{R},w:A\supset B,\Gamma\Rightarrow\Delta$

Thm. 3.1-(i)-(a) $\mathcal{R},w\leq v,\Gamma,w:A\Rightarrow v:A,\Delta$
$\mathcal{R},w\leq v,\Gamma,w:A,v:A\Rightarrow\Delta$ $(cut)$
$\mathcal{R},w\leq v,\Gamma,w:A\Rightarrow\Delta$

∎

######  Lemma 8.3.

The rules $(id^{n}_{q})$, $(\neg_{l})$, $(\neg_{r})$, $(\supset_{l}^{*})$,
$(lift)$, $(\exists^{n}_{r})$, $(\forall^{n}_{l})$, $(\exists^{in}_{r})$, and
$(\forall^{in}_{l})$ are admissible in $\mathsf{G3IntQ}$.

######  Proof 8.4.

The $(id^{n}_{q})$ rule can be derived by using $(id_{q})$, $(ref)$, and
$(nd)$. The admissibility of $(\supset_{l}^{*})$ and $(lift)$ are shown
similarly as in Lem. 8.1. Recall that $\neg A:=A\supset\bot$; using this fact,
the proofs of the admissibility of $(\neg_{l})$ and $(\neg_{r})$ are as shown
below:

$\mathcal{R},w:A\supset\bot,\Gamma\Rightarrow\Delta,w:A$ $(wk)$
$\mathcal{R},w\leq w,w:A\supset\bot,\Gamma\Rightarrow\Delta,w:A$ $(\bot_{l})$
$\mathcal{R},w:A\supset\bot,w:\bot,\Gamma\Rightarrow\Delta$ $(wk)$
$\mathcal{R},w\leq w,w:A\supset\bot,w:\bot,\Gamma\Rightarrow\Delta$
$(\supset_{l})$ $\mathcal{R},w\leq w,w:A\supset\bot,\Gamma\Rightarrow\Delta$
$(ref)$ $\mathcal{R},w:A\supset\bot,\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq v,\Gamma,v:A\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq
v,\Gamma,v:A\Rightarrow v:\bot,\Delta$ $(\supset_{r})$
$\mathcal{R},\Gamma\Rightarrow w:A\supset\bot,\Delta$

The admissibility of $(\exists^{n}_{r})$ and $(\forall^{n}_{l})$ are shown
below. We assume that there exists a directed path from $v$ to $w$ of a length
greater than $0$ in $\mathcal{R}$, i.e. $v\leq u_{1},\ldots,u_{n}\leq
w\in\mathcal{R}$. The cases where the directed path from $v$ to $w$ is of
length $0$ (i.e. $v=w$) are simple and are handled similarly.

$\mathcal{R},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(wk)$
$\mathcal{R},\underline{a}\in D_{v},\underline{a}\in
D_{u_{1}},\ldots,\underline{a}\in D_{u_{n}},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$
$(\exists_{r})$ $\mathcal{R},\underline{a}\in D_{v},\underline{a}\in
D_{u_{1}},\ldots,\underline{a}\in D_{u_{n}},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:\exists xA$ $(nd)\times(n+1)$
$\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:\exists xA$

$\mathcal{R},\underline{a}\in D_{v},\Gamma,w:A(\underline{a}/x),w:\forall
xA\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq w,\underline{a}\in
D_{v},\underline{a}\in D_{u_{1}},\ldots,\underline{a}\in
D_{u_{n}},\underline{a}\in D_{w},\Gamma,w:A(\underline{a}/x),w:\forall
xA\Rightarrow\Delta$ $(\forall_{l})$ $\mathcal{R},w\leq w,\underline{a}\in
D_{v},\underline{a}\in D_{u_{1}},\ldots,\underline{a}\in
D_{u_{n}},\underline{a}\in D_{w},\Gamma,w:\forall xA\Rightarrow\Delta$ $(ref)$
$\mathcal{R},\underline{a}\in D_{v},\underline{a}\in
D_{u_{1}},\ldots,\underline{a}\in D_{u_{n}},\underline{a}\in
D_{w},\Gamma,w:\forall xA\Rightarrow\Delta$ $(nd)\times(n+1)$
$\mathcal{R},\underline{a}\in D_{v},\Gamma,w:\forall xA\Rightarrow\Delta$

Similar to the previous two proofs, to show the admissibility of
$(\exists^{in}_{r})$ and $(\forall^{in}_{l})$, we assume that $v\leq
u_{1},\ldots,u_{n}\leq w\in\mathcal{R}$, i.e. there exists a directed path of
length greater than $0$ in $\mathcal{R}$. The cases where the directed path
from $v$ to $w$ is of length $0$ (i.e. $v=w$) are simple and are handled
similarly.

$\mathcal{R},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(wk)$
$\mathcal{R},\underline{a}\in D_{v},\underline{a}\in
D_{u_{1}},\ldots,\underline{a}\in D_{u_{n}},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$
$(\exists_{r})$ $\mathcal{R},\underline{a}\in D_{v},\underline{a}\in
D_{u_{1}},\ldots,\underline{a}\in D_{u_{n}},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:\exists xA$ $(nd)\times(n+1)$
$\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:\exists xA$
$(ihd)$ $\mathcal{R},\Gamma\Rightarrow\Delta,w:\exists xA$

$\mathcal{R},\underline{a}\in D_{v},\Gamma,w:A(\underline{a}/x),w:\forall
xA\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq w,\underline{a}\in
D_{v},\underline{a}\in D_{u_{1}},\ldots,\underline{a}\in
D_{u_{n}},\underline{a}\in D_{w},\Gamma,w:A(\underline{a}/x),w:\forall
xA\Rightarrow\Delta$ $(\forall_{l})$ $\mathcal{R},w\leq w,\underline{a}\in
D_{v},\underline{a}\in D_{u_{1}},\ldots,\underline{a}\in
D_{u_{n}},\underline{a}\in D_{w},\Gamma,w:\forall xA\Rightarrow\Delta$ $(ref)$
$\mathcal{R},\underline{a}\in D_{v},\underline{a}\in
D_{u_{1}},\ldots,\underline{a}\in D_{u_{n}},\underline{a}\in
D_{w},\Gamma,w:\forall xA\Rightarrow\Delta$ $(nd)\times(n+1)$
$\mathcal{R},\underline{a}\in D_{v},\Gamma,w:\forall xA\Rightarrow\Delta$
$(ihd)$ $\mathcal{R},\Gamma,w:\forall xA\Rightarrow\Delta$

∎

######  Lemma 8.5.

The rules $(id^{c}_{q})$, $(\neg_{l})$, $(\neg_{r})$, $(\supset_{l}^{*})$,
$(lift)$, $(\forall^{c}_{r})$, $(\exists^{c}_{r})$, $(\forall^{c}_{l})$,
$(\exists^{ic}_{r})$, and $(\forall^{ic}_{l})$ are admissible in
$\mathsf{G3IntQC}$.

######  Proof 8.6.

The admissibility of $(id^{c}_{q})$, $(\neg_{l})$, $(\neg_{r})$,
$(\supset_{l}^{*})$, $(lift)$, $(\exists^{c}_{r})$, $(\forall^{c}_{l})$,
$(\exists^{ic}_{r})$, and $(\forall^{ic}_{l})$ are shown similarly to the
admissibility of the corresponding rules in $\mathsf{G3IntQ}$ (Lem. 8.3
above). The admissibility of $(\forall^{c}_{r})$ is shown below; we assume
that $v$ is a fresh label.

$\Pi_{1}$ $\Pi_{2}$ $(cut)$ $\mathcal{R},w\leq v,\underline{a}\in
D_{w},\underline{a}\in D_{v},\Gamma\Rightarrow v:A(\underline{a}/x),\Delta$
$(cd)$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},\Gamma\Rightarrow
v:A(\underline{a}/x),\Delta$ $(\forall_{r})$ $\mathcal{R},\Gamma\Rightarrow
w:\forall xA,\Delta$

$\Pi_{1}$ | $=\Big{\\{}$ |  $\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow w:A(\underline{a}/x),\Delta$ $(wk)$ $\mathcal{R},w\leq v,\underline{a}\in D_{w},\underline{a}\in D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),v:A(\underline{a}/x),\Delta$
---|---|---

$\Pi_{2}$ | $=\Big{\\{}$ |  Thm. 3.1-(i)-(c) $\mathcal{R},w\leq v,\underline{a}\in D_{w},\underline{a}\in D_{v},\Gamma,w:A(\underline{a}/x)\Rightarrow v:A(\underline{a}/x),\Delta$
---|---|---

∎

######  Theorem 8.7.

Every derivation of a labelled sequent $\Lambda$ in $\mathsf{IntL}$,
$\mathsf{IntQL}$, and $\mathsf{IntQCL}$ can be effectively transformed into a
derivation of $\Lambda$ in $\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and
$\mathsf{G3IntQC}$, respectively, and vice-versa.

######  Proof 8.8.

The forward directions follow from Thm. 5.7, 6.8, and 7.8. The backward
directions follow from Lem. 8.1, 8.3, and 8.5, respectively. ∎

######  Theorem 8.9.

(i) If a nestedlike labelled sequent $\Lambda$ is derivable in
$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$, then
$\mathfrak{N}(\Lambda)$ is derivable in $\mathsf{NInt}$, $\mathsf{NIntQ}$, and
$\mathsf{NIntQC}$, respectively. (ii) Every derivation in $\mathsf{NInt}$,
$\mathsf{NIntQ}$, and $\mathsf{NIntQC}$ of a nested sequent $\Sigma$ can be
effectively translated into a derivation of the labelled sequent
$\mathfrak{L}(\Sigma)$ in $\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and
$\mathsf{G3IntQC}$, respectively.

######  Proof 8.10.

Follows from Thm. 5.11, 6.14, 6.16, 7.12, 7.14, and 8.7. ∎

###  8.2 Corollaries and Inheritance

An appealing consequence of our refinement and translation procedures is that
our nested calculi inherit desirable proof-theoretic properties from their
associated labelled calculi. Such properties are stated in Cor. 8.11–8.16
below.

As mentioned near the end of Sect. 6, the translation of proofs from
$\mathsf{IntQL}$ into proofs in $\mathsf{NIntQ}$ (Thm. 6.14) relies on the
completeness of the latter (Thm. 3.5); hence, we are barred from leveraging
this proof-theoretic translation to conclude that $\mathsf{NIntQ}$ ultimately
inherits completeness from $\mathsf{G3IntQ}$. (NB. In Sect. 6, we also
discussed methods of proof that would free us from relying on the completeness
of $\mathsf{NIntQ}$, thus allowing for this inheritance result to go through.)
Nevertheless, this issue does not arise in our work concerning propositional
intuitionistic logic $\mathsf{Int}$ and first-order intuitionistic logic with
constant domains $\mathsf{IntQC}$, and so, we may conclude the following
corollary:

######  Corollary 8.11.

The calculi $\mathsf{NInt}$ and $\mathsf{NIntQC}$ have inherited soundness and
completeness from $\mathsf{G3Int}$ and $\mathsf{G3IntQC}$, respectively.

######  Proof 8.12.

Soundness follows from Thm. 3.1 and 8.9. Regarding completeness, observe that
if $A$ is a theorem of $\mathsf{Int}$ or $\mathsf{IntQC}$, then $\vec{a}\in
D_{w}\Rightarrow w:A$ is derivable in $\mathsf{G3Int}$ or $\mathsf{G3IntQC}$
(respectively) by Thm. 3.1. By Thm. 5.7 and 5.11, or Thm. 7.8 and 7.12, the
derivation of $\vec{a}\in D_{w}\Rightarrow w:A$ may be transformed and
translated into a derivation of $A$ in $\mathsf{NInt}$ or $\mathsf{NIntQC}$,
respectively. ∎

$\Sigma\\{X\rightarrow Y\\}$ $(wk_{l})$ $\Sigma\\{X,Z\rightarrow Y\\}$ |  $\Sigma$ $(psub)$ $\Sigma(\underline{a}/\underline{b})$
---|---

$\Sigma\\{X,Z,Z\rightarrow Y\\}$ $(ctr_{l})$ $\Sigma\\{X,Z\rightarrow Y\\}$ |  $\Sigma$ $(nr)$ $\ \rightarrow[\Sigma]$
---|---

$\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}],[\Sigma^{\prime}]\\}$ $(mrg_{1})$ $\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}]\\}$ |  $\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]\\}$ $(mrg_{2})$ $\Sigma\\{X_{1},X_{2}\rightarrow Y_{1},Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]\\}$
---|---

$\Sigma\\{X\rightarrow Y\\}$ $(ew_{1})$ $\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}]\\}$ |  $\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]\\}$ $(ew_{2})$ $\Sigma\\{X_{1}\rightarrow Y_{1},[\ \rightarrow\ [X_{2}\rightarrow Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]]\\}$
---|---

$\Sigma\\{X_{1}\rightarrow A,Y_{1},[X_{2}\rightarrow A,Y_{2}]\\}$ $(lwr)$ $\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow A,Y_{2}]\\}$ |  $\Sigma\\{X\rightarrow A,Y\\}$ $\Sigma\\{X,A\rightarrow Y\\}$ $(cut)$ $\Sigma\\{X\rightarrow Y\\}$
---|---

Figure 8: The set $\mathrm{NR}$ of admissible rules in $\mathsf{NInt}$,
$\mathsf{NIntQ}$, and $\mathsf{NIntQC}$.

Furthermore, we obtain the admissibility of the set of structural rules
presented in Fig. 8. This set of structural rules was primarily identified by
investigating the variety of ways in which labelled structural rules (e.g.
$(wk)$, $(ctr_{r})$, etc.) can be applied to manipulate treelike labelled
sequents. Therefore, such rules offer a more fine-grained view of the types of
operations inherent in the more general functionality of the aforementioned
labelled structural rules. Although the admissibility of the rules in Fig. 8
can be established by confirming the soundness of each rule, and recognizing
that each nested calculus is complete (Thm. 3.5), we provide proof-theoretic
arguments which demonstrate how such rules are obtained from their associated
labelled structural rules. The proof of this admissibility result (Cor. 8.13
below) can be found in Appendix A for the interested reader.

######  Corollary 8.13.

All rules in $\mathrm{NR}$ are admissible in $\mathsf{NInt}$, $\mathsf{NIntQ}$
and $\mathsf{NIntQC}$.

Additionally, we obtain the invertibility of the rules in our nested calculi:

######  Corollary 8.14.

All rules in $\mathsf{NInt}$, $\mathsf{NIntQ}$ and $\mathsf{NIntQC}$ are
invertible.

######  Proof 8.15.

Follows from Lem. 4.13 and Thm. 8.9. ∎

By making use of the previous two corollaries, we can prove that derivability
of a nested sequent is equivalent to the derivability of its formula
interpretation (Def. 3.4). Note that in the propositional case the universal
closure $\forall\vv{x}$ is vacuous, and so,
$\rightarrow\forall\vv{x}\iota(\Sigma)$ is identical to
$\rightarrow\iota(\Sigma)$.

######  Corollary 8.16.

The nested sequent $\Sigma$ is derivable in $\mathsf{NInt}$, $\mathsf{NIntQ}$
and $\mathsf{NIntQC}$ iff the nested sequent
$\rightarrow\forall\vv{x}\iota(\Sigma)$ is derivable in $\mathsf{NInt}$,
$\mathsf{NIntQ}$ and $\mathsf{NIntQC}$, respectively.

######  Proof 8.17.

We begin with the forward direction, and assume that $\Sigma$ is derivable in
one of our nested systems. By the admissibility of $(nr)$ (Cor. 8.13), we know
that $\rightarrow[\Sigma]$ is derivable. Starting at the leaves of the nested
sequent and continuously applying $(\land_{l})$, $(\lor_{r})$, and
$(\supset_{r})$, we eventually obtain a derivation of
$\rightarrow\iota(\Sigma)$. From here, we have three cases to consider: (i) If
we are working in the nested system $\mathsf{NInt}$, then we are done. (ii) If
we are working in the nested system $\mathsf{NIntQ}$, and
$\rightarrow\iota(\Sigma)$ contains no free variables (i.e. parameters), then
we are done. Otherwise, if the free variables (i.e. parameters)
$\underline{a}_{1},\ldots,\underline{a}_{n}$ occur in $\iota(\Sigma)$, then we
apply the $(nr)$ rule $n$ times to obtain:

$\underbrace{\rightarrow\ [\ldots[\rightarrow\iota(\Sigma)]\ldots]}_{n}$

Applying the $(\forall^{n}_{r})$ rule $n$ times gives a derivation of
$\rightarrow\forall\vv{x}\iota(\Sigma)$. (iii) If we are working in the nested
system $\mathsf{NIntQC}$ and $\rightarrow\iota(\Sigma)$ does not contain any
occurences of free variables (i.e. parameters), then we are done. Otherwise,
we repeatedly apply $(\forall^{c}_{r})$ to obtain a derivation of the desired
conclusion.

For the backwards direction, we invoke the invertibility of $(\land_{l})$,
$(\lor_{r})$, $(\supset_{r})$, $(\forall^{n}_{r})$, and $(\forall^{c}_{r})$
(Cor. 8.14), as well as the admissibility of $(mrg_{2})$ (Cor. 8.14), to
obtain a derivation of $\Sigma$. ∎

Last, by making use of the admissibility of $(mrg_{2})$, we can show that each
derivation in $\mathsf{NIntQ}$ can be transformed into a derivation in
$\mathsf{NIntQC}$. We also show that the same embedding holds between
$\mathsf{IntQL}$ and $\mathsf{IntQCL}$ to complete our mapping of the
relationships mentioned in Fig. 1 of Sect. 1.

######  Corollary 8.18.

(i) Every derivation in $\mathsf{IntQL}$ is transformable into a derivation in
$\mathsf{IntQCL}$. (ii) Every derivation in $\mathsf{NIntQ}$ is transformable
into a derivation in $\mathsf{NIntQC}$.

######  Proof 8.19.

Observe that the $(\exists^{n}_{r})$, $(\exists^{in}_{r})$,
$(\forall^{n}_{l})$, and $(\forall^{in}_{l})$ rules in $\mathsf{IntQL}$ are
instances of the $(\exists^{c}_{r})$, $(\exists^{ic}_{r})$,
$(\forall^{c}_{l})$, and $(\forall^{ic}_{l})$ rules in $\mathsf{IntQCL}$.
Additionally, the same relationship holds true of the $(\exists_{r})$ and
$(\forall_{l})$ rules in $\mathsf{NIntQ}$ and $\mathsf{NIntQC}$. Thus, the
only rules that differ between the systems $\mathsf{IntQL}$ and
$\mathsf{IntQCL}$ are the $(\forall_{r})$ and $(\forall^{c}_{r})$ rules, and
the only rules that differ between the systems $\mathsf{NIntQ}$ and
$\mathsf{NIntQC}$ are the $(\forall^{n}_{r})$ and $(\forall^{c}_{r})$ rules.
Therefore, we show below that $(\forall_{r})$ and $(\forall^{n}_{r})$ are
admissible in $\mathsf{IntQCL}$ and $\mathsf{NIntQC}$, respectively, which
proves the claim since all remaining cases are straightforward.

$\mathcal{R},w\leq v,\underline{a}\in D_{v},\Gamma\Rightarrow v:A(\underline{a}/x),\Delta$ $(lsub)$ $\mathcal{R},w\leq w,\underline{a}\in D_{w},\Gamma\Rightarrow w:A(\underline{a}/x),\Delta$ $(ref)$ $\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow w:A(\underline{a}/x),\Delta$ $(\forall^{c}_{r})$ $\mathcal{R},\Gamma\Rightarrow w:\forall xA,\Delta$ |  $\Sigma\\{X\rightarrow Y,[\ \rightarrow A(\underline{a}/x)]\\}$ $(mrg_{2})$ $\Sigma\\{X\rightarrow A(\underline{a}/x),Y\\}$ $(\forall^{c}_{r})$ $\Sigma\\{X\rightarrow\forall xA,Y\\}$
---|---

∎

##  9 Conclusion

In this paper, we mapped out the interrelationships between semantic systems
and Fitting’s nested calculi for intuitionistic logics. We focused extensively
on _how_ to eliminate the structural rules of the labelled calculi
$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$ from derivations,
by considering how to strengthen their logical rules, or via the addition of
new rules. We referred to this process as the method of _refinement_ since it
ultimately yielded the more refined (sound and complete) calculi
$\mathsf{IntL}$, $\mathsf{IntQL}$, and $\mathsf{IntQCL}$ which omitted the use
of semantically explicit structural rules (e.g. $(ref)$ and $(nd)$) and only
required treelike labelled sequents in derivations. We saw that fragments of
these refined labelled calculi were equivalent to Fitting’s nested calculi
[9]. Moreover, we also observed that Fitting’s nested calculi inherited proof-
theoretic properties from their associated labelled calculi; e.g. soundness
and completeness, invertibility of rules, and admissibility of $(cut)$. Such
results suggest that structural rule elimination is a natural method for
connecting the relational semantics of a logic to a nested calculus for the
logic (via the labelled sequent paradigm).

The method of refining labelled calculi into nested calculi for intuitionistic
logics is part of a larger project that seeks to investigate the extent to
which such refinements can be performed. Due to general results concerning the
construction of labelled calculi, their modularity, and the confirmation of
their proof-theoretic properties [5, 6, 11, 24], the exposition of a method
for deriving refined (or, nested) calculi—which utilize sequents with a
simpler underlying data structure (e.g. trees) and have proven to be well-
suited for certain automated reasoning tasks (e.g. proof-search [25], counter-
model extraction [17, 25], and effective interpolation [19])—from semantic
systems could prove to be of practical consequence. Moreover, since labelled
calculi are easily obtained from a logic’s semantics, the method of refinement
provides a means by which (nested) proof calculi with favorable properties may
be obtained directly from a logic’s semantics.

###### Acknowledgements.

Work funded by FWF projects I2982 and W1255-N23.

## References

  * [1] Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics.  In: W. Hodges, M. Hyland, C. Steinhorn, J. Truss (eds.) Logic: From Foundations to Applications: European Logic Colloquium, p. 1–32. Clarendon Press, USA (1996)
  * [2] Belnap, N.D.: Display logic.  Journal of philosophical logic 11(4), 375–417 (1982)
  * [3] Brünnler, K.: Deep sequent systems for modal logic.  Arch. Math. Log. 48(6), 551–577 (2009).  10.1007/s00153-009-0137-3.  URL https://doi.org/10.1007/s00153-009-0137-3
  * [4] Bull, R.A.: Cut elimination for propositional dynamic logic without *.  Z. Math. Logik Grundlag. Math. 38(2), 85–100 (1992)
  * [5] Ciabattoni, A., Maffezioli, P., Spendier, L.: Hypersequent and labelled calculi for intermediate logics.  In: D. Galmiche, D. Larchey-Wendling (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, _Lecture Notes in Computer Science_ , vol. 8123, pp. 81–96. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)
  * [6] Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics.  Archive for Mathematical Logic 51(1-2), 71–92 (2012)
  * [7] Fitting, M.: Tableau methods of proof for modal logics.  Notre Dame Journal of Formal Logic 13(2), 237–247 (1972)
  * [8] Fitting, M.: Prefixed tableaus and nested sequents.  Annals of Pure and Applied Logic 163(3), 291 – 313 (2012).  https://doi.org/10.1016/j.apal.2011.09.004
  * [9] Fitting, M.: Nested sequents for intuitionistic logics.  Notre Dame Journal of Formal Logic 55(1), 41–61 (2014)
  * [10] Gabbay, D., Shehtman, V., Skvortsov, D.: Quantification in Non-classical Logics.  Studies in Logic and Foundations of Mathematics. Elsevier (2009)
  * [11] Gabbay, D.M.: Labelled deductive systems, _Oxford Logic guides_ , vol. 33.  Clarendon Press/Oxford Science Publications (1996)
  * [12] Gentzen, G.: Untersuchungen uber das logische schliessen.  Mathematische Zeitschrift 39(3), 405–431 (1935)
  * [13] Goré, R., Ramanayake, R.: Labelled tree sequents, tree hypersequents and nested (deep) sequents.  In: T. Bolander, T. Braüner, S. Ghilardi, L.S. Moss (eds.) Advances in Modal Logic 9, papers from the ninth conference on ”Advances in Modal Logic,” held in Copenhagen, Denmark, 22-25 August 2012, pp. 279–299. College Publications (2012).  URL http://www.aiml.net/volumes/volume9/Gore-Ramanayake.pdf
  * [14] Kashima, R.: Cut-free sequent calculi for some tense logics.  Studia Logica 53(1), 119–135 (1994)
  * [15] Kripke, S.A.: Semantical analysis of intuitionistic logic i.  In: J. Crossley, M. Dummett (eds.) Formal Systems and Recursive Functions, _Studies in Logic and the Foundations of Mathematics_ , vol. 40, pp. 92 – 130. Elsevier (1965).  https://doi.org/10.1016/S0049-237X(08)71685-9.  URL http://www.sciencedirect.com/science/article/pii/S0049237X08716859
  * [16] Lyon, T.: On deriving nested calculi for intuitionistic logics from semantic systems.  In: S.N. Artëmov, A. Nerode (eds.) Logical Foundations of Computer Science - International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4-7, 2020, Proceedings, _Lecture Notes in Computer Science_ , vol. 11972, pp. 177–194. Springer (2020).  10.1007/978-3-030-36755-8_12.  URL https://doi.org/10.1007/978-3-030-36755-8_12
  * [17] Lyon, T., van Berkel, K.: Automating agential reasoning: Proof-calculi and syntactic decidability for stit logics.  In: M. Baldoni, M. Dastani, B. Liao, Y. Sakurai, R. Zalila Wenkstern (eds.) PRIMA 2019: Principles and Practice of Multi-Agent Systems - 22nd International Conference, Turin, Italy, October 28-31, 2019, Proceedings, _Lecture Notes in Computer Science_ , vol. 11873, pp. 202–218. Springer International Publishing, Cham (2019)
  * [18] Lyon, T., Ittner, C., Eckhardt, T., Gratzl, N.: The basics of display calculi.  Kriterion – Journal of Philosophy 31(2), 55–100 (2017)
  * [19] Lyon, T., Tiu, A., Goré, R., Clouston, R.: Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents.  In: M. Fernández, A. Muscholl (eds.) 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, _LIPIcs_ , vol. 152, pp. 28:1–28:16. Schloss Dagstuhl \- Leibniz-Zentrum für Informatik (2020).  10.4230/LIPIcs.CSL.2020.28.  URL https://doi.org/10.4230/LIPIcs.CSL.2020.28
  * [20] Minari, P.: Labeled sequent calculi for modal logics and implicit contractions.  Arch. Math. Log. 52(7-8), 881–907 (2013).  10.1007/s00153-013-0350-y
  * [21] Pimentel, E.: A semantical view of proof systems.  In: L.S. Moss, R.J.G.B. de Queiroz, M. Martinez (eds.) Logic, Language, Information, and Computation - 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018, Proceedings, _Lecture Notes in Computer Science_ , vol. 10944, pp. 61–76. Springer (2018).  10.1007/978-3-662-57669-4_3.  URL https://doi.org/10.1007/978-3-662-57669-4_3
  * [22] Poggiolesi, F.: A cut-free simple sequent calculus for modal logic $s5$.  The Review of Symbolic Logic 1(1), 3–15 (2008)
  * [23] Poggiolesi, F.: The method of tree-hypersequents for modal propositional logic.  In: D. Makinson, J. Malinowski, H. Wansing (eds.) Towards Mathematical Philosophy, _Trends in logic_ , vol. 28, pp. 31–51. Springer (2009).  10.1007/978-1-4020-9084-4_3.  URL https://doi.org/10.1007/978-1-4020-9084-4_3
  * [24] Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic.  Ph.D. thesis, University of Edinburgh. College of Science and Engineering. School of Informatics (1994)
  * [25] Tiu, A., Ianovski, E., Goré, R.: Grammar logics in nested sequent calculus: Proof theory and decision procedures.  In: T. Bolander, T. Braüner, S. Ghilardi, L.S. Moss (eds.) Advances in Modal Logic 9, papers from the ninth conference on ”Advances in Modal Logic,” held in Copenhagen, Denmark, 22-25 August 2012, pp. 516–537. College Publications (2012).  URL http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf
  * [26] Troelstra, A., van Dalen, D.: Constructivism in Mathematics, vol. 1.  Elsevier Science (1988)
  * [27] Viganò, L.: Labelled Non-Classical Logics.  Springer Science & Business Media (2000)
  * [28] Wansing, H.: Sequent calculi for normal modal propositional logics.  Journal of Logic and Computation 4(2), 125–142 (1994)

##  Appendix A Proofs

###### Theorem 3.1.

Let $\mathsf{G3X}\in\\{\mathsf{G3IntQ},\mathsf{G3IntQC}\\}$. The calculi
$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$ have the following
properties:

  * $(i)$

    * (a)

For all $A\in\mathcal{L}$, $\vdash_{\mathsf{G3Int}}\mathcal{R},w\leq
v,w:A,\Gamma\Rightarrow v:A,\Delta$;

    * (b)

For all $A\in\mathcal{L}$,
$\vdash_{\mathsf{G3Int}}\mathcal{R},w:A,\Gamma\Rightarrow\Delta,w:A$;

    * (c)

For all $A\in\mathcal{Q}$, $\vdash_{\mathsf{G3X}}\mathcal{R},w\leq
v,\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}}),\Gamma\Rightarrow
v:A(\vv{\underline{a}}),\Delta$;

    * (d)

For all $A\in\mathcal{Q}$,
$\vdash_{\mathsf{G3X}}\mathcal{R},\vv{\underline{a}}\in
D_{w},w:A(\vv{\underline{a}}),\Gamma\Rightarrow\Delta,w:A(\vv{\underline{a}})$;

  * $(ii)$

All rules in $\mathrm{LR}-\\{(cut)\\}$ are hp-admissible;

  * $(iii)$

All rules are hp-invertible;

  * $(iv)$

The $(cut)$ rule is admissible;

  * $(v)$

$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$ are sound and
complete for $\mathsf{Int}$, $\mathsf{IntQ}$, and $\mathsf{IntQC}$,
respectively.

######  Proof A.1.

We argue that properties (i)–(v) obtain for $\mathsf{G3IntQC}$; by omitting
consideration of the $(cd)$ rule, we obtain proofs of these properties for
$\mathsf{G3IntQ}$ as well.

Claim (i). Claims (a) and (b) are shown in [6, Lem. 1], so we focus on proving
(c) and (d). We prove claims (c) and (d) together by mutual induction on the
complexity of $A$.

Claim (i)-(c). The base case is resolved using the $(id_{q})$ rule for atomic
formulae and the $(\bot_{l})$ rule for $\bot$. We provide the cases for
$\supset$, $\exists$, and $\forall$ for the inductive step; the $\lor$ and
$\land$ cases are simple to verify. Note that for the $\supset$ case the
parameters $\vv{\underline{a}_{1}}$ and $\vv{\underline{a}_{2}}$ are all and
only those parameters that occur in $\vv{\underline{a}}$, with
$\vv{\underline{a}_{1}}$ and $\vv{\underline{a}_{2}}$ potentially
intersecting. Also, the $\supset$ and $\forall$ cases rely on claim (d) (shown
below), and we occasionally use primes (e.g. $\Gamma^{\prime}$ and
$\Delta^{\prime}$) to indicate that formulae explicitly occurring lower in the
proof have been absorbed into the context in order to save space. Last, we let
$\vec{\underline{a}}:=\underline{a}_{1},\ldots,\underline{a}_{n}$.

$\Pi_{1}$ $\Pi_{2}$ $(\supset_{l})$ $\mathcal{R},w\leq v,v\leq u,w\leq
u,\vv{\underline{a}}\in D_{w},\vv{\underline{a}}\in
D_{u},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),u:A(\vv{\underline{a}_{1}}),\Gamma\Rightarrow
u:B(\vv{\underline{a}_{2}}),\Delta$ $(nd)\times n$ $\mathcal{R},w\leq v,v\leq
u,w\leq u,\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),u:A(\vv{\underline{a}_{1}}),\Gamma\Rightarrow
u:B(\vv{\underline{a}_{2}}),\Delta$ $(tra)$ $\mathcal{R},w\leq v,v\leq
u,\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),u:A(\vv{\underline{a}_{1}}),\Gamma\Rightarrow
u:B(\vv{\underline{a}_{2}}),\Delta$ $(\supset_{r})$ $\mathcal{R},w\leq
v,\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),\Gamma\Rightarrow v:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),\Delta$
---

$\Pi_{1}$ | $=\Big{\\{}$ |  (d) $\mathcal{R}^{\prime},\vv{\underline{a}}\in D_{w},\vv{\underline{a}}\in D_{u},u:A(\vv{\underline{a}_{1}}),\Gamma^{\prime}\Rightarrow u:A(\vv{\underline{a}_{1}}),\Delta^{\prime}$
---|---|---

$\Pi_{2}$ | $=\Big{\\{}$ |  (d) $\mathcal{R}^{\prime},\vv{\underline{a}}\in D_{w},\vv{\underline{a}}\in D_{u},u:B(\vv{\underline{a}_{2}}),\Gamma^{\prime}\Rightarrow u:B(\vv{\underline{a}_{2}}),\Delta$
---|---|---

IH $\mathcal{R},w\leq v,\underline{b}\in D_{w},\vv{\underline{a}}\in
D_{w},w:A(\vv{\underline{a}})(\underline{b}/x),\Gamma\Rightarrow
v:A(\vv{\underline{a}})(\underline{b}/x),\Delta^{\prime}$ $(\exists_{r})$
$\mathcal{R},w\leq v,\underline{b}\in D_{w},\vv{\underline{a}}\in
D_{w},w:A(\vv{a})(\underline{b}/x),\Gamma\Rightarrow v:\exists
xA(\vv{a}),\Delta$ $(\exists_{l})$ $\mathcal{R},w\leq v,\vv{a}\in
D_{w},w:\exists xA(\vv{a}),\Gamma\Rightarrow v:\exists xA(\vv{a}),\Delta$
---

IH $\mathcal{R}^{\prime},w\leq u,\vv{\underline{a}}\in D_{u},\underline{b}\in
D_{u},u:A(\vv{\underline{a}})(\underline{b}/x),w:\forall
xA(\vv{\underline{a}}),\Gamma\Rightarrow
u:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(\forall_{l})$
$\mathcal{R}^{\prime},w\leq u,\vv{\underline{a}}\in D_{u},\underline{b}\in
D_{u},w:\forall xA(\vv{\underline{a}}),\Gamma\Rightarrow
u:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(nd)\times n$
$\mathcal{R}^{\prime},w\leq u,\underline{b}\in D_{u},w:\forall
xA(\vv{\underline{a}}),\Gamma\Rightarrow
u:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(tra)$
$\mathcal{R}^{\prime},\underline{b}\in D_{u},w:\forall
xA(\vv{\underline{a}}),\Gamma\Rightarrow
u:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(\forall_{r})$
$\mathcal{R},w\leq v,\vv{\underline{a}}\in D_{w},w:\forall
xA(\vv{a}),\Gamma\Rightarrow v:\forall xA(\vv{a}),\Delta$
---

In the $\forall$ case above, we let $\mathcal{R}^{\prime}:=\mathcal{R},w\leq
v,v\leq u,\vv{\underline{a}}\in D_{w}$.

Claim (i)-(d). The base case for atomic formulae is shown below; the case for
$\bot$ is omitted as it is simple to verify using the $(\bot_{l})$ rule. We
provide the $\supset$, $\exists$, and $\forall$ cases as the cases for the
other connectives are straightforward to prove.

$(id_{q})$ $\mathcal{R},w\leq w,\vv{\underline{a}}\in
D_{w},w:p(\vv{\underline{a}}),\Gamma\Rightarrow
w:p(\vv{\underline{a}}),\Delta$ $(ref)$ $\mathcal{R},\vv{\underline{a}}\in
D_{w},w:p(\vv{\underline{a}}),\Gamma\Rightarrow
w:p(\vv{\underline{a}}),\Delta$
---

$\Pi_{1}$ $\Pi_{2}$ $(\supset_{l})$ $\mathcal{R},w\leq v,\vv{\underline{a}}\in
D_{w},\vv{\underline{a}}\in D_{v},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),v:A(\vv{\underline{a}_{1}}),\Gamma\Rightarrow
v:B(\vv{\underline{a}_{2}}),\Delta$ $(nd)\times n$ $\mathcal{R},w\leq
v,\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),v:A(\vv{\underline{a}_{1}}),\Gamma\Rightarrow
v:B(\vv{\underline{a}_{2}}),\Delta$ $(\supset_{r})$
$\mathcal{R},\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),\Gamma\Rightarrow w:A(\vv{\underline{a}_{1}})\supset
B(\vv{\underline{a}_{2}}),\Delta$
---

$\Pi_{1}$ | $=\Big{\\{}$ |  IH $\mathcal{R},w\leq v,\vv{\underline{a}}\in D_{w},\vv{\underline{a}}\in D_{v},v:A(\vv{\underline{a}_{1}}),\Gamma^{\prime}\Rightarrow v:A(\vv{\underline{a}_{1}}),\Delta^{\prime}$
---|---|---

$\Pi_{2}$ | $=\Big{\\{}$ |  IH $\mathcal{R},w\leq v,\vv{\underline{a}}\in D_{w},\vv{\underline{a}}\in D_{v},v:B(\vv{\underline{a}_{2}}),\Gamma^{\prime}\Rightarrow v:B(\vv{\underline{a}_{2}}),\Delta$
---|---|---

IH $\mathcal{R},\underline{b}\in D_{w},\vv{\underline{a}}\in
D_{w},w:A(\vv{\underline{a}})(\underline{b}/x),\Gamma\Rightarrow
w:A(\vv{\underline{a}})(\underline{b}/x),\Delta^{\prime}$ $(\exists_{r})$
$\mathcal{R},\underline{b}\in D_{w},\vv{\underline{a}}\in
D_{w},w:A(\vv{\underline{a}})(\underline{b}/x),\Gamma\Rightarrow w:\exists
xA(\vv{\underline{a}}),\Delta$ $(\exists_{l})$
$\mathcal{R},\vv{\underline{a}}\in D_{w},w:\exists
xA(\vv{\underline{a}}),\Gamma\Rightarrow w:\exists
xA(\vv{\underline{a}}),\Delta$
---

IH $\mathcal{R},w\leq v,\underline{b}\in D_{u},\vv{\underline{a}}\in
D_{w},\vv{\underline{a}}\in
D_{v},v:A(\vv{\underline{a}})(\underline{b}/x),w:\forall
xA(\vv{\underline{a}}),\Gamma\Rightarrow
v:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(\forall_{l})$
$\mathcal{R},w\leq v,\underline{b}\in D_{v},\vv{\underline{a}}\in
D_{w},\vv{\underline{a}}\in D_{v},w:\forall xA(\vv{a}),\Gamma\Rightarrow
v:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(nd)\times n$
$\mathcal{R},w\leq v,\underline{b}\in D_{v},\vv{\underline{a}}\in
D_{w},w:\forall xA(\vv{a}),\Gamma\Rightarrow
v:A(\vv{\underline{a}})(\underline{b}/x),\Delta$ $(\forall_{r})$
$\mathcal{R},\vv{\underline{a}}\in D_{w},w:\forall
xA(\vv{\underline{a}}),\Gamma\Rightarrow w:\forall
xA(\vv{\underline{a}}),\Delta$
---

Claim (ii). We consider two sets of rules from $\mathrm{LR}$ in turn.

The $\\{(lsub),(psub)\\}$ rules. Hp-admissibility of $(lsub)$ and $(psub)$ are
proven by induction on the height of the given derivation; both are similar to
[6, Lem. 3]. The only non-trivial cases for the former are the $(\supset_{r})$
and $(\forall_{r})$ rules of the inductive step, and the non-trivial cases for
the latter are the $(\exists_{l})$, $(\forall_{r})$, and $(ihd)$ rules of the
inductive step. In such cases, the side condition must be preserved if the
rule is to be applied. Nevertheless, this can be ensured in the usual way (cf.
[6, Lem. 5.1]) by invoking IH twice: first, IH replaces the eigenvariable of
the $(\supset_{r})$, $(\exists_{l})$, $(\forall_{r})$, or $(ihd)$ rule with a
fresh one, and second, the substitution of $(lsub)$ or $(psub)$ is performed,
after which, the corresponding rule may be applied to derive the desired
conclusion.

The $\\{(wk),(ctr_{\mathcal{R}}),(ctr_{l}),(ctr_{r})\\}$ rules. The hp-
admissibility of $(wk)$, $(ctr_{\mathcal{R}})$, $(ctr_{l})$, and $(ctr_{r})$
is shown by induction on the height of the given derivation. Hp-admissibility
of $(wk)$ is relatively straightforward; the only non-trivial cases are the
$(\supset_{r})$, $(\exists_{l})$, $(\forall_{r})$, and $(ihd)$ rules of the
inductive step due to the eigenvariable condition. Such cases are resolved,
however, by potentially applying hp-admissibility of $(lsub)$ or $(psub)$
(argued above), then IH, and last the corresponding rule. Hp-admissibility of
$(ctr_{\mathcal{R}})$ is simple; any application of the rule to an initial
sequent yields an initial sequent, and every case in the inductive step is
resolved by applying IH followed by the corresponding rule. The $(ctr_{l})$
and $(ctr_{r})$ cases are also quite straightforward. The only non-trivial
cases occur when a principal occurrence of an $(\supset_{r})$,
$(\exists_{l})$, or $(\forall_{r})$ rule is contracted. In such cases, the
inductive step is solved by invoking the hp-invertibility of each rule
(property (iii) below), followed by a potential application of $(lsub)$ or
$(psub)$, an application of IH, and finally, the hp-admissibility of
$(ctr_{\mathcal{R}})$ if needed.

Claim (iii). The cases for the propositional rules are straightforward to
check, so we omit them. By hp-admissibility of $(wk)$, we know that
$(\exists_{r})$, $(\forall_{l})$, $(ihd)$, $(nd)$, and $(cd)$ are hp-
invertible (note that the proof of $(wk)$ admissibility does not depend on the
hp-invertibility of rules holding, so we may invoke it). We therefore only
need to check that $(\forall_{r})$ and $(\exists_{l})$ are hp-invertible. We
prove the claim by induction on the height of the given derivation of
$\mathcal{R},\Gamma\Rightarrow w:\forall xA,\Delta$ for the $(\forall_{r})$
rule; the proof for $(\exists_{l})$ is similar.

Base case. If the height of the derivation is $0$, then $\mathcal{R},w\leq
v,a\in D_{v},\Gamma\Rightarrow v:A(\underline{a}/x),\Delta$ is either an
instance of $(\bot_{l})$ or $(id_{q})$.

Inductive step. If the last rule applied in the derivation is $(\wedge_{l})$,
$(\wedge_{r})$, $(\vee_{l})$, $(\vee_{r})$, $(\supset_{l})$, $(ref)$, $(tra)$,
$(\exists_{r})$, $(\forall_{l})$, $(nd)$, or $(cd)$, then the conclusion
follows by applying IH followed by an application of the associated rule. If
the last rule applied is $(\supset_{r})$, $(\exists_{l})$, $(\forall_{r})$, or
$(ihd)$ (where the principal formula of $(\forall_{r})$ is in $\Delta$), then
we potentially apply hp-admissibility of $(lsub)$ or $(psub)$ (property (ii)
above), followed by IH, and then an application of the corresponding rule. If
the last rule applied is $(\forall_{r})$, with $w:\forall xA$ the principal
formula, then the premise of the inference gives the desired result.

Claim (iv). We prove the admissibility of $(cut)$ by induction on the
lexicographic ordering of tuples $(|A|,h_{1},h_{2})$, where $|A|$ is the
complexity of the cut formula $A$, $h_{1}$ is the height of the left premise
of $(cut)$, and $h_{2}$ is the height of the right premise of $(cut)$. We only
consider the cases where the cut formula is principal in both premises of
$(cut)$; the other cases where the cut formula is not principal in one
premise, or in both premises, are relatively straightforward to verify, though
the large number of cases makes the proof tedious. By the cut admissibility
theorem for $\mathsf{G3Int}$ [6, Thm. 5.6], we need only verify the cases
where the cut formula is of the form $\forall xB$ or $\exists xB$. We show
each case in turn below:

$\Pi_{1}$ $\Pi_{2}$ $(cut)$ $\mathcal{R},w\leq v,\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$
---

$\Pi_{1}$ | $=\Bigg{\\{}$ |  $\mathcal{R},w\leq v,w\leq u,\underline{a}\in D_{v},\underline{b}\in D_{u},\Gamma\Rightarrow\Delta,u:B(\underline{b}/x)$ $(\forall_{r})$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:\forall xB$
---|---|---

$\Pi_{2}$ | $=\Bigg{\\{}$ |  $\mathcal{R},w\leq v,\underline{a}\in D_{v},v:B(\underline{a}/x),w:\forall xB,\Gamma\Rightarrow\Delta$ $(\forall_{l})$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},w:\forall xB,\Gamma\Rightarrow\Delta$
---|---|---

The case is resolved as follows:

$\Pi_{1}^{\prime}$ $\Pi_{2}^{\prime}$ $(cut)$ $\mathcal{R},w\leq
v,\underline{a}\in D_{v},\Gamma\Rightarrow\Delta$
---

$\Pi_{1}^{\prime}$ | $=\Bigg{\\{}$ |  $\mathcal{R},w\leq u,\underline{b}\in D_{u},\Gamma\Rightarrow\Delta,u:B(\underline{b}/x)$ $(lsub)$ $\mathcal{R},w\leq v,\underline{b}\in D_{v},\Gamma\Rightarrow\Delta,v:B(\underline{b}/x)$ $(psub)$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,v:B(\underline{a}/x)$
---|---|---

$\Pi_{2}^{\prime}$ | $=\Bigg{\\{}$ |  $\mathcal{R},w\leq v,w\leq u,\underline{a}\in D_{v},\underline{b}\in D_{u},\Gamma\Rightarrow\Delta,u:B(\underline{b}/x)$ $(wk)$ $\mathcal{R},w\leq v,w\leq u,\underline{a}\in D_{v},\underline{b}\in D_{u},v:B(\underline{a}/x),\Gamma\Rightarrow\Delta,u:B(\underline{b}/x)$ $(\forall_{r})$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},v:B(\underline{a}/x),\Gamma\Rightarrow\Delta,w:\forall xB$ $\Lambda$ $(cut)$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},v:B(\underline{a}/x),\Gamma\Rightarrow\Delta$
---|---|---

$\Lambda=\mathcal{R},w\leq v,\underline{a}\in
D_{v},v:B(\underline{a}/x),w:\forall xB,\Gamma\Rightarrow\Delta$

Observe that the $(cut)$ in $\Pi_{2}^{\prime}$ has a height $h_{2}$ that is
one less than the original $(cut)$, and the second $(cut)$ is on a formula
$B(\underline{a}/x)$ that is of less complexity than the original $(cut)$. Let
us examine the $\exists xB$ case.

$\mathcal{R},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:B(\underline{a}/x),w:\exists xB$
$(\exists_{r})$ $\mathcal{R},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:\exists xB$ $\mathcal{R},\underline{a}\in
D_{w},\underline{b}\in D_{w},w:B(\underline{b}/x),\Gamma\Rightarrow\Delta$
$(\exists_{l})$ $\mathcal{R},\underline{a}\in D_{w},w:\exists
xB,\Gamma\Rightarrow\Delta$ $(cut)$ $\mathcal{R},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$
---

The case is resolved as follows:

$\Pi_{1}^{\prime}$ $\Pi_{2}^{\prime}$ $(cut)$ $\mathcal{R},a\in
D_{w},\Gamma\Rightarrow\Delta$
---

$\Pi_{1}^{\prime}$ | $=\Bigg{\\{}\qquad$ |  $\Lambda$ $\mathcal{R},\underline{a}\in D_{w},\underline{b}\in D_{w},w:B(\underline{b}/x),\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R},\underline{a}\in D_{w},\underline{b}\in D_{w},w:B(\underline{b}/x),\Gamma\Rightarrow w:B(\underline{a}/x),\Delta$ $(\exists_{l})$ $\mathcal{R},\underline{a}\in D_{w},w:\exists xB,\Gamma\Rightarrow w:B(\underline{a}/x),\Delta$ $(cut)$ $\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow w:B(\underline{a}/x),\Delta$
---|---|---

$\Lambda=\mathcal{R},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:B(\underline{a}/x),w:\exists xB$

$\Pi_{2}^{\prime}$ | $=\Bigg{\\{}$ |  $\mathcal{R},\underline{a}\in D_{w},\underline{b}\in D_{w},w:B(\underline{b}/x),\Gamma\Rightarrow\Delta$ $(psub)$ $\mathcal{R},\underline{a}\in D_{w},\underline{a}\in D_{w},w:B(\underline{a}/x),\Gamma\Rightarrow\Delta$ $(ctr_{\mathcal{R}})$ $\mathcal{R},\underline{a}\in D_{w},w:B(\underline{a}/x),\Gamma\Rightarrow\Delta$
---|---|---

Observe that the $(cut)$ in the $\Pi_{1}^{\prime}$ inference has a height
$h_{1}$ that is one less than the original $(cut)$, and the second $(cut)$ is
on a formula of smaller complexity.

Claim (v). Soundness is straightforward and is shown by interpreting labelled
sequents on $\mathsf{IntQC}$-models (or $\mathsf{IntQ}$\- models in the case
of $\mathsf{G3IntQ}$) and proving that validity is preserved from premise to
conclusion. By [6], we know that $\mathsf{G3Int}$ is complete relative to
$\mathsf{Int}$, so we need only show that $\mathsf{G3IntQC}$ can derive
quantifier axioms and simulate the inference rules of the axiomatization for
$\mathsf{IntQC}$ (see [10, Ch. 2.6]); we assume that none of the quantifiers
occurring in formulae are vacuous, and note that the vacuous cases can be
derived in a similar fashion. We say that a formula $A(\vv{\underline{a}})$ is
derivable in $\mathsf{G3IntQC}$ if and only if $\vv{\underline{a}}\in
D_{w}\Rightarrow w:A(\vv{\underline{a}})$ is derivable in $\mathsf{G3IntQC}$.
Also, we use the notation $(nd)\times n$ to indicate that the rule $(nd)$ was
applied some number of times to shift a group of domain atoms forward (which
will be made clear by the context).

Prop. (i) $w\leq u,u\leq u,\vv{\underline{a}}\in D_{w},\underline{a}\in
D_{w},\underline{a}\in D_{u},\vv{\underline{a}}\in D_{u},u:\forall
xA(\vv{\underline{a}},x),u:A(\vv{\underline{a}},\underline{a})\Rightarrow
u:A(\vv{\underline{a}},\underline{a})$ $(\forall_{l})$ $w\leq u,u\leq
u,\vv{\underline{a}}\in D_{w},\underline{a}\in D_{w},\underline{a}\in
D_{u},\vv{\underline{a}}\in D_{u},u:\forall
xA(\vv{\underline{a}},x)\Rightarrow u:A(\vv{\underline{a}},\underline{a})$
$(nd)\times n$ $w\leq u,u\leq u,\vv{\underline{a}}\in D_{w},\underline{a}\in
D_{w},u:\forall xA(\vv{\underline{a}},x)\Rightarrow
u:A(\vv{\underline{a}},\underline{a})$ $(ref)$ $w\leq u,\vv{\underline{a}}\in
D_{w},\underline{a}\in D_{w},u:\forall xA(\vv{\underline{a}},x)\Rightarrow
u:A(\vv{\underline{a}},\underline{a})$ $(\supset_{r})$ $\vv{\underline{a}}\in
D_{w},\underline{a}\in D_{w}\Rightarrow w:\forall
xA(\vv{\underline{a}},x)\supset A(\vv{\underline{a}},\underline{a})$
---

Prop. (i) $w\leq u,\vv{\underline{a}}\in D_{w},\underline{a}\in
D_{w},\vv{\underline{a}}\in D_{u},\underline{a}\in
D_{u},u:A(\vv{\underline{a}},\underline{a})\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),u:\exists xA(\vv{\underline{a}},x)$
$(\exists_{r})$ $w\leq u,\vv{\underline{a}}\in D_{w},\underline{a}\in
D_{w},\vv{\underline{a}}\in D_{u},\underline{a}\in
D_{u},u:A(\vv{\underline{a}},\underline{a})\Rightarrow u:\exists
xA(\vv{\underline{a}},x)$ $(nd)\times n$ $w\leq u,\vv{\underline{a}}\in
D_{w},\underline{a}\in D_{w},u:A(\vv{\underline{a}},\underline{a})\Rightarrow
u:\exists xA(\vv{\underline{a}},x)$ $(\supset_{r})$ $\vv{\underline{a}}\in
D_{w},\underline{a}\in D_{w}\Rightarrow
w:A(\vv{\underline{a}},\underline{a})\supset\exists xA(\vv{\underline{a}},x)$
---

$\Pi_{1}$ $\Pi_{2}$ $(\supset_{l})$ $\mathcal{R},v\leq z,z\leq
z,z:B(\vv{\underline{b}})\supset A(\vv{\underline{a}},\underline{a}),v:\forall
x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x)),u:B(\vv{\underline{b}})\Rightarrow
z:A(\vv{\underline{a}},\underline{a})$ $(ref)$ $\mathcal{R},v\leq
z,z:B(\vv{\underline{b}})\supset A(\vv{\underline{a}},\underline{a}),v:\forall
x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x)),u:B(\vv{\underline{b}})\Rightarrow
z:A(\vv{\underline{a}},\underline{a})$ $(\forall_{l})$ $\mathcal{R},v\leq
z,v:\forall x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x)),u:B(\vv{\underline{b}})\Rightarrow
z:A(\vv{\underline{a}},\underline{a})$ $(tra)$ $\mathcal{R},v:\forall
x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x)),u:B(\vv{\underline{b}})\Rightarrow
z:A(\vv{\underline{a}},\underline{a})$ $(\forall_{r})$ $w\leq v,v\leq
u,\vv{\underline{a}}\in D_{w},\vv{\underline{b}}\in D_{w},v:\forall
x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x)),u:B(\vv{\underline{b}})\Rightarrow u:\forall
xA(\vv{\underline{a}},x)$ $(\supset_{r})$ $w\leq v,\vv{\underline{a}}\in
D_{w},\vv{\underline{b}}\in D_{w},v:\forall x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x))\Rightarrow v:B(\vv{\underline{b}})\supset\forall
xA(\vv{\underline{a}},x)$ $(\supset_{r})$ $\vv{\underline{a}}\in
D_{w},\vv{\underline{b}}\in D_{w}\Rightarrow w:\forall
x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x))\supset(B(\vv{\underline{b}})\supset\forall
xA(\vv{\underline{a}},x))$
---

To save space, we let $\mathcal{R}:=w\leq v,v\leq u,u\leq
z,\vv{\underline{a}}\in D_{w},\vv{\underline{b}}\in D_{w},\underline{a}\in
D_{z}$ and $\Gamma:=z:B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},\underline{a}),v:\forall x(B(\vv{\underline{b}})\supset
A(\vv{\underline{a}},x))$. The proofs $\Pi_{1}$ and $\Pi_{2}$ are as follows:

$\Pi_{1}$ | $=\Bigg{\\{}$ |  Prop. (i) $\mathcal{R},v\leq z,z\leq z,\vv{\underline{b}}\in D_{v},\vv{\underline{b}}\in D_{u},\Gamma,u:B(\vv{\underline{b}})\Rightarrow z:B(\vv{\underline{b}}),z:A(\vv{\underline{a}},\underline{a})$ $(nd)\times k_{1}$ $\mathcal{R},v\leq z,z\leq z,\Gamma,u:B(\vv{\underline{b}})\Rightarrow z:B(\vv{\underline{b}}),z:A(\vv{\underline{a}},\underline{a})$
---|---|---

$\Pi_{2}$ | $=\Bigg{\\{}$ |  Prop. (i) $\mathcal{R},v\leq z,z\leq z,\vv{\underline{a}}\in D_{v},\vv{\underline{a}}\in D_{z},\Gamma,u:B(\vv{\underline{b}}),z:A(\vv{\underline{a}},\underline{a})\Rightarrow z:A(\vv{\underline{a}},\underline{a})$ $(nd)\times k_{2}$ $\mathcal{R},v\leq z,z\leq z,\Gamma,u:B(\vv{\underline{b}}),z:A(\vv{\underline{a}},\underline{a})\Rightarrow z:A(\vv{\underline{a}},\underline{a})$
---|---|---

The proof of the axiom $\forall x(A(x)\supset B)\supset(\exists xA(x)\supset
B)$ is similar to the previous proof. The generalization rule is simulated as
shown below:

$\vv{\underline{a}}\in D_{w},\underline{a}\in D_{w}\Rightarrow
w:A(\vv{\underline{a}},\underline{a})$ $(wk)$ $u\leq w,\vv{\underline{a}}\in
D_{u},\vv{\underline{a}}\in D_{w},\underline{a}\in D_{w}\Rightarrow
w:A(\vv{\underline{a}},\underline{a})$ $(nd)\times n$ $u\leq
w,\vv{\underline{a}}\in D_{u},\underline{a}\in D_{w}\Rightarrow
w:A(\vv{\underline{a}},\underline{a})$ $(\forall_{r})$ $\vv{\underline{a}}\in
D_{u}\Rightarrow u:\forall xA(\vv{\underline{a}},x)$ $(lsub)$
$\vv{\underline{a}}\in D_{w}\Rightarrow w:\forall xA(\vv{\underline{a}},x)$
---

$\Pi_{1}$ $\Pi_{2}$ $(\vee_{l})$ $\mathcal{R},v\leq v,\underline{a}\in
D_{v},v:A(\vv{\underline{a}},\underline{a})\lor
B(\vv{\underline{b}}),v:\forall x(A(\vv{\underline{a}},x)\lor
B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$ $(\forall_{l})$
$\mathcal{R},v\leq v,\underline{a}\in D_{v},v:\forall
x(A(\vv{\underline{a}},x)\lor B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$ $(cd)$
$\mathcal{R},v\leq v,v:\forall x(A(\vv{\underline{a}},x)\lor
B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$ $(ref)$
$\mathcal{R},v:\forall x(A(\vv{\underline{a}},x)\lor
B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$ $(\forall_{r})$
$w\leq v,\vv{\underline{a}}\in D_{w},\vv{\underline{b}}\in D_{w},v:\forall
x(A(\vv{\underline{a}},x)\lor B(\vv{\underline{b}}))\Rightarrow v:\forall
xA(\vv{\underline{a}},x),v:B(\vv{\underline{b}})$ $(\vee_{r})$ $w\leq
v,\vv{\underline{a}}\in D_{w},\vv{\underline{b}}\in D_{w},v:\forall
x(A(\vv{\underline{a}},x)\lor B(\vv{\underline{b}}))\Rightarrow v:\forall
xA(\vv{\underline{a}},x)\lor B(\vv{\underline{b}})$ $(\supset_{r})$
$\vv{\underline{a}}\in D_{w},\vv{\underline{b}}\in D_{w}\Rightarrow w:\forall
x(A(\vv{\underline{a}},x)\lor B(\vv{\underline{b}}))\supset\forall
xA(\vv{\underline{a}},x)\lor B(\vv{\underline{b}})$
---

to save space, we let $\mathcal{R}:=w\leq v,v\leq u,\vv{\underline{a}}\in
D_{w},\vv{\underline{b}}\in D_{w},\underline{a}\in D_{u}$. The proofs
$\Pi_{1}$ and $\Pi_{2}$ are as follows (resp.).

Prop. (i) $\mathcal{R},v\leq v,\vv{\underline{a}}\in D_{v},\underline{a}\in
D_{v},v:A(\vv{\underline{a}},\underline{a}),v:\forall
x(A(\vv{\underline{a}},x)\lor B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$ $(nd)\times
k_{1}$ $\mathcal{R},v\leq v,\underline{a}\in
D_{v},v:A(\vv{\underline{a}},\underline{a}),v:\forall
x(A(\vv{\underline{a}},x)\lor B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$
---

Prop. (i) $\mathcal{R},v\leq v,\underline{a}\in D_{v},\vv{\underline{b}}\in
D_{v},v:B(\vv{\underline{b}}),v:\forall x(A(\vv{\underline{a}},x)\lor
B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$ $(nd)\times
k_{2}$ $\mathcal{R},v\leq v,\underline{a}\in
D_{v},v:B(\vv{\underline{b}}),v:\forall x(A(\vv{\underline{a}},x)\lor
B(\vv{\underline{b}}))\Rightarrow
u:A(\vv{\underline{a}},\underline{a}),v:B(\vv{\underline{b}})$
---

To show that modus ponens can be simulated, we let $\vv{a}$ be all parameters
occurring in $A$, $\vv{b}$ be all parameters occurring in $B$, and let
$\vv{c}$ consist of all parameters occurring in $B$, but not $A$. The last
inference consists of a sequence of $k$ $(ihd)$ applications that delete all
domains atoms containing parameters from $A$, but not $B$.

$\vv{\underline{a}}\in D_{w}\Rightarrow w:A(\vv{\underline{a}})$ $(wk)$
$\vv{\underline{a}}\in D_{w},\vv{\underline{c}}\in D_{w}\Rightarrow
w:A(\vv{\underline{a}})$ $\vv{\underline{a}}\in D_{w},\vv{\underline{c}}\in
D_{w}\Rightarrow w:A(\vv{\underline{a}})\supset B(\vv{\underline{b}})$ Prop.
(iii) $w\leq u,\vv{\underline{a}}\in D_{w},\vv{\underline{c}}\in
D_{w},u:A(\vv{\underline{a}})\Rightarrow u:B(\vv{\underline{b}})$ $(lsub)$
$w\leq w,\vv{\underline{a}}\in D_{w},\vv{\underline{c}}\in
D_{w},w:A(\vv{\underline{a}})\Rightarrow w:B(\vv{\underline{b}})$ $(ref)$
$\vv{\underline{a}}\in D_{w},\vv{\underline{c}}\in
D_{w},w:A(\vv{\underline{a}})\Rightarrow w:B(\vv{\underline{b}})$ $(cut)$
$\vv{\underline{a}}\in D_{w},\vv{\underline{c}}\in D_{w}\Rightarrow
w:B(\vv{\underline{b}})$ $(ihd)\times k$ $\vv{\underline{b}}\in
D_{w}\Rightarrow w:B(\vv{\underline{b}})$
---

∎

###### Lemma 4.13.

Let $\mathsf{G3X}^{*}\in\\{\mathsf{G3IntQ}^{*},\mathsf{G3IntQC}^{*}\\}$. The
calculi $\mathsf{G3Int}^{*}$, $\mathsf{G3IntQ}^{*}$, and
$\mathsf{G3IntQC}^{*}$ have the following properties:

  * $(i)$

    * (a)

For all $A\in\mathcal{L}$, $\vdash_{\mathsf{G3Int}^{*}}\mathcal{R},w\leq
v,w:A,\Gamma\Rightarrow v:A,\Delta$;

    * (b)

For all $A\in\mathcal{L}$,
$\vdash_{\mathsf{G3Int}^{*}}\mathcal{R},w:A,\Gamma\Rightarrow\Delta,w:A$;

    * (c)

For all $A\in\mathcal{Q}$, $\vdash_{\mathsf{G3X}^{*}}\mathcal{R},w\leq
v,\vv{\underline{a}}\in D_{w},w:A(\vv{\underline{a}}),\Gamma\Rightarrow
v:A(\vv{\underline{a}}),\Delta$;

    * (d)

For all $A\in\mathcal{Q}$,
$\vdash_{\mathsf{G3X}^{*}}\mathcal{R},\vv{\underline{a}}\in
D_{w},w:A(\vv{\underline{a}}),\Gamma\Rightarrow\Delta,w:A(\vv{\underline{a}})$;

  * (ii)

The rules $\\{(lsub),(psub),(wk),(ctr_{\mathcal{R}}),(ctr_{r})\\}$ are hp-
admissible;

  * (iii)

With the exception of $\\{(\wedge_{l}),(\exists_{l})\\}$, all rules are hp-
invertible;

  * (iv)

The rules $\\{(\wedge_{l}),(\exists_{l})\\}$ are invertible;

  * (v)

The rule $(ctr_{l})$ is admissible.

######  Proof A.2.

We show that the results hold when all rules from $\mathsf{G3Int}^{*}$,
$\mathsf{G3IntQ}^{*}$, and $\mathsf{G3IntQC}^{*}$ are considered.

Claim (i). Similar to Thm. 3.1-(i).

Claim (ii). By induction on the height of the given derivation—similar to the
proofs given for Thm. 3.1-(ii). Note that the hp-admissibility of $(ctr_{r})$
invokes property (iii) below.

Claim (iii). Hp-invertibility of $(\supset_{l})$, $(\supset_{l}^{*})$,
$(\neg_{l})$, $(ref)$, $(tra)$, $(lift)$, $(ihd)$, $(\exists_{r})$,
$(\exists^{n}_{r})$, $(\exists^{in}_{r})$, $(\exists^{c}_{r})$,
$(\exists^{ic}_{r})$, $(\forall_{l})$, $(\forall^{n}_{l})$,
$(\forall^{in}_{l})$, $(\forall^{c}_{l})$, $(\forall^{ic}_{l})$, $(nd)$,
$(cd)$ follow from hp-admissibility of $(wk)$ (property (ii) above). Hence, we
need only prove invertibility of the $(\supset_{r})$, $(\wedge_{r})$,
$(\vee_{l})$, $(\vee_{r})$, $(\neg_{r})$, $(\forall_{r})$, and
$(\forall^{c}_{r})$ rules. The result is shown by induction on the height of
the given derivation and is similar to Thm. 3.1-(iii).

Claim (iv). The addition of $(lift)$ and $(nd)$ to our calculus breaks the
_height preserving_ invertibility of $(\wedge_{l})$ and $(\exists_{l})$.
Nevertheless, it is worthwhile to note that the rule $(lift^{\prime})$ (shown
below) ought to allow for hp-invertibility of $(\wedge_{l})$ in the
propositional calculus, and $(nd^{\prime})$ (shown below) ought to allow for
the hp-invertibility of $(\wedge_{l})$ and $(\exists_{l})$ in the first-order
calculi (which would have the effect that $(ctr_{l})$ is _hp-admissible_ in
both calculi) while retaining the soundness and cut-free completeness of each
system. The notation $v:\Gamma^{\prime}$ is used to represent multisets of
formulae labelled with $v$.

$\mathcal{R},w\leq u,\Gamma,w:\Gamma^{\prime},u:\Gamma^{\prime}\Rightarrow\Delta$ $(lift^{\prime})$ $\mathcal{R},w\leq u,\Gamma,w:\Gamma^{\prime}\Rightarrow\Delta$ |  $\mathcal{R},w\leq u,\vv{\underline{a}}\in D_{w},\vv{\underline{a}}\in D_{u},\Gamma,w:\Gamma^{\prime},u:\Gamma^{\prime}\Rightarrow\Delta$ $(nd^{\prime})$ $\mathcal{R},w\leq u,\vv{\underline{a}}\in D_{w},\Gamma,w:\Gamma^{\prime}\Rightarrow\Delta$
---|---

Despite this shortcoming, the rules are still invertible. To show this, we
prove the following two claims by induction on the height of the given
derivation.

  * (a)

If $\mathcal{R},w_{1}:A\land B,\ldots,w_{n}:A\land B,\Gamma\Rightarrow\Delta$
is provable, then so is the sequent
$\mathcal{R},w_{1}:A,w_{1}:B,\ldots,w_{n}:A,w_{n}:B,\Gamma\Rightarrow\Delta$.

  * (b)

If $\mathcal{R},w_{1}:\exists xA,\ldots,w_{n}:\exists
xA,\Gamma\Rightarrow\Delta$ is provable, then so is the sequent
$\mathcal{R},\underline{a}_{1}\in D_{w_{1}},\ldots,\underline{a}_{n}\in
D_{w_{n}},w_{1}:A(\underline{a}_{1}/x),\ldots,w_{n}:A(\underline{a}_{n}/x),\Gamma\Rightarrow\Delta$.

Claim (a). The base case is trivial, so we move on to the inductive step.

Inductive step. Excluding the case of $(lift)$, the result follows by applying
IH followed by the relevant rule, or in the case where one of the conjunction
formulae is principal in a $(\wedge_{r})$ inference, apply IH to the premise
(if needed) to obtain the desired result. If none of the conjunctions are
active in a $(lift)$ inference, then apply IH followed by an application of
$(lift)$. If one of the conjunctions is principal in an application of
$(lift)$ (as shown below top), then resolve the case as shown below bottom; we
assume w.l.o.g. that the label of the principal formula is $w_{1}$.

$\mathcal{R},u\leq w_{1},u:A\land B,w_{1}:A\land B,\ldots,w_{n}:A\land
B,\Gamma\Rightarrow\Delta$ $(lift)$ $\mathcal{R},u\leq w_{1},u:A\land
B,\ldots,w_{n}:A\land B,\Gamma\Rightarrow\Delta$

IH $\mathcal{R},u\leq
w_{1},u:A,u:B,w_{1}:A,w_{1}:B,\ldots,w_{n}:A,w_{n}:B,\Gamma\Rightarrow\Delta$
$(lift)$ $\mathcal{R},u\leq
w_{1},u:A,u:B,w_{1}:B,\ldots,w_{n}:A,w_{n}:B,\Gamma\Rightarrow\Delta$ $(lift)$
$\mathcal{R},u\leq
w_{1},u:A,u:B,\ldots,w_{n}:A,w_{n}:B,\Gamma\Rightarrow\Delta$

Notice that the two applications of $(lift)$ needed to derive the desired
conclusion break the hp-invertibility of the $(\wedge_{l})$ rule.

Claim (b). The base case is trivial, so we move on to the inductive step.

Inductive step. All cases, with the exception of the one given below top
(where one of our existential formulae is principal in an application of
$(lift)$), are either resolved by applying IH followed by the corresponding
rule, or if one of the existential formulae is principal in an $(\exists_{r})$
inference, then apply IH to the premise (if needed) to obtain the desired
result. The non-trivial case given below top is resolved as shown below
bottom; we assume w.l.o.g. that the label of the principal formula is $w_{1}$.

$\mathcal{R},u\leq w_{1},u:\exists xA,w_{1}:\exists xA,\ldots,w_{n}:\exists
xA,\Gamma\Rightarrow\Delta$ $(lift)$ $\mathcal{R},u\leq w_{1},u:\exists
xA,\ldots,w_{n}:\exists xA,\Gamma\Rightarrow\Delta$

IH $\mathcal{R},u\leq w_{1},\underline{a}\in D_{u},\underline{a}_{1}\in
D_{w_{1}},\ldots,\underline{a}_{n}\in
D_{w_{n}},u:A(\underline{a}/x),w_{1}:A(\underline{a}_{1}/x),\ldots,w_{n}:A(\underline{a}_{n}/x),\Gamma\Rightarrow\Delta$
$(psub)$ $\mathcal{R},u\leq w_{1},\underline{a}\in D_{u},\underline{a}\in
D_{w_{1}},\ldots,\underline{a}_{n}\in
D_{w_{n}},u:A(\underline{a}/x),w_{1}:A(\underline{a}/x),\ldots,w_{n}:A(\underline{a}_{n}/x),\Gamma\Rightarrow\Delta$
$(lift)$ $\mathcal{R},u\leq w_{1},\underline{a}\in D_{u},\underline{a}\in
D_{w_{1}},\ldots,\underline{a}_{n}\in
D_{w_{n}},u:A(\underline{a}/x),\ldots,w_{n}:A(\underline{a}_{n}/x),\Gamma\Rightarrow\Delta$
$(nd)$ $\mathcal{R},u\leq w_{1},\underline{a}\in
D_{u},\ldots,\underline{a}_{n}\in
D_{w_{n}},u:A(\underline{a}/x),\ldots,w_{n}:A(\underline{a}_{n}/x),\Gamma\Rightarrow\Delta$

Observe that the use of $(lift)$ and $(nd)$ breaks height-preserving
invertibility of the rule.

Propositions (a) and (b) imply the invertibility of $(\wedge_{l})$ and
$(\exists_{l})$.

Claim (v). By induction on pairs of the form $(|A|,h)$ where $|A|$ is the
complexity of the contraction formula $A$ and $h$ is the height of the
derivation. The proof makes use of properties (ii)– (iv). ∎

###### Lemma 6.1.

The $(ref)$ and $(tra)$ rules are admissible in the calculus
$\mathsf{G3IntQ}^{*}$.

######  Proof A.3.

The $(tra)$ elimination cases are given below with each non-trivial case being
followed by a proof of how it is resolved. In the $(id^{n}_{q})$ case, We let
$\mathcal{R}^{\prime}:=\mathcal{R},\underline{a}_{1}\in
D_{v_{1}},\ldots,\underline{a}_{n}\in D_{v_{n}}$.

$(id_{q}^{n})$ $\mathcal{R}^{\prime},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$ $(tra)$ $\mathcal{R}^{\prime},u\leq z,z\leq
z^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$
---

$(id_{q}^{n})$ $\mathcal{R}^{\prime},u\leq z,z\leq
z^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$
---

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\underline{a}\in
D_{v},\Gamma,w:A(\underline{a}/x),w:\forall xA\Rightarrow\Delta$
$(\forall^{n}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\underline{a}\in D_{v},\Gamma,w:\forall xA\Rightarrow\Delta$
$(tra)$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma,w:\forall xA\Rightarrow\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},w:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$
$(\forall^{n}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\underline{a}\in
D_{v},\Gamma,w:A(\underline{a}/x),w:\forall xA\Rightarrow\Delta$
$(\forall^{in}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\Gamma,w:\forall xA\Rightarrow\Delta$ $(tra)$ $\mathcal{R},u\leq
z,z\leq z^{\prime},\Gamma,w:\forall xA\Rightarrow\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},w:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$
$(\forall^{in}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},w:\forall
xA,\Gamma\Rightarrow\Delta$

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{n}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\underline{a}\in D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$
$(tra)$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{n}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\Gamma,\underline{a}\in
D_{v}\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{in}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\Gamma\Rightarrow w:\exists xA,\Delta$ $(tra)$ $\mathcal{R},u\leq
z,z\leq z^{\prime},\Gamma\Rightarrow w:\exists xA,\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{in}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},\Gamma\Rightarrow
w:\exists xA,\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ $(nd)$ $\mathcal{R},w\leq u,u\leq v,w\leq
v,\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$ $(tra)$ $\mathcal{R},w\leq
u,u\leq v,\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq u,u\leq v,w\leq
v,\underline{a}\in D_{w},\underline{a}\in D_{u},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ IH $\mathcal{R},w\leq u,u\leq
v,\underline{a}\in D_{w},\underline{a}\in D_{u},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ $(nd)$ $\mathcal{R},w\leq u,u\leq
v,\underline{a}\in D_{w},\underline{a}\in D_{u},\Gamma\Rightarrow\Delta$
$(nd)$ $\mathcal{R},w\leq u,u\leq v,\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$

As with the admissibility proof for $(ref)$, the side condition of the
$(id^{n}_{q})$ rule still holds after $u\leq z^{\prime}$ is deleted, and the
side condition of the $(\exists^{n}_{r})$, $(\exists^{in}_{r})$,
$(\forall^{n}_{l})$, and $(\forall^{in}_{l})$ cases continues to hold after
the invocation of IH. If a directed path traverses the relational atom $u\leq
z^{\prime}$ in the $(id^{n}_{q})$ case, a directed path still exists by
replacing $u\leq z^{\prime}$ with $u\leq z,z\leq z^{\prime}$ in the given
path. In the other cases, if the directed path traverses the $u\leq
z^{\prime}$ relational atom, then the relational atoms $u\leq z,z\leq
z^{\prime}$ are still present in the sequent after invoking IH, ensuring that
a path between $v$ and $w$ continues to exist. ∎

###### Lemma 7.1.

The $(ref)$ and $(tra)$ rules are admissible in the calculus
$\mathsf{G3IntQC}^{*}$.

######  Proof A.4.

We prove the result by induction on the height of the given derivation. We
assume w.l.o.g. that the last inference in the given derivation is an instance
of $(ref)$ or $(tra)$, and that this is the only instance of the rule in the
given derivation. The general result follows by successively eliminating
topmost occurrences of $(ref)$ or $(tra)$ from a given derivation until it is
free of such inferences. By Lem. 4.15 and Lem. 7.3, we need only consider the
non-trivial $(id^{c}_{q})$, $(\exists^{c}_{r})$, $(\exists^{ic}_{r})$,
$(\forall^{c}_{l})$, $(\forall^{ic}_{l})$, $(nd)$, and $(cd)$ cases.

Base case. We let $\mathcal{R}^{\prime}:=\mathcal{R},\underline{a}_{1}\in
D_{v_{1}},\ldots,\underline{a}_{n}\in D_{v_{n}}$ in the $(id^{n}_{q})$ cases
below. In both the $(ref)$ and $(tra)$ cases, the side condition that there is
an undirected path from $v_{i}$ to $w$, for each $i\in\\{1,\ldots,n\\}$, holds
in the end sequent. If none of the undirected paths from $v_{i}$ to $w$
contain $u\leq u$ ($u\leq z^{\prime}$), then the paths are present in
$\mathcal{R}^{\prime}$ ($\mathcal{R}^{\prime},u\leq z,z\leq z^{\prime}$,
resp.), and if an undirected path from $v_{i}$ to $w$ contains $u\leq u$
($u\leq z^{\prime}$, resp.), then deleting each occurrence of $u\leq u$ from
the undirected path (replacing each occurrence of $u\leq z^{\prime}$ with
$u\leq z,z\leq z^{\prime}$, resp.) gives a new path from $v_{i}$ to $w$.

$(id^{n}_{q})$ $\mathcal{R}^{\prime},u\leq u,\Gamma,w:p(\vv{\underline{a}})\Rightarrow w:p(\vv{\underline{a}}),\Delta$ $(ref)$ $\mathcal{R}^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow w:p(\vv{\underline{a}}),\Delta$ |  $(id^{c}_{q})$ $\mathcal{R}^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow w:p(\vv{\underline{a}}),\Delta$
---|---

$(id_{q}^{c})$ $\mathcal{R}^{\prime},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$ $(tra)$ $\mathcal{R}^{\prime},u\leq z,z\leq
z^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$
---

$(id_{q}^{c})$ $\mathcal{R}^{\prime},u\leq z,z\leq
z^{\prime},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$
---

Inductive step. For the inductive step, we consider the non-trivial
$(\exists^{c}_{r})$, $(\exists^{ic}_{r})$, $(\forall^{c}_{l})$,
$(\forall^{ic}_{l})$, $(nd)$, and $(cd)$ cases. We first show how to permute
$(ref)$ above each of these rules, and then focus on the permutation of
$(tra)$ above each considered rule.

$\mathcal{R},u\leq u,\underline{a}\in D_{v},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{c}_{r})$
$\mathcal{R},u\leq u,\underline{a}\in D_{v},\Gamma\Rightarrow w:\exists
xA,\Delta$ $(ref)$ $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow
w:\exists xA,\Delta$

IH $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{c}_{r})$
$\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$

$\mathcal{R},u\leq u,\underline{a}\in D_{v},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{ic}_{r})$
$\mathcal{R},u\leq u,\Gamma\Rightarrow w:\exists xA,\Delta$ $(ref)$
$\mathcal{R},\Gamma\Rightarrow w:\exists xA,\Delta$

IH $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{ic}_{r})$
$\mathcal{R},\Gamma\Rightarrow w:\exists xA,\Delta$

$\mathcal{R},u\leq u,\underline{a}\in D_{v},w:A(\underline{a}/x),w:\forall
xA,\Gamma\Rightarrow\Delta$ $(\forall^{c}_{l})$ $\mathcal{R},u\leq
u,\underline{a}\in D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$ $(ref)$
$\mathcal{R},\underline{a}\in D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$

IH $\mathcal{R},\underline{a}\in D_{v},w:A(\underline{a}/x),w:\forall
xA,\Gamma\Rightarrow\Delta$ $(\forall^{c}_{l})$ $\mathcal{R},\underline{a}\in
D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$

$\mathcal{R},u\leq u,\underline{a}\in
D_{v},\Gamma,w:A(\underline{a}/x),w:\forall xA\Rightarrow\Delta$
$(\forall^{ic}_{l})$ $\mathcal{R},u\leq u,\Gamma,w:\forall
xA\Rightarrow\Delta$ $(ref)$ $\mathcal{R},w:\forall
xA,\Gamma\Rightarrow\Delta$

IH $\mathcal{R},\underline{a}\in D_{v},\Gamma,w:A(\underline{a}/x),w:\forall
xA,\Gamma\Rightarrow\Delta$ $(\forall^{ic}_{l})$ $\mathcal{R},w:\forall
xA,\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq w,\underline{a}\in D_{w},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$ $(nd)$ $\mathcal{R},w\leq w,\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$ $(ref)$ $\mathcal{R},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq w,\underline{a}\in D_{w},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$ $(ctr_{\mathcal{R}})$ $\mathcal{R},w\leq
w,\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$ IH
$\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq w,\underline{a}\in D_{w},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$ $(cd)$ $\mathcal{R},w\leq w,\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$ $(ref)$ $\mathcal{R},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq w,\underline{a}\in D_{w},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$ $(ctr_{\mathcal{R}})$ $\mathcal{R},w\leq
w,\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$ IH
$\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$

In the $(\exists^{c}_{r})$, $(\exists^{ic}_{r})$, $(\forall^{c}_{l})$, and
$(\forall^{ic}_{l})$ cases above, observe that each rule can be applied after
invoking IH for the following reason: if the undirected path from $v$ to $w$
does not go through $u$, then the path is still present after applying IH, and
if the undirected path contains $u\leq u$, then deleting all occurrences of
$u\leq u$ from the undirected path yields another undirected path between $v$
and $w$. The $(tra)$ cases are considered below:

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\underline{a}\in
D_{v},\Gamma,w:A(\underline{a}/x),w:\forall xA\Rightarrow\Delta$
$(\forall^{c}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\underline{a}\in D_{v},\Gamma,w:\forall xA\Rightarrow\Delta$
$(tra)$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma,w:\forall xA\Rightarrow\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},w:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$
$(\forall^{c}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\underline{a}\in
D_{v},\Gamma,w:A(\underline{a}/x),w:\forall xA\Rightarrow\Delta$
$(\forall^{ic}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\Gamma,w:\forall xA\Rightarrow\Delta$ $(tra)$ $\mathcal{R},u\leq
z,z\leq z^{\prime},\Gamma,w:\forall xA\Rightarrow\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},w:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$
$(\forall^{ic}_{l})$ $\mathcal{R},u\leq z,z\leq z^{\prime},w:\forall
xA,\Gamma\Rightarrow\Delta$

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{c}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\underline{a}\in D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$
$(tra)$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{c}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$

$\mathcal{R},u\leq z,z\leq z^{\prime},u\leq z^{\prime},\Gamma,\underline{a}\in
D_{v}\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{ic}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},u\leq
z^{\prime},\Gamma\Rightarrow w:\exists xA,\Delta$ $(tra)$ $\mathcal{R},u\leq
z,z\leq z^{\prime},\Gamma\Rightarrow w:\exists xA,\Delta$

IH $\mathcal{R},u\leq z,z\leq z^{\prime},\underline{a}\in
D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$
$(\exists^{ic}_{r})$ $\mathcal{R},u\leq z,z\leq z^{\prime},\Gamma\Rightarrow
w:\exists xA,\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ $(nd)$ $\mathcal{R},w\leq u,u\leq v,w\leq
v,\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$ $(tra)$ $\mathcal{R},w\leq
u,u\leq v,\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq u,u\leq v,w\leq
v,\underline{a}\in D_{w},\underline{a}\in D_{u},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ IH $\mathcal{R},w\leq u,u\leq
v,\underline{a}\in D_{w},\underline{a}\in D_{u},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta$ $(nd)$ $\mathcal{R},w\leq u,u\leq
v,\underline{a}\in D_{w},\underline{a}\in D_{u},\Gamma\Rightarrow\Delta$
$(nd)$ $\mathcal{R},w\leq u,u\leq v,\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,a\in D_{w},a\in
D_{v},\Gamma\Rightarrow\Delta$ $(cd)$ $\mathcal{R},w\leq u,u\leq v,w\leq
v,a\in D_{v},\Gamma\Rightarrow\Delta$ $(tra)$ $\mathcal{R},w\leq u,u\leq
v,a\in D_{v},\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,a\in D_{w},a\in
D_{v},\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq u,u\leq v,w\leq
v,a\in D_{w},a\in D_{u},a\in D_{v},\Gamma\Rightarrow\Delta$ IH
$\mathcal{R},w\leq u,u\leq v,a\in D_{w},a\in D_{u},a\in
D_{v},\Gamma\Rightarrow\Delta$ $(cd)$ $\mathcal{R},w\leq u,u\leq v,a\in
D_{u},a\in D_{v},\Gamma\Rightarrow\Delta$ $(cd)$ $\mathcal{R},w\leq u,u\leq
v,a\in D_{v},\Gamma\Rightarrow\Delta$

We now argue that the side condition $v\sim^{\mathcal{R}}w$ of
$(\exists^{c}_{r})$, $(\exists^{ic}_{r})$, $(\forall^{c}_{l})$, and
$(\forall^{ic}_{l})$ continues to hold after applying IH. If the undirected
path from $v$ to $w$ does not contain $u\leq z^{\prime}$, then the side
condition trivially holds. If, on the other hand, the undirected path from $v$
to $w$ contains $u\leq z^{\prime}$, then another undirected path from $v$ to
$w$ is found by replacing all occurrences of $u\leq z^{\prime}$ with $u\leq
z,z\leq z^{\prime}$, which continues to be present after the invocation of IH.
∎

###### Corollary 8.13.

All rules in $\mathrm{NR}$ are admissible in $\mathsf{NInt}$, $\mathsf{NIntQ}$
and $\mathsf{NIntQC}$.

######  Proof A.5.

We prove the admissibility of each rule of $\mathrm{NR}$ in turn. The first
three cases we consider are the $(wk_{l})$, $(wk_{r})$, and $(psub)$ cases,
though we omit the $(wk_{r})$ case since it is similar to the $(wk_{l})$ case.

$\Sigma\\{X\rightarrow Y\\}$ Thm. 8.9 $\mathfrak{L}(\Sigma\\{X\rightarrow Y\\})$ . = $\mathcal{R},\Gamma,w:X\Rightarrow w:Y,\Delta$ $(wk)$ $\mathcal{R}^{\prime},\Gamma,w:X,w:Z\Rightarrow w:Y,\Delta$ Thm. 8.9 $\mathfrak{N}(\mathcal{R},\Gamma,w:X,w:Z\Rightarrow w:Y,\Delta)$ . = $\Sigma\\{X,Z\rightarrow Y\\}$ |  $\Sigma$ Thm. 8.9 $\mathfrak{L}(\Sigma)$ . = $\Lambda$ $(psub)$ $\Lambda(\underline{a}/\underline{b})$ Thm. 8.9 $\mathfrak{N}(\Lambda(\underline{a}/\underline{b}))$ . = $\Sigma(\underline{a}/\underline{b})$
---|---

We assume that $\mathcal{R}^{\prime}:=\mathcal{R},\vv{\underline{a}}\in D_{w}$
where $\vv{\underline{a}}$ are all parameters occurring in the labelled
formulae of $w:Z$. This ensures that the labelled sequent
$\mathcal{R}^{\prime},\Gamma,w:X,w:Z\Rightarrow w:Y,\Delta$ is nestedlike (cf.
Def. 4.7 and 4.8). Also, the labelled sequent
$\Lambda(\underline{a}/\underline{b})$ in the $(psub)$ derivation is trivially
nestedlike since
$\mathfrak{L}(\Sigma(\underline{a}/\underline{b}))=\Lambda(\underline{a}/\underline{b})$
(up to a change of labels). This implies that the second invocation of Thm.
8.9 in both cases is valid.

We next consider the $(ctr_{l})$, $(ctr_{r})$, $(nr)$, and $(mrg_{1})$ cases,
but omit the proof of $(ctr_{r})$ since it is similar to $(ctr_{l})$. In the
top right (i.e. $(nr)$) derivation, we assume that $v$ is the root of
$G(\mathfrak{L}(\Sigma))$ and that $w$ is fresh, meaning we effectively change
the root from $v$ to $w$ after applying $(wk)$.

$\Sigma\\{X,Z,Z\rightarrow Y\\}$ Thm. 8.9 $\mathfrak{L}(\Sigma\\{X,Z,Z\rightarrow Y\\})$ . = $\mathcal{R},\Gamma,w:X,w:Z,w:Z\Rightarrow w:Y,\Delta$ $(ctr_{l})+(ctr_{\mathcal{R}})$ $\mathcal{R},\Gamma,w:X,w:Z\Rightarrow w:Y,\Delta$ Thm. 8.9 $\mathfrak{N}(\mathcal{R},\Gamma,w:X,w:Z\Rightarrow w:Y,\Delta)$ . = $\Sigma\\{X,Z\rightarrow Y\\}$ |  $\Sigma$ Thm. 8.9 $\mathfrak{L}(\Sigma)$ . = $\mathcal{R},\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R},w\leq v,\Gamma\Rightarrow\Delta$ Thm. 8.9 $\mathfrak{N}(\mathcal{R},w\leq v,\Gamma\Rightarrow\Delta)$ . = $\rightarrow[\Sigma]$
---|---

$\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}],[\Sigma^{\prime}]\\}$ Thm. 8.9
$\mathfrak{L}(\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}],[\Sigma^{\prime}]\\})$
. =
$\mathcal{R},\mathcal{R}^{\prime},\mathcal{R}^{\prime\prime},\Gamma,\Gamma^{\prime},\Gamma^{\prime\prime}\Rightarrow\Delta^{\prime},\Delta^{\prime\prime},\Delta$
$(lsub)\times n$
$\mathcal{R},\mathcal{R}^{\prime},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime},\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta^{\prime},\Delta$
$(ctr_{\mathcal{R}})+(ctr_{l})+(ctr_{r})$
$\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta$
Thm. 8.9
$\mathfrak{N}(\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta)$
. = $\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}]\\}$

The labelled sequents $\mathcal{R},\Gamma,w:X,w:Z\Rightarrow w:Y,\Delta$,
$\mathcal{R},w\leq v,\Gamma\Rightarrow\Delta$, and
$\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta$
are nestedlike, as the conclusion of each derivation _is_ the nested sequent
that when input into $\mathfrak{L}$ outputs each such labelled sequent (up to
a change of labels). In the bottom (i.e. $(mrg_{1})$) derivation, we assume
that the first copy of $\Sigma^{\prime}$ is translated to
$\mathcal{R}^{\prime},\Gamma^{\prime}\Rightarrow\Delta^{\prime}$ under
$\mathfrak{L}$ and that the second copy of $\Sigma^{\prime}$ is translated to
$\mathcal{R}^{\prime\prime},\Gamma^{\prime\prime}\Rightarrow\Delta^{\prime\prime}$
under $\mathfrak{L}$. Therefore, the graphs
$G(\mathcal{R}^{\prime},\Gamma^{\prime}\Rightarrow\Delta^{\prime})$ and
$G(\mathcal{R}^{\prime\prime},\Gamma^{\prime\prime}\Rightarrow\Delta^{\prime\prime})$
are isomorphic, and so, the $n$ applications of $(lsub)$ correspond to the
replacement of labels in
$\mathcal{R}^{\prime\prime},\Gamma^{\prime\prime}\Rightarrow\Delta^{\prime\prime}$
with labels in
$\mathcal{R}^{\prime},\Gamma^{\prime}\Rightarrow\Delta^{\prime}$ to make these
two _identical_. Then, using $(ctr_{\mathcal{R}})$, $(ctr_{l})$, and
$(ctr_{r})$, we contract all duplicate copies of relational atoms and labelled
formulae to obtain
$\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta$.

We prove the admissibility of the $(mrg_{2})$ rule below. We assume that the
label $w$ is associated with the component $X_{1}\rightarrow Y_{1}$ and the
label $v$ is associated with the component $X_{2}\rightarrow Y_{2}$. As
before, the conclusion of the derivation serves as the nested sequent that
when input into $\mathfrak{L}$ yields
$\mathcal{R}(w/v),\Gamma(w/v),w:X_{1},w:X_{2}\Rightarrow
w:Y_{1},w:Y_{2},\Delta(w/v)$ (up to a change of labels), thus showing the
validity of our second use of Thm. 8.9.

$\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow
Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]\\}$ Thm. 8.9
$\mathfrak{L}(\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow
Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]\\})$ . = $\mathcal{R},w\leq
v,\Gamma,w:X_{1},v:X_{2}\Rightarrow w:Y_{1},v:Y_{2},\Delta$ $(lsub)$
$\mathcal{R}(w/v),w\leq w,\Gamma(w/v),w:X_{1},w:X_{2}\Rightarrow
w:Y_{1},w:Y_{2},\Delta(w/v)$ $(ref)$
$\mathcal{R}(w/v),\Gamma(w/v),w:X_{1},w:X_{2}\Rightarrow
w:Y_{1},w:Y_{2},\Delta(w/v)$ Thm. 8.9
$\mathfrak{N}(\mathcal{R}(w/v),\Gamma(w/v),w:X_{1},w:X_{2}\Rightarrow
w:Y_{1},w:Y_{2},\Delta(w/v))$ . = $\Sigma\\{X_{1},X_{2}\rightarrow
Y_{1},Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]\\}$

Next we consider the $(ew_{1})$ case. We assume that
$\mathfrak{L}(\Sigma^{\prime})=\mathcal{R}^{\prime},\Gamma^{\prime}\Rightarrow\Delta^{\prime}$,
which shows that the conclusion of the derivation serves as the nested
sequent, which when input into $\mathfrak{L}$ outputs
$\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta$
(up to a change of labels). Therefore, the second use of Thm. 8.9 is valid.

$\Sigma\\{X\rightarrow Y\\}$ Thm. 8.9 $\mathfrak{L}(\Sigma\\{X\rightarrow
Y\\})$ . = $\mathcal{R},\Gamma\Rightarrow\Delta$ $(wk)$
$\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta$
Thm. 8.9
$\mathfrak{N}(\mathcal{R},\mathcal{R}^{\prime},\Gamma,\Gamma^{\prime}\Rightarrow\Delta^{\prime},\Delta)$
. = $\Sigma\\{X\rightarrow Y,[\Sigma^{\prime}]\\}$

In the proof of the admissibility of $(ew_{2})$ below, we assume that the
label $w$ is associated with the component $X_{1}\rightarrow Y_{1}$, the label
$v$ is associated with the component $X_{2}\rightarrow Y_{2}$, and that the
label $u$ is fresh. Up to a change of labels, the conclusion of the derivation
is the nested sequent that when input into $\mathfrak{L}$ outputs the labelled
sequent $\mathcal{R},w\leq u,u\leq v,\Gamma,w:X_{1},v:X_{2}\Rightarrow
w:Y_{1},v:Y_{2},\Delta$, justifying our second use of Thm. 8.9.

$\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow
Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]\\}$ Thm. 8.9
$\mathfrak{L}(\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow
Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]\\})$ . = $\mathcal{R},w\leq
v,\Gamma,w:X_{1},v:X_{2}\Rightarrow w:Y_{1},v:Y_{2},\Delta$ $(wk)$
$\mathcal{R},w\leq u,u\leq v,w\leq v,\Gamma,w:X_{1},v:X_{2}\Rightarrow
w:Y_{1},v:Y_{2},\Delta$ $(tra)$ $\mathcal{R},w\leq u,u\leq
v,\Gamma,w:X_{1},v:X_{2}\Rightarrow w:Y_{1},v:Y_{2},\Delta$ Thm. 8.9
$\mathfrak{N}(\mathcal{R},w\leq u,u\leq v,\Gamma,w:X_{1},v:X_{2}\Rightarrow
w:Y_{1},v:Y_{2},\Delta)$ . = $\Sigma\\{X_{1}\rightarrow Y_{1},[\
\rightarrow[X_{2}\rightarrow Y_{2},[\Sigma_{1}],\ldots,[\Sigma_{n}]]]\\}$

Last, we show the admissibility of $(lwr)$ and $(cut)$. In the proof of the
admissibility of $(lwr)$ below, we assume that the label $w$ is associated
with the component $X_{1}\rightarrow A,Y_{1}$ and that the label $v$ is
associated with the component $X_{2}\rightarrow A,Y_{2}$. In the proof of the
admissibility of $(cut)$, we assume that the label $w$ is associated with
$X\rightarrow A,Y$ and $X,A\rightarrow Y$. As in all previous cases, the end
sequent of each derivation serves as the nested sequent (up to a change of
labels) that when input into $\mathfrak{L}$ yields the labelled sequent before
the (second) invocation of Thm. 8.9, thus showing that our use of the theorem
is valid.

$\Sigma\\{X_{1}\rightarrow A,Y_{1},[X_{2}\rightarrow A,Y_{2}]\\}$ Thm. 8.9
$\mathfrak{L}(\Sigma\\{X_{1}\rightarrow A,Y_{1},[X_{2}\rightarrow
A,Y_{2}]\\})$ . = $\mathcal{R},w\leq v,\Gamma\Rightarrow w:A,v:A,\Delta$ Thm.
3.1-(i)-(c) $\mathcal{R},w\leq v,\Gamma,w:A\Rightarrow v:A,\Delta$ $(cut)$
$\mathcal{R},w\leq v,\Gamma\Rightarrow v:A\Rightarrow\Delta$ Thm. 8.9
$\mathfrak{N}(\mathcal{R},w\leq v,\Gamma\Rightarrow v:A,\Delta)$ . =
$\Sigma\\{X_{1}\rightarrow Y_{1},[X_{2}\rightarrow A,Y_{2}]\\}$

$\Sigma\\{X\rightarrow A,Y\\}$ Thm. 8.9 $\mathfrak{L}(\Sigma\\{X\rightarrow
A,Y\\})$ . = $\mathcal{R},\Gamma\Rightarrow w:A,\Delta$
$\Sigma\\{X,A\rightarrow Y\\}$ Thm. 8.9 $\mathfrak{L}(\Sigma\\{X,A\rightarrow
Y\\})$ . = $\mathcal{R},\Gamma,w:A\Rightarrow\Delta$ $(cut)$
$\mathcal{R},\Gamma\Rightarrow\Delta$ Thm. 8.9
$\mathfrak{N}(\mathcal{R},\Gamma\Rightarrow\Delta)$ . = $\Sigma\\{X\rightarrow
Y\\}$

∎