11institutetext: Institut für Logic and Computation, Technische Universität
Wien, 1040 Wien, Austria
11email<EMAIL_ADDRESS>
# On the Correspondence between Nested Calculi and Semantic Systems for
Intuitionistic Logics

Tim Lyon

###### Abstract

This paper studies the relationship between labelled and nested calculi for
propositional intuitionistic logic, first-order intuitionistic logic with non-
constant domains, and first-order intuitionistic logic with constant domains.
It is shown that Fitting’s nested calculi naturally arise from their
corresponding labelled calculi—for each of the aforementioned logics—via the
elimination of structural rules in labelled derivations. The translational
correspondence between the two types of systems is leveraged to show that the
nested calculi inherit proof-theoretic properties from their associated
labelled calculi, such as completeness, invertibility of rules, and cut-
admissibility. Since labelled calculi are easily obtained via a logic’s
semantics, the method presented in this paper can be seen as one whereby
refined versions of labelled calculi (containing nested calculi as fragments)
with favorable properties are derived directly from a logic’s semantics.

###### keywords:

First-order · Intuitionistic logic · Kripke semantics · Labelled calculi ·
Nested calculi · Proof theory · Propositional · Refinement

##  1 Introduction

In his seminal work [12], Gentzen introduced the _sequent calculus_ framework
for classical and intuitionistic logic, and proved the celebrated _Hauptsatz_
, i.e. _cut-elimination theorem_ , for the systems. As a corollary of his
theorem, it can be observed that any formula provable in one of Gentzen’s
systems, is provable with an _analytic derivation_ , that is, a derivation
where all formulae used to _reach_ the conclusion of the derivation, _occur_
in the conclusion of the derivation. This method of proof happens to be of
practical consequence, and as such, many variations and extensions of
Gentzen’s sequent calculi have been assembled and proposed—examples include
tableaux calculi [7, 9], display calculi [2, 18, 28], hypersequent calculi [1,
22], labelled calculi [11, 24, 27], and nested calculi [3, 4, 14]. Such
calculi have been applied to provide decision algorithms [12, 22], to automate
the extraction of interpolants [19], and to automated counter-model extraction
[17, 25].

In this paper, we focus entirely on the labelled and nested proof-theoretic
paradigms. The labelled paradigm may be qualified as _semantic_ as calculi are
built by transforming the semantic clauses and Kripke-frame properties of a
logic into inference rules [24, 27]. Despite some drawbacks and criticisms of
this approach [1], the labelled paradigm offers many advantages. First, it is
relatively straightforward to transform the semantics of a logic into a
calculus; in fact, this process has been shown to be _automatable_ [5].
Second, the approach is exceptionally modular—allowing for the addition or
deletion of rules to immediately obtain calculi for weaker or stronger
logics—and is applicable to a wide variety of logics [6, 17, 24, 27]. Last,
labelled calculi consistently possess fundamental proof-theoretic properties
such as invertibility of rules, admissibility of structural rules, and cut-
admissibility—with fairly general results provided for large classes of modal,
intuitionistic, and related logics [6, 17, 24, 27]. Although these
characteristics are certainly favorable, a drawback of labelled calculi is
that they typically involve a complicated syntax (which incorporates a large
amount of semantic information), the sequents utilized in proofs encode
general graphs, and inference rules often violate the subformula property
(i.e. labelled calculi are not usually analytic). Such properties cause an
unnecessary increase in the size of sequents/proofs, and a decrease in the
efficiency of associated automated reasoning algorithms.

In contrast to the data structures (called, _labelled sequents_) employed in
labelled calculi—which can be viewed as general graphs—the nested paradigm
employs treelike data structures (called, _nested sequents_) which manipulate
logical information and are used to derive theorems. The inception of the
paradigm is often attributed to Bull [4] and Kashima [14], though it should be
noted that nested calculi can be considered ‘upside down’ versions of prefixed
tableaux calculi, which were introduced much earlier in 1972 by Fitting [7].
(NB. See [9] for a discussion on the relationship between nested and tableaux
systems). A strength of the nested paradigm is that the nested sequents
employed reduce the bureaucracy and syntactic structures appearing in proofs,
showing the nested formalism to be more parsimonious than the labelled
formalism. Also, the nested formalism has proven itself useful in applications
such as constructing analytic calculi [3, 23], developing automated reasoning
methods [25], and verifying interpolation [19]. Still, in spite of these
advantages, the construction of nested calculi and the confirmation of their
proof-theoretic properties is often done on a case-by-case basis. That is to
say, the nested paradigm lacks general results—like those of the labelled
paradigm—regarding the immediate construction of calculi in possession of
fundamental properties.

Due to the fact that the labelled formalism is well-suited for constructing
calculi possessing essential proof-theoretic properties, and the nested
formalism is more refined and better suited for a variety of applications, a
method of extracting nested calculi from labelled calculi—with the properties
of the latter preserved—is highly desirable. This _refinement_ process allows
us to capture the best of both worlds: we invoke the general results of the
labelled setting to obtain satisfactory labelled calculi for a class of
logics, and via refinement, transform the systems into nested calculi better
suited for applications. Similar ideas and relationships have been discussed
in the literature [13, 17, 16, 20, 21], where refined calculi (which can be
considered nested calculi) were derived from labelled calculi for modal,
intuitionistic, and related logics. (NB. The paper [21] mentions results
strongly related to Sect. 5. Although the results presented here were
discovered independently, the work of Sect. 5 can be seen as a detailed
explication and expansion of the work presented in [21]. Moreover, [21] does
not consider the non-trivial and interesting first-order cases considered
here.)

In this paper we advance our understanding of the aforementioned method, and
show how to extract _slight_ variants of Fitting’s nested calculi for
propositional intuitionistic logic, first-order intuitionistic logic with non-
constant domains, and first-order intuitionistic logic with constant domains
from the labelled calculi for these logics. Additionally, we demonstrate the
converse translation—showing how to transform each considered nested calculus
into its associated labelled calculus. These translations are worthwhile in
that they show how each nested calculus inherits properties from its
corresponding labelled calculus, and also shed light on how the semantics of
each logic affects the shape of rules and syntactic structures inherent in
nested derivations (via the labelled calculi).

The organization of this paper is as follows: Sect. 2 introduces the semantics
and axiomatizations for the intuitionistic logics we will consider. Sect. 3
introduces the labelled and nested calculi for these logics. Sect. 4
introduces preliminary definitions and lemmata sufficient to translate
intuitionistic labelled calculi into nested calculi, and vice-versa. Sect. 5,
Sect. 6, and Sect. 7 show how to refine each labelled calculus through
structural rule elimination, allowing for the extraction of the nested
calculus from the labelled calculus for propositional intuitionistic logic,
first-order intuitionistic logic with non-constant domains, and first-order
intuitionisitic logic with constant domains, respectively. Sect. 8 shows how
to translate each nested calculus into its associated labelled calculus, and
discusses corollaries of the translational correspondence between the
calculi—primarily focusing on the properties inherited by each nested calculus
from its corresponding labelled calculus. The last section, Sect. 9,
concludes.

This paper serves as an enhanced and revised version of the conference paper
[16]. Most significantly, the nested-to-labelled translation of Sect. 4, the
content of Sect. 6, and the majority of content in Sect. 8 are entirely new.
Beyond this, the paper was written with an increased focus and more detailed
exposition on _how_ the labelled calculi are refined in order to extract each
nested calculus—this provides the paper with more explanatory force than [16].
Also, it should be noted that this paper corrects an error that occurs in the
conference version. In [16], the labelled calculus $\mathsf{G3IntQC}$ is
lacking a structural rule (called $(ihd)$ in this paper) corresponding to the
condition that domains in first-order intuitionistic models are _non-empty_ ,
or _inhabited_. Without the inclusion of this rule, $\mathsf{G3IntQC}$ is
incomplete as modus ponens cannot be simulated in the calculus (see Thm. 3.1
and Appendix A for details). We have included this rule here and adjusted the
content of [16] regarding $\mathsf{G3IntQC}$ accordingly. Furthermore, to
increase the flow and readability of the paper, some results outside the scope
of, or auxiliary to, our main focus (i.e. the translational correspondence
between labelled and nested calculi for intuitionistic logics) have been moved
to a technical appendix (Appendix A) for the interested reader.

Last, Fig. 1 shows the transformations (indicated by a solid arrow) and
translations (indicated by a dotted arrow) between the various intuitionistic
calculi considered. Transformations indicate that derivations in one system
(or in a fragment of the system) are effectively (i.e. algorithmically)
transformable to derivations in another system, and translations indicate a
transformation along with a change in notation. The symbols $\mathfrak{N}$ and
$\mathfrak{L}$ represent a change from labelled to nested notation, and nested
to labelled notation, respectively. The inclusion sign $\subset$ is taken to
mean that one calculus consists of a proper subset of the rules in another
calculus.

$\textstyle{\mathsf{G3Int}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Thm.
5.7$\scriptstyle{\bigcap}$$\textstyle{\mathsf{IntL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{N}}$Lem.
8.1$\scriptstyle{\bigcap}$$\textstyle{\mathsf{NInt}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{L}}$$\scriptstyle{\bigcap}$Thm.
5.11$\textstyle{\mathsf{G3IntQ}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Thm.
6.8$\scriptstyle{\bigcap}$$\textstyle{\mathsf{IntQL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{N}}$Thm.
6.14Lem. 8.3Cor.
8.18$\textstyle{\mathsf{NIntQ}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{L}}$Thm.
6.16Cor.
8.18$\textstyle{\mathsf{G3IntQC}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Thm.
7.8$\textstyle{\mathsf{IntQCL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{N}}$Thm.
7.12Lem.
8.5$\textstyle{\mathsf{NIntQC}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathfrak{L}}$Thm.
7.14
---

Figure 1: Transformations and translations between the intuitionistic calculi
considered.

##  2 Logical Preliminaries

In this section, we introduce the language, semantics, and axiomatizations for
propositional intuitionistic logic $\mathsf{Int}$, first-order intuitionistic
logic with non-constant domains $\mathsf{IntQ}$, and first-order
intuitionistic logic with constant domains $\mathsf{IntQC}$. The first
subsection will discuss the propositional setting, whereas the second
subsection will discuss the first-order setting.

###  2.1 Propositional Intuitionistic Logic

The propositional language $\mathcal{L}$ is defined via the BNF grammar shown
below:

$A::=p\ |\ \bot\ |\ (A\vee A)\ |\ (A\wedge A)\ |\ (A\supset A)$

where $p$ is among a denumerable set of _propositional variables_
$\mathrm{Prop}=\\{p,q,r,\ldots\\}$. As usual, we define intuitionistic
negation as $\neg A:=A\supset\bot$. Moreover, the language admits a relational
(or, Kripke-style) semantics as defined below (cf. [15]).

######  Definition 2.1 ($\mathsf{Int}$-Frame, $\mathsf{Int}$-Model).

An _$\mathsf{Int}$ -frame_ is an ordered pair $F=(W,\leq)$ such that:

  * $\blacktriangleright$

$W$ is a non-empty set of worlds $\\{w,u,v,\ldots\\}$;

  * $\blacktriangleright$

$\leq\ \subseteq W\times W$ is a reflexive and transitive binary relation on
$W$.111The properties imposed on $\leq$ are defined as follows: (reflexivity)
for all $w\in W$, $w\leq w$, and (transitivity) for all $w,u,v\in W$, if
$w\leq v$ and $v\leq u$, then $w\leq u$.

An _$\mathsf{Int}$ -model_ is an ordered pair $M=(F,V)$ where $F$ is an
$\mathsf{Int}$-frame and $V:$ is a _valuation function_ mapping propositional
variables to subsets of $W$ satisfying the following _monotonicity condition_
:

$\mathbf{(M)}$ If $w\in V(p)$ and $w\leq v$, then $v\in V(p)$.

######  Definition 2.2 (Propositional Semantic Clauses).

Let $M=(W,\leq,V)$ be an $\mathsf{Int}$-model with $w\in W$. The _satisfaction
relation_ $M,w\Vdash A$ between $w\in W$ and a formula $A$ from $\mathcal{L}$
is inductively defined as follows:

  * $\blacktriangleright$

$M,w\not\Vdash\bot$;

  * $\blacktriangleright$

$M,w\Vdash p$ iff $w\in V(p)$;

  * $\blacktriangleright$

$M,w\Vdash A\vee B$ iff $M,w\Vdash A$ or $M,w\Vdash B$;

  * $\blacktriangleright$

$M,w\Vdash A\land B$ iff $M,w\Vdash A$ and $M,w\Vdash B$;

  * $\blacktriangleright$

$M,w\Vdash A\supset B$ iff for all $u\in W$, if $w\leq u$ and $M,u\Vdash A$,
then $M,u\Vdash B$.

We say that a formula $A$ is _globally true on $M$_, written $M\Vdash A$, iff
$M,u\Vdash A$ for all worlds $u\in W$. A formula $A$ is _$\mathsf{Int}$
-valid_, written $\Vdash_{\mathsf{Int}}A$, iff it is globally true on all
$\mathsf{Int}$-models. Last, we say that a set $\Phi$ of formulae
_semantically implies_ a formula $A$, written $\Phi\Vdash A$, iff for all
intuitionistic models $M$ with $w\in W$, if $M,w\Vdash B$ for all $B\in\Phi$,
then $M,w\Vdash A$.222We note that we could define a _global_ version of
semantic implication as follows: A set of formulae $\Phi$ _globally implies_ a
formula $A$ iff for all intuitionistic models $M$, if $M\Vdash B$ for all
$B\in\Phi$, then $M\Vdash A$. We make use of the local version in Def. 2.2
however, because the axiomatization we use for $\mathsf{Int}$ (shown in Fig.
2) is sound and complete relative to the local version of semantic implication
(Thm. 2.5) [10].

The monotonicity condition $\mathbf{(M)}$, together with the intuitionistic
semantics defined above, necessitates a general form of monotonicity as
detailed below:

######  Lemma 2.3 (General Monotonicity).

Let $M$ be a model with $w,v\in W$ of $M$. If $M,w\Vdash A$ and $w\leq v$,
then $M,v\Vdash A$.

######  Proof 2.4.

See [10, Lem. 3.2.16] for details. ∎

Additionally, propositional intuitionistic logic $\mathsf{Int}$ is finitely
axiomatizable. The axioms and inference rule syntactically characterizing
$\mathsf{Int}$ are given in Fig. 2. We define an _$\mathsf{Int}$ -derivation_
(relative to the axiomatization of $\mathsf{Int}$) from a set of formulae
$\Phi$ (written $\Phi\vdash A$) in the usual way (cf. [10, 26]). It is well-
known that the notion of semantic consequence for $\mathsf{Int}$ is equivalent
to the syntactic notion of an $\mathsf{Int}$-derivation from a set of
formulae:

######  Theorem 2.5 (Soundness and Completeness [10]).

For any $A\in\mathcal{L}$, $\Phi\Vdash A$ iff $\Phi\vdash A$.

$A\supset(B\supset A)\qquad(A\supset(B\supset C))\supset((A\supset
B)\supset(A\supset C))\qquad A\supset(B\supset(A\land B))$

$(A\land B)\supset A\qquad(A\land B)\supset B\qquad A\supset(A\lor
B)\qquad\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.41666pt\hbox{\vbox{\hbox{\hbox{\hskip 4.0pt\hbox{$A$}\hskip
4.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip 4.0pt\hbox{$A\supset B$}\hskip
4.0pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to64.09612pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt$(mp)$}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
24.00465pt\hbox{\hbox{\hskip 4.0pt\hbox{$B$}\hskip 4.0pt}}}}}\ignorespaces$

$B\supset(A\lor B)\qquad\bot\supset A\qquad(A\supset C)\supset((B\supset
C)\supset((A\lor B)\supset C))$

Figure 2: An axiomatization of propositional intuitionistic logic
$\mathsf{Int}$ [10].

###  2.2 First-Order Intuitionistic Logics

The language $\mathcal{Q}$ for our first-order logics is defined via the BNF
grammar below:

$A::=p(x_{1},\ldots,x_{n})\ |\ \bot\ |\ (A\vee A)\ |\ (A\land A)\ |\ (A\supset
A)\ |\ (\forall x)A\ |\ (\exists x)A$

where $p$ is among a denumerable set of $n$-ary _predicate symbols_
$\mathrm{Pred}=\\{p,q,r,\ldots\\}$ and $x_{1},\ldots,x_{n},x$ are _variables_
(with $n\in\mathbb{N}$). We refer to formulae of the form
$p(x_{1},\ldots,x_{n})$ as _atomic formulae_ when $n>0$, and refer to formulae
of the form $p$ as _propositional variables_ when $n=0$ (i.e. a $0$-ary
predicate $p$ is a propositional variable). Furthermore, we define a variable
$x$ to be a _free variable_ in $A$ iff it is not within the scope of a
quantifier $\forall x$ or $\exists x$, and to be a _bound variable_ iff it is
within the scope of a quantifier. Last, as in the propositional case, our
language admits a relational semantics, defined below.

######  Definition 2.6 ($\mathsf{IntQ}$-Frames, $\mathsf{IntQ}$-Models [10]).

We define an _$\mathsf{IntQ}$ -frame_ to be a tuple $F=(W,\leq,D)$ such that:

  * $\blacktriangleright$

$W$ is a non-empty set of worlds $\\{w,u,v,\ldots\\}$;

  * $\blacktriangleright$

$\leq\ \subseteq W\times W$ is a reflexive and transitive binary relation on
$W$;

  * $\blacktriangleright$

$D$ is a _domain function_ mapping a world $w\in W$ to a non-empty set $D_{w}$
of _objects_ $\\{a,b,c,\dots\\}$ satisfying the _nested domain condition_
shown below:

$\mathbf{(ND)}$ If $a\in D_{w}$ and $w\leq v$, then $a\in D_{v}$.

A _$\mathsf{IntQC}$ -frame_ is an _$\mathsf{IntQ}$ -frame_ that additionally
satisfies the following _constant domain condition_ shown below:

$\mathbf{(CD)}$ If $a\in D_{v}$ and $w\leq v$, then $a\in D_{w}$.

An _$\mathsf{IntQ}$ -model_ (_$\mathsf{IntQC}$ -model_) $M$ is an ordered pair
$(F,V)$ where $F$ is an $\mathsf{IntQ}$-frame ($\mathsf{IntQC}$-frame) and $V$
is a _valuation function_ such that $V(p,w)\subseteq(D_{w})^{n}$ (with
$n\in\mathbb{N}$) satisfying the following _monotonicity condition_ :

$\mathbf{(M)}$ If $w\in V(p,w)$ and $w\leq v$, then $v\in V(p,v)$ (if $p$ is
of arity $0$);

If $w\leq v$, then $V(p,w)\subseteq V(p,v)$ (if $p$ is of arity $n>0$).

We uphold the convention in [10] and assume that for each world $w\in W$,
$(D_{w})^{0}=\\{w\\}$, so $V(p,w)=\\{w\\}$ or $V(p,w)=\emptyset$, for a
propositional variable $p$.

As in [10], we forgo the direct interpretation of formulae from $\mathcal{Q}$
on relational models, and instead, introduce $D_{w}$-sentences (Def. 2.7) to
be interpreted on such models. Defining satisfaction relative to
$D_{w}$-sentences gives rise to a notion of validity for formulae in
$\mathcal{Q}$ (Def. 2.8). However, this notion of validity also depends on the
_universal closure_ of a formula: given that $A\in\mathcal{Q}$ contains only
$x_{1},\ldots,x_{n}$ as free variables, the universal closure $\forall\vv{x}A$
is taken to be the formula $\forall x_{1}\ldots\forall x_{n}A$.

######  Definition 2.7 ($D_{w}$-Sentence).

Let $M=(W,\leq,D,V)$ be an $\mathsf{IntQ}$-model with $w\in W$. We define
$\mathcal{Q}({D_{w}})$ to be the language $\mathcal{Q}$ expanded with
parameters $\underline{a},\underline{b},\underline{c},\ldots$ corresponding to
the objects in the set $D_{w}=\\{a,b,c,\ldots\\}$. We define a _$D_{w}$
-formula_ to be a formula in $\mathcal{Q}(D_{w})$, and we define a _$D_{w}$
-sentence_ to be a $D_{w}$-formula that does not contain any free variables.

######  Definition 2.8 (First-Order Semantic Clauses).

Let $M=(W,\leq,D,V)$ be an $\mathsf{IntQ}$\- or $\mathsf{IntQC}$-model with
$w\in W$. The _satisfaction relation_ $M,w\Vdash A$ between $w$ and a
$D_{w}$-sentence $A$ is inductively defined as follows:

  * $\blacktriangleright$

If $p$ is a propositional variable, then $M,w\Vdash p$ iff $w\in V(p,w)$;

  * $\blacktriangleright$

If $p$ is an $n$-ary predicate symbol $($with $n>0)$, then $M,w\Vdash
p(\underline{a}_{1},\cdots,\underline{a}_{n})$ iff $(a_{1},\cdots,a_{n})\in
V(p,w)$;

  * $\blacktriangleright$

$M,w\Vdash\forall xA$ iff for all $v\in W$ and all $a\in D_{v}$, if $w\leq v$,
then $M,v\Vdash A(\underline{a}/x)$;

  * $\blacktriangleright$

$M,w\Vdash\exists xA$ iff there exists an $a\in D_{w}$ such that $M,w\Vdash
A(\underline{a}/x)$.

The clauses for the $\lor$, $\land$, and $\supset$ connectives are the same as
in Def. 2.2. We say that a formula $A$ is _globally true on $M$_, written
$M\Vdash A$, iff $M,u\Vdash\forall\vv{x}A$ for all worlds $u\in W$. A formula
$A$ is _$\mathsf{IntQ}$ -valid_ (_$\mathsf{IntQC}$ -valid_), written
$\Vdash_{\mathsf{IntQ}}A$ ($\Vdash_{\mathsf{IntQC}}A$, resp.), iff it is
globally true on all $\mathsf{IntQ}$-models ($\mathsf{IntQC}$-models).

Similar to the propositional case, the monotonicity condition imposed on
atomic formulae in models generalizes:

######  Lemma 2.9 (General Monotonicity).

Let $M$ be an $\mathsf{IntQ}$\- or $\mathsf{IntQC}$-model with $w,v\in W$ of
$M$. For any $D_{w}$-sentence $A$, if $M,w\Vdash A$ and $w\leq v$, then
$M,v\Vdash A$.

######  Proof 2.10.

See [10, Lem. 3.2.16] for details. ∎

Sound and complete axiomatizations for our first-order intuitionistic logics
(viz. $\mathsf{IntQ}$ and $\mathsf{IntQC}$) are provided in Fig. 3. We define
the _substitution_ $(y/x)$ of the variable $y$ for the free variable $x$ on a
formula $A$ in the standard way as the replacement of all free occurrences of
$x$ in $A$ with $y$. Last, the side condition _$y$ is free for $x$_ (see Fig.
3) is taken to mean that $y$ does not become bound by a quantifier if
substituted for $x$.

$\forall x(B\supset A)\supset(B\supset\forall xA)~{}\textit{ with $x\not\in
B$}\qquad\forall x(A\supset B)\supset(\exists xA\supset B)~{}\textit{ with
$x\not\in B$}$

$\forall xA\supset A(y/x)~{}\textit{y free for x}\qquad A(y/x)\supset\exists
xA~{}\textit{y free for x}\qquad\forall xAA$

$\forall x(A\vee B)\supset\forall xA\vee B~{}\textit{ with $x\not\in B$}$

Figure 3: The axiomatization for the logic $\mathsf{IntQ}$ is given by
extending the axiomatization of $\mathsf{Int}$ with the first two rows. The
axiomatization for the logic $\mathsf{IntQC}$ is given by extending the
axiomatization of $\mathsf{Int}$ with all three rows. Both axiomatizations can
be found in [10].

The logics $\mathsf{IntQ}$ and $\mathsf{IntQC}$ are defined to be the smallest
set of formulae from $\mathcal{Q}$ closed under substitutions of the axioms
and applications of the inference rules in their axiomatizations. The sole
difference between the axiomatizations for $\mathsf{IntQ}$ and
$\mathsf{IntQC}$ is that the former omits the _constant domain axiom_ $\forall
x(A\vee B)\supset\forall xA\vee B$ (with $x\not\in B$) whereas the latter
includes it. We write $\vdash_{\mathsf{IntQ}}A$ ($\vdash_{\mathsf{IntQC}}A$)
to denote that $A$ is an element, or _theorem_ , of $\mathsf{IntQ}$
($\mathsf{IntQC}$, resp.).

######  Theorem 2.11 (Soundness and Completeness [10]).

For any $A\in\mathcal{Q}$, $\Vdash_{\mathsf{IntQ}}A$
($\Vdash_{\mathsf{IntQC}}A$) iff $\vdash_{\mathsf{IntQ}}A$
($\vdash_{\mathsf{IntQC}}A$, resp.).

##  3 Proof Calculi for Intuitionistic Logics

In this section, we introduce the labelled and nested proof systems for the
intuitionistic logics $\mathsf{Int}$, $\mathsf{IntQ}$, and $\mathsf{IntQC}$.
The first subsection presents the labelled system $\mathsf{G3Int}$ for
propositional intuitionistic logic from [6] as well as the first-order
extensions of this calculus, that makes use of quantifier and structural rules
motivated by those (viz. $\forall L$, $\forall R$, $id$, and $dd$) given in
[27, Ch. 6]. The second subsection introduces (slight variants of) Fitting’s
nested calculi for intuitionistic logics from [9].

###  3.1 The Labelled Calculi $\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and
$\mathsf{G3IntQC}$

We define _propositional $($first-order$)$ labelled sequents_ to be syntactic
objects of the form $L_{1}\Rightarrow L_{2}$ ($L_{1}^{\prime}\Rightarrow
L_{2}^{\prime}$, resp.), where $L_{1}$ and $L_{2}$ ($L_{1}^{\prime}$ and
$L_{2}^{\prime}$, resp.) are formulae defined via the BNF grammar below top
(below bottom, resp.).

$L_{1}::=\varepsilon\ |\ w:A\ |\ w\leq v\ |\ L_{1},L_{1}$ | $L_{2}::=\varepsilon\ |\ w:A\ |\ L_{2},L_{2}$
---|---
$L_{1}^{\prime}::=\varepsilon\ |\ w:A\ |\ \underline{a}\in D_{w}\ |\ w\leq v\ |\ L_{1}^{\prime},L_{1}^{\prime}$ | $L_{2}^{\prime}::=\varepsilon\ |\ w:A\ |\ L_{2}^{\prime},L_{2}^{\prime}$
---|---

In the propositional case, $A$ is in the language $\mathcal{L}$ and $w$ is
among a denumerable set of labels $\\{w,v,u,\ldots\\}$. In the first-order
case, $A$ is in the language $\mathcal{Q}$, $\underline{a}$ is among a
denumerable set of _parameters_
$\\{\underline{a},\underline{b},\underline{c},\ldots\\}$, and $w$ is among a
denumerable set of labels $\\{w,v,u,\ldots\\}$. We refer to formulae of the
forms $w\leq v$ and $\underline{a}\in D_{w}$ as _relational atoms_ (with
formulae of the form $\underline{a}\in D_{w}$ sometimes referred to as _domain
atoms_ , more specifically) and refer to formulae of the form $w:A$ as
_labelled formulae_. Due to the two types of formulae occurring in a labelled
sequent, we often use $\mathcal{R}$ to denote relational atoms, and $\Gamma$
and $\Delta$ to denote labelled formulae, thus distinguishing between the two.
Labelled sequents are therefore written in a general form as
$\mathcal{R},\Gamma\Rightarrow\Delta$.

$(id)$ $\mathcal{R},w\leq v,w:p,\Gamma\Rightarrow\Delta,v:p$ |  $\mathcal{R},w\leq v,v:A,\Gamma\Rightarrow\Delta,v:B$ $(\supset_{r})^{{\dagger}_{1}}$ $\mathcal{R},\Gamma\Rightarrow\Delta,w:A\supset B$
---|---

$\mathcal{R},w:A,w:B,\Gamma\Rightarrow\Delta$ $(\wedge_{l})$ $\mathcal{R},w:A\wedge B,\Gamma\Rightarrow\Delta$ |  $\mathcal{R},\Gamma\Rightarrow\Delta,w:A$ $\mathcal{R},\Gamma\Rightarrow\Delta,w:B$ $(\wedge_{r})$ $\mathcal{R},\Gamma\Rightarrow\Delta,w:A\wedge B$
---|---

$\mathcal{R},w:A,\Gamma\Rightarrow\Delta$ $\mathcal{R},w:B,\Gamma\Rightarrow\Delta$ $(\vee_{l})$ $\mathcal{R},w:A\vee B,\Gamma\Rightarrow\Delta$ |  $\mathcal{R},w\leq v,v\leq u,w\leq u,\Gamma\Rightarrow\Delta$ $(tra)$ $\mathcal{R},w\leq v,v\leq u,\Gamma\Rightarrow\Delta$
---|---

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

$\mathcal{R},w\leq w,\Gamma\Rightarrow\Delta$ $(ref)$ $\mathcal{R},\Gamma\Rightarrow\Delta$ |  $(\bot_{l})$ $\mathcal{R},w:\bot,\Gamma\Rightarrow\Delta$
---|---

$(id_{q})$ $\mathcal{R},w\leq v,\vv{\underline{a}}\in D_{w},w:p(\vv{\underline{a}}),\Gamma\Rightarrow\Delta,v:p(\vv{\underline{a}})$ |  $\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow\Delta$ $(ihd)^{{\dagger}_{2}}$ $\mathcal{R},\Gamma\Rightarrow\Delta$
---|---

$\mathcal{R},w\leq v,\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,v:A(\underline{a}/x)$ $(\forall_{r})^{{\dagger}_{3}}$ $\mathcal{R},\Gamma\Rightarrow\Delta,w:\forall xA$ |  $\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(\exists_{r})$ $\mathcal{R},\underline{a}\in D_{w},\Gamma\Rightarrow\Delta,w:\exists xA$
---|---

$\mathcal{R},\underline{a}\in D_{w},w:A(\underline{a}/x),\Gamma\Rightarrow\Delta$ $(\exists_{l})^{{\dagger}_{2}}$ $\mathcal{R},w:\exists xA,\Gamma\Rightarrow\Delta$ |  $\mathcal{R},w\leq v,\underline{a}\in D_{v},v:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$ $(\forall_{l})$ $\mathcal{R},w\leq v,\underline{a}\in D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$
---|---

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

Figure 4: The labelled calculus $\mathsf{G3Int}$ for $\mathsf{Int}$ consists
of $(id)$, $(\bot_{l})$, $(\wedge_{l})$, $(\wedge_{r})$, $(\vee_{l})$,
$(\vee_{r})$, $(\supset_{l})$, $(\supset_{r})$, $(ref)$, and $(tra)$ (see
[6]). The labelled calculus $\mathsf{G3IntQ}$ for $\mathsf{IntQ}$ consists of
all rules minus the $(cd)$ rule, and all rules give the calculus
$\mathsf{G3IntQC}$ for $\mathsf{IntQC}$. The side condition ${\dagger}_{1}$
states that the variable $v$ does not occur in the conclusion, ${\dagger}_{2}$
states that $\underline{a}$ does not occur in the conclusion, and
${\dagger}_{3}$ states that neither $\underline{a}$ nor $v$ occurs in the
conclusion. Labels and parameters restricted from occurring in the conclusion
of an inference are called _eigenvariables_.

Moreover, we take the comma operator to be commutative and associative; for
example, we identify the labelled sequent $w\leq u,w:A,\underline{a}\in
D_{w}\Rightarrow v:C,u:B$ with $\underline{a}\in D_{w},w\leq u,w:A\Rightarrow
u:B,v:C$. This interpretation of comma lets us view $\mathcal{R},\Gamma$ (the
_antecedent_) and $\Delta$ (the _succedent_) of a labelled sequent
$\mathcal{R},\Gamma\Rightarrow\Delta$ as multisets. Also, we use $\varepsilon$
to denote the _empty string_ which acts as the identity element for the comma
operator (e.g. we identify $w\leq v,\varepsilon,v:B$ with $w\leq v,v:B$), and
we stipulate that if $\varepsilon$ is the antecedent or succedent of a
sequent, then the antecedent or succedent is left empty. Therefore,
$\varepsilon$ will be implicit in labelled sequents, but will never explicitly
appear.

In the first-order setting, we syntactically distinguish between _bound
variables_ $\\{x,y,z,\ldots\\}$ and _free variables_ , which are replaced with
_parameters_ $\\{\underline{a},\underline{b},\underline{c},\ldots\\}$, to
avoid clashes between the two categories (cf. [9, Sect. 8]). Therefore,
instead of using formulae directly from the first-order language, we use
formulae from the first-order language where each freely occurring variable
$x$ has been replaced by a distinct parameter $\underline{a}$. For example, we
would make use of the labelled formula $w:(\forall x)p(\underline{a},x)\lor
q(\underline{a},\underline{b})$ instead of $w:(\forall x)p(y,x)\lor q(y,z)$ in
a first-order sequent. Last, we use the notation
$A(\underline{a}_{1},\ldots,\underline{a}_{n})$, with $n\in\mathbb{N}$, to
denote that the parameters $\underline{a}_{1},\ldots,\underline{a}_{n}$ are
all parameters occurring in the formula $A$. (NB. We will occasionally abuse
notation and write $A(\underline{a})$ to indicate that the formula $A$
contains a parameter $\underline{a}$ in which we are interested; however, when
using this notation we leave open the possibility that $A$ may contain other
parameters as well.) We write $A(\vv{\underline{a}})$ as shorthand for
$A(\underline{a}_{1},\ldots,\underline{a}_{n})$ and $\vv{\underline{a}}\in
D_{w}$ as shorthand for $\underline{a}_{1}\in
D_{w},\ldots,\underline{a}_{n}\in D_{w}$. The labelled calculi are given in
Fig. 4.

Each labelled calculus is obtained from the models and semantic clauses of
$\mathsf{Int}$, $\mathsf{IntQ}$, and $\mathsf{IntQC}$. We note that the
labelled calculus $\mathsf{G3Int}$ for $\mathsf{Int}$ is presented in [6],
whereas the labelled calculi $\mathsf{G3IntQ}$ and $\mathsf{G3IntQC}$ for
$\mathsf{IntQ}$ and $\mathsf{IntQC}$ (respectively) are new. The rules
$(\bot_{l})$, $(\wedge_{l})$, $(\wedge_{r})$, $(\vee_{l})$, $(\vee_{r})$,
$(\supset_{l})$, $(\supset_{r})$, $(\exists_{l})$, $(\exists_{r})$,
$(\forall_{l})$, and $(\forall_{r})$ are rule representations of the semantic
clauses given in Def. 2.2 and Def. 2.8. The $(ref)$ and $(tra)$ rules allow
inferences arising from the fact that frames are reflexive and transitive,
whereas $(ihd)$, $(nd)$, and $(cd)$ allow inferences based on the fact that
the domains of frames are always inhabited (i.e. non-empty), are nested, and
are constant, respectively. The rules $(id)$ and $(id_{q})$ encode the
monotonicity condition imposed on models; note that $(id)$ is an instance of
$(id_{q})$ (the same holds for the corresponding rules in the nested setting,
which are introduced in the next subsection). Last, we write
$\vdash_{\mathsf{G3Int}}\Lambda$, $\vdash_{\mathsf{G3IntQ}}\Lambda$, and
$\vdash_{\mathsf{G3IntQC}}\Lambda$ to indicate that the labelled sequent
$\Lambda$ is derivable in $\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and
$\mathsf{G3IntQC}$, respectively—this notation extends straightforwardly to
the other calculi we will consider.

We define a _label substitution_ $(w/v)$ on a multiset of labelled formulae or
relational atoms in the usual way as the replacement of all labels $v$
occurring in the mulitset with the label $w$. Similarly, we define a
_parameter substitution_ $(\underline{a}/\underline{b})$ on a multiset of
labelled formulae or relational atoms as the replacement of all parameters
$\underline{b}$ occurring in the multiset with the parameter $\underline{a}$.

Our labelled calculi possess desirable proof-theoretic properties such as the
_height-preserving (hp-) admissibility_ of substitutions and structural rules
(e.g. $(psub)$ and $(wk)$), the _height-preserving (hp-) invertibility_ of all
rules, and admissibility of $(cut)$. These properties are detailed in the
theorem below (Thm. 3.1) with the (hp-)admissible rules shown in Fig. 5.

$\mathcal{R},\Gamma\Rightarrow\Delta$ $(lsub)$ $\mathcal{R}(w/v),\Gamma(w/v)\Rightarrow\Delta(w/v)$ |  $\mathcal{R},\Gamma\Rightarrow\Delta$ $(psub)$ $\mathcal{R}(\underline{a}/\underline{b}),\Gamma(\underline{a}/\underline{b})\Rightarrow\Delta(\underline{a}/\underline{b})$
---|---

$\mathcal{R},\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R}^{\prime},\mathcal{R},\Gamma^{\prime},\Gamma\Rightarrow\Delta^{\prime},\Delta$ |  $\mathcal{R},\Gamma^{\prime},\Gamma^{\prime},\Gamma\Rightarrow\Delta$ $(ctr_{l})$ $\mathcal{R},\Gamma^{\prime},\Gamma\Rightarrow\Delta$
---|---

$\mathcal{R},\Gamma\Rightarrow\Delta,\Delta^{\prime},\Delta^{\prime}$ $(ctr_{r})$ $\mathcal{R},\Gamma\Rightarrow\Delta,\Delta^{\prime}$ |  $\mathcal{R},\Gamma\Rightarrow\Delta,w:A$ $\mathcal{R},w:A,\Gamma\Rightarrow\Delta$ $(cut)$ $\mathcal{R},\Gamma\Rightarrow\Delta$
---|---

Figure 5: The set $\mathrm{LR}$ of admissible labelled rules consists of all
rules shown above.

######  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 3.2.

We refer the reader to [6] for proofs of properties (i)–(v) for
$\mathsf{G3Int}$; note that hp-admissibility of $(psub)$ is trivial in the
propositional setting since formulae do not contain parameters. The proofs of
properties (i)–(v) for $\mathsf{G3IntQ}$ and $\mathsf{G3IntQC}$ are similar to
those for $\mathsf{G3Int}$ and can be found in Appendix A. ∎

###  3.2 The Nested Calculi $\mathsf{NInt}$, $\mathsf{NIntQ}$, and
$\mathsf{NIntQC}$

We define a propositional (or, first-order) nested sequent $\Sigma$ to be a
syntactic object defined via the following BNF grammars:

$X::=\varepsilon\ |\ A\ |\ X,X$ | $\Sigma::=X\rightarrow X\ |\ X\rightarrow X,[\Sigma],\ldots,[\Sigma]$
---|---

where $A$ is in the propositional language $\mathcal{L}$ (first-order language
$\mathcal{Q}$, resp.). As in the previous section, we take the comma operator
to be commutative and associative, allowing us to view syntactic entities $X$
as multisets, and we let $\varepsilon$ represent the empty string which—as in
the labelled setting—occurs implicitly, but not explicitly, in sequents.

In the first-order setting, we syntactically distinguish between bound
variables and free variables in first-order formulae, using
$\\{x,y,z,\ldots\\}$ for bound variables and replacing the occurrence of free
variables in formulae with parameters
$\\{\underline{a},\underline{b},\underline{c},\ldots\\}$. For example, we
would use $p(\underline{a})\rightarrow
p(\underline{b}),[\bot\rightarrow\forall xq(x,\underline{b})]$ instead of the
sequent $p(x)\rightarrow p(y),[\bot\rightarrow\forall xq(x,y)]$ in a nested
derivation (where the free variable $x$ has been replaced by the parameter
$\underline{a}$ and $y$ has been replaced by $\underline{b}$).

Nested sequents are often written as $\Sigma\\{X\rightarrow
Y,[\Sigma_{1}],\ldots,[\Sigma_{n}]\\}$, which indicates that $X\rightarrow
Y,[\Sigma_{1}],\ldots,[\Sigma_{n}]$ occurs at some depth in the nestings of
the sequent $\Sigma$. For example, if $\Sigma$ is taken to be
$p(\underline{a})\rightarrow[\bot\rightarrow\forall xq(x,\underline{b}),[\
\rightarrow\top]]$, then $\Sigma\\{\bot\rightarrow\forall
xq(x,\underline{b})\\}$, $\Sigma\\{\bot\rightarrow\forall
xq(x,\underline{b}),[\ \rightarrow\top]\\}$, and $\Sigma\\{\rightarrow\top\\}$
are correct representations of $\Sigma$ in our notation.

The nested calculi are given in Fig. 6 and are _slight_ variants of the
calculi presented by Fitting in [9]. The only difference is that the rules
$(\neg_{l})$, $(lift)$, $(\supset_{l})$, $(\exists_{r})$, and $(\forall_{l})$
preserve copies of the principal formula in the premise of the rule. Since we
will be extracting Fitting’s nested calculi from our labelled calculi, it will
be seen that these copies of principal formulae are residua of this process,
which is based on the fact that our labelled calculi preserve copies of
principal formulae in the premise(s) of certain rules. Howbeit, it is easy to
confirm that the calculi $\mathsf{NInt}$, $\mathsf{NIntQ}$, and
$\mathsf{NIntQC}$ are equivalent to Fitting’s calculi from [9], as it is
straightforward to transform a derivation from one calculus into a derivation
in the other, and vice-versa.

$(id)$ $\Sigma\\{X,p\rightarrow p,Y\\}$ |  $\Sigma\\{X,A\rightarrow Y,[X^{\prime},A\rightarrow Y^{\prime}]\\}$ $(lift)$ $\Sigma\\{X,A\rightarrow Y,[X^{\prime}\rightarrow Y^{\prime}]\\}$
---|---

$\Sigma\\{X,A\rightarrow Y\\}$ $\Sigma\\{X,B\rightarrow Y\\}$ $(\vee_{l})$ $\Sigma\\{X,A\lor B\rightarrow Y\\}$ |  $\Sigma\\{X\rightarrow A,Y\\}$ $\Sigma\\{X\rightarrow B,Y\\}$ $(\wedge_{r})$ $\Sigma\\{X\rightarrow A\land B,Y\\}$
---|---

$\Sigma\\{X\rightarrow Y,[A\rightarrow]\\}$ $(\neg_{r})$ $\Sigma\\{X\rightarrow Y,\neg A\\}$ |  $\Sigma\\{X\rightarrow A,B,Y\\}$ $(\vee_{r})$ $\Sigma\\{X\rightarrow A\lor B,Y\\}$
---|---

$\Sigma\\{X\rightarrow Y,[A\rightarrow B]\\}$ $(\supset_{r})$ $\Sigma\\{X\rightarrow A\supset B,Y\\}$ |  $\Sigma\\{X,A\supset B\rightarrow A,Y\\}$ $\Sigma\\{X,A\supset B,B\rightarrow Y\\}$ $(\supset_{l})$ $\Sigma\\{X,A\supset B\rightarrow Y\\}$
---|---

$(id_{q})$ $\Sigma\\{X,p(\vv{\underline{a}})\rightarrow p(\vv{\underline{a}}),Y\\}$ |  $\Sigma\\{X\rightarrow A(\underline{a}/x),\exists xA,Y\\}$ $(\exists_{r})^{{\dagger}_{1}}$ $\Sigma\\{X\rightarrow\exists xA,Y\\}$
---|---

$\Sigma\\{X,A(\underline{a}/x)\rightarrow Y\\}$ $(\exists_{l})^{{\dagger}_{2}}$ $\Sigma\\{X,\exists xA\rightarrow Y\\}$ |  $\Sigma\\{X\rightarrow Y,[\ \rightarrow A(\underline{a}/x)]\\}$ $(\forall^{n}_{r})^{{\dagger}_{2}}$ $\Sigma\\{X\rightarrow\forall xA,Y\\}$
---|---

$\Sigma\\{X\rightarrow A(\underline{a}/x),Y\\}$ $(\forall^{c}_{r})^{{\dagger}_{2}}$ $\Sigma\\{X\rightarrow\forall xA,Y\\}$ |  $\Sigma\\{X,\forall xA,A(\underline{a}/x)\rightarrow Y\\}$ $(\forall_{l})^{{\dagger}_{1}}$ $\Sigma\\{X,\forall xA\rightarrow Y\\}$
---|---

Figure 6: The nested calculus $\mathsf{NInt}$ for propositional intuitionistic
logic consists of $(id)$, $(\wedge_{l})$, $(\wedge_{r})$, $(\vee_{r})$,
$(\vee_{l})$, $(\neg_{l})$, $(\neg_{r})$, $(\supset_{r})$, $(\supset_{l})$,
and $(lift)$. The nested calculus $\mathsf{NIntQ}$ extends $\mathsf{NInt}$
with $(id_{q})$, $(\exists_{l})$, $(\exists_{r})$, $(\forall_{l})$, and
$(\forall^{n}_{r})$. The nested calculus $\mathsf{NIntQC}$ extends
$\mathsf{NInt}$ with $(id_{q})$, $(\exists_{l})$, $(\exists_{r})$,
$(\forall_{l})$, and $(\forall^{c}_{r})$ and omits the side condition
${\dagger}_{1}$ on the $(\exists_{r})$ and $(\forall_{l})$ rules [9]. The side
condition ${\dagger}_{1}$ states that the parameter $\underline{a}$ is either
available or is an eigenvariable, and ${\dagger}_{2}$ states that
$\underline{a}$ is an eigenvariable.

The two distinguishing factors between the nested calculi $\mathsf{NIntQ}$ and
$\mathsf{NIntQC}$ are that (i) the former uses the $(\forall^{n}_{r})$ rule
whereas the latter uses the $(\forall^{c}_{r})$ rule, and (ii) the former
imposes a side condition (see Fig. 6) on the $(\exists_{r})$ and
$(\forall_{l})$ rules, whereas the latter does not. This side condition
ensures the soundness of the $(\exists_{r})$ and $(\forall_{l})$ rules with
respect to $\mathsf{IntQ}$-models, that is, with respect to models where
domains are _not necessarily constant_ (cf. [9]). The side condition relies on
the notion of an _available parameter_ , which we define below:

######  Definition 3.3 (Available Parameter [9]).

Let $\Sigma\\{X\rightarrow Y,[\Sigma_{1}],\ldots,[\Sigma_{n}]\\}$ be a nested
sequent. If there exists a formula $A(\underline{a})\in X,Y$, then the
parameter $\underline{a}$ is available in $X\rightarrow Y$ and in all boxed
subsequents $\Sigma_{i}$ (with $i\in\\{1,\ldots,n\\}$).

As explained in the following section, a nested sequent can be seen as a tree
of sequents of the form $X\rightarrow Y$. Intuitively, if a parameter is
available at some point $X\rightarrow Y$ in the tree, then it will be
available at all points in the future of that point, i.e. in the subtree with
$X\rightarrow Y$ as its root. Since a nested sequent can be seen as an
abstraction of an $\mathsf{IntQ}$-model encoding the model’s underlying
treelike structure, the notion of an available parameter corresponds to the
fact that if a parameter denotes an object in the domain of a world, then—due
to the nested domain condition (Def. 2.6)—that parameter denotes that object
at all future worlds and is _available_ for use in sentences at such worlds.

A feature which distinguishes the nested formalism from the labelled is that
nested sequents may readily be converted into an _equivalent formula_ , that
is, nested sequents allow for a straightforward formula translation (see Def.
3.4 below). As a consequence of our refinement procedure, we will see in Sect.
8 (viz. Cor. 8.16) that a nested sequent $\Sigma$ is provable if and only if
its formula interpretation is provable.

######  Definition 3.4 (Formula Interpretation).

The _formula interpretation_ of a nested sequent is defined inductively as
follows:

$\iota(X\rightarrow Y):=\displaystyle{\bigwedge X\supset\bigvee Y}$
$\iota(X\rightarrow
Y,[\Sigma_{1}],\ldots,[\Sigma_{n}]):=\displaystyle{\bigwedge
X\supset\bigg{(}\bigvee Y\vee\bigvee_{1\leq i\leq
n}\iota(\Sigma_{i})\bigg{)}}$

In the propositional setting, $\iota(\Sigma)$ is a formula in $\mathcal{L}$.
In the first-order setting, we interpret a nested sequent $\Sigma$ as a
formula in $\mathcal{Q}$ by taking the universal closure
$\forall\vv{x}\iota(\Sigma)$ of $\iota(\Sigma)$. Also, as usual
$\bigwedge\varepsilon:=\top$ and $\bigvee\varepsilon:=\bot$, i.e. empty
antecedents translate to $\top$ and empty succedents translate to $\bot$.

Proof-theoretic properties of $\mathsf{NInt}$, $\mathsf{NIntQ}$, and
$\mathsf{NIntQC}$ will be discussed in Sect. 8, though we do state the
essential properties of soundness and completeness below, which were proven by
Fitting in [9]. By _strongly_ sound and complete, we mean that a nested
sequent $\Sigma$ is valid (relative to an $\mathsf{Int}$-, $\mathsf{IntQ}$-,
or $\mathsf{IntQC}$-model) iff it is derivable (in $\mathsf{NInt}$,
$\mathsf{NIntQ}$, or $\mathsf{NIntQC}$, respectively).

######  Theorem 3.5 (Soundness and Completeness).

$\mathsf{NInt}$, $\mathsf{NIntQ}$, and $\mathsf{NIntQC}$ are strongly sound
and complete for $\mathsf{Int}$, $\mathsf{IntQ}$, and $\mathsf{IntQC}$,
respectively.

Interestingly, the correspondence we establish between $\mathsf{G3Int}$ and
$\mathsf{NInt}$, and $\mathsf{G3IntQC}$ and $\mathsf{NIntQC}$, can be
leveraged to show that $\mathsf{NInt}$ and $\mathsf{NIntQC}$ inherit soundness
and completeness from their associated labelled calculi. The correspondence
between $\mathsf{NIntQ}$ and $\mathsf{G3IntQ}$ cannot be leveraged to conclude
the completeness of $\mathsf{NIntQ}$ however, because of the use of a lemma
(Lem. 6.13 in Sect. 6) that invokes the strong completeness of
$\mathsf{NIntQ}$ (i.e. it invokes Thm. 3.5 above). Still, we note in that
section how the lemma may be proved independent of the completeness of
$\mathsf{NIntQ}$, thus allowing for $\mathsf{NIntQ}$ to inherit the
completeness of $\mathsf{G3IntQ}$ via our refinement and translation
processes. Last, in Sect. 8, we will show that our nested calculi inherit
additional properties from their corresponding labelled calculi such as the
admissibilty of certain structural rules (Cor. 8.13) and the invertibility of
all rules (Cor. 8.14).

##  4 Fundamentals for Establishing Correspondence

This section consists of two parts: in the first subsection, we define
translation functions that transform labelled sequents into nested sequents
and vice-versa, as well as define classes of labelled sequents that are
fruitful for carrying out our proof-theoretic transformation and translation
work. In the second subsection, we establish preliminary results that are
convenient for refining our labelled calculi, that is, such results will
assist us in eliminating the structural rules (e.g. $(ref)$ and $(nd)$) from
$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$ (which will
ultimately yield systems that are close variants of Fitting’s nested systems).

###  4.1 Translating Notation: Labelled and Nested

It is instructive to observe that both nested and labelled sequents can be
viewed as graphs (with the former restricted to trees and the latter more
general). Graphs of sequents are significant for two reasons: the first
(technical) reason is that graphs can be leveraged to switch from labelled to
nested notation; thus, graphs will play a role in deriving our nested calculi
from our labelled calculi, and vice-versa. Second, graphs offer insight into
_why_ structural rule elimination yields nested systems, which will be
discussed in the next section (Sect. 5).

It is straightforward to define the graph of each type of sequent. To do this,
we first introduce a bit of notation and define the multiset
$\Gamma\restriction w:=\\{A\ |\ w:A\in\Gamma\\}$. For a labelled sequent
$\Lambda:=\mathcal{R},\Gamma\Rightarrow\Delta$, the _graph_ $G(\Lambda)$ is
the tuple $(V,E,\lambda)$, where (i) $V:=\\{w\ |\ \text{$w$ is a label in
$\Lambda$.}\\}$, (ii) $(w,v)\in E$ iff $w\leq v\in\mathcal{R}$, and

$(iii)\quad\lambda:=\\{(w,\Gamma^{\prime}\Rightarrow\Delta^{\prime})\ |\
\Gamma^{\prime}=\Gamma\restriction w\text{,
}\Delta^{\prime}=\Delta\restriction w\text{, and }w\in V\\}.$

For a nested sequent, the graph is defined inductively on the structure of the
nestings; we use strings $\sigma$ of natural numbers to denote vertices in the
graph, similar to the prefixes used in prefixed tableaux [7, 8, 9].

_Base case._ Let our nested sequent be of the form $X\rightarrow Y$ with $X$
and $Y$ multisets of formulae. Then, $G_{\sigma}(X\rightarrow
Y):=(V_{\sigma},E_{\sigma},\lambda_{\sigma})$, where (i)
$V_{\sigma}:=\\{\sigma\\}$, (ii) $E_{\sigma}:=\emptyset$, and (iii)
$\lambda_{\sigma}:=\\{(\sigma,X\rightarrow Y)\\}$.

_Inductive step._ Suppose our nested sequent is of the form $X\rightarrow
Y,[\Sigma_{1}],\ldots,[\Sigma_{n}]$. We assume that each
$G_{\sigma.i}(\Sigma_{i})=(V_{\sigma.i},E_{\sigma.i},\lambda_{\sigma.i})$
(with $i\in\\{1,\ldots,n\\}$) is already defined, and define
$G_{\sigma}(X\rightarrow
Y,[\Sigma_{1}],\ldots,[\Sigma_{n}]):=(V_{\sigma},E_{\sigma},\lambda_{\sigma})$
as follows:

$(i)\quad V_{\sigma}:=\\{\sigma\\}\cup\displaystyle{\bigcup_{1\leq i\leq
n}V_{\sigma.i}}\qquad(ii)\quad E_{\sigma}:=\\{(\sigma,\sigma.i)\ |\ 1\leq
i\leq n\\}\cup\displaystyle{\bigcup_{1\leq i\leq n}E_{\sigma.i}}$
$(iii)\quad\lambda_{\sigma}:=\\{(\sigma,X\rightarrow
Y)\\}\cup\displaystyle{\bigcup_{1\leq i\leq n}\lambda_{\sigma.i}}$

We will occasionally refer to a sequent of the form $X\rightarrow Y$ in a
nested sequent $\Sigma$ such that $(\sigma,X\rightarrow Y)\in\lambda_{0}$
(with $G_{0}(\Sigma)=(V_{0},E_{0},\lambda_{0})$) as a _component_ of the
nested sequent $\Sigma$.

######  Definition 4.1.

Let $G_{0}=(V_{0},E_{0},\lambda_{0})$ and $G_{1}=(V_{1},E_{1},\lambda_{1})$ be
two graphs. We define an _isomorphism_ $f:V_{0}\mapsto V_{1}$ between $G_{0}$
and $G_{1}$ to be a function such that: (i) $f$ is bijective, (ii) $(x,y)\in
E_{0}$ iff $(fx,fy)\in E_{1}$, (iii) $\lambda_{0}(x)=\lambda_{1}(fx)$. We say
$G_{0}$ and $G_{1}$ are _isomorphic_ iff there exists an isomorphism between
them.

Although the formal definitions above may appear somewhat cumbersome, the
example below shows that transforming a sequent into its graph—or conversely,
obtaining the sequent from its graph—is relatively straightforward.

######  Example 4.2.

The nested sequent $\Sigma$ is given below with its corresponding graph
$G_{0}(\Sigma)$ shown on the left, and the labelled sequent $\Lambda$ is given
below with its corresponding graph $G(\Lambda)$ on the right. Regarding the
labelled sequent, we assume that $\Gamma_{i}$ and $\Delta_{i}$ consist solely
of formulae labelled with $w_{i}$ (for $i\in\\{0,1,2,3\\}$).

$\Sigma=X_{0}\rightarrow Y_{0},[X_{1}\rightarrow Y_{1},[X_{2}\rightarrow Y_{2}]],[X_{3}\rightarrow Y_{3}]$ $\textstyle{\underset{0}{\boxed{X_{0}\rightarrow Y_{0}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\underset{0.1}{\boxed{X_{3}\rightarrow Y_{3}}}}$$\textstyle{\underset{0.0}{\boxed{X_{1}\rightarrow Y_{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\underset{0.0.0}{\boxed{X_{2}\rightarrow Y_{2}}}}$ | $\textstyle{\underset{w_{0}}{\boxed{\Gamma_{0}\restriction w_{0}\Rightarrow\Delta_{0}\restriction w_{0}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\underset{w_{3}}{\boxed{\Gamma_{3}\restriction w_{3}\Rightarrow\Delta_{3}\restriction w_{3}}}}$$\textstyle{\underset{w_{1}}{\boxed{\Gamma_{1}\restriction w_{1}\Rightarrow\Delta_{1}\restriction w_{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\underset{w_{2}}{\boxed{\Gamma_{2}\restriction w_{2}\Rightarrow\Delta_{2}\restriction w_{2}}}}$
---|---
$\Lambda=w_{0}\leq w_{0},w_{0}\leq w_{1},w_{1}\leq w_{2},w_{0}\leq
w_{2},w_{0}\leq
w_{3},\Gamma_{0},\Gamma_{1},\Gamma_{2},\Gamma_{3}\Rightarrow\Delta_{0},\Delta_{1},\Delta_{2},\Delta_{3}$

In the above example there is a loop from $w_{0}$ to itself in the graph of
the labelled sequent; furthermore, there is an undirected cycle occurring
between $w_{0}$, $w_{1}$, and $w_{2}$. As will be explained in the next
section (specifically, Thm. 5.9), the $(ref)$ and $(tra)$ rules allow for such
structures to appear in the graphs of labelled sequents used to derive
theorems; however, the elimination of these rules in our labelled calculi has
the effect that such structures _can no longer_ occur in the labelled
derivation of a theorem. Consequently, it will be seen that eliminating such
rules yields a labelled derivation where every sequent has a purely _treelike_
structure (cf. [13]). This implies that each labelled sequent in the
derivation has a graph isomorphic to the graph of a nested sequent. It is this
idea which ultimately permits the extraction of our nested calculi from our
labelled calculi.

######  Definition 4.3.

Let $\Lambda$ be a labelled sequent and $G(\Lambda)=(V,E,\lambda)$. We say
that $\Lambda$ is _treelike_ iff there exists a unique vertex $w\in V$, called
the _root_ , such that there exists a unique path from $w$ to every other
vertex $v\in V$.333Treelike sequents are equivalently characterized as
sequents with graphs that are: (i) connected, (ii) acyclic, and (iii) contain
no backwards branching. We say that a labelled derivation is _treelike_ iff
every labelled sequent in the derivation is treelike.

If we take the graph of a treelike labelled sequent, then it can be viewed as
the graph of a nested sequent, as the example below demonstrates:

######  Example 4.4.

The treelike labelled sequent $\Lambda^{\prime}$ and its graph are given
below. We assume that $\Gamma_{i}$ and $\Delta_{i}$ contain only formulae
labelled with $w_{i}$ (for $i\in\\{0,1,2,3\\}$).

$\Lambda^{\prime}=w_{0}\leq w_{1},w_{1}\leq w_{2},w_{0}\leq
w_{3},\Gamma_{0},\Gamma_{1},\Gamma_{2},\Gamma_{3}\Rightarrow\Delta_{0},\Delta_{1},\Delta_{2},\Delta_{3}$
$\textstyle{\underset{w_{2}}{\boxed{\Gamma_{2}^{\prime}\Rightarrow\Delta_{2}^{\prime}}}}$$\textstyle{\underset{w_{1}}{\boxed{\Gamma_{1}^{\prime}\Rightarrow\Delta_{1}^{\prime}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\underset{w_{0}}{\boxed{\Gamma_{0}^{\prime}\Rightarrow\Delta_{0}^{\prime}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\underset{w_{3}}{\boxed{\Gamma_{3}^{\prime}\Rightarrow\Delta_{3}^{\prime}}}}$
---

Also, if we assume that $\Gamma_{i}^{\prime}=\Gamma_{i}\restriction
w_{i}=X_{i}$ and $\Delta_{i}^{\prime}=\Delta_{i}\restriction w_{i}=Y_{i}$ (for
$i\in\\{0,1,2,3\\}$), then the above graph is isomorphic to the graph of the
nested sequent in Example 4.2, meaning that $\Lambda$ can be translated as
that nested sequent.

To make the above translation precise, we introduce the _$w$ -downward
closure_ of the graph of a labelled sequent. We may utilize this notion to
explicitly define the _translation_ $\mathfrak{N}$ (see Def. 4.6) that
translates labelled sequents into nested sequents. This translation will prove
itself useful in extracting Fitting’s nested calculi from our labelled
calculi.

######  Definition 4.5 (Downward Closure).

Let $\Lambda$ be a treelike labelled sequent with graph
$G(\Lambda)=(V,E,\lambda)$ and $w\in V$. We define the _$w$ -downward closure_
$G_{w}(\Lambda)=(V^{\prime},E^{\prime},\lambda^{\prime})$ to be the smallest
subgraph of $G(\Lambda)$ such that $w\in V^{\prime}$ and

  * $\blacktriangleright$

if $v\in V^{\prime}$ and $(v,u)\in E$, then $u\in V^{\prime}$;

  * $\blacktriangleright$

$E^{\prime}=\\{(u,v)\ |\ u,v\in V^{\prime}\\}$;

  * $\blacktriangleright$

$\lambda^{\prime}=\\{(v,\Gamma^{\prime}\Rightarrow\Delta^{\prime})\ |\ v\in
V^{\prime}\text{ and
}(v,\Gamma^{\prime}\Rightarrow\Delta^{\prime})\in\lambda\\}$.

######  Definition 4.6 (The Translation $\mathfrak{N}$).

Let $\Lambda$ be a treelike labelled sequent with root $w$. We inductively
define $\mathfrak{N}(\Lambda):=\mathfrak{N}(G_{w}(\Lambda))$ to be the nested
sequent obtained from the graph $G_{w}(\Lambda)$ as follows:

  * $\blacktriangleright$

If $G_{u}(\Lambda)=(V,E,\lambda)$, where $V=\\{u\\}$, $E=\emptyset$, and
$\lambda=\\{(u,\Gamma^{\prime}\Rightarrow\Delta^{\prime})\\}$, then

$\mathfrak{N}(G_{u}(\Lambda)):=\Gamma^{\prime}\rightarrow\Delta^{\prime}.$

  * $\blacktriangleright$

If $G_{u}(\Lambda)=(V,E,\lambda)$, where $u,v_{1},\ldots,v_{n}\in V$,
$(u,v_{1}),\ldots,(u,v_{n})\in E$, and
$(u,\Gamma^{\prime}\Rightarrow\Delta^{\prime})\in\lambda$, then

$\mathfrak{N}(G_{u}(\Lambda)):=\Gamma^{\prime}\rightarrow\Delta^{\prime},[\mathfrak{N}(G_{v_{1}}(\Lambda))],\ldots,[\mathfrak{N}(G_{v_{n}}(\Lambda))].$

We also define a converse translation $\mathfrak{L}$ that translates nested
sequents into labelled sequents. Whereas the former translation $\mathfrak{N}$
is useful in extracting our nested calculi from our labelled calculi, the
translation $\mathfrak{L}$ is useful in transferring proof-theoretic
properties of the latter to the former as well as establishing the converse
translation (see Sect. 8). In order to define this translation, we first
define two operations: (i) If $X$ is a multiset of formulae from $\mathcal{L}$
or $\mathcal{Q}$, then $w:X:=\\{w:A\ |\ A\in X\\}$, that is, $w:X$ is the
multiset of all formulae from $X$ labelled with $w$, and (ii) If
$\Lambda_{1}=\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1}$ and
$\Lambda_{2}=\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2}$, then we define
the _sequent composition_
$\Lambda_{1}\oplus\Lambda_{2}:=\mathcal{R}_{1},\mathcal{R}_{2},\Gamma_{1},\Gamma_{2}\Rightarrow\Delta_{1},\Delta_{2}$.

######  Definition 4.7 (The Translation $\mathfrak{L}$).

Let $\Sigma$ be a nested sequent. We inductively define
$\mathfrak{L}(\Sigma):=\mathfrak{L}(G_{0}(\Sigma))$ to be the labelled sequent
obtained from the graph $G_{0}(\Sigma)$ as follows:

  * $\blacktriangleright$

If $G_{\sigma}(\Sigma)=(V_{\sigma},E_{\sigma},\lambda_{\sigma})$ with
$V=\\{\sigma\\}$, $E=\emptyset$, $\lambda=\\{(\sigma,X\rightarrow Y)\\}$, and
$\vv{a}$ are all parameters occurring in $X,Y$, then

$\mathfrak{L}(G_{\sigma}(\Sigma)):=\vv{a}\in
D_{\sigma},\sigma:X\Rightarrow\sigma:Y.$

  * $\blacktriangleright$

If $G_{\sigma}(\Sigma)=(V_{\sigma},E_{\sigma},\lambda_{\sigma})$ with
$\sigma,\sigma.1,\ldots,\sigma.n\in V$,
$(\sigma,\sigma.1),\ldots,(\sigma,\sigma.n)\in E$, $(\sigma,X\rightarrow
Y)\in\lambda$, and $\vv{a}$ are all parameters occurring in $X,Y$, then

$\mathfrak{L}(G_{\sigma}(\Sigma)):=\Big{(}\sigma\leq\sigma.1,\ldots,\sigma\leq\sigma.n,\vv{a}\in
D_{\sigma},\sigma:X\Rightarrow\sigma:Y\Big{)}$

$\oplus\Big{(}\mathfrak{L}(G_{\sigma.1}(\Sigma))\Big{)}\oplus\cdots\oplus\Big{(}\mathfrak{L}(G_{\sigma.n}(\Sigma))\Big{)}$.

To simplify notation when making use of the $\mathfrak{L}$ translation, we
will use the same labels $w$, $u$, $v$, $\ldots$ employed in our labelled
calculi in place of strings $\sigma$ of natural numbers.

Before finishing this subsection, we introduce a fundamental notion useful for
completing our translation from labelled to nested, which is based on the
above definition—the notion of a _nestedlike_ labelled sequent:

######  Definition 4.8 (Nestedlike).

We say that a labelled sequent $\Lambda$ is _nestedlike_ iff there exists a
nested sequent $\Sigma$ such that $\mathfrak{L}(\Sigma)=\Lambda$.

It is not difficult to see that the following lemma holds:

######  Lemma 4.9.

Let $\Lambda:=\mathcal{R},\Gamma\Rightarrow\Delta$ be a nestedlike labelled
sequent. Then, (i) $\Lambda$ is treelike, (ii)
$\mathfrak{L}(\mathfrak{N}(\Lambda))=\Lambda$ (up to a change in labels), and
(iii) there exists a domain atom $\underline{a}\in D_{w}\in\mathcal{R}$ iff
there exists a labelled formula $w:A(\underline{a})\in\Gamma,\Delta$.

###  4.2 Setting the Stage for Refinement: Preliminary Results

In order to extract Fitting’s nested calculi from our labelled calculi, we
will expand our labelled calculi with rules sufficient for the elimination of
certain structural rules. Therefore, we first inflate our calculi to a large
collection of rules, and use the new additions to systematically eliminate
certain rules from each calculus, thus obtaining a refined variant of each
calculus. To avoid lengthy names for our inflated and refined calculi, we will
use the following abbreviations throughout the remainder of the paper (see
Fig. 7 for newly introduced rules):

######  Definition 4.10.

The inflated ($\mathsf{G3Int}^{*}$, $\mathsf{G3IntQ}^{*}$, and
$\mathsf{G3IntQC}^{*}$) and refined ($\mathsf{IntL}$, $\mathsf{IntQL}$, and
$\mathsf{IntQCL}$) labelled calculi are defined as follows:

$\begin{split}&\mathsf{G3Int}^{*}:=\mathsf{G3Int}+\\{(id^{*}),(\neg_{l}),(\neg_{r}),(\supset_{l}^{*}),(lift)\\}\\\
&\mathsf{G3IntQ}^{*}:=\mathsf{G3IntQ}+\\{(id_{q}^{n}),(\neg_{l}),(\neg_{r}),(\supset_{l}^{*}),(lift),(\exists^{n}_{r}),(\forall^{n}_{l}),(\exists^{in}_{r}),(\forall^{in}_{l})\\}\\\
&\mathsf{G3IntQC}^{*}:=\mathsf{G3IntQC}+\\{(id_{q}^{c}),(\neg_{l}),(\neg_{r}),(\supset_{l}^{*}),(lift),(\exists^{c}_{r}),(\forall^{c}_{l}),(\exists^{ic}_{r}),(\forall^{ic}_{l}),(\forall^{c}_{r})\\}\end{split}$
$\begin{split}&\mathsf{IntL}:=\mathsf{G3Int}^{*}-\\{(id),(\bot_{l}),(\supset_{l}),(ref),(tra)\\}\\\
&\mathsf{IntQL}:=\mathsf{G3IntQ}^{*}-\\{(id_{q}),(\bot_{l}),(\supset_{l}),(ref),(tra),(\exists_{r}),(\forall_{l}),(nd),(ihd)\\}\\\
&\mathsf{IntQCL}:=\\\ &\hskip
25.00003pt\mathsf{G3IntQC}^{*}-\\{(id_{q}),(\bot_{l}),(\supset_{l}),(ref),(tra),(\exists_{r}),(\forall_{l}),(\forall_{r}),(nd),(cd),(ihd)\\}\end{split}$

$(id^{*})$ $\mathcal{R},\Gamma,w:p\Rightarrow w:p,\Delta$ |  $(id_{q}^{n})^{{\dagger}_{1}}$ $\mathcal{R},\underline{a}_{1}\in D_{v_{1}},\ldots,\underline{a}_{n}\in D_{v_{n}},\Gamma,w:p(\vv{\underline{a}})\Rightarrow w:p(\vv{\underline{a}}),\Delta$
---|---

$(id_{q}^{c})^{{\dagger}_{2}}$ $\mathcal{R},\underline{a}_{1}\in
D_{v_{1}},\ldots,\underline{a}_{n}\in
D_{v_{n}},\Gamma,w:p(\vv{\underline{a}})\Rightarrow
w:p(\vv{\underline{a}}),\Delta$
---

$\mathcal{R},w\leq v,v:A,\Gamma\Rightarrow\Delta$ $(\neg_{r})^{{\dagger}_{3}}$ $\mathcal{R},\Gamma\Rightarrow\Delta,w:\neg A$ |  $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(\exists^{n}_{r})^{{\dagger}_{4}}$ $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:\exists xA$
---|---

$\mathcal{R},w:\neg A,\Gamma\Rightarrow w:A,\Delta$ $(\neg_{l})$ $\mathcal{R},w:\neg A,\Gamma\Rightarrow\Delta$ |  $\mathcal{R},\underline{a}\in D_{v},w:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$ $(\forall^{n}_{l})^{{\dagger}_{4}}$ $\mathcal{R},\underline{a}\in D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$
---|---

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

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

$\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{in}_{r})^{{\dagger}_{7}}$ $\mathcal{R},\Gamma\Rightarrow w:\exists xA,\Delta$ |  $\mathcal{R},\underline{a}\in D_{v},\Gamma,w:\forall xA,w:A(\underline{a}/x)\Rightarrow\Delta$ $(\forall^{in}_{l})^{{\dagger}_{7}}$ $\mathcal{R},\Gamma,w:\forall xA,\Rightarrow\Delta$
---|---

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

$\mathcal{R},w:A\supset B,\Gamma\Rightarrow\Delta,w:A$ $\mathcal{R},w:A\supset
B,w:B,\Gamma\Rightarrow\Delta$ $(\supset_{l}^{*})$ $\mathcal{R},w:A\supset
B,\Gamma\Rightarrow\Delta$

Figure 7: Rules used to derive $\mathsf{NInt}$, $\mathsf{NIntQ}$, and
$\mathsf{NIntQC}$ from $\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and
$\mathsf{G3IntQC}$, respectively. Let $\mathcal{R}$ be the relational atoms
occurring in the relevant rule; the side condition ${\dagger}_{1}$ states that
$v_{i}\leadsto^{\mathcal{R}}w$ for each $i\in\\{1,\ldots,n\\}$,
${\dagger}_{2}$ states that $v_{i}\sim^{\mathcal{R}}w$ for each
$i\in\\{1,\ldots,n\\}$, ${\dagger}_{3}$ states that $v$ is an eigenvariable,
${\dagger}_{4}$ states that $v\leadsto^{\mathcal{R}}w$, ${\dagger}_{5}$ states
that $v\sim^{\mathcal{R}}w$, ${\dagger}_{6}$ states that $\underline{a}$ is an
eigenvariable, ${\dagger}_{7}$ states that $v\leadsto^{\mathcal{R}}w$ and
$\underline{a}$ is an eigenvariable, and ${\dagger}_{8}$ states that
$v\sim^{\mathcal{R}}w$ and $\underline{a}$ is an eigenvariable.

The next three sections will focus on the non-trivial refinement and
translation of our labelled calculi into our nested calculi. As such, we
present two useful lemmata below which will aid us in the aforementioned
endeavor and allow for us to focus our attention on the refinement and
translation from labelled to nested, thus freeing us from being sidetracked by
too many auxiliary details. Moreover, we present the rules (mentioned in the
abbreviations above and lemmata below) that we expand each labelled calculus
with in Fig. 7 below. Some of these rules depend on the notion of a _directed
path_ or _undirected path_ , whose definitions are as follows:

######  Definition 4.11 (Directed Path).

Let $\Lambda=\mathcal{R},\Gamma\Rightarrow\Delta$ be a labelled sequent. We
say that there exists a _directed path_ from $w$ to $u$ in $\mathcal{R}$
(written $w\leadsto^{\mathcal{R}}u$) iff $w=u$, or there exist worlds $v_{i}$
(with $i\in\\{1,\ldots,n\\}$) such that $w\leq v_{1},\ldots,v_{n}\leq
u\in\mathcal{R}$ holds (we stipulate that $w\leq u\in\mathcal{R}$ when $n=0$).

######  Definition 4.12 (Undirected Path).

Let $\Lambda=\mathcal{R},\Gamma\Rightarrow\Delta$ be a labelled sequent and
$w\sim v\in\\{w\leq u,u\leq w\\}$. We say that there exists an _undirected
path_ from $w$ to $u$ in $\mathcal{R}$ (written $w\sim^{\mathcal{R}}u$) iff
$w=u$, or there exist worlds $v_{i}$ (with $i\in\\{1,\ldots,n\\}$) such that
$w\sim v_{1},\ldots,v_{n}\sim u\in\mathcal{R}$ holds (we stipulate that $w\sim
u\in\mathcal{R}$ when $n=0$).

The following lemma confirms that the expansion of our labelled calculi
$\mathsf{G3Int}$, $\mathsf{G3IntQ}$, and $\mathsf{G3IntQC}$ with rules from
Fig. 7 preserves (to a degree) favorable proof-theoretic properties:

######  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 4.14.

See Appendix A for details. ∎

The following lemma is useful in that it explicates what rules freely permute
with each other, thus letting us focus only on the non-trivial cases in the
sequel.

######  Lemma 4.15.

The following hold in $\mathsf{G3Int}^{*}$, $\mathsf{G3IntQ}^{*}$, and
$\mathsf{G3IntQC}^{*}$:

  * (i)

The $(ref)$ and $(tra)$ rules can be permuted above $(id^{*})$, $(\bot_{l})$,
$(\wedge_{l})$, $(\wedge_{r})$, $(\vee_{l})$, $(\vee_{r})$,
$(\supset_{l}^{*})$, $(\supset_{r})$, $(\neg_{l})$, $(\neg_{r})$, $(ihd)$,
$(\exists_{l})$, $(\exists_{r})$, and $(\forall^{c}_{r})$.

  * (ii)

The $(nd)$, $(cd)$, and $(ihd)$ rules can be permuted above $(id)$,
$(id^{*})$, $(\bot_{l})$, $(\wedge_{l})$, $(\wedge_{r})$, $(\vee_{l})$,
$(\vee_{r})$, $(\supset_{l})$, $(\supset_{l}^{*})$, $(\supset_{r})$,
$(\neg_{l})$, $(\neg_{r})$, $(lift)$, $(ihd)$, $(\exists_{l})$,
$(\exists^{in}_{r})$, $(\exists^{ic}_{r})$, $(\forall^{in}_{l})$,
$(\forall^{ic}_{l})$, $(\forall_{r})$, and $(\forall^{c}_{r})$.

######  Proof 4.16.

The claim of (i) follows from the fact that none of the rules mentioned have
active relational atoms of the form $w\leq u$ in the conclusion, and so,
$(ref)$ and $(tra)$ may be freely permuted above each rule. The claim of (ii)
follows from the fact that none of the rules mentioned contain active domain
atoms in the conclusion, allowing for $(nd)$, $(cd)$, and $(ihd)$ to be
permuted above each rule. ∎

##  5 Deriving the Calculus $\mathsf{NInt}$ from $\mathsf{G3Int}$

Deriving the calculus $\mathsf{NInt}$ from $\mathsf{G3Int}$ depends on a
crucial observation concerning labelled derivations: _rules such as $(ref)$
and $(tra)$ allow for theorems to be derived in proofs containing non-treelike
labelled sequents_. To demonstrate this fact, observe the following derivation
in $\mathsf{G3Int}$:

$w\leq v,v\leq v,v:p\Rightarrow v:p$ $(ref)$ $w\leq v,v:p\Rightarrow v:p$
$(\supset_{r})$ $\Rightarrow w:p\supset p$

The initial sequent is non-treelike due to the presence of the $v\leq v$
relational atom; however, the application of $(ref)$ deletes this structure
from the initial sequent and produces a treelike sequent as the conclusion.

In fact, it is true in general that every labelled derivation ending with a
treelike sequent can be partitioned into a top derivation consisting of non-
treelike sequents, and a bottom derivation consisting of treelike sequents.
Note that if a derivation ends with a treelike sequent, then the derivation
must necessarily contain a bottom treelike fragment. By contrast, the top non-
treelike fragment of the derivation may be empty (e.g. the minimal derivation
of $\Rightarrow w:\bot\supset p$).

To demonstrate why the aforementioned partition always exists, suppose you are
given a labelled derivation of a treelike sequent and consider the derivation
in a bottom-up manner. Observe the each bottom-up application of a rule in
$\mathsf{G3Int}$—with the exception of $(ref)$ and $(tra)$—will produce a
treelike sequent (see Thm. 5.9 for auxiliary details). If, however, at some
point in the derivation $(ref)$ or $(tra)$ is applied, then all sequents above
the inference will inherit the (un)directed cycle produced by the rule, thus
producing the non-treelike fragment of the proof.

One can therefore imagine that permuting instances of the $(ref)$ and $(tra)$
rules upward in a given derivation would potentially increase the bottom
treelike fragment of the derivation and decrease the top non-treelike
fragment. As it so happens, this intuition is correct so long as we choose
_adequate_ rules—that bottom-up preserve the treelike structure of sequents—to
replace certain instances of the $(ref)$ and $(tra)$ rules in a derivation,
when necessary. We will first examine permuting instances of the $(ref)$ rule,
and motivate which adequate rules we ought to add to our calculus in order to
achieve the complete elimination of $(ref)$. After, we will turn our attention
toward eliminating the $(tra)$ rule, and conclude the section by leveraging
our results to show that $\mathsf{NInt}$ can be derived from $\mathsf{G3Int}$.

Let us first observe an application of $(ref)$ to an initial sequent obtained
via the $(id)$ rule. There are two possible cases to consider: either the
relational atom principal in the initial sequent is active in the $(ref)$
inference (shown below left), or it is not (shown below right):

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

In the case shown above right, the end sequent is an instance of the $(id)$
rule, regardless of if $u=w$, $u=v$, or $u$ is distinct from $w$ and $v$. The
case shown above left however, indicates that we ought to add the $(id^{*})$
rule (see Fig. 7) to our calculus if we aim to eliminate $(ref)$ from any
given derivation. These facts, coupled with Lem. 4.15, imply that any
application of $(ref)$ to an initial sequent, produces an initial sequent.

Concerning the remaining rules of $\mathsf{G3Int}$, we need only investigate
the permutation of $(ref)$ above the $(\supset_{l})$ rule, if we rely on Lem.
4.15. There are two cases: either the relational atom principal in the
$(\supset_{l})$ inference is active in the $(ref)$ inference, or it is not.
The latter case is easily resolved, so we observe the former:

$\mathcal{R},w\leq w,w:A\supset B,\Gamma\Rightarrow\Delta,w:A$
$\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$
---

Applying $(ref)$ to each premise of the $(\supset_{l})$ inference yields the
following:

$\mathcal{R},w\leq w,w:A\supset B,\Gamma\Rightarrow\Delta,w:A$ $(ref)$ $\mathcal{R},w:A\supset B,\Gamma\Rightarrow\Delta,w:A$ |  $\mathcal{R},w\leq w,w:A\supset B,w:B,\Gamma\Rightarrow\Delta$ $(ref)$ $\mathcal{R},w:A\supset B,w:B,\Gamma\Rightarrow\Delta$
---|---

The above observation suggests that we ought to add the $(\supset_{l}^{*})$
rule (see Fig. 7) to our calculus if we wish to permute $(ref)$ above the
$(\supset_{l})$ rule; a single application of the $(\supset_{l}^{*})$ rule to
the end sequents above gives the desired conclusion. With the
$(\supset_{l}^{*})$ rule added to our calculus, we may freely permute the
$(ref)$ rule above any $(\supset_{l})$ inference.

On the basis of our investigation, together with Lem. 4.15, we may conclude
the following lemma:

######  Lemma 5.1.

The $(ref)$ rule is eliminable in
$\mathsf{G3Int}+\\{(id^{*}),(\supset^{*}_{l})\\}-(tra)$.

Let us turn our attention toward eliminating the $(tra)$ rule from a labelled
derivation. Since our aim is to eliminate _both_ $(ref)$ and $(tra)$ from any
derivation, we assume that the rules $\\{(id^{*}),(\supset^{*}_{l})\\}$ have
been added to our calculus.

By Lem. 4.15, $(tra)$ permutes with $(\bot_{l})$ and $(id^{*})$, so we only
consider the $(id)$ case. As with the $(ref)$ rule, there are two cases to
consider when permuting $(tra)$ above an $(id)$ inference: either, the active
formula of $(tra)$ is principal in $(id)$, or it is not. In the latter case,
the result of the $(tra)$ rule is an initial sequent, implying that the
$(tra)$ rule may be eliminated from the derivation. The former case proves
trickier and is explicitly given below:

$(id)$ $\mathcal{R},w\leq u,u\leq v,w\leq v,w:p,\Gamma\Rightarrow\Delta,v:p$
$(tra)$ $\mathcal{R},w\leq u,u\leq v,w:p,\Gamma\Rightarrow\Delta,v:p$
---

Observe that the end sequent is not an initial sequent as it is not obtainable
from an $(id)$, $(id^{*})$, or $(\bot_{l})$ rule. The issue is solved by
considering the $(lift)$ rule (see Fig. 7), which allows us to obtain the
desired end sequent without the use of $(tra)$, as the following derivation
demonstrates:

$(id^{*})$ $\mathcal{R},w\leq u,u\leq v,w:p,u:p,v:p,\Gamma\Rightarrow
v:p,\Delta$ $(lift)$ $\mathcal{R},w\leq u,u\leq v,w:p,u:p,\Gamma\Rightarrow
v:p,\Delta$ $(lift)$ $\mathcal{R},w\leq u,u\leq v,w:p,\Gamma\Rightarrow
v:p,\Delta$

Thus, the addition of $(lift)$ to our calculus resolves the issue of permuting
$(tra)$ above any initial sequent. Nevertheless, by Lem. 4.15, we still need
to consider the permutation of $(tra)$ above the $(\supset_{l})$ and $(lift)$
rules. However, due to the following lemma, we may omit consideration of the
$(\supset_{l})$ case.

######  Lemma 5.2.

The rule $(\supset_{l})$ is admissible in
$\mathsf{G3Int}+\\{(id^{*}),(\supset^{*}_{l}),(lift)\\}$.

######  Proof 5.3.

The derivation below proves the admissibility of the rule:

$\mathcal{R},x\leq y,x:A\supset B,\Gamma\Rightarrow\Delta,y:A$ $(wk)$
$\mathcal{R},x\leq y,x:A\supset B,y:A\supset B,\Gamma\Rightarrow\Delta,y:A$
$\mathcal{R},x\leq y,x:A\supset B,y:B,\Gamma\Rightarrow\Delta$ $(wk)$
$\mathcal{R},x\leq y,x:A\supset B,y:A\supset B,y:B,\Gamma\Rightarrow\Delta$
$(\supset^{*}_{l})$ $\mathcal{R},x\leq y,x:A\supset B,y:A\supset
B,\Gamma\Rightarrow\Delta$ $(lift)$ $\mathcal{R},x\leq y,x:A\supset
B,\Gamma\Rightarrow\Delta$
---

∎

Last, the $(tra)$ rule is permutable with the $(lift)$ rule. In the case where
the principal relational atom of $(lift)$ is not active in the ensuing $(tra)$
application, the two rules freely permute. The alternative case is resolved as
shown below:

$\mathcal{R},w\leq u,u\leq v,w\leq v,w:A,v:A,\Gamma\Rightarrow\Delta$ $(lift)$
$\mathcal{R},w\leq u,u\leq v,w\leq v,w:A,\Gamma\Rightarrow\Delta$ $(tra)$
$\mathcal{R},w\leq u,u\leq v,w:A,\Gamma\Rightarrow\Delta$

$\mathcal{R},w\leq u,u\leq v,w\leq v,w:A,v:A,\Gamma\Rightarrow\Delta$ $(tra)$
$\mathcal{R},w\leq u,u\leq v,w:A,v:A,\Gamma\Rightarrow\Delta$ $(wk)$
$\mathcal{R},w\leq u,u\leq v,w:A,u:A,v:A,\Gamma\Rightarrow\Delta$ $(lift)$
$\mathcal{R},w\leq u,u\leq v,w:A,u:A,\Gamma\Rightarrow\Delta$ $(lift)$
$\mathcal{R},w\leq u,u\leq v,w:A,\Gamma\Rightarrow\Delta$

Hence, we obtain the following:

######  Lemma 5.4.

The $(tra)$ rule is eliminable in
$\mathsf{G3Int}+\\{(id^{*}),(\supset^{*}_{l}),(lift)\\}-(ref)$.

Enough groundwork has been laid to state one of our main lemmata, which is
also a consequence of the work in [21].

######  Lemma 5.5.

The $(ref)$ and $(tra)$ rules are admissible in the calculus
$\mathsf{G3Int}+\\{(id^{*}),(\supset^{*}_{l}),(lift)\\}$.

######  Proof 5.6.

Suppose we are given a derivation in
$\mathsf{G3Int}+\\{(id^{*}),(\supset^{*}_{l}),(lift)\\}$, and consider the
topmost occurrence of either $(ref)$ or $(tra)$. If we can show that the
$(ref)$ rule permutes above the $(lift)$ rule, then we may invoke Lem. 5.1 and
Lem. 5.4 to conclude that each topmost occurrence of $(ref)$ and $(tra)$ can
be eliminated from the given derivation in succession. This yields a $(ref)$\-
and $(tra)$-free proof of the end sequent and establishes the claim. Thus, we
prove that the $(ref)$ rule permutes above the $(lift)$ rule.

In the case where the relational atom active in $(ref)$ is not principal in
the $(lift)$ inference, the two rules may be permuted; the alternative case is
resolved as shown below:

$\mathcal{R},w\leq w,w:A,w:A,\Gamma\Rightarrow\Delta$ $(lift)$ $\mathcal{R},w\leq w,w:A,\Gamma\Rightarrow\Delta$ $(ref)$ $\mathcal{R},w:A,\Gamma\Rightarrow\Delta$ |  IH $\mathcal{R},w:A,w:A,\Gamma\Rightarrow\Delta$ $(ctr_{l})$ $\mathcal{R},w:A,\Gamma\Rightarrow\Delta$
---|---

∎

The addition of the rules $\\{(id^{*}),(\supset_{l}^{*}),(lift)\\}$ to our
calculus and the above admissibility results demonstrate that we are readily
advancing toward our goal of deriving $\mathsf{NInt}$. Howbeit, our labelled
calculus is still distinct since it makes use of the logical signature
$\\{\bot,\land,\lor,\supset\\}$, whereas $\mathsf{NInt}$ uses the signature
$\\{\neg,\land,\lor,\supset\\}$. Therefore, we need to show that $(\bot_{l})$
(we define $\bot:=p\land\neg p$) is admissible in the presence of (labelled
versions of) the $(\neg_{r})$ and $(\neg_{l})$ rules (see Fig. 7). This
admissibility result is explained in the theorem below.

######  Theorem 5.7.

The rules $\\{(id),(\bot_{l}),(\supset_{l}),(ref),(tra)\\}$ are admissible in
$\mathsf{IntL}$.

######  Proof 5.8.

Follows from Lem. 4.15, Lem. 5.5, the fact that $(id)$ is derivable using
$(id^{*})$ and $(lift)$, and the fact that $(\bot_{l})$ is derivable from
$(\neg_{l})$ and $(\wedge_{l})$. Also, the admissibility of $(\supset_{l})$ is
shown as in Lem. 5.2. ∎

Although the above theorem is sufficient to conclude the completeness of
$\mathsf{IntL}$, we obtain a stronger result. As shown in the theorem below,
we may conclude that $\mathsf{IntL}$ is _complete relative to treelike
derivations_ possessing the _fixed root property_ ; i.e. for every
$\mathsf{Int}$-valid formula $A\in\mathcal{L}$, (i) $\Rightarrow w:A$ is
derivable in $\mathsf{IntL}$ with a treelike derivation, and (ii) the label
$w$ is the root of each treelike labelled sequent in the derivation.

######  Theorem 5.9.

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

######  Proof 5.10.

We prove (i), as (ii) is proven similarly. By Thm. 5.7 above, we know that
$\mathsf{IntL}$ is complete. To prove claim (i) then, we assume that we are
given a derivation in $\mathsf{IntL}$ of a labelled theorem, i.e. the end
sequent is of the form $\Rightarrow w:A$. It is not difficult to see that the
derivation of $\Rightarrow w:A$ must be treelike with the fixed root property
since applying inference rules from the calculus bottom-up to $\Rightarrow
w:A$ either preserves relational structure or adds forward relational
structure (e.g. $(\supset_{r})$ and $(\neg_{r})$), thus constructing a tree
emanating from the root $w$. ∎

We may leverage the above theorem and the translation $\mathfrak{N}$ (from
Def. 4.6) to complete the extraction of the nested calculus $\mathsf{NInt}$
from the labelled calculus $\mathsf{G3Int}$ (via the calculus
$\mathsf{IntL}$). The theorem below shows that (the treelike fragment of)
$\mathsf{IntL}$ and $\mathsf{NInt}$ are notational variants of one another:

######  Theorem 5.11.

(i) Every derivation in $\mathsf{IntL}$ of a nestedlike labelled sequent
$\Lambda$ is effectively translatable to a derivation of the nested sequent
$\mathfrak{N}(\Lambda)$ in $\mathsf{NInt}$. (ii) Every derivation in
$\mathsf{NInt}$ of a nested sequent $\Sigma$ is effectively translatable to a
derivation of the labelled sequent $\mathfrak{L}(\Sigma)$ in $\mathsf{IntL}$.

######  Proof 5.12.

By Lem. 4.9, we know that $\Lambda$ is treelike, implying that our derivation
of $\Lambda$ is treelike by Thm. 5.9, which further implies that the
translation function $\mathfrak{N}$ is defined for each labelled sequent in
the derivation. It is straightforward to verify that each rule in
$\mathsf{IntL}$ translates to an instance of the corresponding rule in
$\mathsf{NInt}$ under the $\mathfrak{N}$ translation, and every rule of
$\mathsf{NInt}$ translates to an instance of the corresponding rule in
$\mathsf{IntL}$ under the $\mathfrak{L}$ translation. ∎

##  6 Deriving the Calculus $\mathsf{NIntQ}$ from $\mathsf{G3IntQ}$

In the preceding section, we observed that the elimination of the $(ref)$ and
$(tra)$ rules yielded derivations where every labelled sequent was of a
treelike shape. In this section (and the succeeding section) the same effect
obtains via the elimination of these two structural rules. Therefore, the
majority of this section is dedicated to investigating the effects of
eliminating the $(nd)$ and $(ihd)$ structural rules instead.

Similar to our analysis of eliminating the $(ref)$ and $(tra)$ rules, we
motivate and explain the _adequate_ rules we ought to add to $\mathsf{G3IntQ}$
in order to obtain the complete elimination of $(nd)$ and $(ihd)$. Although
the reader may refer to Fig. 7 to witness what rules are needed for the
admissibility of $(nd)$ and $(ihd)$, a central aim of this section is to
demonstrate _how_ such rules emerge from our analysis when attempting to
eliminate $(nd)$ and $(ihd)$ from a derivation—this begets a deeper
understanding of how the semantics of $\mathsf{IntQ}$ affects the shape of
rules in $\mathsf{NIntQ}$ (via the labelled calculus $\mathsf{G3IntQ}$).
Ultimately, our admissibility results will permit the extraction of
$\mathsf{NIntQ}$ from $\mathsf{G3IntQ}$.

######  Lemma 6.1.

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

######  Proof 6.2.

We prove the result by induction on the height of the given derivation and
assume w.l.o.g. that the derivation ends with $(ref)$ or $(tra)$, and that no
other instances of $(ref)$ or $(tra)$ occur in the derivation. The general
result follows by considering a topmost occurrence of $(ref)$ or $(tra)$ and
eliminating each topmost occurrence in succession until a proof free of
$(ref)$ and $(tra)$ inferences is obtained.

By Lem. 4.15, we need only show that $(ref)$ and $(tra)$ permute above the
rules $(id_{q}),(id^{n}_{q}),(\supset_{l})$, $(lift)$, $(\exists^{n}_{r})$,
$(\exists^{in}_{r})$, $(\forall_{l})$, $(\forall^{n}_{l})$,
$(\forall^{in}_{l})$, and $(nd)$. The cases of permuting $(ref)$ and $(tra)$
above $(lift)$ are similar as for Thm. 5.7 and Lem. 5.4, respectively. Also,
$(\supset_{l})$ is admissible in the presence of $(\supset^{*}_{l})$ (similar
to Lem. 5.2), $(id_{q})$ is an instance of $(id^{n}_{q})$ (by Lem. 6.3 below),
and $(\forall_{l})$ is an instance of $(\forall^{n}_{l})$ (also by Lem. 6.3
below), so these cases may be omitted. Hence, we focus only on the nontrivial
cases involving the $(id^{n}_{q})$, $(\exists^{n}_{r})$, $(\exists^{in}_{r})$,
$(\forall^{n}_{l})$, $(\forall^{in}_{l})$, and $(nd)$ rules, which are shown
below to the left and resolved as shown below on the right. We prove the
elimination of $(ref)$ and refer the reader to Appendix A for the similar
proof of $(tra)$ elimination.

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})$ case
below. Observe that the end sequent of the derivation below left is an
instance of $(id^{n}_{q})$ since the side condition that
$v_{i}\leadsto^{\mathcal{R}^{\prime}}w$ for $i\in\\{1,\ldots,n\\}$ holds: if
none of the directed paths from $v_{i}$ to $w$ contain $u\leq u$, then the
paths are present in $\mathcal{R}^{\prime}$, and if a directed path from
$v_{i}$ to $w$ does contain $u\leq u$, then deleting each occurrence of $u\leq
u$ from the directed path gives a new path from $v_{i}$ to $w$ in
$\mathcal{R}^{\prime}$.

$(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^{n}_{q})$ $\mathcal{R}^{\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^{n}_{r})$, $(\exists^{in}_{r})$, $(\forall^{n}_{l})$,
$(\forall^{in}_{l})$, and $(nd)$ cases.

$\mathcal{R},u\leq u,\underline{a}\in D_{v},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{n}_{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^{n}_{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^{in}_{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^{in}_{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^{n}_{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^{n}_{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^{in}_{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^{in}_{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$

We now argue that the side condition ($v\leadsto^{\mathcal{R}}w$) of
$(\exists^{n}_{r})$, $(\exists^{in}_{r})$, $(\forall^{n}_{l})$, and
$(\forall^{in}_{l})$ continues to hold after applying IH above. If the
directed path from $v$ to $w$ does not go through $u$, then the side condition
trivially holds. Alternatively, if the directed path from $v$ to $w$ does go
through $u$, then by deleting each occurrence of $u\leq u$ from the path, we
obtain a new directed path from $v$ to $w$, which continues to be present
after the invocation of IH. ∎

We now analyze the admissibility of $(nd)$ in
$\mathsf{G3IntQ}^{*}-\\{(ref),(tra)\\}$, and afterward, analyze the
admissibility of the $(ihd)$ rule. It will be instructive to first consider
the case of permuting $(nd)$ above the $(\exists_{r})$ rule solely. It will be
seen that in order to permute $(nd)$ above $(\exists_{r})$, it is sufficient
to strengthen the $(\exists_{r})$ rule through the addition of a side
condition; this motivates a similar side condition that we will impose on
$(id_{q})$ (yielding the rule $(id^{n}_{q})$) and on $(\forall_{l})$ (yielding
the rule $(\forall^{n}_{l})$).

To begin our analysis, observe (1) a non-trivial application of $(nd)$ after
an $(\exists_{r})$ inference, and (2) the result of applying $(nd)$ to the top
sequent in (1).

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

$\mathcal{R},v\leq w,\underline{a}\in D_{v},\underline{a}\in
D_{w},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(nd)$
$\mathcal{R},v\leq w,\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ (2)

In (2), the application of $(nd)$ has generated a labelled sequent where the
domain atom (i.e. $\underline{a}\in D_{v}$) is associated with the label $v$
_one step in the past_ of $w$ (due to the presence of the $v\leq w$ relational
atom). One possible solution to overcome this obstacle, and to allow for the
permutation of $(nd)$ above $(\exists_{r})$, would be to add the following
rule to our calculus:

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

In the rule above, the domain atom $\underline{a}\in D_{v}$ is associated with
the label $v$, which is _one step in the past_ of $w$. Although the addition
of the above rule solves the problem of permuting $(nd)$ above the
$(\exists_{r})$ rule, its inclusion into our calculus would inevitably place
us in a similar, undesirable circumstance:

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

It appears that now we would need to add a new version of the $(\exists_{r})$
rule allowing us to delete $w:A(\underline{a})$ when the required relational
atom $\underline{a}\in D_{u}$ is associated with a label (viz. $u$) that is
_two steps in the past_ of $w$ (due to the occurrence of $u\leq v,v\leq w$).
Including such a rule however, would inevitably force us to add another
existential rule where the required relational atom is associated with a label
_three steps in the past_ —such rule inclusions would then continue ad
infinitum. To resolve the problem, and capture all such possibilities, we add
the following rule to our calculus, which has the side condition
$v\leadsto^{\mathcal{R}}w$ (see Def. 4.11 and Fig. 7):

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

This rule generalizes the shifting behaviour of the domain atom witnessed
above to include all possible _shifts_. Furthermore, due to the fact that the
labelled sequents we are considering encode an $\mathsf{IntQ}$-model—which
satisfies the _nested domain_ condition—it is appropriate to impose the above
side condition, which essentially states that _if an object is an element of
some domain $D_{v}$ in the past of $w$, then it is an element of the domain
$D_{w}$_. It is straightforward to verify that the $(\exists^{n}_{r})$ rule is
sound relative to $\mathsf{IntQ}$-models.

If one analyzes the cases of permuting $(nd)$ above the $(id_{q})$ and
$(\forall_{l})$ rules, then they will observe the same shifting behavior of
domain atoms as in the $(\exists_{r})$ case. We therefore impose a similar
side condition on $(id_{q})$ and $(\forall_{l})$ to obtain the $(id^{n}_{q})$
and $(\forall^{n}_{l})$ rules (see Fig. 7). It is not difficult to see that
the following holds:

######  Lemma 6.3.

The $(id_{q})$, $(\exists_{r})$, and $(\forall_{l})$ rules are instances of
the $(id^{n}_{q})$, $(\exists^{n}_{r})$, and $(\forall^{n}_{l})$ rules,
respectively.

The lemma below shows that the $(id^{n}_{q})$, $(\forall^{n}_{l})$, and
$(\exists^{n}_{r})$ rules are sufficient to prove the admissibility of $(nd)$:

######  Lemma 6.4.

The rule $(nd)$ is admissible in the calculus
$\mathsf{G3IntQ}^{*}-\\{(ref),(tra)\\}$.

######  Proof 6.5.

We prove the result by induction on the height of the given derivation. By
Lem. 4.15 and Lem. 6.1, we need only consider the non-trivial $(id^{n}_{q})$,
$(\exists^{n}_{r})$, and $(\forall^{n}_{l})$ cases.

Base case. We let $\mathcal{R}^{\prime}:=\mathcal{R},u\leq
v,\underline{a}_{1}\in D_{v_{1}},\ldots,\underline{a}_{n}\in D_{v_{n}}$ and
assume that both $v\leadsto^{\mathcal{R}^{\prime}}w$ and
$v_{i}\leadsto^{\mathcal{R}^{\prime}}w$ (for $i\in\\{1,\ldots,n\\}$) hold.
Observe that the end sequent is an instance of $(id^{n}_{q})$ since (i) the
paths from $v_{i}$ to $w$ are still present and (ii) there is a directed path
from $u$ to $w$ composed of the relational atom $u\leq v$ and the direct path
from $v$ to $w$ (i.e. $u\leadsto^{\mathcal{R}^{\prime}}w$ holds).

$(id^{n}_{q})$ $\mathcal{R}^{\prime},\underline{b}\in D_{u},\underline{b}\in
D_{v},\Gamma,w:p(\vv{\underline{a}},\underline{b})\Rightarrow
w:p(\vv{\underline{a}},\underline{b}),\Delta$ $(nd)$
$\mathcal{R}^{\prime},\underline{b}\in
D_{u},\Gamma,w:p(\vv{\underline{a}},\underline{b})\Rightarrow
w:p(\vv{\underline{a}},\underline{b}),\Delta$
---

Inductive step. We provide each proof below showing that $(nd)$ can be
permuted above $(\exists^{n}_{r})$ and $(\forall^{n}_{l})$ (we consider only
the non-trivial cases). Also, we assume that there is a directed path from $v$
to $w$, i.e. the side condition $v\leadsto^{\mathcal{R}}w$ holds.

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

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

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

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

By assumption, there is a directed path from $v$ to $w$ in $\mathcal{R}$.
Observe that the side condition is still satisfied after the invocation of IH
since there is a directed path from $u$ to $w$ composed of the relational atom
$u\leq v$ and the directed path from $v$ to $w$ in $\mathcal{R}$. ∎

We now turn our attention toward analyzing the admissibility of $(ihd)$ in the
calculus $\mathsf{G3IntQ}^{*}-\\{(ref),(tra),(nd)\\}$. We will see that
sufficient modifications must be made to the $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ rules to necessitate the elimination of $(ihd)$ from a
given derivation. (NB. Due to Lem. 6.3, we may omit consideration of permuting
$(ihd)$ above $(\exists_{r})$ and $(\forall_{l})$.) Let us consider non-
trivial applications of $(ihd)$ after an $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ inference:

$\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{n}_{r})$ $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow w:\exists xA,\Delta$ $(ihd)$ $\mathcal{R},\Gamma\Rightarrow w:\exists xA,\Delta$ |  $\mathcal{R},\underline{a}\in D_{v},\Gamma,w:\forall xA,w:A(\underline{a}/x)\Rightarrow\Delta$ $(\forall^{n}_{l})$ $\mathcal{R},\underline{a}\in D_{v},\Gamma,w:\forall xA,\Rightarrow\Delta$ $(ihd)$ $\mathcal{R},\Gamma,w:\forall xA,\Rightarrow\Delta$
---|---

Observe that the $(ihd)$ rule cannot be permuted above the $(\exists^{n}_{r})$
or $(\forall^{n}_{l})$ rules due to the existence of the labelled formula
$w:A(\underline{a}/x)$ in the top sequent which violates the side condition on
$(ihd)$ stating that $\underline{a}$ must be an eigenvariable. Our solution to
this issue is to _absorb_ the $(ihd)$ rule into the $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ rules yielding the new versions $(\exists^{in}_{r})$ and
$(\forall^{in}_{l})$:

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

where we impose the side condition that $v\leadsto^{\mathcal{R}}w$ and
$\underline{a}$ is an eigenvariable. This side condition essentially states
that _there exists an element of $D_{w}$, which is also in a domain $D_{v}$ in
the past of $w$_. It can be shown that each rule is sound relative to
$\mathsf{IntQ}$-models, and relies both on the nested domain condition and the
fact that such domains are _non-empty_ , i.e. _inhabited_.

######  Lemma 6.6.

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

######  Proof 6.7.

We prove the result by induction on the height of the given derivation. The
base case is simple as any application of $(ihd)$ to $(id^{n}_{q})$ or
$(\bot_{l})$ yields another instance of the rule. By Lem. 4.15 and Lem. 6.3,
the only cases we need to consider in the inductive step are the non-trivial
$(\exists^{n}_{r})$ and $(\forall^{n}_{l})$ cases; however, as we saw above,
the non-trivial cases can be handled by applying $(\exists^{in}_{r})$ or
$(\forall^{in}_{l})$, respectively. ∎

######  Theorem 6.8.

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

######  Proof 6.9.

The admissibility of $\\{(ref),(tra)\\}$,
$\\{(id_{q}),(\exists_{r}),(\forall_{l})\\}$, $(nd)$, and $(ihd)$ follow from
Lem. 6.1, Lem. 6.3, Lem. 6.4, and Lem. 6.6, respectively. Admissibility of
$(\supset_{l})$ is similar to Lem. 5.2 and admissibility of $(\bot_{l})$
follows from the fact that the rule can be derived using $(\neg_{l})$ and
$(\land_{l})$. ∎

######  Theorem 6.10.

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

######  Proof 6.11.

Similar to Thm. 5.9. ∎

Although the above theorem is fundamental for translating derivations in
$\mathsf{IntQL}$ into derivations in $\mathsf{NIntQ}$, additional work needs
to be done to ensure that the $(\exists^{n}_{r})$ and $(\forall^{n}_{l})$
rules properly translate to instances of the $(\exists_{r})$ and
$(\forall_{l})$ rules. The side condition imposed on $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ relies on the existence of a domain atom containing a
parameter $\underline{a}$, whereas the side condition imposed on the nested
$(\exists_{r})$ and $(\forall_{l})$ rules stipulates that the parameter
$\underline{a}$ must either be an eigenvariable or available. The question
arises: how do we reconcile these seemingly distinct side conditions?

Interestingly, our process of refinement has offered us an unadulterated
perspective of the nested $(\exists_{r})$ and $(\forall_{l})$ rules. As will
be argued below (Thm. 6.14), the rules $(\exists^{in}_{r})$ and
$(\forall^{in}_{l})$ in $\mathsf{IntQL}$ translate to instances of the nested
$(\exists_{r})$ and $(\forall_{l})$ rules where the relevant parameter of the
inference is an _eigenvariable_ , and the rules $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ translate to instances of the nested $(\exists_{r})$ and
$(\forall_{l})$ rules where the relevant parameter of the inference is
_available_. In other words, what are single rules with a disjunctive side
condition in the nested setting have bifurcated into distinct sets of rules
with atomic side conditions in the labelled setting.

In order to ensure that instances of $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ properly translate to instances of the nested
$(\exists_{r})$ and $(\forall_{l})$ rules then, we must show that if the side
condition of the former rules holds, then the side condition of the latter
rules holds. This motivates the definition of a _nested form_ derivation:

######  Definition 6.12 (Nested Form).

Let $\Pi$ be a derivation of a labelled sequent $\Lambda$ in $\mathsf{IntQL}$.
We define $\Pi$ to be in _nested form_ iff (i) $\Lambda$ is nestedlike, and
(ii) for each instance of $(\exists^{n}_{r})$ and $(\forall^{n}_{l})$ in
$\Pi$:

$\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(\exists^{n}_{r})$ $\mathcal{R},\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:\exists xA$ |  $\mathcal{R},\underline{a}\in D_{v},w:A(\underline{a}/x),w:\forall xA,\Gamma\Rightarrow\Delta$ $(\forall^{n}_{l})$ $\mathcal{R},\underline{a}\in D_{v},w:\forall xA,\Gamma\Rightarrow\Delta$
---|---

there exists a formula $u:B(\underline{a})$ such that
$u\leadsto^{\mathcal{R}}w$ in the conclusion of the inference.

Assuming we are given a nested form derivation in $\mathsf{IntQL}$, condition
(ii) of the above definition ensures that instances of $(\exists^{n}_{r})$ and
$(\forall^{n}_{l})$ will properly translate into instances of $(\exists_{r})$
and $(\forall_{l})$ in $\mathsf{NIntQ}$. Additionally, nested form proofs are
significant because one can view the space of nested form proofs in
$\mathsf{IntQL}$ as being equivalent to the space of proofs generated by
$\mathsf{NIntQ}$, as confirmed by Thm. 6.14 and 6.16 below. Before we
establish this correspondence however, the following lemma is needed for the
proof of Thm. 6.14, that is, for showing that if a nestedlike labelled sequent
$\Lambda$ is provable in $\mathsf{IntQL}$, then $\mathfrak{N}(\Lambda)$ is
provable in $\mathsf{NIntQ}$.

######  Lemma 6.13.

If a nestedlike labelled sequent $\Lambda$ is derivable in $\mathsf{IntQL}$,
then $\Lambda$ has a nested form derivation in $\mathsf{IntQL}$.

The truth of the above lemma can be seen to follow from Thm. 6.16 below (which
states that each derivation in $\mathsf{NIntQ}$ of a nested sequent $\Sigma$
can be translated into a nested form derivation of $\mathfrak{L}(\Sigma)$ in
$\mathsf{IntQL}$) in conjunction with a few facts: (i) $\mathsf{IntQL}$ is
sound, (ii) one can show by semantic arguments that if a nestedlike labelled
sequent $\Lambda$ is valid, then so is $\mathfrak{N}(\Lambda)$, (iii) by
Fitting’s work in [9], we know that $\mathsf{NIntQ}$ is strongly complete
(Thm. 3.5), and (iv) for any nestedlike labelled sequent $\Lambda$,
$\mathfrak{L}(\mathfrak{N}(\Lambda))=\Lambda$ (Lem. 4.9).444The soundness of
$\mathsf{IntQL}$ is established by Thm. 8.7 in Sect. 8, where it is shown that
every derivation in $\mathsf{IntQL}$ can be effectively transformed into a
derivation of the same labelled sequent in $\mathsf{G3IntQ}$. Since
$\mathsf{G3IntQ}$ is sound by Thm. 3.1, this establishes the soundness of
$\mathsf{IntQL}$. Hence, given a derivable nestedlike labelled sequent
$\Lambda$, which is therefore valid since $\mathsf{IntQL}$ is sound by (i), it
follows that $\mathfrak{N}(\Lambda)$ is valid by (ii), meaning that
$\mathfrak{N}(\Lambda)$ is derivable by (iii), and so by Thm. 6.16 below,
$\mathfrak{L}(\mathfrak{N}(\Lambda))$ has a nested form derivation, i.e.
$\Lambda$ has a nested form derivation by (iv). Although this argument serves
as a proof of Lem. 6.13, it is not entirely satisfactory.

The above argument relies on the completeness of $\mathsf{NIntQ}$, and so, if
our aim were to extract $\mathsf{NIntQ}$ from $\mathsf{G3IntQ}$ without any
prior knowledge of $\mathsf{NIntQ}$ or its properties, or to show
$\mathsf{NIntQ}$ complete via this extraction, then since the above argument
relies on the completeness of $\mathsf{NIntQ}$ (i.e. Thm. 3.5), we would fail
to reach our aim. The author sees at least two possible strategies for
confirming the above lemma without relying on the completeness of
$\mathsf{NIntQ}$. In the first method, one could write a (potentially non-
terminating) proof-search procedure for $\mathsf{IntQL}$ that takes a
nestedlike labelled sequent $\Lambda$ as input and attempts to construct a
nested form proof of $\Lambda$, showing that a counter-model for $\Lambda$ can
be constructed given that the procedure does not halt with a nested form proof
of the input. Such a method of proof would effectively prove the completeness
of $\mathsf{IntQL}$ relative to valid nestedlike labelled sequents while
showing that every such sequent possesses a nested form proof. The second
method consists of showing how to algorithmically transform any derivation of
a nestedlike labelled sequent $\Lambda$ in $\mathsf{IntQL}$ into a nested form
proof of $\Lambda$. Such methods of proof are desirable as they would
effectively demonstrate that $\mathsf{NIntQ}$ inherits completeness from its
associated labelled calculus $\mathsf{G3IntQ}$, however, we leave such results
to future work, and continue our investigation of the correspondence between
semantic and nested systems.

######  Theorem 6.14.

If a nestedlike labelled sequent $\Lambda$ is derivable in $\mathsf{IntQL}$,
then $\mathfrak{N}(\Lambda)$ is derivable in $\mathsf{NIntQ}$.

######  Proof 6.15.

Since $\Lambda$ is nestedlike and derivable by assumption, we know that
$\Lambda$ is treelike (by Lem. 4.9) and has a nested form derivation $\Pi$ (by
Lem. 6.13), implying that $\Pi$ is treelike by Thm. 6.10. Hence, the
translation function $\mathfrak{N}$ is defined for each labelled sequent in
$\Pi$. It is straightforward to verify that each rule in $\mathsf{IntQL}$—with
the exception of $(\exists^{n}_{r})$, $(\exists^{in}_{r})$,
$(\forall^{n}_{l})$, and $(\forall^{in}_{l})$—translates to an instance of the
corresponding rule in $\mathsf{NIntQ}$ under the $\mathfrak{N}$ translation.
We show the translation of the $(\exists^{n}_{r})$ and $(\exists^{in}_{r})$
inferences below; the $(\forall^{n}_{l})$ and $(\forall^{in}_{l})$ inferences
are similar.

In the $(\exists^{n}_{r})$ inference top-left below, we know that there exists
a labelled formula $u:B(\underline{a})\in\Gamma,\Delta$ where
$u\leadsto^{\mathcal{R}}w$ since our given derivation is in nested form (Def.
6.12). Hence, after applying $\mathfrak{N}$ to the premise of the
$(\exists^{n}_{r})$ inference, the parameter $\underline{a}$ will occur in the
formula $B(\underline{a})$ that is either in the component $\Gamma\restriction
w\rightarrow A(\underline{a}/x),\exists xA,\Delta\restriction w$ (and is
different than the occurrence of $A(\underline{a}/x)$) or is in the past of
the component in the nested sequent $\Sigma\\{\Gamma\restriction w\rightarrow
A(\underline{a}/x),\exists xA,\Delta\restriction w\\}$. Hence, the parameter
$\underline{a}$ is available, and so, the necessary side condition of the
$(\exists_{r})$ inference is met. In the $(\exists^{in}_{r})$ inference below,
the parameter $\underline{a}$ is an eigenvariable and continues to be so after
applying the translation $\mathfrak{N}$, implying that the nested
$(\exists_{r})$ inference is valid.

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

$\mathfrak{N}(\mathcal{R},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA)$ . =
$\Sigma\\{\Gamma\restriction w\rightarrow A(\underline{a}/x),\exists
xA,\Delta\restriction w\\}$ $(\exists_{r})$ $\Sigma\\{\Gamma\restriction
w\rightarrow\exists xA,\Delta\restriction w\\}$ . =
$\mathfrak{N}(\mathcal{R},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:\exists xA)$

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

$\mathfrak{N}(\mathcal{R},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA)$ . =
$\Sigma\\{\Gamma\restriction w\rightarrow A(\underline{a}/x),\exists
xA,\Delta\restriction w\\}$ $(\exists_{r})$ $\Sigma\\{\Gamma\restriction
w\rightarrow\exists xA,\Delta\restriction w\\}$ . =
$\mathfrak{N}(\mathcal{R},\Gamma\Rightarrow\Delta,w:\exists xA)$

∎

######  Theorem 6.16.

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

######  Proof 6.17.

We show how to translate the $(\vee_{l})$, $(lift)$, $(\supset_{r})$ and
$(\exists_{r})$ rules as all other cases are simple or similar. Last, we argue
that the derivation obtained in $\mathsf{IntQL}$ is in nested form.

$(\vee_{l})$. Our given $(\vee_{l})$ inference is shown below top. Let
$\vec{\underline{a}}:=\underline{a}_{1},\ldots,\underline{a}_{n}$ be all free
parameters in $A,X,Y$ that do not occur in $B,X,Y$, and let
$\vec{\underline{b}}:=\underline{b}_{1},\ldots,\underline{b}_{k}$ be all free
parameters in $B,X,Y$ that do not occur in $A,X,Y$. To obtain the desired
conclusion, we first apply the hp-admissibility of $(wk)$ (Lem. 4.13) in order
to ensure that the contexts of the premises match, followed by an application
of the $(\vee_{l})$ rule. We assume that $w$ is the label assigned to the
formulae of the components $X,A\rightarrow Y$ and $X,B\rightarrow Y$ in
$\Sigma\\{X,A\rightarrow Y\\}$ and $\Sigma\\{X,B\rightarrow Y\\}$,
respectively.

$\Sigma\\{X,A\rightarrow Y\\}$ $\Sigma\\{X,B\rightarrow Y\\}$ $(\vee_{l})$
$\Sigma\\{X,A\lor B\rightarrow Y\\}$

$\mathfrak{L}(\Sigma\\{X,A\rightarrow Y\\})$ . =
$\mathcal{R},\vec{\underline{a}}\in D_{w},w:A,\Gamma\Rightarrow\Delta$ $(wk)$
$\mathcal{R},\vec{\underline{a}}\in D_{w},\vec{\underline{b}}\in
D_{w},w:A,\Gamma\Rightarrow\Delta$ $\mathfrak{L}(\Sigma\\{X,B\rightarrow
Y\\})$ . = $\mathcal{R},\vec{\underline{b}}\in
D_{w},w:B,\Gamma\Rightarrow\Delta$ $(wk)$ $\mathcal{R},\vec{\underline{a}}\in
D_{w},\vec{\underline{b}}\in D_{w},w:B,\Gamma\Rightarrow\Delta$ $(\vee_{l})$
$\mathcal{R},\vec{\underline{a}}\in D_{w},\vec{\underline{b}}\in D_{w},w:A\vee
B,\Gamma\Rightarrow\Delta$ . = $\mathfrak{L}(\Sigma\\{X,A\lor B\rightarrow
Y\\})$

$(lift)$. Our given $(lift)$ inference is shown below top-left. Let
$\vec{\underline{a}}:=\underline{a}_{1},\ldots,\underline{a}_{n}$ be all free
parameters occurring in $A$ that do not occur in $X^{\prime},Y^{\prime}$, $w$
be the label assigned to the formulae of the component $X,A\rightarrow Y$, and
$u$ be the label assigned to the formulae of the component
$X^{\prime},A\rightarrow Y^{\prime}$. If we invoke the admissibility of $(nd)$
(Thm. 6.8) $n$ times to delete all domain atoms $\vec{\underline{a}}\in
D_{u}$, then after an application of $(lift)$, we obtain the desired
conclusion.

$\Sigma\\{X,A\rightarrow Y,[X^{\prime},A\rightarrow Y^{\prime}]\\}$ $(lift)$
$\Sigma\\{X,A\rightarrow Y,[X^{\prime}\rightarrow Y^{\prime}]\\}$

$\mathfrak{L}(\Sigma\\{X,A\rightarrow Y,[X^{\prime},A\rightarrow
Y^{\prime}]\\})$ . = $\mathcal{R},\vec{\underline{a}}\in
D_{w},\vec{\underline{a}}\in D_{u},w\leq u,w:A,u:A,\Gamma\Rightarrow\Delta$
$(nd)\times n$ $\mathcal{R},\vec{\underline{a}}\in D_{w},w\leq
u,w:A,u:A,\Gamma\Rightarrow\Delta$ $(lift)$
$\mathcal{R},\vec{\underline{a}}\in D_{w},w\leq u,w:A,\Gamma\Rightarrow\Delta$
. = $\mathfrak{L}(\Sigma\\{X,A\rightarrow Y,[X^{\prime}\rightarrow
Y^{\prime}]\\})$

$(\supset_{r})$. Let
$\vec{\underline{a}}:=\underline{a}_{1},\ldots,\underline{a}_{n}$ be the free
parameters occurring in the active formulae $A$ and $B$ (shown in the
$(\supset_{r})$ inference below). Let $w$ be the label assigned to the
formulae of the component $X\rightarrow Y$ and $v$ be the label assigned to
the formulae of the component $A\rightarrow B$ after applying the translation
function $\mathfrak{L}$. In order to obtain the desired conclusion, we first
apply the hp-admissibility of $(wk)$ (Lem. 4.13), which introduces the domain
atoms $\vec{\underline{a}}^{\prime}\in D_{w}:=\underline{a}_{i_{1}}\in
D_{w},\ldots,\underline{a}_{i_{k}}\in D_{w}$ such that
$\underline{a}_{i_{j}}\in D_{w}\not\in\mathcal{R}$ for
$i_{j}\in\\{1,\ldots,n\\}$ and $j\in\\{1,\ldots,k\\}$, i.e. for each parameter
$\underline{a}_{i_{j}}$ in $\vec{\underline{a}}$ we introduce the domain atom
$\underline{a}_{i_{j}}\in D_{w}$ given that it does not already occur in
$\mathcal{R}$. Next, we apply admissibility of $(nd)$ (Thm. 6.8) $n$ times to
delete all domain atoms $\vec{\underline{a}}\in D_{v}$, making $v$ an
eigenvarible, and permitting $(\supset_{r})$ to be applied.

$\Sigma\\{X\rightarrow Y,[A\rightarrow B]\\}$ $(\supset_{r})$
$\Sigma\\{X\rightarrow A\supset B,Y\\}$

$\mathfrak{L}(\Sigma\\{X\rightarrow Y,[A\rightarrow B]\\})$ . =
$\mathcal{R},\vec{\underline{a}}\in D_{v},w\leq
v,v:A,\Gamma\Rightarrow\Delta,v:B$ $(wk)$
$\mathcal{R},\vec{\underline{a}}^{\prime}\in D_{w},\vec{\underline{a}}\in
D_{v},w\leq v,v:A,\Gamma\Rightarrow\Delta,v:B$ $(nd)\times n$
$\mathcal{R},\vec{\underline{a}}^{\prime}\in D_{w},w\leq
v,v:A,\Gamma\Rightarrow\Delta,v:B$ $(\supset_{r})$
$\mathcal{R},\vec{\underline{a}}^{\prime}\in
D_{w},\Gamma\Rightarrow\Delta,w:A\supset B$ . =
$\mathfrak{L}(\Sigma\\{X\rightarrow A\supset B,Y\\})$

$(\exists_{r})$. If the relevant parameter $\underline{a}$ (in the active
formula $A(\underline{a}/x)$) is an _eigenvariable_ in the $(\exists_{r})$
inference below, then the inference translates to an instance of
$(\exists^{in}_{r})$. If the relevant parameter is _available_ in the
inference, then the translation requires more care, so we focus on showing how
to translate this case below.

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

Since the parameter $\underline{a}$ is available in $(\exists_{r})$, this
implies that there exists some formula $B(\underline{a})$ (different than the
occurrence of $A(\underline{a}/x)$) occurring in, or in the past of, the
displayed component $X\rightarrow A(\underline{a}/x),\exists xA,Y$ of the
nested sequent $\Sigma\\{X\rightarrow A(\underline{a}/x),\exists xA,Y\\}$
(i.e. the premise of the $(\exists_{r})$ inference above). We assume 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. By the definition of
$\mathfrak{L}$ (Def. 4.7), this 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 we have
explicitly included in the derivation below). Because $B(\underline{a})$ is
available and is associated with the label $u$, this implies that there is a
directed path $u\leq v_{1}$, $\ldots$, $v_{n}\leq w$ from $u$ to $w$ in
$\mathcal{R}$, i.e. $u\leadsto^{\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 directed path, invoke the admissibility of
$(nd)$ (Thm. 6.8), and then apply $(\exists^{n}_{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(n+1)$
$\mathcal{R},\underline{a}\in D_{u},\Gamma\Rightarrow
w:A(\underline{a}/x),w:\exists xA,\Delta$ $(\exists^{n}_{r})$
$\mathcal{R},\underline{a}\in D_{u},\Gamma\Rightarrow w:\exists xA,\Delta$ . =
$\mathfrak{L}(\Sigma\\{X\rightarrow\exists xA,Y\\})$
---

To see why the output derivation is in nested form, first observe that the
conclusion of the derivation will be $\mathfrak{L}(\Sigma)$, which, _ipso
facto_ , makes the conclusion a nestedlike labelled sequent; hence, the
derivation satisfies property (i) of Def. 6.12. Second, observe that the
output derivation in $\mathsf{IntQL}$ satisfies property (ii) of Def. 6.12
since each $(\exists^{n}_{r})$ and $(\forall^{n}_{r})$ inference is obtained
from an $(\exists_{r})$ or $(\forall_{l})$ inference in the input derivation,
ensuring the existence of a labelled formula $u:B(\underline{a})$ in the
conclusion of any $(\exists^{n}_{r})$ or $(\forall^{n}_{r})$ inference such
that there is a directed path from $u$ to the label $w$ prefixing the
principal formula. ∎

##  7 Deriving the Calculus $\mathsf{NIntQC}$ from $\mathsf{G3IntQC}$

In the previous section, we saw that strengthening the $(\exists_{r})$ and
$(\forall_{l})$ rules allowed for the rules $(nd)$ and $(ihd)$ to be
eliminated from any given derivation. In this section, we will focus on how to
strengthen these rules even further to additionally obtain the elimination of
$(cd)$ from any given derivation. We begin our analysis after first stating
the following admissibility result:

######  Lemma 7.1.

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

######  Proof 7.2.

The proof is similar to Lem. 6.1 and is detailed in Appendix A for the
interested reader. ∎

The exclusion of $(ref)$ and $(tra)$ implies the completeness of
$\mathsf{G3IntQC}^{*}-\\{(ref),(tra)\\}$ relative to treelike derivations,
similar to Lem. 6.10. We therefore assume for the rest of the section that all
labelled sequents we consider are treelike—this assumption will ease our
admissibility analyses of $(nd)$, $(cd)$, and $(ihd)$, though note that the
assumption can be omitted, if desired.

Previously, we saw that permutations of the $(nd)$ rule above the $(id_{q})$,
$(\exists_{r})$, and $(\forall_{l})$ rules shifted domain atoms to the past.
We now investigate how permutations of the $(cd)$ rule affect domain atoms in
$(id_{q})$, $(\exists_{r})$, and $(\forall_{l})$. As before, we first
concentrate on permuting $(cd)$ above the $(\exists_{r})$ rule solely.
Observing the effect of permuting $(cd)$ above $(\exists_{r})$ will motivate
how we strengthen the rule—and the $(id_{q})$ and $(\forall_{l})$ rules—to
obtain the complete elimination of $(cd)$ from any given derivation.

To begin our analysis, observe (3) a non-trivial application of $(cd)$ after
an $(\exists_{r})$ inference, and (4) the result of applying $(cd)$ to the top
sequent in (3).

$\mathcal{R},w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$
$(\exists_{r})$ $\mathcal{R},w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:\exists xA$ $(cd)$ $\mathcal{R},w\leq
v,\underline{a}\in D_{v},\Gamma\Rightarrow\Delta,w:\exists xA$ (3)

$\mathcal{R},w\leq v,\underline{a}\in D_{w},\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ $(cd)$
$\mathcal{R},w\leq v,\underline{a}\in
D_{v},\Gamma\Rightarrow\Delta,w:A(\underline{a}/x),w:\exists xA$ (4)

The application of $(cd)$ has generated a labelled sequent where the domain
atom (i.e. $\underline{a}\in D_{v}$) is associated with the label $v$ _one
step in the future_ of $w$ (due to the presence of the $w\leq v$ relational
atom). By analogy to what we saw in the last section (in the case of permuting
$(nd)$ above $(\exists_{r})$), it is not hard to see that successive (non-
trivial) permutations of $(cd)$ above an $(\exists_{r})$ inference will
continually shift the domain atom to the future. If—at the same time—we also
consider (non-trivial) permutations of the $(nd)$ rule above the
$(\exists_{r})$ rule, then the domain atom can shift either to the future or
the past.

Recall that we have restricted our analysis to only consider derivations in
$\mathsf{G3IntQC}^{*}-\\{(ref),(tra)\\}$ that employ treelike labelled
sequents. Observe that _any node_ in the graph of a treelike labelled sequent
is reachable from any other node by a sequence of forward and backwards edges.
This property of treelike labelled sequents, accompanied by the witnessed
shifting behavior discussed in the previous paragraph, suggests that we ought
to add the following $(\exists^{c}_{r})$ rule (see Fig. 7) to our calculus:

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

with the side condition that $v\sim^{\mathcal{R}}w$, i.e. there is an
undirected path from the label $v$ to the label $w$. Observe that this side
condition generalizes the shifting behaviour of the domain atom to include all
possible forward and backward _shifts_. Intuitively, this side condition
states that _if an object is an element of some domain $D_{v}$, then it is an
element of the domain $D_{w}$_, which always holds in the _constant domain_
setting.

The same shifting behavior can be witnessed by considering the permutation of
$(nd)$ and $(cd)$ above the $(id_{q})$ and $(\forall_{l})$ rules. Thus, we
strengthen those rules in a similar way to obtain the $(id^{c}_{q})$ and
$(\forall^{c}_{l})$ rules (see Fig. 7).

######  Lemma 7.3.

The $(id_{q})$, $(\exists_{r})$, and $(\forall_{l})$ rules are instances of
the $(id^{c}_{q})$, $(\exists^{c}_{r})$, and $(\forall^{c}_{l})$ rules,
respectively.

The lemma below confirms that the strengthened versions of $(id_{q})$,
$(\exists_{r})$, and $(\forall_{l})$ are sufficient to prove the admissibility
of the $(nd)$ and $(cd)$ rules in the calculus
$\mathsf{G3IntQC}^{*}-\\{(ref),(tra)\\}$:

######  Lemma 7.4.

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

######  Proof 7.5.

The proof is similar to the proof of Lem. 6.4, but where undirected paths
(Def. 4.12) are used instead of directed paths (Def. 4.11). ∎

In the previous section, we saw that permutations of $(ihd)$ above the
$(\exists^{n}_{r})$ and $(\forall^{n}_{l})$ rules could not be performed in
certain cases. To resolve this issue, we introduced versions of the rules that
absorbed the $(ihd)$ rule. The same phenomenon occurs in the case of the
$(\exists^{c}_{r})$ and $(\forall^{c}_{l})$ rules, implying that we need to
add $(\exists^{ic}_{r})$ and $(\forall^{ic}_{l})$ to our calculus (see Fig.
7).