# Constructive Interpolation and Concept-Based Beth Definability for
Description Logics via Sequents

Tim S. Lyon  Jonas KargeInstitute of Artificial Intelligence, Technische
Universität Dresden {timothy_stephen.lyon<EMAIL_ADDRESS>
###### Abstract

We introduce a constructive method applicable to a large number of description
logics (DLs) for establishing the concept-based Beth definability property
(CBP) based on sequent systems. Using the highly expressive DL $\mathcal{RIQ}$
as a case study, we introduce novel sequent calculi for
$\mathcal{RIQ}$-ontologies and show how certain interpolants can be computed
from sequent calculus proofs, which permit the extraction of explicit
definitions of implicitly definable concepts. To the best of our knowledge,
this is the first sequent-based approach to computing interpolants and
definitions within the context of DLs, as well as the first proof that
$\mathcal{RIQ}$ enjoys the CBP. Moreover, due to the modularity of our sequent
systems, our results hold for any restriction of $\mathcal{RIQ}$, and are
applicable to other DLs by suitable modifications.

##  1 Introduction

Defining new concepts in terms of given concepts and relations is an important
operation within the context of description logics (DLs), and logic more
generally. Typically, a new concept $\mathsf{NewC}$ can be defined in one of
two ways: (1) _implicitly_ , by specifying a set of axioms such that the
interpretation of $\mathsf{NewC}$ is uniquely determined by the interpretation
of the given concepts and relations, or (2) _explicitly_ , by writing a
definition $\mathsf{NewC}\equiv\mathsf{D}$ where $\mathsf{NewC}$ does not
appear in $\mathsf{D}$. Description logics for which implicit definability
implies explicit definability are said to be _definitorially complete_ Baader
and Nutt (2003); ten Cate et al. (2006), or to exhibit the _concept-based Beth
definability property (CBP)_ ten Cate et al. (2013). This is Beth’s
definability property Beth (1956) from first-order logic rephrased for DLs.

Beth definability and variations thereof have found numerous applications in
DLs. For example, the property has been used in ontology engineering to
extract acyclic terminologies from general ones Baader and Nutt (2003); ten
Cate et al. (2006). This is of particular importance since reasoning with
acyclic terminologies is usually less complex than with general ones, e.g.
satisfiability over acyclic $\mathcal{ALC}$-terminologies is
$\mathsf{PSPACE}$-complete while being $\mathsf{EXPTIME}$-complete over
general $\mathcal{ALC}$-terminologies Donini (2003). Other applications
include, rewriting ontology-mediated queries Franconi and Kerhet (2019);
Seylan et al. (2009); Toman and Weddell (2022), learning concepts separating
positive and negative examples Artale et al. (2023); Funk et al. (2019), and
computing referring expressions, which is of value in computational
linguistics and data management Areces et al. (2008); Borgida et al. (2016);
Artale et al. (2021).

A number of methods have been used to confirm the existence of, or actually
compute, explicit definitions of implicitly definable concepts for expressive
DLs; e.g. model-theoretic mosaic-based methods have been employed to decide
the existence of explicit definitions for $\mathcal{ALC}\mathcal{H}$,
$\mathcal{ALC}\mathcal{O}$, and
$\mathcal{ALC}\mathcal{H}\mathcal{O}\mathcal{I}$ Artale et al. (2023); Jung et
al. (2022). However, as noted in these works, these methods are _non-
constructive_ , confirming the existence of explicit definitions without
necessarily providing them. Thus, interest has been expressed in developing
constructive methods that _actually compute_ explicit definitions. We note
that constructive methods have been employed in the literature, e.g. methods
relying on the computation of normal forms and uniform interpolants ten Cate
et al. (2006) or which compute explicit definitions using tableau-based
algorithms ten Cate et al. (2013). With the aim of furthering this programme,
we present a constructive method applicable to a large number of DLs, which
computes explicit concept-based definitions of implicitly definable concepts
and establishes the CBP by means of _sequent systems_.

Since its introduction in the 1930’s, Gentzen’s sequent calculus has become
one of the preferred formalisms for the construction of proof calculi Gentzen
(1935a, b). A sequent calculus is a set of inference rules operating over
expressions (called _sequents_) of the form $\Gamma\vdash\Delta$ with $\Gamma$
and $\Delta$ sequences or (multi)sets of formulae. Sequent systems have found
fruitful applications, being exploited in the development of automated
reasoning methods Slaney (1997) and being used to establish non-trivial
properties of logics such as consistency Gentzen (1935a, b), decidability
Dyckhoff (1992), and interpolation Maehara (1960). Regarding this last point,
it was first shown by Maehara that sequent systems could be leveraged to
_constructively_ prove the Craig interpolation property Craig (1957) of a
logic. Since this seminal work, Maehara’s interpolation method has been
extended and adapted in a variety of ways to prove Craig interpolation for
diverse classes of logics with sequent-style systems, including modal logics
Fitting and Kuznets (2015), intermediate logics Kuznets and Lellmann (2018),
and temporal logics Lyon et al. (2020). As Craig interpolation implies Beth
definability, it follows that the sequent-based methodology is applicable to
the latter.

In this paper, we provide the first sequent calculi for
$\mathcal{RIQ}$-ontologies and show how these calculi can be used to compute
interpolants, explicit definitions, and to confirm the CBP. Although our work
is inspired by Maehara’s method, we note that it is a non-trivial
generalization of that method. As discussed in Lyon et al. (2020), Maehara’s
original method is quite restricted, being inapplicable in many cases to even
basic modal logics, which _a fortiori_ means the method is inapplicable to
expressive DLs. To overcome these difficulties, we use a generalized notion of
sequent and interpolant that encodes a tree whose nodes are multisets of DL
concepts accompanied by (in)equalities over nodes. Given a proof with such
sequents, we show that all axiomatic sequents can be assigned
interpolants—which are themselves sequents—and that such interpolants can be
‘propagated’ through the proof yielding an interpolant of the conclusion.
Explicit definitions can then be readily extracted from these interpolants. We
note that our method is constructive in the sense that interpolants are
computed relative to a _given proof_ of a general concept inclusion implied by
a $\mathcal{RIQ}$-ontology. Although such proofs are in principle computable,
we left the specification of an explicit proof-search algorithm that builds
such proofs to future work, noting that such algorithms can be written by
adapting known techniques; e.g. Horrocks and Sattler (2004).

Finally, we remark that although our work shares similarities with that of ten
Cate et al. (2013), our method goes beyond this work as we establish the CBP
for the highly expressive DL $\mathcal{RIQ}$, and due to the modularity of our
sequent systems, our method is applicable to any restriction of
$\mathcal{RIQ}$, e.g. logics within the $\mathcal{FL}$ and $\mathcal{EL}$
families Donini et al. (1997); Baader et al. (2005). By _modularity_ we mean
that the deletion of inference rules or modification of side conditions on
rules allows for sequent systems to be provided for fragments of
$\mathcal{RIQ}$. Our work also intersects that of ten Cate et al. (2006),
which establishes the CBP for $\mathcal{ALC}$ extended with PUR Horn
conditions, but differs both in terms of methodology and our consideration of
qualified number restrictions.

Outline of Paper: In Section 2, we define the logic $\mathcal{RIQ}$, define
the CBP and related notions, and explicate certain grammar theoretic concepts
used in formulating inference rules. In Section 3, we present our sequent
systems and establish that each system enjoys fundamental properties. Section
4 develops and explains our new sequent-based method that computes explicit
definitions of implicitly definable concepts and establishes the CBP, using
$\mathcal{RIQ}$ as case study. To the best of our knowledge, this is the first
proof that $\mathcal{RIQ}$ has the CBP. In Section 5, we conclude and discuss
future work. We note that all proofs have been deferred to the appendix.

##  2 Preliminaries

In the first part of this section, we introduce the language and semantics for
the description logic $\mathcal{RIQ}$, which subsumes various expressive and
lightweight DLs Baader et al. (2005); Calvanese and De Giacomo (2003).
Subsequently, we discuss and define a notion of interpolation and concept-
based Beth definability, which will be of pivotal interest in this paper. In
the last part of this section, we introduce special types of semi-Thue systems
Post (1947), referred to as _$\mathbf{R}$ -systems_, which are essential in
the formulation of our sequent calculi.

###  2.1 Language and Semantics: $\mathcal{RIQ}$

The description logic $\mathcal{RIQ}$ is defined relative to a _vocabulary_
$\mathcal{V}=(\mathsf{N_{R}},\mathsf{N_{C}})$, which is a pair containing
pairwise disjoint, countable sets. The set $\mathsf{N_{R}}$ contains _role
names_ used to denote binary relations and the set $\mathsf{N_{C}}$ contains
_concept names_ used to denote classes of entities. We use the (potentially
annotated) symbols $r$, $s$, $\ldots$ to denote role names, and $A$, $B$,
$\ldots$ to denote concept names. We define a _role_ to be a role name or an
_inverse role_ ${r}^{-}$ such that $r\in\mathsf{N_{R}}$. We define the
_inverse_ of a role to be $\mathsf{Inv}(r)={r}^{-}$ and
$\mathsf{Inv}({r}^{-})=r$ given that $r\in\mathsf{N_{R}}$. We let
$\mathbf{R}:=\mathsf{N_{R}}\cup\\{\mathsf{Inv}(r)\ |\ r\in\mathsf{N_{R}}\\}$
denote the set of roles.

A _complex role inclusion axiom (RIA)_ is an expression $r_{1}\circ\cdots\circ
r_{n}\sqsubseteq s$ such that $r_{1},\ldots,r_{n}$ and $s$ are roles, and
$\circ$ denotes the usual composition operation over binary relations; we
assume $n$-ary compositions $r_{1}\circ\cdots\circ r_{n}$ associate to the
left. We define an _RBox_ $\mathcal{R}$ to be a finite collection of RIAs. As
identified by Horrocks and Sattler Horrocks and Sattler (2004), to ensure the
decidability of reasoning with $\mathcal{RIQ}$, only _regular RBoxes_ may be
used in ontologies (defined below).111Note, our interpolation results go
through for general RBoxes, i.e. this restriction is not needed for the work
in Sections 3 and 4. Let $\prec$ be a strict partial order on the set
$\mathsf{N_{R}}$ of role names; we define an RIA $w\sqsubseteq r$ to be
_$\prec$ -regular_ iff $r$ is a role name, and either (1) $w=rr$, (2)
$w=r^{-}$, (3) $w=s_{1}\circ\cdots\circ s_{n}$ and $s_{i}\prec r$ for all
$1\leq i\leq n$, (4) $w=r\circ s_{1}\circ\cdots\circ s_{n}$ and $s_{i}\prec r$
for all $1\leq i\leq n$, or (5) $w=s_{1}\circ\cdots\circ s_{n}\circ r$ and
$s_{i}\prec r$ for all $1\leq i\leq n$. An RBox $\mathcal{R}$ is defined to be
_regular_ iff a strict partial order $\prec$ over $\mathsf{N_{R}}$ exists such
that every RIA in $\mathcal{R}$ is $\prec$-regular.

We recursively define a role name $r$ to be _simple_ (with respect to an RBox
$\mathcal{R}$) iff either (1) no RIA of the form $w\sqsubseteq r$ occurs in
$\mathcal{R}$, or (2) for each $s\sqsubseteq r\in\mathcal{R}$, $s$ is a simple
role name or its inverse is. Also, an inverse role ${r}^{-}$ is defined to be
_simple_ if $r$ is simple.

We define _complex concepts_ to be formulae in negation normal form generated
by the following grammar in BNF:

$C::=A\ |\ \neg A\ |\ (C\odot C)\ |\ (Q.C)\ |\ ({\leqslant}ns.C)\ |\
({\geqslant}ns.C)$

where $A\in\mathsf{N_{C}}$, $\odot\in\\{\sqcup,\sqcap\\}$, $Q\in\\{\exists
r,\forall r\ |\ r\in\mathbf{R}\\}$, $s$ is a simple role, and
$n\in\mathbb{N}$. We use the symbols $C$, $D$, $\ldots$ (potentially
annotated) to denote complex concepts. We define $\top=A\sqcup\neg A$ and
$\bot=A\sqcap\neg A$ for a fixed $A\in\mathsf{N_{C}}$, and define a _literal_
$L$ to be either a concept name or its negation, i.e. $L\in\\{A,\neg A\ |\
A\in\mathsf{N_{C}}\\}$. For a concept name $A$, we define $\dot{\neg}A:=\neg
A$ and $\dot{\neg}\neg A:=A$, and we lift the definition of negation to
complex concepts in the usual way, noting that
$\dot{\neg}({\leqslant}nr.C):=({\geqslant}(n{+}1)r.C)$, and

$\dot{\neg}({\geqslant}nr.C):=\begin{cases}\bot&\text{if $n=0$,}\\\
{\leqslant}(n{-}1)r.C&\text{otherwise.}\end{cases}$

We recursively define the _weight_ of a concept $C$ as follows: (1) $w(L)=1$
with $L\in\\{A,\neg A\ |\ A\in\mathsf{N_{C}}\\}$, (2) $w(C\odot
D)=w(C)+w(D)+1$ with $\odot\in\\{\sqcap,\sqcup\\}$, (3) $w(Q.C)=w(C)+1$ with
$Q\in\\{\exists r,\forall r\ |\ r\in\mathbf{R}\\}$, (4)
$w({\leqslant}ns.C)=w(C)+n+1$, and (5) $w({\geqslant}ns.C)=w(C)+n$.

A _general concept inclusion axiom (GCI)_ is a formula of the form
$C\sqsubseteq D$ such that $C$ and $D$ are complex concepts. A _TBox_
$\mathcal{T}$ is a finite set of GCIs and we make the simplifying assumption
that every GCI in a TBox $\mathcal{T}$ is of the form $\top\sqsubseteq C$. We
define a _$\mathcal{RIQ}$ -ontology_ $\mathcal{O}$ (which we refer to as an
_ontology_ for short) to be the union of an RBox $\mathcal{R}$ and TBox
$\mathcal{T}$, that is, $\mathcal{O}=\mathcal{R}\cup\mathcal{T}$. For a set
$X$ of concepts, GCIs, or RIAs, we let $\mathrm{con}(X)$ denote the set of all
concept names occurring in $X$, and we let $\mathrm{sig}(X)$ denote the set of
all concept names and roles occurring in $X$. Symbols from a vocabulary
$\mathcal{V}$ are interpreted accordingly:

######  Definition 1 (Interpretation).

An _interpretation_ $\mathcal{I}=(\Delta^{\mathcal{I}},{\cdot}^{\mathcal{I}})$
is a pair consisting of a non-empty set $\Delta^{\mathcal{I}}$ called the
_domain_ and a map ${\cdot}^{\mathcal{I}}$ such that

$\bullet$

if $A\in\mathsf{N_{C}}$, then ${A}^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}$
with ${\neg A}^{\mathcal{I}}=\Delta^{\mathcal{I}}\setminus{A}^{\mathcal{I}}$;

$\bullet$

if $r\in\mathsf{N_{R}}$, then
${r}^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$.

We define ${({r}^{-})}^{\mathcal{I}}=\\{(b,a)\ |\
(a,b)\in{r}^{\mathcal{I}}\\}$ and interpret compositions over roles in the
usual way. We lift interpretations to complex concepts accordingly:

$\bullet$

${(C\sqcup D)}^{\mathcal{I}}={C}^{\mathcal{I}}\cup{D}^{\mathcal{I}}$;

$\bullet$

${(C\sqcap D)}^{\mathcal{I}}={C}^{\mathcal{I}}\cap{D}^{\mathcal{I}}$;

$\bullet$

${\exists r.C}^{\mathcal{I}}=\\{a\in\Delta^{\mathcal{I}}\ |\ \exists
b\in\Delta^{\mathcal{I}},(a,b)\in{r}^{\mathcal{I}}\ \&\
b\in{C}^{\mathcal{I}}\\}$;

$\bullet$

${\forall r.C}^{\mathcal{I}}=\\{a\in\Delta^{\mathcal{I}}\ |\ \forall
b\in\Delta^{\mathcal{I}},(a,b)\in{r}^{\mathcal{I}}\Rightarrow
b\in{C}^{\mathcal{I}}\\}$;

$\bullet$

${{\leqslant}ns.C}^{\mathcal{I}}{:=}\\{a{\in}\Delta^{\mathcal{I}}\ :\ |\\{b\
:\ (a,b)\in{s}^{\mathcal{I}}\ \&\ b\in{C}^{\mathcal{I}}\\}|\leq n\\}$;

$\bullet$

${{\geqslant}ns.C}^{\mathcal{I}}{:=}\\{a{\in}\Delta^{\mathcal{I}}\ :\ |\\{b\
:\ (a,b)\in{s}^{\mathcal{I}}\ \&\ b\in{C}^{\mathcal{I}}\\}|\geq n\\}$.

An interpretation _satisfies_ $C\sqsubseteq D$ or $r_{1}\circ\cdots\circ
r_{n}\sqsubseteq s$, written $\mathcal{I}\vDash C\sqsubseteq D$ and
$\mathcal{I}\vDash r_{1}\circ\cdots\circ r_{n}\sqsubseteq s$ iff
${C}^{\mathcal{I}}\subseteq{D}^{\mathcal{I}}$ and ${(r_{1}\circ\cdots\circ
r_{n})}^{\mathcal{I}}\subseteq{s}^{\mathcal{I}}$, respectively. An
interpretation $\mathcal{I}$ is defined to be a _model_ of an ontology
$\mathcal{O}$, written $\mathcal{I}\vDash\mathcal{O}$, iff it satisfies all
GCIs and RIAs in $\mathcal{O}$. We write $\mathcal{O}\vDash C\sqsubseteq D$
iff for every interpretation $\mathcal{I}$, if $\mathcal{I}\vDash\mathcal{O}$,
then $\mathcal{I}\vDash C\sqsubseteq D$, and we write $\mathcal{O}\vDash
C\equiv D$ when $\mathcal{O}\vDash C\sqsubseteq D$ and $\mathcal{O}\vDash
D\sqsubseteq C$.

###  2.2 Definability and Interpolation

The notion of Beth definability, first defined within the context of first-
order logic Beth (1956), takes on a number of distinct formulations within the
context of DLs. In Baader and Nutt (2003); ten Cate et al. (2006), Beth
definability is reinterpreted as the notion of _definitorial completeness_ ,
which has also been named _concept-based Beth definability (CBP)_ ten Cate et
al. (2013). Intuitively, a DL $\mathcal{L}$ has the CBP when the implicit
definability of a concept $C$ under an $\mathcal{L}$-ontology $\mathcal{O}$
using a signature $\Theta=\Xi\cup\mathsf{N_{R}}$ with
$\Xi\subseteq\mathrm{con}(C,\mathcal{O})$ implies its explicit definability
using symbols from $\Theta$. This is distinct from the _projective Beth
definability property (PBDP)_ , which is defined in the same way but relative
to a signature $\Theta\subseteq\mathrm{sig}(C,\mathcal{O})$, or the weaker
_Beth definability property (BDP)_ where the signature $\Theta$ is the set of
all symbols distinct from the concept defined Artale et al. (2023). In this
paper, we focus on the CBP, and leave the investigation of sequent-based
methodologies for establishing other definability properties to future work.
Let us now formally define the CBP.

Let $\mathcal{L}$ be a DL, $C$ be a complex concept in $\mathcal{L}$,
$\mathcal{O}$ an $\mathcal{L}$-ontology, and
$\Theta\subseteq\mathrm{con}(C,\mathcal{O})$.222In this paper, we take a DL
$\mathcal{L}$ to be $\mathcal{RIQ}$ or a fragment thereof. We define $C$ to be
_implicitly concept-definable_ from $\Theta$ under $\mathcal{O}$ iff for any
two models $\mathcal{I}$ and $\mathcal{J}$ of $\mathcal{O}$ such that
$\Delta^{\mathcal{I}}=\Delta^{\mathcal{J}}$ and for each
$P\in\Theta\cup\mathsf{N_{R}}$, $P^{\mathcal{I}}=P^{\mathcal{J}}$, it follows
that $C^{\mathcal{I}}=C^{\mathcal{J}}$. We remark that this notion can be
reformulated as a standard reasoning problem, that is, $C$ is implicitly
concept-definable from $\Theta$ under $\mathcal{O}$ iff

$\mathcal{O}\cup\mathcal{O}_{\Theta}\vDash C\sqsubseteq C_{\Theta}$ (1)

where $\mathcal{O}_{\Theta}$ and $C_{\Theta}$ are obtained from $\mathcal{O}$
and $C$, respectively, by uniformly replacing every concept name
$A\not\in\Theta$ by a fresh concept name. We define $C$ to be _explicitly
concept-definable_ from $\Theta$ under $\mathcal{O}$ iff there exists a
complex concept $D$ (called an _explicit concept-definition_) such that
$\mathcal{O}\vDash C\equiv D$ and $\mathrm{con}(D)\subseteq\Theta$.

######  Definition 2 (Concept-Based Beth Definability).

Let $\mathcal{L}$ be a DL, $C$ be a complex concept in $\mathcal{L}$,
$\mathcal{O}$ be an $\mathcal{L}$-ontology, and
$\Theta\subseteq\mathrm{con}(C,\mathcal{O})$. We say that $\mathcal{L}$ has
the _concept-name Beth definability property (CBP)_ iff if $C$ is implicitly
concept-definable from $\Theta$ under $\mathcal{O}$, then $C$ is explicitly
concept-definable from $\Theta$ under $\mathcal{O}$.

It is typical to establish definability properties by means of an
interpolation theroem (cf. ten Cate et al. (2013); Craig (1957); Jung et al.
(2022)). We therefore define a suitable notion of interpolation that implies
the CBP, which we call _concept interpolation_.

######  Definition 3 (Concept Interpolation Property).

Let $\mathcal{L}$ be a DL, $\mathcal{O}_{1}$ and $\mathcal{O}_{2}$ be
$\mathcal{L}$-ontologies with
$\mathcal{O}=\mathcal{O}_{1}\cup\mathcal{O}_{2}$, and $C$ and $D$ be
$\mathcal{L}$-concepts. We define an $\mathcal{L}$-concept $I$ to be a
_concept interpolant_ for $C\sqsubseteq D$ under $\mathcal{O}$ iff (1)
$\mathrm{con}(I)\subseteq\mathrm{con}(\mathcal{O}_{1},C)\cap\mathrm{con}(\mathcal{O}_{2},D)$,
(2) $\mathcal{O}\vDash C\sqsubseteq I$, and (3) $\mathcal{O}\vDash
I\sqsubseteq D$. A DL $\mathcal{L}$ enjoys the _concept interpolation
property_ if for all $\mathcal{L}$-ontologies $\mathcal{O}_{1}$,
$\mathcal{O}_{2}$ with $\mathcal{O}=\mathcal{O}_{1}\cup\mathcal{O}_{2}$ and
$\mathcal{L}$-concepts $C$, $D$ such that $\mathcal{O}\vDash C\sqsubseteq D$
there exists a concept interpolant for $C\sqsubseteq D$ under $\mathcal{O}$.

######  Lemma 1.

If a DL $\mathcal{L}$ enjoys the concept interpolation property, then it
enjoys the CBP.

###  2.3 $\mathbf{R}$-Systems

We let $\mathbf{R}$ serve as our _alphabet_ with each role serving as a
_character_. The set $\mathbf{R}^{*}$ of _strings over $\mathbf{R}$_ is
defined to be the smallest set satisfying the following conditions: (i)
$\mathbf{R}\cup\\{\varepsilon\\}\subseteq\mathbf{R}^{*}$ with $\varepsilon$
the _empty string_ , and (ii) $\text{If }S\in\mathbf{R}^{*}\text{ and
}r\in\mathbf{R}\text{, then }Sr\in\mathbf{R}^{*}$, where $Sr$ represents the
_concatenation_ of $S$ and $r$. We use $S,R,\ldots$ (potentially annotated) to
denote strings from $\mathbf{R}^{*}$, and we have $S\varepsilon=\varepsilon
S=S$, for the empty string $\varepsilon$. The inverse operation on strings is
defined as: (1) $\mathsf{Inv}(\varepsilon):=\varepsilon$, and (2) $\text{If
}S=r_{1}\cdots r_{n}\text{, then
}\mathsf{Inv}(S):=\mathsf{Inv}(r_{n})\cdots\mathsf{Inv}(r_{1})$.

We now define _$\mathbf{R}$ -systems_, which are special types of _Semi-Thue
systems_ Post (1947), relative to ontologies. These will permit us to derive
strings of roles from a given role and encode the information present in a
given ontology.

######  Definition 4 ($\mathbf{R}$-system).

Let $\mathcal{O}$ be an ontology. We define the _$\mathbf{R}$ -system_
$\mathrm{G}(\mathcal{O})$ to be the smallest set of _production rules_ of the
form $r\longrightarrow S$, where $r\in\mathbf{R}$ and $S\in\mathbf{R}^{*}$,
such that if $r_{1}\circ\cdots\circ r_{n}\sqsubseteq s\in\mathcal{O}$, then

$(s\longrightarrow r_{1}\cdots
r_{n}),(\mathsf{Inv}(s)\longrightarrow\mathsf{Inv}(r_{n})\cdots\mathsf{Inv}(r_{1}))\in\mathrm{G}(\mathcal{O}).$

######  Definition 5 (Derivation, Language).

Let $\mathcal{O}$ be an ontology and $\mathrm{G}(\mathcal{O})$ be its
$\mathbf{R}$-system. We write $S\longrightarrow_{\mathrm{G}(\mathcal{O})}R$
and say that the string $R$ may be derived from the string $S$ in _one-step_
iff there are strings $S^{\prime},R^{\prime}\in\mathbf{R}^{*}$ and
$r\longrightarrow T\in\mathrm{G}(\mathcal{O})$ such that
$S=S^{\prime}rR^{\prime}$ and $R=S^{\prime}TR^{\prime}$. We define the
_derivation relation_ $\longrightarrow^{*}_{\mathrm{G}(\mathcal{O})}$ to be
the reflexive and transitive closure of
$\longrightarrow_{\mathrm{G}(\mathcal{O})}$. For $S,R\in\mathbf{R}^{*}$, we
call $S\longrightarrow^{*}_{\mathrm{G}(\mathcal{O})}R$ a _derivation of $R$
from $S$_, and define the _length_ of a derivation to be the minimal number of
one-step derivations required to derive $R$ from $S$ in
$\mathrm{G}(\mathcal{O})$. Last, we define the _language_
$L_{\mathrm{G}(\mathcal{O})}(r):=\\{S\ |\
r\longrightarrow^{*}_{\mathrm{G}(\mathcal{O})}S\\}$, where $r\in\mathbf{R}$.

##  3 Sequent Systems

We let $\mathrm{Lab}=\\{x,y,z,\ldots\\}$ be a countably infinite set of
labels, define a _role atom_ to be an expression of the form $r(x,y)$ with
$r\in\mathbf{R}$ and $x,y\in\mathrm{Lab}$, define an _equality atom_ and
_inequality atom_ to be an expression of the form $x\,\dot{=}\,y$ and
$x\,{\not}{\dot{=}}\,y$ with $x,y\in\mathrm{Lab}$, respectively, and define a
_labeled concept_ to be an expression $x:C$ with $x\in\mathrm{Lab}$ and $C$ a
complex concept. We refer to role, equality, and inequality atoms as
_structural atoms_ more generally. For a (multi)set $X$ and $Y$ of structural
atoms and/or labeled concepts, we let $X,Y$ represent their union and let
$\mathrm{Lab}(X)$ be the set of labels occurring therein. We say that a set
$\Gamma$ of structural atoms _forms a tree_ iff the graph $T(\Gamma)=(V,E)$ is
a directed tree with $V=\mathrm{Lab}(\Gamma)$, and $(x,y)\in E$ iff
$r(x,y)\in\Gamma$. A _sequent_ is defined to be an expression of the form
$S:=\Gamma\vdash\Delta$ such that (1) $\Gamma$ is a set of structural atoms
that forms a tree, (2) $\Delta$ is a multiset of labeled concepts, (3) if
$\Gamma\neq\emptyset$, then
$\mathrm{Lab}(\Delta)\subseteq\mathrm{Lab}(\Gamma)$, and (4) if
$\Gamma=\emptyset$, then $|\mathrm{Lab}(\Delta)|=1$. In a sequent
$\Gamma\vdash\Delta$, we refer to $\Gamma$ as the _antecedent_ , $\Delta$ as
the _consequent_ , and we define $\Delta{\restriction}x:=\\{C\ |\
x:C\in\Delta\\}$.

Recall that every GCI in an ontology $\mathcal{O}$ is assumed to be of the
form $\top\sqsubseteq C$. For an ontology
$\mathcal{O}=\mathcal{R}\cup\mathcal{T}$ and label $x\in\mathrm{Lab}$, we let
$x:\dot{\neg}\mathcal{T}_{\mathcal{O}}=x:\dot{\neg}C_{1},\ldots,x:\dot{\neg}C_{n}$
such that $\mathcal{T}=\\{\top\sqsubseteq C_{1},\ldots,\top\sqsubseteq
C_{n}\\}$. For labels $x_{1},\ldots,x_{n}\in\mathrm{Lab}$, we define
$\Gamma^{\not\dot{=}}(x_{1},\ldots,x_{n})=\\{x_{i}\,{\not}{\dot{=}}\,x_{j}\ |\
1\leq i<j\leq n\\}$. We let $x\approx y\in\\{x\,\dot{=}\,y,y\,\dot{=}\,x\\}$
and write $x=^{*}_{\Gamma}y$ iff there exist
$z_{1},\ldots,z_{n}\in\mathrm{Lab}(\Gamma)$ such that $z_{1}\approx
z_{2},\ldots,z_{n-1}\approx z_{n}$ with $x=z_{1}$ and $y=z_{n}$. We make use
of equivalence classes of labels in the formulation of certain inference rules
below and define $[x]_{\Gamma}:=\\{y\ |\ x=^{*}_{\Gamma}y\\}$ for a sequent
$\Gamma\vdash\Delta$.

$(id)$ $\Gamma\vdash x:A,x:\neg A,\Delta$ |  $\Gamma\vdash x:C,x:D,\Delta$ $(\sqcup)$ $\Gamma\vdash x:C\sqcup D,\Delta$
---|---

$\Gamma\vdash x:C,\Delta$ $\Gamma\vdash x:D,\Delta$ $(\sqcap)$ $\Gamma\vdash x:C\sqcap D,\Delta$ |  $\Gamma,r(x,y)\vdash y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$ $(\forall r)^{{\dagger}_{3}}$ $\Gamma\vdash x:\forall r.C,\Delta$
---|---

$\Gamma^{\prime}\vdash y_{0}:\dot{\neg}C,y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n}:\dot{\neg}C,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$ $({\leqslant}nr)^{{\dagger}_{4}}$ $\Gamma\vdash x:{\leqslant}nr.C,\Delta$ $\Gamma^{\prime}=\Gamma,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),r(x,y_{0}),\ldots,r(x,y_{n})$ |  $\Gamma\vdash y_{i}:C,x:{\geqslant}nr.C,\Delta\ |\ 1\leq i\leq n$ $\Gamma,y_{i}\,\dot{=}\,y_{j}\vdash x:{\geqslant}nr.C,\Delta\ |\ 1\leq i<j\leq n$ $({\geqslant}nr)^{{\dagger}_{5}}$ $\Gamma\vdash x:{\geqslant}nr.C,\Delta$
---|---

Side Conditions:

${\dagger}_{1}=$

‘$x=^{*}_{\Gamma}y$.’

${\dagger}_{2}=$

‘$\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$.’

${\dagger}_{3}=$

‘$y$ is fresh.’

${\dagger}_{4}=$

‘For each $0\leq i\leq n$, $y_{i}$ is fresh.’

${\dagger}_{5}=$

‘For each $1\leq i\leq n$, $\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y_{i}]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$.’

Figure 1: The calculus $\mathsf{S}(\mathcal{O})$ for the
$\mathcal{RIQ}$-ontology $\mathcal{O}$. The rules with side conditions
${\dagger}_{1}$ – ${\dagger}_{5}$ are applicable only if that side condition
holds.

A uniform presentation of our sequent systems in presented in Figure 1. We
note that each sequent calculus $\mathsf{S}(\mathcal{O})$ takes a
$\mathcal{RIQ}$-ontology $\mathcal{O}$ as an input parameter, which determines
the functionality of certain inference rules depending on the contents of
$\mathcal{O}$. The calculus $\mathsf{S}(\mathcal{O})$ contains the _initial
rules_ $(id)$ and $(id_{\dot{=}})$, which generate axioms that are used to
begin a proof, the _logical rules_ $(\sqcup)$, $(\sqcap)$, $(\exists r)$,
$(\forall r)$, $({\leqslant}nr)$, and $({\geqslant}nr)$, which introduce
complex concepts, and the _substitution rule_ $(s_{\dot{=}})$. We note that
$A\in\mathsf{N_{C}}$ in the $(id)$ rule and $L$ is a literal in the
$(s_{\dot{=}})$ rule. The $(id_{\dot{=}})$ and $(s_{\dot{=}})$ rules are
subject to a side condition, namely, each rule is applicable only if
$x=^{*}_{\Gamma}y$. The $(\forall r)$ and $({\leqslant}nr)$ rules are subject
to side conditions as well: the label $y$ and the labels $y_{0},\ldots,y_{n}$
must be _fresh_ in $(\forall r)$ and $({\leqslant}nr)$, respectively, meaning
such labels may not occur in the conclusion of a rule application. Last, we
note that the $(\exists r)$ and $({\geqslant}nr)$ rules are special types of
logical rules, referred to as _propagation rules_ ; cf. Castilho et al.
(1997); Fitting (1972). These rules operate by viewing sequents as types of
automata, referred to as _propagation graphs_ , which bottom-up propagate
formulae along special paths, referred to as _propagation paths_ (see Example
1 below).

######  Definition 6 (Propagation Graph).

We define the _propagation graph_ $\mathrm{PG}(\Gamma)=(V,E)$ of a sequent
$\Gamma\vdash\Delta$ such that $[x]_{\Gamma}\in V$ iff
$x\in\mathrm{Lab}(\Gamma)$, and
$([x]_{\Gamma},r,[y]_{\Gamma}),([y]_{\Gamma},\mathsf{Inv}(r),[x]_{\Gamma})\in
E$ iff there exist $z\in[x]_{\Gamma}$ and $w\in[y]_{\Gamma}$ such that
$r(z,w)\in\Gamma$. If we write $[x]_{\Gamma}\in\mathrm{PG}(\Gamma)$, then we
mean $[x]_{\Gamma}\in V$, and if we write
$([x]_{\Gamma},r,[y]_{\Gamma})\in\mathrm{PG}(\Gamma)$, we mean
$([x]_{\Gamma},r,[y]_{\Gamma})\in E$.

We note that our propagation graphs are generalizations of those employed in
sequent systems for modal and non-classical logics Ciabattoni et al. (2021);
Goré et al. (2011); Lyon (2021). In particular, due to the inclusion of
equality atoms, we must define propagation graphs over equivalence classes of
labels, rather than over labels themselves. This lets us define novel and
correct propagation rules in the presence of (in)equalities and counting
quantifiers.

######  Definition 7 (Propagation Path).

Given a propagation graph $\mathrm{PG}(\Gamma)=(V,E)$,
$[x]_{\Gamma},[y]_{\Gamma}\in V$, and $r\in\mathbf{R}$, we write
$\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ iff $([x]_{\Gamma},r,[y]_{\Gamma})\in E$. Given a string
$rS\in\mathbf{R}^{*}$ where $r\in\mathbf{R}$, we define
$\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{rS}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ as ‘$\exists_{[z]_{\Gamma}\in V}\
\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r}}{\leadsto}$}\hskip
3.0pt[z]_{\Gamma}$ and $\mathrm{PG}(\Gamma)\vDash[z]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{S}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$’, and we take $\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{\varepsilon}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ to mean that $[x]_{\Gamma}=[y]_{\Gamma}$. Additionally,
when $\mathrm{PG}(\Gamma)$ is clear from the context we may simply write
$[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{S}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ to express $\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{S}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$. Finally, given a language $L_{\mathrm{G}(\mathcal{O})}(r)$
of some $\mathbf{R}$-system $\mathrm{G}(\mathcal{O})$ and $r\in\mathbf{R}$, we
use $[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$ iff there is a
string $S\in L_{\mathrm{G}(\mathcal{O})}(r)$ such that $[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{S}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$.

To provide intuition concerning the functionality of propagation rules, we
illustrate a (bottom-up) application of $({\geqslant}nr)$.

######  Example 1.

Let us consider the sequent $\Gamma\vdash x:{\geqslant}2r.C$ with
$\Gamma=r(x,y),r(x,z),r(x,w),z\,\dot{=}\,w$. A pictorial representation of the
propagation graph $\mathrm{PG}(\Gamma)$ is shown below.

$\\{y\\}$$\\{x\\}$$\\{z,w\\}$$r$$\mathsf{Inv}(r)$$r$$\mathsf{Inv}(r)$

One can see that there are two labels $y$ and $z$ such that
$[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ and $[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r}}{\leadsto}$}\hskip
3.0pt[z]_{\Gamma}$. Note that $r\in L_{\mathrm{G}(\mathcal{O})}(r)$ by
definition. Therefore, we may (bottom-up) apply the $({\geqslant}nr)$ rule to
obtain the three premises $\Gamma\vdash x:{\geqslant}2r.C,y:C$, $\Gamma\vdash
x:{\geqslant}2r.C,z:C$, and $\Gamma,y\,\dot{=}\,z\vdash x:{\geqslant}2r.C$.

We define a _proof_ in $\mathsf{S}(\mathcal{O})$ inductively: (1) each
instance of an initial rule $(r)$, as shown below left, is a proof with
conclusion $S$, and (2) if $n$ proofs exist with the respective conclusions
$S_{1}$, $\ldots$, $S_{n}$, then applying an $n$-ary rule $(r^{\prime})$, as
shown below right, yields a new proof with conclusion $S$.

$(r)$ $S$ |  $S_{1}\ \cdots\ S_{n}$ $(r^{\prime})$ $S$
---|---

We use $\pi$ (potentially annotated) to denote proofs, and we say a sequent
$S$ is _provable_ with $\pi$ in $\mathsf{S}(\mathcal{O})$, written
$\mathsf{S}(\mathcal{O}),\pi\Vdash S$ iff $S$ is the conclusion of $\pi$. We
write $\mathsf{S}(\mathcal{O})\Vdash S$ to indicate that $S$ is provable with
some $\pi$ in $\mathsf{S}(\mathcal{O})$. Observe that each proof is a tree of
sequents with the conclusion as the root. We define the _height_ of a proof to
be the number of sequents along a maximal branch from the conclusion to an
initial rule of the proof. The _size_ of a proof $\pi$ is defined to be the
sum of the weights of the sequents it contains; in other words,
$s(\pi):=\sum_{S\in\pi}w(S)$, where the _weight_ of a sequent
$S=\Gamma\vdash\Delta$ is defined to be
$w(S):=|\Gamma|+\sum_{x:C\in\Delta}w(C)$. Ignoring labeled concepts of the
form $x:\dot{\neg}\mathcal{T}_{\mathcal{O}}$, we refer to the formulae that
are explicitly mentioned in the premises of a rule as _active_ , and those
explicitly mentioned in the conclusion as _principal_. For example, $r(x,y)$
and $y:C$ are active in $(\forall r)$ while $x:\forall r.C$ is principal.

$(\top)$ $\Gamma\vdash\Delta,x:\top$ |  $\Gamma\vdash\Delta$ $(w_{\,{\not}{\dot{=}}\,})^{{\dagger}_{2}}$ $\Gamma,x\,{\not}{\dot{=}}\,y\vdash\Delta$
---|---

$\Gamma\vdash\Delta$ $(w)^{{\dagger}_{3}}$ $\Gamma\vdash\Delta,x:C$ |  $\Gamma,x\,{\not}{\dot{=}}\,y,y\,{\not}{\dot{=}}\,x\vdash\Delta$ $(s_{\,{\not}{\dot{=}}\,})$ $\Gamma,x\,{\not}{\dot{=}}\,y\vdash\Delta$
---|---

Figure 2: (Hp-)admissible rules in $\mathsf{S}(\mathcal{O})$. The side
conditions are: ${\dagger}_{1}$ = ‘$x$ is fresh,’ ${\dagger}_{2}$ =
‘$x,y\in\mathrm{Lab}(\Gamma,\Delta)$,’ and ${\dagger}_{3}$ =
‘$x\in\mathrm{Lab}(\Gamma,\Delta)$.’

We now define a semantics for our sequents, which is used to establish our
sequent systems sound and complete.

######  Definition 8 (Sequent Semantics).

Let $\mathcal{I}=(\Delta^{\mathcal{I}},{\cdot}^{\mathcal{I}})$ be an
interpretation, $S=\Gamma\vdash\Delta$ a sequent,
$\lambda:\mathrm{Lab}(\Gamma,\Delta)\to\Delta^{\mathcal{I}}$ a _label
assignment_ , and $\mathcal{O}$ an ontology.

$\bullet$

$\mathcal{I},\lambda\vDash^{\forall}\Gamma$ iff for each
$r(x,y),x\,\dot{=}\,y,x\,{\not}{\dot{=}}\,y\in\Gamma$, we have
$(\lambda(x),\lambda(y))\in{r}^{\mathcal{I}}$, $\lambda(x)=\lambda(y)$, and
$\lambda(x)\neq\lambda(y)$;

$\bullet$

$\mathcal{I},\lambda\vDash^{\exists}\Delta$ iff for some $x:C\in\Delta$,
$\lambda(x)\in{C}^{\mathcal{I}}$.

A sequent $S=\Gamma\vdash\Delta$ is _satisfied_ in $\mathcal{I}$ with
$\lambda$ relative to $\mathcal{O}$, written
$\mathcal{I},\lambda\vDash_{\mathcal{O}}S$, iff if
$\mathcal{I}\vDash\mathcal{O}$ and
$\mathcal{I},\lambda\vDash^{\forall}\Gamma$, then
$\mathcal{I},\lambda\vDash^{\exists}\Delta$. A sequent $S=\Gamma\vdash\Delta$
is _true_ in $\mathcal{I}$ relative to $\mathcal{O}$, written
$\mathcal{I}\vDash_{\mathcal{O}}S$, iff
$\mathcal{I},\lambda\vDash_{\mathcal{O}}S$ for all label assignments
$\lambda$. A sequent $S=\Gamma\vdash\Delta$ is _valid_ relative to
$\mathcal{O}$, written $\vDash_{\mathcal{O}}S$, iff
$\mathcal{I}\vDash_{\mathcal{O}}S$ for all interpretations $\mathcal{I}$, and
we say that $S$ is _invalid_ relative to $\mathcal{O}$ otherwise, writing
$\not\vDash_{\mathcal{O}}S$.

######  Lemma 2.

Let $\mathcal{I}=(\Delta^{\mathcal{I}},{\cdot}^{\mathcal{I}})$ be an
interpretation, $\mathcal{O}$ be a $\mathcal{RIQ}$ ontology, $\lambda$ be a
label assignment, and $\Gamma$ be a set of structural atoms. If
$\mathcal{I}\vDash\mathcal{O}$, $\mathcal{I},\lambda\vDash^{\forall}\Gamma$,
and $\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$, then
$(\lambda(x),\lambda(y))\in{r}^{\mathcal{I}}$.

######  Theorem 1 (Soundness).

If $\mathsf{S}(\mathcal{O})\Vdash\Gamma\vdash\Delta$, then
$\vDash_{\mathcal{O}}\Gamma\vdash\Delta$.

We now confirm that $\mathsf{S}(\mathcal{O})$ enjoys desirable proof-theoretic
properties, viz. certain rules are height-preserving admissible or invertible.
A rule is _(height-preserving) admissible, i.e. (hp-)admissible_ , if the
premises of the rule have proofs (of heights $h_{1},\ldots,h_{n}$), then the
conclusion of the rule has a proof (of height
$h\leq\max\\{h_{1},\ldots,h_{n}\\}$). If we let $(r^{-1})$ be the inverse of
the rule $(r)$ whose premise is the conclusion of $(r)$ and conclusion is the
premises of $(r)$, then we say that $(r)$ is _(height-preserving) invertible,
i.e. (hp-)invertible_ iff $(r^{-1})$ is (hp-)admissible. For a sequent
$S=\Gamma\vdash\Delta$, we let $S(x/y)=\Gamma(x/y)\vdash\Delta(x/y)$ denote
the sequent obtained by substituting each occurrence of the label $y$ in $S$
by $x$; for example, if $S=r(x,y),x\neq y\vdash y:A$, then
$S(z/y)=r(x,z),x\neq z\vdash z:A$. Important (hp-)admissible rules are
displayed in Figure 2.

######  Lemma 3.

The $(\top)$ rule is provable in $\mathsf{S}(\mathcal{O})$, and the
$(\ell^{x}_{y})$, $(w_{\,\dot{=}\,})$, $(w_{\,{\not}{\dot{=}}\,})$, $(w)$,
$(c)$, and $(s_{\,{\not}{\dot{=}}\,})$ rules are hp-admissible.

######  Lemma 4.

All non-initial rules in $\mathsf{S}(\mathcal{O})$ are hp-invertible.

The completeness of $\mathsf{S}(\mathcal{O})$ (stated below) is shown by
taking a sequent of the form $\emptyset\vdash
x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$ as input and showing that if the
sequent is not provable, then $\mathsf{S}(\mathcal{O})$ can be used to
construct a counter-model thereof, witnessing the invalidity of the sequent
relative to $\mathcal{O}$.

######  Theorem 2 (Completeness).

If $\vDash_{\mathcal{O}}\emptyset\vdash x:C$, then
$\mathsf{S}(\mathcal{O})\Vdash\emptyset\vdash
x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$.

The following corollary is a consequence of Theorem 1 and Theorem 2. We write
$\mathsf{S}(\mathcal{O})\Vdash C\sqsubseteq D$ as shorthand for
$\mathsf{S}(\mathcal{O})\Vdash\emptyset\vdash
x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:\dot{\neg}C\sqcup D$.

######  Corollary 1.

$\mathcal{O}\vDash C\sqsubseteq D$ iff $\mathsf{S}(\mathcal{O})\Vdash
C\sqsubseteq D$.

Last, we emphasize the modularity of our sequent systems and approach. By
omitting inference rules for certain connectives and/or only accepting certain
ontologies as the input parameter $\mathcal{O}$, sequent calculi can be
obtained for expressive and lightweight DLs serving as fragments of
$\mathcal{RIQ}$; cf. Baader et al. (2005); Calvanese and De Giacomo (2003).
For example, sequent calculi for $\mathcal{ALC}$ ontologies are easily
obtained by omitting the $(id_{\dot{=}})$, $(s_{\dot{=}})$, $({\geqslant}nr)$,
and $({\leqslant}nr)$ rules. The constructive method presented next applies to
fragments of $\mathcal{RIQ}$ by leveraging this feature, thus demonstrating
its generality.

##  4 Constructive Sequent-Based Method

We now describe our methodology for computing concept interpolants, and by
extension, explicit concept-definitions of implicitly defined concepts (by
Lemma 1). The central idea is to generalize the notion of a concept
interpolant from GCIs to sequents. Then, given a proof of a sequent $S$, we
assign concept interpolants to all initial sequents of the proof, and show how
a concept interpolant can be defined for the conclusion of a rule application
from those of its premises, culminating in a concept interpolant for $S$. As
sequents are more general than GCIs, this approach will establish, in a
constructive manner, that $\mathcal{RIQ}$ (and its various sublogics) enjoy
the concept interpolation property and the CBP.

######  Definition 9 (Interpolant).

We define an _interpolant_ to be a set
$\mathcal{G}:=\\{\Gamma_{i}\vdash\Delta_{i}\ |\ 1\leq i\leq n\\}$ such that
$\Gamma_{i}$ is a set of (in)equalities of the form $x\,\dot{=}\,y$ and
$x\,{\not}{\dot{=}}\,y$ with $x,y\in\mathrm{Lab}$ distinct labels, and
$\Delta_{i}$ is a set of labeled concepts. Given an interpolant $\mathcal{G}$
of the above form, we define its _orthogonal_ $\overline{\mathcal{G}}$ as
follows: $\Gamma\vdash\Delta\in\overline{\mathcal{G}}$ iff for each $1\leq
i\leq|\Gamma,\Delta|$, one and only one of the following holds: (1)
$x\,\dot{=}\,y\in\Gamma$ with $x\,{\not}{\dot{=}}\,y\in\Gamma_{i}$, (2)
$x\,{\not}{\dot{=}}\,y\in\Gamma$ with $x\,\dot{=}\,y\in\Gamma_{i}$, or (3)
$x:\dot{\neg}C\in\Delta$ with $x:C\in\Delta_{i}$. We use $\mathcal{G}$ and
annotated versions for interpolants.

######  Example 2.

Let $\mathcal{G}=\\{(x\,\dot{=}\,y\vdash x:A),(z\,{\not}{\dot{=}}\,u\vdash
z:\neg B)\\}$. Then, the orthogonal $\overline{\mathcal{G}}$ is the set
containing $(x\,{\not}{\dot{=}}\,y,z\,\dot{=}\,u\vdash\ )$,
$(x\,{\not}{\dot{=}}\,y\vdash z\\!:\\!B)$, $(z\,\dot{=}\,u\vdash x\\!:\\!\neg
A)$, and $(\ \vdash x\\!:\\!\neg A,z\\!:\\!B)$, that is, each member of
$\overline{\mathcal{G}}$ is formed by including a negated element from each
member of $\mathcal{G}$.

In order to fully specify our interpolant construction algorithm, we need to
define two special interpolants, named $\forall r.\mathcal{G}$ and
${\leqslant}{n}r.\mathcal{G}$, which appear in quantifier and qualified number
restriction rules. We let $\vv{C}$ denote a set of complex concepts, define
$x:\vv{C}:=\\{x:C\ |\ C\in\vv{C}\\}$, and define $\bigsqcap\vv{C}$,
$\bigsqcup\vv{C}$, and $\dot{\neg}\vv{C}$ to be the conjunction, disjunction,
and negation of all complex concepts in $\vv{C}$, respectively.

######  Definition 10.

Let $\mathcal{G}=\\{\Gamma\vdash\Delta_{i},y:\vv{C}_{i}\ |\ 1\leq i\leq m\\}$
such that $y\not\in\mathrm{Lab}(\Gamma)$ and
$\Delta_{i}{\restriction}y=\emptyset$, then we define:

$\forall r.\mathcal{G}:=\\{\Gamma\vdash\Delta_{i},x:\forall
r.\bigsqcup\vv{C}_{i}\ |\ 1\leq i\leq m\\}.$

Let
$\mathcal{G}=\\{\Gamma,\Gamma^{\prime}\vdash\Delta_{i},y_{0}:\vv{C}_{0,i},\ldots,y_{n}:\vv{C}_{n,i}\
|\ 1\leq i\leq m\\}$ such that
$\mathrm{Lab}(\Gamma)\cap\\{y_{0},\ldots,y_{n}\\}=\emptyset$,
$\Gamma^{\prime}\subseteq\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})$,
$\Delta_{i}{\restriction}y_{j}=\emptyset$ for $0\leq j\leq n$, and
$\vv{C}_{i}=\vv{C}_{0,i},\ldots,\vv{C}_{n,i}$. Then,

${\leqslant}{n}r.\mathcal{G}:=\\{(\Gamma\vdash\Delta_{i},x:{\leqslant}{n}r.\dot{\neg}\bigsqcup\vv{C}_{i})\
|\ 1\leq i\leq m\\}.$

An _interpolation sequent_ is defined to be an expression of the form
$\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ \Sigma\ \|\
\mathcal{G}$ such that $\Gamma$ is a set of role and equality atoms,
$\Phi,\Psi$ is a set of inequality atoms, $\Delta,\Sigma$ is a multiset of
labeled concepts, $\mathcal{G}$ is an interpolant, and $a,b\in\\{1,2\\}$ with
$a\neq b$. For an interpolation sequent of the aforementioned form, we refer
to $\Gamma,\Phi\vdash\Delta$ as the _left partition_ and
$\Gamma,\Psi\vdash\Sigma$ as the _right partition_. Recall that for a concept
interpolant $I$ of a GCI $C\sqsubseteq D$ under $\mathcal{O}$, the ontology
$\mathcal{O}$ is the union of two ontologies $\mathcal{O}_{1}$ and
$\mathcal{O}_{2}$ such that
$\mathrm{con}(I)\subseteq\mathrm{con}(\mathcal{O}_{1},C)\cap\mathrm{con}(\mathcal{O}_{2},D)$
(see Definition 3). The use of $a,b\in\\{1,2\\}$ in an interpolation sequent
is to keep track of which partition is associated with which ontology, e.g. in
$\Gamma;\Phi\ {}^{1}|^{2}\ \Psi\vdash\Delta\ {}^{1}|^{2}\ \Sigma\ \|\
\mathcal{G}$ the left (right) partition is associated with $\mathcal{O}_{1}$
($\mathcal{O}_{2}$, respectively).

$(id^{I}_{1})$ $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta,x:A\ {}^{a}|^{b}\ x:\neg A,\Sigma\ \|\ \\{(\ \vdash x:\neg A)\\}$ |  $(id^{I}_{2})$ $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ x:A,x:\neg A,\Sigma\ \|\ \\{(\ \vdash x:\top)\\}$
---|---

$(id_{\dot{=}}^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\
\Psi,x\,{\not}{\dot{=}}\,y\vdash\Delta\ {}^{a}|^{b}\ \Sigma\ \|\
\\{(x\,{\not}{\dot{=}}\,y\vdash\ )\\}$

$\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ \Sigma\ \|\ \mathcal{G}$ $(O)$ $\Gamma;\Psi\ {}^{b}|^{a}\ \Phi\vdash\Sigma\ {}^{b}|^{a}\ \Delta\ \|\ \overline{\mathcal{G}}$ |  $\Gamma,r(x,y);\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Sigma\ \|\ \mathcal{G}$ $(\forall r^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ x:\forall r.C,\Sigma\ \|\ \forall r.\mathcal{G}$
---|---

$\Gamma,r(x,y_{0}),\ldots,r(x,y_{n});\Phi\ {}^{a}|^{b}\
\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})\vdash\Delta\ {}^{a}|^{b}\
y_{0}:\dot{\neg}C,y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n}:\dot{\neg}C,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Sigma\
\|\ \mathcal{G}$ $({\leqslant}nr^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\
\Psi\vdash\Delta\ {}^{a}|^{b}\ x:{\leqslant}nr.C,\Sigma\ \|\
{\leqslant}{n}r.\mathcal{G}$
---

Figure 3: Rules in $\mathsf{SI}(\mathcal{O})$. The $(id_{\dot{=}}^{I})$,
$(\forall r^{I})$, and $({\leqslant}nr^{I})$ rules satisfy the same side
conditions as $(id_{\dot{=}})$, $(\forall r)$, and $({\leqslant}nr)$,
respectively.

######  Definition 11 (Interpolant Preserving Rules).

Let $(r)$ be a rule in the set $\\{(s_{\dot{=}}),(\sqcup),(\sqcap),(\exists
r),({\geqslant}nr)\\}$ of the form shown below and assume that the active
equalities and/or labeled concepts occur in $\Gamma_{i}$ and/or $\Sigma_{i}$,
respectively, with the principal formula in $\Sigma$.

$\Gamma_{i},\Phi,\Psi\vdash\Delta,\Sigma_{i}\ |\ 1\leq i\leq n$ $(r)$
$\Gamma,\Phi,\Psi\vdash\Delta,\Sigma$

We define its corresponding _interpolant rule_ as follows:

$\Gamma_{i};\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ \Sigma_{i}\ \|\
\mathcal{G}_{i}\ |\ 1\leq i\leq n$ $(r^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\
\Psi\vdash\Delta\ {}^{a}|^{b}\ \Sigma\ \|\
\mathcal{G}_{1}\cup\cdots\cup\mathcal{G}_{n}$

We refer to a rule $(s_{\dot{=}}^{I})$, $(\sqcup^{I})$, $(\sqcap^{I})$,
$(\exists r^{I})$, or $({\geqslant}nr^{I})$ as an _interpolant preserving
rule_ , or _IP-rule_. We stipulate that $(\exists r^{I})$ and
$({\geqslant}nr^{I})$ are subject to the same side conditions as $(\exists r)$
and $({\geqslant}nr)$, respectively, w.r.t. the propagation graph
$\mathrm{PG}(\Gamma)$.

For each sequent calculus $\mathsf{S}(\mathcal{O})$, we define its
corresponding _interpolation calculus_ accordingly:

$\mathsf{SI}(\mathcal{O}):=\\{(id^{I}_{1}),(id^{I}_{2}),(O)\\}\cup\\{(r^{I})\
|\ (r)\in\mathsf{S}(\mathcal{O})\setminus(id)\\}$

Observe that interpolation calculi contain IP-rules as well as rules from
Figure 3. In an interpolation calculus $\mathsf{SI}(\mathcal{O})$, the
$(id^{I}_{1})$, $(id^{I}_{2})$, and $(id_{\dot{=}}^{I})$ rules are the
_initial rules_ , $(O)$ is the _orthogonal rule_ , $(s_{\dot{=}}^{I})$ is the
_substitution rule_ , and all remaining rules are _logical rules_. The
orthogonal rule cuts the number of rules needed in $\mathsf{SI}(\mathcal{O})$
roughly in half as it essentially ‘swaps’ the left and right partition
permitting rules to be defined that only operate within the right partition;
cf. Lyon et al. (2020). A _proof_ , its _height_ , and the provability
relation $\Vdash$ are defined in $\mathsf{SI}(\mathcal{O})$ in the same manner
as for $\mathsf{S}(\mathcal{O})$.

We now put forth a sequence of lemmas culminating in the main interpolation
theorem (Theorem 3), which implies that $\mathcal{RIQ}$ has the CBP (Corollary
2). We remark that Lemmas 5 and 7 describe proof transformation algorithms
between $\mathsf{S}(\mathcal{O})$ and $\mathsf{SI}(\mathcal{O})$. In
particular, Lemma 5 states that each proof in $\mathsf{S}(\mathcal{O})$ of a
sequent $\Gamma,\Phi,\Psi\vdash\Delta,\Sigma$ in a special form can be
transformed into a proof in $\mathsf{SI}(\mathcal{O})$ of a specific
interpolation sequent $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\
{}^{a}|^{b}\ \Sigma\ \|\ \mathcal{G}$. Then, via Lemma 7, this proof can be
transformed into two proofs in $\mathsf{S}(\mathcal{O})$ witnessing that the
interpolant $\mathcal{G}$ is ‘implied by’ the left partition
$\Gamma,\Phi\vdash\Delta$ and ‘implies’ the right partition
$\Gamma,\Psi\vdash\Sigma$. Both Lemmas 5 and 7 are shown by induction on the
height of the given proof. Last, when we use the notation
$\Gamma,\Phi_{a},\Phi_{b}\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta_{a},\Delta_{b},\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}$
or the notation $\Gamma;\Phi_{a}\ {}^{a}|^{b}\
\Phi_{b}\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta_{a}\ {}^{a}|^{b}\
\Delta_{b},\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}\ \|\ \mathcal{G}$, we
assume that
$\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}}:=x_{1}:\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}},\ldots,x_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}}$
such that $\mathrm{Lab}(\Gamma,\Phi_{c},\Delta_{c})=\\{x_{1},\ldots,x_{n}\\}$
and $c\in\\{a,b\\}$. The use of $\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}}$
ensures each partition satisfies its respective ontology.

######  Lemma 5.

Let $\mathcal{O}=\mathcal{O}_{1}\cup\mathcal{O}_{2}$ be an ontology and
suppose that
$\Gamma,\Phi,\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}$
has a proof $\pi$ in $\mathsf{S}(\mathcal{O})$ with $\Phi\cap\Psi=\emptyset$.
Then, $\pi$ can be transformed into a proof in $\mathsf{SI}(\mathcal{O})$ of
$\Gamma;\Phi\ {}^{a}|^{b}\
\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta\ {}^{a}|^{b}\
\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}\ \|\ \mathcal{G}$ such that:

  * (1)

If $x\,\dot{=}\,y$ occurs in $\mathcal{G}$, then
$x\,{\not}{\dot{=}}\,y\in\Phi$;

  * (2)

If $x\,{\not}{\dot{=}}\,y$ occurs in $\mathcal{G}$, then
$x\,{\not}{\dot{=}}\,y\in\Psi$;

  * (3)

$\mathrm{Lab}(\mathcal{G})\subseteq\mathrm{Lab}(\Gamma,\Phi,\Psi,\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}})$;

  * (4)

$\mathrm{con}(\mathcal{G})\subseteq\mathrm{con}(\mathcal{O}_{a},\Delta)\cap\mathrm{con}(\Sigma,\mathcal{O}_{b})$.

The following lemma states that a double orthogonal transformation always
‘preserves’ some of the sequents from the original interpolant. As shown in
the appendix, the lemma is helpful in proving Lemma 7.

######  Lemma 6.

If $(\Sigma\vdash\Pi)\in\overline{\overline{\mathcal{G}}}$, then there exists
a $(\Gamma\vdash\Delta)\in\mathcal{G}$ such that $\Gamma\subseteq\Sigma$ and
$\Delta\subseteq\Pi$.

######  Lemma 7.

If $\mathsf{SI}(\mathcal{O})\Vdash\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\
{}^{a}|^{b}\ \Sigma\ \|\ \mathcal{G}$, then

  * (1)

For each $(\Gamma^{\prime}\vdash\Pi_{i})\in\mathcal{G}$,
$\mathsf{S}(\mathcal{O})\Vdash\Gamma,\Gamma^{\prime},\Phi\vdash\Delta,\Pi_{i}$;

  * (2)

For each $(\Gamma^{\prime}\vdash\Pi_{i})\in\overline{\mathcal{G}}$,
$\mathsf{S}(\mathcal{O})\Vdash\Gamma,\Gamma^{\prime},\Psi\vdash\Pi_{i},\Sigma$.

Next, we prove that an interpolant containing at most a single label, i.e. an
interpolant of the form

$\mathcal{G}:=\\{(\ \vdash x:C_{i,1},\ldots,x:C_{i,k_{i}})\ |\ 1\leq i\leq
n\\}$

can be transformed into a single labeled concept within the context of a
proof. Toward this end, we define
$x:\bigsqcap\bigsqcup\mathcal{G}:=x:\bigsqcap_{1\leq i\leq n}\bigsqcup_{1\leq
j\leq k_{i}}C_{i,j}$, where $\mathcal{G}$ is as above. The following two
lemmas are straightforward and follow by applying the $(\sqcup)$ and
$(\sqcap)$ rules in $\mathsf{S}(\mathcal{O})$ a sufficient number of times.

######  Lemma 8.

If $\Gamma\vdash\Delta,\Sigma$ is provable in $\mathsf{S}(\mathcal{O})$ for
all $(\ \vdash\Sigma)\in\mathcal{G}$ and $\mathrm{Lab}(\mathcal{G})=\\{x\\}$,
then
$\mathsf{S}(\mathcal{O})\Vdash\Gamma\vdash\Delta,x:\bigsqcap\bigsqcup\mathcal{G}$.

######  Lemma 9.

If $\Gamma\vdash\Delta,\Sigma$ is provable in $\mathsf{S}(\mathcal{O})$ for
all $(\ \vdash\Sigma)\in\overline{\mathcal{G}}$ and
$\mathrm{Lab}(\mathcal{G})=\\{x\\}$, then
$\mathsf{S}(\mathcal{O})\Vdash\Gamma\vdash\Delta,x:\dot{\neg}\bigsqcap\bigsqcup\mathcal{G}$.

Our main theorem below is a consequence of Lemmas 4–9. Given a proof of
$\vdash x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:\dot{\neg}C\sqcup D$, we
obtain proofs of $\vdash
x:\dot{\neg}\mathcal{T}_{\mathcal{O}_{1}},x:\dot{\neg}C,x:I$ and $\vdash
x:\dot{\neg}\mathcal{T}_{\mathcal{O}_{2}},x:D,x:\dot{\neg}I$ in
$\mathsf{S}(\mathcal{O})$ by Lemmas 4, 5, and 7–9 with
$I=\bigsqcap\bigsqcup\mathcal{G}$. The concept interpolant $I$ is computed in
$\mathsf{EXPTIME}$ due to the potential use of the $(O)$ rule, which may
exponentially increase the size of interpolants.

######  Theorem 3.

Let $\mathcal{O}=\mathcal{O}_{1}\cup\mathcal{O}_{2}$ be a $\mathcal{RIQ}$
ontology. If $\mathcal{O}\vDash C\sqsubseteq D$, i.e.
$\mathsf{S}(\mathcal{O}),\pi\Vdash C\sqsubseteq D$, then a concept interpolant
$I$ can be computed in $\mathsf{EXPTIME}$ relative to $s(\pi)$ such that
$\mathsf{S}(\mathcal{O})\Vdash C\sqsubseteq I$ and
$\mathsf{S}(\mathcal{O})\Vdash I\sqsubseteq D$, i.e. $\mathcal{O}\vDash
C\sqsubseteq I$ and $\mathcal{O}\vDash I\sqsubseteq D$.

Let $C$ be a complex concept, $\mathcal{O}$ be a $\mathcal{RIQ}$ ontology,
$\Theta\subseteq\mathrm{con}(C,\mathcal{O})$, and suppose $C$ is implicitly
concept-definable from $\Theta$ under $\mathcal{O}$. If we want to find the
explicit concept-definition of $C$ from $\Theta$ under $\mathcal{O}$, we
utilize the sequent calculus $\mathsf{S}(\mathcal{O}^{\prime})$ with
$\mathcal{O}^{\prime}=\mathcal{O}\cup\mathcal{O}_{\Theta}$. Since $C$ is
implicitly concept-definable, we know by (1) in Section 2.2 and Corollary 1
that $\mathsf{S}(\mathcal{O}^{\prime})\Vdash C\sqsubseteq C_{\Theta}$. By
applying Theorem 3, we obtain a concept interpolant $I$ for $C\sqsubseteq
C_{\Theta}$ under $\mathcal{O}$, which serves as an explicit concept-
definition by Lemma 1. Therefore, we have a constructive proof of the
following corollary.

######  Corollary 2.

$\mathcal{RIQ}$ has the concept interpolation property and the CBP.

##  5 Concluding Remarks

We have provided novel sequent calculi for $\mathcal{RIQ}$ ontologies, showing
them sound and complete, as well as showing that each calculus enjoys useful
hp-admissibility and hp-invertibility properties. Our sequent systems are
modular as the omission of certain rules or constructs from ontologies yields
sequent systems for restrictions of $\mathcal{RIQ}$. Moreover, we presented a
sequent-based methodology for computing concept interpolants and explicit
definitions of implicitly definable concepts using $\mathcal{RIQ}$ as a case
study, thus satisfying a demand for developing constructive interpolation and
definability methods. To the best of our knowledge, we have provided the first
proof of the CBP for $\mathcal{RIQ}$.

There are various avenues of future research. First, it would be interesting
to know the size and complexity of computing a concept interpolant $I$
relative to $C\sqsubseteq D$ rather than from a proof $\pi$ witnessing
$\mathcal{O}\vDash C\sqsubseteq D$. This can be achieved by supplying a proof-
search algorithm that generates a proof of $C\sqsubseteq D$, whose relative
complexity and size can then be determined. Second, we aim to generalize our
methodology to decide and compute the existence of _Craig interpolants_ for
$\mathcal{RIQ}$ and related DLs, which is a non-trivial problem (see ten Cate
et al. (2013)). Last, we could generalize our method to consider constructs
beyond those in $\mathcal{RIQ}$, e.g. negations over roles, intersections of
roles, nominals, or the @ operator; it is known that for some of these
extensions, e.g. nominals, even concept interpolation fails Artale et al.
(2023), requiring an increase in complexity to decide the existence of
interpolants.

## Acknowledgments

Tim S. Lyon is supported by the European Research Council (ERC) Consolidator
Grant 771779 (DeciGUT). Jonas Karge is supported by BMBF (Federal Ministry of
Education and Research) in DAAD project 57616814 (SECAI, School of Embedded
Composite AI) as well as by BMBF in the Center for Scalable Data Analytics and
Artificial Intelligence (ScaDS.AI).

## References

  * Areces et al. [2008] Carlos Areces, Alexander Koller, and Kristina Striegnitz.  Referring expressions as formulas of description logic.  In Proceedings of the Fifth International Natural Language Generation Conference, INLG’08, page 42–49, USA, 2008. Association for Computational Linguistics.
  * Artale et al. [2021] Alessandro Artale, Andrea Mazzullo, Ana Ozaki, and Frank Wolter.  On free description logics with definite descriptions.  In Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem, editors, Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021, pages 63–73, 2021.
  * Artale et al. [2023] Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter.  Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions.  ACM Transactions on Computational Logic, 24(4):1–51, 2023.
  * Baader and Nutt [2003] Franz Baader and Werner Nutt.  Basic Description Logics, page 43–95.  Cambridge University Press, USA, 2003.
  * Baader et al. [2005] Franz Baader, Sebastian Brandt, and Carsten Lutz.  Pushing the EL envelope.  In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pages 364–369. Professional Book Center, 2005.
  * Beth [1956] Evert Willem Beth.  On padoa’s method in the theory of definition.  Journal of Symbolic Logic, 21(2):194–195, 1956.
  * Borgida et al. [2016] Alexander Borgida, David Toman, and Grant E. Weddell.  On referring expressions in query answering over first order knowledge bases.  In Chitta Baral, James P. Delgrande, and Frank Wolter, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, pages 319–328. AAAI Press, 2016\.
  * Calvanese and De Giacomo [2003] Diego Calvanese and Giuseppe De Giacomo.  Expressive Description Logics, page 178–218.  Cambridge University Press, USA, 2003.
  * Castilho et al. [1997] Marcos A Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig.  Modal tableaux with propagation rules and structural rules.  Fundamenta Informaticae, 32(3, 4):281–297, 1997.
  * Ciabattoni et al. [2021] Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake, and Alwen Tiu.  Display to labeled proofs and back again for tense logics.  ACM Trans. Comput. Logic, 22(3), 2021.
  * Craig [1957] William Craig.  Three uses of the herbrand-gentzen theorem in relating model theory and proof theory.  The Journal of Symbolic Logic, 22(3):269–285, 1957.
  * Donini et al. [1997] Francesco M Donini, Maurizio Lenzerini, Daniele Nardi, and Werner Nutt.  The complexity of concept languages.  Information and Computation, 134(1):1–58, 1997.
  * Donini [2003] Francesco M. Donini.  Complexity of Reasoning, page 96–136.  Cambridge University Press, USA, 2003.
  * Dyckhoff [1992] Roy Dyckhoff.  Contraction-free sequent calculi for intuitionistic logic.  The Journal of Symbolic Logic, 57(3):795–807, 1992.
  * Fitting and Kuznets [2015] Melvin Fitting and Roman Kuznets.  Modal interpolation via nested sequents.  Annals of pure and applied logic, 166(3):274–305, 2015.
  * Fitting [1972] Melvin Fitting.  Tableau methods of proof for modal logics.  Notre Dame Journal of Formal Logic, 13(2):237–247, 1972.
  * Franconi and Kerhet [2019] Enrico Franconi and Volha Kerhet.  Effective query answering with ontologies and dboxes.  In Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, and Frank Wolter, editors, Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, pages 301–328. Springer International Publishing, Cham, 2019.
  * Funk et al. [2019] Maurice Funk, Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, and Frank Wolter.  Learning description logic concepts: When can positive and negative examples be separated?  In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, pages 1682–1688. ijcai.org, 2019.
  * Gentzen [1935a] Gerhard Gentzen.  Untersuchungen über das logische schließen. i.  Mathematische zeitschrift, 39(1):176–210, 1935.
  * Gentzen [1935b] Gerhard Gentzen.  Untersuchungen über das logische schließen. ii.  Mathematische Zeitschrift, 39(1):405–431, 1935.
  * Goré et al. [2011] Rajeev Goré, Linda Postniece, and Alwen Tiu.  On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.  Log. Methods Comput. Sci., 7(2), 2011.
  * Horrocks and Sattler [2004] Ian Horrocks and Ulrike Sattler.  Decidability of shiq with complex role inclusion axioms.  Artificial Intelligence, 160(1-2):79–104, 2004.
  * Jung et al. [2022] Jean Christoph Jung, Andrea Mazzullo, and Frank Wolter.  More on interpolants and explicit definitions for description logics with nominals and/or role inclusions.  Proceedings of DL2022, 2022.
  * Kuznets and Lellmann [2018] Roman Kuznets and Björn Lellmann.  Interpolation for intermediate logics via hyper- and linear nested sequents.  In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic, Proceedings, pages 473–492. College Publications, 2018.
  * Lyon et al. [2020] Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston.  Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents.  In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, volume 152 of LIPIcs, pages 28:1–28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * Lyon [2021] Tim S. Lyon.  Nested sequents for intuitionistic modal logics via structural refinement.  In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 409–427, Cham, 2021. Springer International Publishing.
  * Maehara [1960] Shoji Maehara.  On the interpolation theorem of craig.  Sûgaku, 12(4):235–237, 1960.
  * Post [1947] Emil L Post.  Recursive unsolvability of a problem of thue.  The Journal of Symbolic Logic, 12(1):1–11, 1947.
  * Seylan et al. [2009] Inanç Seylan, Enrico Franconi, and Jos de Bruijn.  Effective query rewriting with ontologies over dboxes.  In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pages 923–925, 2009.
  * Slaney [1997] John K. Slaney.  Minlog: A minimal logic theorem prover.  In William McCune, editor, Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Proceedings, volume 1249 of Lecture Notes in Computer Science, pages 268–271. Springer, 1997.
  * ten Cate et al. [2006] Balder ten Cate, Willem Conradie, Maarten Marx, and Yde Venema.  Definitorially complete description logics.  In Patrick Doherty, John Mylopoulos, and Christopher A. Welty, editors, Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, pages 79–89. AAAI Press, 2006.
  * ten Cate et al. [2013] Balder ten Cate, Enrico Franconi, and Inanç Seylan.  Beth definability in expressive description logics.  Journal of Artificial Intelligence Research, 48:347–414, 2013.
  * Toman and Weddell [2022] David Toman and Grant E. Weddell.  First order rewritability in ontology-mediated querying in horn description logics.  In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022, pages 5897–5905. AAAI Press, 2022.

##  Appendix A Proofs for Section 2

######  Lemma 1.

If a DL $\mathcal{L}$ enjoys the concept interpolation property, then it
enjoys the CBP.

###### Proof.

Let $\mathcal{O}$ be an $\mathcal{L}$-ontology, $C$ be an
$\mathcal{L}$-concept, and $\Theta\subseteq\mathrm{con}(C,\mathcal{O})$.
Suppose $\mathcal{L}$ enjoys the concept interpolation property and let $C$ be
implicitly concept-definable from $\Theta$ under $\mathcal{O}$, that is,
$\mathcal{O}\cup\mathcal{O}_{\Theta}\vDash C\sqsubseteq C_{\Theta}$ (see (1)
on p. 1). Then, a concept interpolant $I$ exists such that (i)
$\mathrm{con}(I)\subseteq\mathrm{con}(\mathcal{O},C)\cap\mathrm{con}(\mathcal{O}_{\Theta},C_{\Theta})$,
(ii) $\mathcal{O}\cup\mathcal{O}_{\Theta}\vDash C\sqsubseteq I$, and (iii)
$\mathcal{O}\cup\mathcal{O}_{\Theta}\vDash I\sqsubseteq D$. By (i) and the
definitions of $\mathcal{O}_{\Theta}$ and $C_{\Theta}$, we have that
$\mathrm{con}(I)\subseteq\Theta$. We now establish that $\mathcal{O}\vDash
C\equiv I$. We argue that $\mathcal{O}\vDash C\sqsubseteq I$, and note that
the argument showing $\mathcal{O}\vDash I\sqsubseteq C$ is similar.

Suppose $\mathcal{I}\vDash\mathcal{O}$. We aim to show that $\mathcal{I}\vDash
C\sqsubseteq I$. First, recall that each concept name
$B\in\mathrm{con}(C,\mathcal{O})$ such that $B\not\in\Theta$ is replaced by a
fresh concept name in $C_{\Theta}$ and $\mathcal{O}_{\Theta}$, which we denote
by $B^{\prime}$. Now, let us define
$\mathcal{J}=(\Delta^{\mathcal{J}},\cdot^{\mathcal{J}})$ such that
$\Delta^{\mathcal{J}}:=\Delta^{\mathcal{I}}$, for each
$B\in\mathrm{con}(C,\mathcal{O})$ such that $B\not\in\Theta$,
$(B^{\prime})^{\mathcal{J}}:={B}^{\mathcal{I}}$, and for all other symbols
$P$, let $P^{\mathcal{J}}:={P}^{\mathcal{I}}$. Observe that
$\mathcal{J}\vDash\mathcal{O}\cup\mathcal{O}_{\Theta}$, meaning
$\mathcal{J}\vDash C\sqsubseteq I$ by (ii) above. Furthermore, observe that
for $P\in\mathrm{con}(C,\mathcal{O})\cup\mathsf{N_{R}}$,
$P^{\mathcal{J}}={P}^{\mathcal{I}}$, meaning $\mathcal{I}\vDash C\sqsubseteq
I$ as $C$ and $I$ are only composed of symbols from
$\mathrm{con}(C,\mathcal{O})\cup\mathsf{N_{R}}$. It can be argued in a similar
fashion that $\mathcal{O}\vDash I\sqsubseteq C$, meaning, $\mathcal{O}\vDash
C\equiv I$.

Therefore, $I$ serves as an explicit concept-definition of $C$, showing that
$C$ is explicitly concept-definable from $\Theta$ under $\mathcal{O}$, that
is, $\mathcal{L}$ has the CBP. ∎

##  Appendix B Proofs for Section 3

######  Lemma 2.

Let $\mathcal{I}=(\Delta^{\mathcal{I}},{\cdot}^{\mathcal{I}})$ be an
interpretation, $\mathcal{O}$ be a $\mathcal{RIQ}$ ontology, $\lambda$ be a
label assignment, and $\Gamma$ be a set of structural atoms. If
$\mathcal{I}\vDash\mathcal{O}$, $\mathcal{I},\lambda\vDash^{\forall}\Gamma$,
and $\mathrm{PG}(\Gamma)\vDash[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$, then
$(\lambda(x),\lambda(y))\in{r}^{\mathcal{I}}$.

###### Proof.

Suppose $\mathcal{I}\vDash\mathcal{O}$,
$\mathcal{I},\lambda\vDash^{\forall}\Gamma$, and $[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$. We prove the claim
by induction on the length of the derivation of the string $S\in L$ such that
$[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{S}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$.

Base Case. For the base case, we suppose that the derivation of $S$ is of
length $0$. By Definition 5, we know that the only derivation in
$\mathrm{G}(\mathcal{O})$ from $r$ of length $0$ is the derivation of the form
$r$, that is, the derivation consisting solely of $r$. Therefore,
$[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$, which implies that either $r(z,w)\in\Gamma$ or
$\mathsf{Inv}(r)(w,z)\in\Gamma$ for $z\in[x]_{\Gamma}$ and $w\in[y]_{\Gamma}$
by Definition 6. In either case, since
$\mathcal{I},\lambda\vDash^{\forall}\Gamma$, we have that
$(\lambda(x),\lambda(y))\in{r}^{\mathcal{I}}$.

Inductive Step. Let the derivation of $S$ be of length $n+1$. By Definition 5,
there is a derivation $r\longrightarrow^{*}_{\mathrm{G}(\mathcal{O})}RsT$ of
length $n$ and production rule $s\longrightarrow s_{1}\cdots
s_{m}\in\mathrm{G}(\mathcal{O})$ such that $S=Rs_{1}\cdots s_{m}T$. As $S$ is
a string encoding a propagation path in $\mathrm{PG}(\Gamma)$, it follows that
$[z_{1}]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{s_{1}}}{\leadsto}$}\hskip
3.0pt[z_{2}]_{\Gamma}\cdots[z_{m}]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{s_{m}}}{\leadsto}$}\hskip
3.0pt[z_{m+1}]_{\Gamma}$ occurs in $\mathrm{PG}(\Gamma)$. By Definition 6,
$\hat{s}_{1}(z_{1}^{\prime},z_{2}^{\prime}),\ldots,\hat{s}_{m}(z_{m}^{\prime},z_{m+1}^{\prime})\in\Gamma$
with $z_{i}^{\prime}\in[z_{i}]_{\Gamma}$ and

$\hat{s}_{i+1}(z_{i}^{\prime},z_{i+1}^{\prime})\in\\{s_{i+1}(z_{i}^{\prime},z_{i+1}^{\prime}),\mathsf{Inv}(s_{i+1})(z_{i+1}^{\prime},z_{i}^{\prime})\\}$

for $1\leq i\leq m$. This implies that
$(\lambda(z_{1}),\lambda(z_{m+1}))\in{(s_{1}\circ\cdots\circ
s_{m})}^{\mathcal{I}}$ because $\mathcal{I},\lambda\vDash^{\forall}\Gamma$.
Furthermore, since $s\longrightarrow s_{1}\cdots
s_{m}\in\mathrm{G}(\mathcal{O})$, either $s_{1}\circ\cdots\circ
s_{m}\sqsubseteq s\in\mathcal{O}$ or
$\mathsf{Inv}(s_{m})\circ\cdots\circ\mathsf{Inv}(s_{1})\sqsubseteq\mathsf{Inv}(s)\in\mathcal{O}$,
by Definition 4. Regardless of the case,
$(\lambda(z_{1}),\lambda(z_{m+1}))\in{s}^{\mathcal{I}}$. We will use this fact
to complete the proof of the inductive step below.

Let us consider the set
$\Gamma^{\prime}=\Gamma,s(z_{1}^{\prime},z_{m+1}^{\prime})$ of relational
atoms. We know that $\mathcal{I},\lambda\vDash^{\forall}\Gamma^{\prime}$
because $\mathcal{I}^{\prime},\lambda\vDash^{\forall}\Gamma$ by assumption and
$(\lambda(z_{0}),\lambda(z_{m+1}))\in{s}^{\mathcal{I}}$ by what was argued
above. Moreover, we have that
$\mathrm{PG}(\Gamma^{\prime})\vDash[x]_{\Gamma^{\prime}}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{R}}{\leadsto}$}\hskip
3.0pt[z_{1}]_{\Gamma^{\prime}}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{s}}{\leadsto}$}\hskip
3.0pt[z_{m+1}]_{\Gamma^{\prime}}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{T}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma^{\prime}}$. Observe that $RsT$ has a derivation of length $n$
by what was said above. Therefore, we may invoke the induction hypothesis,
from which it follows that $(\lambda(x),\lambda(y))\in{r}^{\mathcal{I}}$. ∎

######  Theorem 1 (Soundness).

If $\mathsf{S}(\mathcal{O})\Vdash\Gamma\vdash\Delta$, then
$\vDash_{\mathcal{O}}\Gamma\vdash\Delta$.

###### Proof.

By induction on the height of the proof of $\Gamma\vdash\Delta$.

Base Case. If the height of the proof is $1$, then our proof is an instance of
$(id)$ or $(id_{\dot{=}})$, as shown below.

$(id)$ $\Gamma\vdash x:A,x:\neg A,\Delta$ |  $(id_{\dot{=}})$ $\Gamma,x\,{\not}{\dot{=}}\,y\vdash\Delta$
---|---

We argue the $(id)$ case first, and assume for a contradiction that
$\Gamma\vdash x:A,x:\neg A,\Delta$ is invalid relative to $\mathcal{O}$. From
this, it follows that there exists an interpretation $\mathcal{I}$ and a label
assignment $\lambda$ such that $\mathcal{I},\lambda\vDash^{\forall}\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:A,x:\neg A,\Delta$. Hence,
$\lambda(x)\notin A^{\mathcal{I}}$ and $\lambda(x)\in A^{\mathcal{I}}$, which
is a contradiction. For the $(id_{\dot{=}})$ case, we assume for a
contradiction that $\Gamma,x\,{\not}{\dot{=}}\,y\vdash\Delta$ is invalid
relative to $\mathcal{O}$. Then, there exists an interpretation $\mathcal{I}$
and label assignment $\lambda$ such that
$\mathcal{I},\lambda\vDash^{\forall}\Gamma,x\,{\not}{\dot{=}}\,y$ and
$\mathcal{I},\lambda\not\vDash^{\exists}\Delta$. By the side condition
$x=^{*}_{\Gamma}y$, we have that $\lambda(x)=\lambda(y)$. However, we also
have that $\lambda(x)\neq\lambda(y)$, which is a contradiction.

Inductive Step. Assume soundness holds for proofs of height $n$. We now show
that it holds for proofs of height $n+1$. We prove each case by contraposition
and argue that if the conclusion of the last inference of the proof is invalid
relative to $\mathcal{O}$, then at least one premise of the inference must be
invalid relative to $\mathcal{O}$.

The $(s_{\dot{=}})$ rule:

$\Gamma\vdash x:L,y:L,\Delta$ $(s_{\dot{=}})$ $\Gamma\vdash x:L,\Delta$

Suppose there exists an interpretation $\mathcal{I}$ and label assignment
$\lambda$ such that $\mathcal{I},\lambda\vDash^{\forall}\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:L,\Delta$. By the side condition
$x=^{*}_{\Gamma}y$ imposed on $(s_{\dot{=}})$, we know that
$\lambda(x)=\lambda(y)$. Since we have that
$\lambda(x)\not\in{L}^{\mathcal{I}}$, it follows that
$\lambda(y)\not\in{L}^{\mathcal{I}}$, which shows the premise invalid relative
to $\mathcal{O}$.

The $(\sqcup)$ rule:

$\Gamma\vdash x:C,x:D,\Delta$ $(\sqcup)$ $\Gamma\vdash x:C\sqcup D,\Delta$
---

Assume $\Gamma\vdash x:C\sqcup D,\Delta$ is invalid relative to $\mathcal{O}$.
By Definition 8, it follows that there exists an interpretation $\mathcal{I}$
and a label assignment $\lambda$ such that
$\mathcal{I},\lambda\vDash^{\forall}\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:C\sqcup D,\Delta$. Hence,
$\lambda(x)\notin{C}^{\mathcal{I}}$ and $\lambda(x)\notin{D}^{\mathcal{I}}$.
Moreover, it holds that $\mathcal{I},\lambda\not\vDash^{\exists}\Delta$. Since
$\mathcal{I},\lambda\vDash\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:C,x:D,\Delta$, the premise is
invalid relative to $\mathcal{O}$ as well.

The $(\sqcap)$ rule:

$\Gamma\vdash x:C,\Delta$ $\Gamma\vdash x:D,\Delta$ $(\sqcap)$ $\Gamma\vdash
x:C\sqcap D,\Delta$
---

Assume $\Gamma\vdash x:C\sqcap D,\Delta$ is invalid relative to $\mathcal{O}$.
By Definition 8, it follows that there exists an interpretation $\mathcal{I}$
and a label assignment $\lambda$ such that
$\mathcal{I},\lambda\vDash^{\forall}\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:C\sqcap D,\Delta$. Either
$\lambda(x)\notin{C}^{\mathcal{I}}$ or $\lambda(x)\notin{D}^{\mathcal{I}}$.
Also, $\mathcal{I},\lambda\not\vDash^{\exists}\Delta$. Therefore, either
$\mathcal{I},\lambda\not\vDash^{\exists}x:C,\Delta$ or
$\mathcal{I},\lambda\not\vDash^{\exists}x:D,\Delta$, meaning, at least one of
the premises must be invalid relative to $\mathcal{O}$ as well.

The $(\exists r)$ rule:

$\Gamma\vdash x:\exists r.C,y:C,\Delta$ $(\exists r)$ $\Gamma\vdash x:\exists
r.C,\Delta$

Suppose there exists an interpretation $\mathcal{I}$ and label assignment
$\lambda$ such that $\mathcal{I},\lambda\vDash^{\forall}\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:\exists r.C,\Delta$. By the side
condition imposed on $(\exists r)$, we know that $[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$. By Lemma 2, we
know that $(\lambda(x),\lambda(y))\in{r}^{\mathcal{I}}$. As
$\lambda(x)\notin{\exists r.C}^{\mathcal{I}}$, we know that
$\lambda(y)\notin{C}^{\mathcal{I}}$, showing that the premise is invalid
relative to $\mathcal{O}$.

The $(\forall r)$ rule:

$\Gamma,r(x,y)\vdash y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$
$(\forall r)$ $\Gamma\vdash x:\forall r.C,\Delta$

Suppose, $\Gamma\vdash x:\forall r.C,\Delta$ is invalid relative to
$\mathcal{O}$. From this, it follows that there exists an interpretation
$\mathcal{I}$ and a label assignment $\lambda$ such that
$\mathcal{I}\vDash\mathcal{O}$, $\mathcal{I},\lambda\vDash^{\forall}\Gamma$
and $\mathcal{I},\lambda\not\vDash^{\exists}x:\forall r.C,\Delta$. Thus, there
is at least one domain element $a\in\Delta^{\mathcal{I}}$ such that
$(\lambda(x),a)\in{r}^{\mathcal{I}}$ and $a\notin{C}^{\mathcal{I}}$. We now
define a new label assignment $\lambda^{\prime}$ such that
$\lambda^{\prime}(z)=\lambda(z)$ if $z\neq y$ and $\lambda^{\prime}(y)=a$.
Hence, $\mathcal{I},\lambda^{\prime}\vDash^{\forall}\Gamma,r(x,y)$ and
$\lambda^{\prime}(y)\notin{C}^{\mathcal{I}}$. Moreover, let
$y_{i}:\dot{\neg}\mathcal{T}_{\mathcal{O}}=y:\dot{\neg}D_{1},\ldots
y:\dot{\neg}D_{k}$. Since $\top\sqsubseteq D_{j}\in\mathcal{O}$ for $1\leq
j\leq k$, we have that
$\mathcal{I},\lambda^{\prime}\not\vDash^{\exists}y:\dot{\neg}\mathcal{T}_{\mathcal{O}}$
as $\mathcal{I}\vDash\mathcal{O}$. Therefore, the premise is invalid relative
to $\mathcal{O}$.

The $({\leqslant}nr)$ rule, where
$\Gamma^{\prime}=\Gamma,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),r(x,y_{0}),\ldots,r(x,y_{n})$:

$\Gamma^{\prime}\vdash
y_{0}:\dot{\neg}C,y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n}:\dot{\neg}C,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$
$({\leqslant}nr)$ $\Gamma\vdash x:{\leqslant}nr.C,\Delta$

Assume, $\Gamma\vdash x:{\leqslant}nr.C,\Delta$ is invalid relative to
$\mathcal{O}$. From this, it follows that there exists an interpretation
$\mathcal{I}$ and a label assignment $\lambda$ such that
$\mathcal{I}\vDash\mathcal{O}$, $\mathcal{I},\lambda\vDash^{\forall}\Gamma$
and $\mathcal{I},\lambda\not\vDash^{\exists}x:{\leqslant}nr.C,\Delta$. It
follows that $\lambda(x)\in{({\geqslant}(n{+}1)r.C)}^{\mathcal{I}}$. Thus,
there are at least $n+1$ many distinct elements
$a_{0},\ldots,a_{n}\in\Delta^{\mathcal{I}}$ such that
$(\lambda(x),a_{i})\in{r}^{\mathcal{I}}$ and $a_{i}\in{C}^{\mathcal{I}}$. We
now define a new label assignment $\lambda^{\prime}$ such that
$\lambda^{\prime}(z)=\lambda(z)$ if $z\neq y_{i}$ with $0\leq i\leq n$ and
$\lambda^{\prime}(y_{i})=a_{i}$. Hence,
$\mathcal{I},\lambda^{\prime}\vDash^{\forall}\Gamma,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),r(x,y_{0}),\ldots,r(x,y_{n})$
and
$\mathcal{I},\lambda^{\prime}\not\vDash^{\exists}y_{0}:\dot{\neg}C,\ldots,y_{n}:\dot{\neg}C,\Delta$
as $\lambda^{\prime}(y_{i})\in{C}^{\mathcal{I}}$ for each $0\leq i\leq n$.
Moreover, let
$y_{i}:\dot{\neg}\mathcal{T}_{\mathcal{O}}=y_{i}:\dot{\neg}D_{1},\ldots
y_{i}:\dot{\neg}D_{k}$ for $0\leq i\leq n$. Since $\top\sqsubseteq
D_{j}\in\mathcal{O}$ for $1\leq j\leq k$, we have that
$\mathcal{I},\lambda\not\vDash^{\exists}y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}}$
as $\mathcal{I}\vDash\mathcal{O}$. Therefore, the premise is invalid relative
to $\mathcal{O}$.

The $({\geqslant}nr)$ rule:

$\Gamma\vdash y_{i}:C,x:{\geqslant}nr.C,\Delta\ |\ 1\leq i\leq n$
$\Gamma,y_{i}\,\dot{=}\,y_{j}\vdash x:{\geqslant}nr.C,\Delta\ |\ 1\leq i<j\leq
n$ $({\geqslant}nr)$ $\Gamma\vdash x:{\geqslant}nr.C,\Delta$

Assume, $\Gamma\vdash x:{\geqslant}nr.C,\Delta$ is invalid relative to
$\mathcal{O}$. It follows that there exists an interpretation $\mathcal{I}$
and a label assignment $\lambda$ such that
$\mathcal{I},\lambda\vDash^{\forall}\Gamma$ and
$\mathcal{I},\lambda\not\vDash^{\exists}x:{\geqslant}nr.C,\Delta$. We note
that if $n=0$, then $\lambda(x)\notin{({\geqslant}0r.C)}^{\mathcal{I}}$, which
cannot be the case, and hence, we may suppose that $n>0$. Then, we have that
$\lambda(x)\in{({\leqslant}(n{-}1)r.C)}^{\mathcal{I}}$. From the side
condition on $({\geqslant}nr)$, there are labels $y_{1},\ldots,y_{n}$ such
that $[x]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y_{i}]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$, which, by
Lemma 2, implies that $(\lambda(x),\lambda(y_{i}))\in{r}^{\mathcal{I}}$ for
each $1\leq i\leq n$. If $\lambda(y_{i})\neq\lambda(y_{j})$ for each $1\leq
i<j\leq n$, then for some $1\leq i\leq n$, we have that
$\lambda(y_{i})\notin{C}^{\mathcal{I}}$; otherwise, we have
$\lambda(y_{i})=\lambda(y_{j})$ for some $1\leq i<j\leq n$. The former cases
show that at least one premise in the first set is invalid relative to
$\mathcal{O}$ and the latter case shows that at least one premise in the
second set of premises is invalid relative to $\mathcal{O}$. ∎

######  Lemma 3.

The $(\top)$ rule is provable in $\mathsf{S}(\mathcal{O})$, and the
$(\ell^{x}_{y})$, $(w_{\,\dot{=}\,})$, $(w_{\,{\not}{\dot{=}}\,})$, $(w)$,
$(c)$, and $(s_{\,{\not}{\dot{=}}\,})$ rules are hp-admissible.

###### Proof.

Recall that $\top=A\sqcup\neg A$ for some fixed $A\in\mathsf{N_{C}}$. The
proof below shows that $(\top)$ provable in $\mathsf{S}(\mathcal{O})$.

$(id)$ $\Gamma\vdash\Delta,x:A,x:\neg A$ $(\sqcup)$
$\Gamma\vdash\Delta,x:A\sqcup\neg A$

The hp-admissibility of $(\ell^{x}_{y})$ is shown by induction on the height
of the given proof. The base cases are trivial as any application of
$(\ell^{x}_{y})$ to an initial rule yields another instance of the initial
rule. In the inductive step, with the exception of the $(\forall r)$ and
$({\leqslant}nr)$ cases, all cases are resolved by invoking IH and then
applying the rule. In the $(\forall r)$ and $({\leqslant}nr)$ cases, the label
substituted into the sequent may be fresh in the $(\forall r)$ or
$({\leqslant}nr)$ inference, requiring two applications of IH in order for the
case to go through. To demonstrate this, we show how a problematic $(\forall
r)$ case is resolved and note that the $({\leqslant}nr)$ case is similar.
Suppose we have an instance of $(\forall r)$ followed by $(\ell^{y}_{z})$ as
shown below left, where $y$ is fresh in $(\forall r)$. The case is resolved as
shown below right, where $(\ell^{v}_{y})$ is applied in the first IH
application with $v$ fresh due to the side condition of the rule,
$(\ell^{y}_{z})$ is then applied in the second IH application, and last,
$(\forall r)$ is applied.

$\Gamma,r(x,y)\vdash y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$ $(\forall r)$ $\Gamma\vdash x:\forall r.C,\Delta$ $(\ell^{y}_{z})$ $\Gamma(y/z)\vdash x:\forall r.C,\Delta(y/z)$ |  $\Gamma,r(x,y)\vdash y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$ IH $\Gamma,r(x,v)\vdash v:C,v:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$ IH $\Gamma(y/z),r(x,v)\vdash v:C,v:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta(y/z)$ $(\forall r)$ $\Gamma(y/z)\vdash x:\forall r.C,\Delta(y/z)$
---|---

The hp-admissibility of $(w_{\,\dot{=}\,})$, $(w_{\,{\not}{\dot{=}}\,})$, and
$(w)$ are shown by induction on the height of the given proof while making a
case distinction on the last rule applied. The base cases are trivial as any
application of either rule to $(id)$ or $(id_{\dot{=}})$ yields another
instance of the rule, and with the exception of the $({\geqslant}nr)$ case,
every case of the inductive step may be resolved by applying IH followed by
the corresponding rule. The $({\geqslant}nr)$ case is trivial when showing the
hp-admissibility of $(w_{\,{\not}{\dot{=}}\,})$ and $(w)$, however, an
interesting case arises when showing the hp-admissibility of
$(w_{\,\dot{=}\,})$. Suppose we have an application of $({\geqslant}nr)$ as
shown below, which weakens in an equality $y_{i}\,\dot{=}\,y_{j}$ that is
active in the $({\geqslant}nr)$ application. Observe that the desired
conclusion is obtained by taking the proof of the premise
$\Gamma,y_{i}\,\dot{=}\,y_{j}\vdash x:{\geqslant}nr.C,\Delta$. All other cases
where $({\geqslant}nr)$ is followed by an application of $(w_{\,\dot{=}\,})$
are simple or resolved similarly.

$\Gamma\vdash y_{i}:C,x:{\geqslant}nr.C,\Delta\ |\ 1\leq i\leq n$
$\Gamma,y_{i}\,\dot{=}\,y_{j}\vdash x:{\geqslant}nr.C,\Delta\ |\ 1\leq i<j\leq
n$ $({\geqslant}nr)$ $\Gamma\vdash x:{\geqslant}nr.C,\Delta$
$(w_{\,\dot{=}\,})$ $\Gamma,y_{i}\,\dot{=}\,y_{j}\vdash
x:{\geqslant}nr.C,\Delta$

The hp-admissibility of $(c)$ is also shown by induction on the height of the
given proof. We note that the hp-admissibility of $(c)$ relies on the hp-
admissibility of another contraction rule $(c_{r})$, shown below left, which
‘fuses’ two children nodes in a sequent. The hp-admissibility of $(c)$ and
$(c_{r})$ is shown simultaneously by induction on the height of the given
proof, though we focus on the $(c)$ case as the $(c_{r})$ case is similar.
Returning back to the proof that $(c)$ is hp-admissible, we note that the base
cases are trivial since any application of $(c)$ to $(id)$ or $(id_{\dot{=}})$
yields another instance of the rule. In the inductive step, if neither of the
contraction formulae $x:C,x:C$ are principal in the conclusion of a rule
application $(r)$, as shown in the example below right, then the case is
resolved by applying IH (i.e. the $(c)$ rule) and then the rule $(r)$.

$\Gamma,r(x,y),r(x,z)\vdash\Delta$ $(c_{r})$ $\Gamma(y/z),r(x,y)\vdash\Delta(y/z)$ |  $\Gamma^{\prime}\vdash\Delta^{\prime},x:C,x:C$ $(r)$ $\Gamma\vdash\Delta,x:C,x:C$ $(c)$ $\Gamma\vdash\Delta,x:C$
---|---

Therefore, let us suppose that one of the contraction formulae $x:C,x:C$ is
principal. We consider the case where the last rule applied above $(c)$ is the
$(\forall r)$ rule, as shown below left. To resolve the case, we apply the hp-
invertibility of $(\forall r)$, followed by the an application of $(c_{r})$
which applies $(y/z)$, followed by a sufficient number of applications of IH
for $(c)$ to contract all of the displayed formulae in the consequent, and
finally, an application of $(\forall r)$, as shown below right.

$\Gamma,r(x,y)\vdash\Delta,y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:\forall r.C$ $(\forall r)$ $\Gamma\vdash\Delta,x:\forall r.C,x:\forall r.C$ $(c)$ $\Gamma\vdash\Delta,x:\forall r.C$ |  $\Gamma,r(x,y)\vdash\Delta,y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:\forall r.C$ Lem. 4 $\Gamma,r(x,y),r(x,z)\vdash\Delta,y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},z:C,z:\dot{\neg}\mathcal{T}_{\mathcal{O}}$ $(c_{r})$ $\Gamma,r(x,y)\vdash\Delta,y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}}$ IH $\Gamma,r(x,y)\vdash\Delta,y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}}$ $(\forall r)$ $\Gamma\vdash\Delta,x:\forall r.C$
---|---

The remaining cases are solved in a similar fashion. Also, note that the proof
of Lemma 4 does not rely on the hp-admissibility of $(c)$ or $(c_{r})$, and
therefore, the above argument is not circular.

Last, we argue the hp-admissibility of $(s_{\,{\not}{\dot{=}}\,})$ by
induction on the height of the given proof. The only interesting case is the
$(id_{\dot{=}})$ case in the base case; the base case for $(id)$ is trivial,
and the inductive step follows in each case by applying IH followed by the
rule. Suppose we have an instance of $(id_{\dot{=}})$ as shown below left,
where the side condition $x=^{*}_{\Gamma}y$ holds. Since $x=^{*}_{\Gamma}y$
holds iff $y=^{*}_{\Gamma}x$ by definition, we have that the application of
$(id_{\dot{=}})$ shown below right is a valid application of $(id_{\dot{=}})$,
thus showing $(s_{\,{\not}{\dot{=}}\,})$ hp-admissible in this case.

$(id_{\dot{=}})$ $\Gamma,x\,{\not}{\dot{=}}\,y,y\,{\not}{\dot{=}}\,x\vdash\Delta$ $(s_{\,{\not}{\dot{=}}\,})$ $\Gamma,y\,{\not}{\dot{=}}\,x\vdash\Delta$ |  $(id_{\dot{=}})$ $\Gamma,y\,{\not}{\dot{=}}\,x\vdash\Delta$
---|---

The other case when $(s_{\,{\not}{\dot{=}}\,})$ is applied to a non-principal
inequality in $(id_{\dot{=}})$ is trivial. ∎

######  Lemma 4.

All non-initial rules in $\mathsf{S}(\mathcal{O})$ are hp-invertible.

###### Proof.

The hp-invertibility of $(s_{\dot{=}})$, $(\exists r)$, and $({\geqslant}nr)$
follows from the fact that $(w)$ (and $(w_{\,\dot{=}\,})$ in the
$({\geqslant}nr)$ case) are hp-admissible (see Lemma 3 above). The remaining
cases are shown by induction on the height of the given proof. We only
consider the $({\leqslant}nr)$ case since all other cases are analogous.

Base case. Suppose we have instances of $(id)$ and $(id_{\dot{=}})$ as shown
below.

$(id)$ $\Gamma\vdash x:A,x:\neg A,\Delta,z:{\leqslant}nr.C$ $(id_{\dot{=}})$
$\Gamma,x\,{\not}{\dot{=}}\,y\vdash\Delta,z:{\leqslant}nr.C$
---

The instance of $(id)$ shown below top and the instance of $(id_{\dot{=}})$
shown below bottom resolve the base case. Note that we take
$\Gamma^{\prime}=\Gamma,\Gamma^{\not\dot{=}}(w_{0},\ldots,w_{n}),r(z,w_{0}),\ldots,r(z,w_{n})$.

$(id)$ $\Gamma^{\prime}\vdash x:A,x:\neg
A,\Delta,w_{0}:\dot{\neg}C,w_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,w_{n}:\dot{\neg}C,w_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}}$

$(id_{\dot{=}})$
$\Gamma^{\prime},x\,{\not}{\dot{=}}\,y\vdash\Delta,w_{0}:\dot{\neg}C,w_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,w_{n}:\dot{\neg}C,w_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}}$

Inductive Step. We only consider the $(s_{\dot{=}})$ and $({\leqslant}nr)$
cases as the remaining cases are similar.

$(s_{\dot{=}})$. Suppose we have an instance of $(s_{\dot{=}})$ as shown below
left. We can resolve the case as shown below right, where
$\Gamma^{\prime}=\Gamma,\Gamma^{\not\dot{=}}(w_{0},\ldots,w_{n}),r(z,w_{0}),\ldots,r(z,w_{n})$.

$\Gamma\vdash x:L,y:L,\Delta,z:{\leqslant}nr.C$ $(s_{\dot{=}})$ $\Gamma\vdash x:L,\Delta,z:{\leqslant}nr.C$ |  $\Gamma\vdash x:L,y:L,\Delta,z:{\leqslant}nr.C$ IH $\Gamma^{\prime}\vdash x:L,y:L,\Delta,w_{0}:\dot{\neg}C,w_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,w_{n}:\dot{\neg}C,w_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}}$ $(s_{\dot{=}})$ $\Gamma^{\prime}\vdash x:L,\Delta,w_{0}:\dot{\neg}C,w_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,w_{n}:\dot{\neg}C,w_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}}$
---|---

$({\leqslant}nr)$. There are two cases to consider when the last rule applied
is $({\leqslant}nr)$. Either, the principal formula is the formula we want to
invert, or it is not. In the first case, shown below, we simply take the proof
of the premise, where
$\Gamma^{\prime}=\Gamma,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),r(x,y_{0}),\ldots,r(x,y_{n})$.

$\Gamma^{\prime}\vdash
y_{0}:\dot{\neg}C,y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n}:\dot{\neg}C,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Delta$
$({\leqslant}nr)$ $\Gamma\vdash x:{\leqslant}nr.C,\Delta$

In the second case, we simply apply IH and then the $({\leqslant}nr)$ rule to
resolve the case. ∎

######  Theorem 2 (Completeness).

If $\vDash_{\mathcal{O}}\emptyset\vdash x:C$, then
$\mathsf{S}(\mathcal{O})\Vdash\emptyset\vdash
x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$.

###### Proof.

We describe a proof-search algorithm $\mathtt{Prove}$ that takes a sequent
$\vdash x:\dot{\neg}\mathcal{T}_{,}x:C$ as input and attempts to construct a
proof thereof. We assume that $\vdash x:\dot{\neg}\mathcal{T}_{,}x:C$ is not
provable in $\mathsf{S}(\mathcal{O})$ and show how to construct an
interpretation $\mathcal{I}=(\Delta^{\mathcal{I}},{\cdot}^{\mathcal{I}})$ and
define a label assignment $\lambda$ such that
$\mathcal{I},\lambda\not\vDash_{\mathcal{O}}\emptyset\vdash
x:\dot{\neg}\mathcal{T}_{,}x:C$, meaning $\mathcal{I}\vDash\mathcal{O}$ and
$\lambda(x)\not\in{C}^{\mathcal{I}}$, that is,
$\not\vDash_{\mathcal{O}}\emptyset\vdash x:C$. Let us now begin our
description of $\mathtt{Prove}$.

$\mathtt{Prove}$. We take $\vdash x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$
as input and move to the step below.

$(id)$ and $(id_{\dot{=}})$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be
all branches of the pseudo-proof $\pi$ currently under construction. Let
$S_{1},\ldots,S_{n}$ be the top sequents of each branch, respectively. For
each $1\leq i\leq n$, if $S_{i}$ is an instance of $(id)$ or $(id_{\dot{=}})$,
then apply $(id)$ and $(id_{\dot{=}})$, respectively, bottom-up on
$\mathcal{B}_{i}$ and close that branch, i.e. halt $\mathtt{Prove}$ on the
branch $\mathcal{B}_{i}$. If $\mathtt{Prove}$ has halted on every branch, then
return $\mathtt{True}$. Otherwise, if a sequent $S_{i}$ exists such that no
rule from $\mathsf{S}(\mathcal{O})$ is bottom-up applicable to it, copy it
above itself and continue to step $(s_{\dot{=}})$ below.

$(s_{\dot{=}})$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all branches
of the pseudo-proof $\pi$ currently under construction. Let
$S_{1},\ldots,S_{n}$ be the top sequents of each branch, respectively. We
consider each branch and its top sequent in turn. Let us suppose we have
already considered $\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that
$\mathcal{B}_{i+1}$ is currently under consideration. Let the top sequent
$S_{i+1}$ be of the form:

$\Gamma\vdash\Delta,x_{1}:L_{1},\ldots,x_{k}:L_{k}$

with all labeled literals displayed. For each $1\leq i\leq k$ and each
$y\in\mathrm{Lab}(\Gamma)$ such that $x_{i}=^{*}_{\Gamma}y$, repeatedly apply
the $(s_{\dot{=}})$ rule bottom-up, extending $\mathcal{B}_{i+1}$. After all
branches have been processed in this way, we move onto the $(\sqcup)$ case
below.

$(\sqcup)$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all branches of
the pseudo-proof $\pi$ currently under construction. Let $S_{1},\ldots,S_{n}$
be the top sequents of each branch, respectively. We consider each branch and
its top sequent in turn. Let us suppose we have already considered
$\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that $\mathcal{B}_{i+1}$ is
currently under consideration. Let the top sequent $S_{i+1}$ be of the form:

$\Gamma\vdash x_{1}:C_{1}\sqcup D_{1},\ldots,x_{k}:C_{k}\sqcup D_{k},\Delta$

with all disjunctive formulae displayed. We repeatedly apply the $(\sqcup)$
rule bottom-up, extending $\mathcal{B}_{i+1}$ so that it now has a top sequent
of the form:

$\Gamma\vdash x_{1}:C_{1},x_{1}:D_{1},\ldots,x_{k}:C_{k},x_{k}:D_{k},\Delta$

After all branches have been processed in this way, we move onto the
$(\sqcap)$ case below.

$(\sqcap)$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all branches of
the pseudo-proof $\pi$ currently under construction. Let $S_{1},\ldots,S_{n}$
be the top sequents of each branch, respectively. We consider each branch and
its top sequent in turn. Let us suppose we have already considered
$\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that $\mathcal{B}_{i+1}$ is
currently under consideration. Let the top sequent $S_{i+1}$ be of the form:

$\Gamma\vdash x_{1}:C_{1}\sqcap D_{1},\ldots,x_{k}:C_{k}\sqcap D_{k},\Delta$

with all conjunctive formulae displayed. We repeatedly apply the $(\sqcap)$
rule bottom-up, extending $\mathcal{B}_{i+1}$ with $2^{k}$ new branches with
each having a top sequent of the form:

$\Gamma\vdash x_{1}:E_{1},\ldots,x_{k}:E_{k},\Delta$

where $E_{j}\in\\{C_{j},D_{j}\\}$ for $1\leq j\leq k$. After all branches have
been processed in this way, we move onto the $(\exists r)$ case below.

$(\exists r)$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all branches of
the pseudo-proof $\pi$ currently under construction. Let $S_{1},\ldots,S_{n}$
be the top sequents of each branch, respectively. We consider each branch and
its top sequent in turn. Let us suppose we have already considered
$\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that $\mathcal{B}_{i+1}$ is
currently under consideration. Let the top sequent $S_{i+1}$ be of the form:

$\Gamma\vdash x_{1}:\exists r_{1}.C_{1},\ldots,x_{k}:\exists
r_{k}.C_{k},\Delta$

with all existential formulae displayed. For each $1\leq j\leq k$ and every
label $y\in\mathrm{Lab}(\Gamma)$ such that $[x_{j}]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r_{j})$, repeatedly
apply the $(\exists r)$ rule bottom-up, extending $\mathcal{B}_{i+1}$. After
all branches have been processed in this way, we move onto the $(\forall r)$
case below.

$(\forall r)$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all branches of
the pseudo-proof $\pi$ currently under construction. Let $S_{1},\ldots,S_{n}$
be the top sequents of each branch, respectively. We consider each branch and
its top sequent in turn. Let us suppose we have already considered
$\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that $\mathcal{B}_{i+1}$ is
currently under consideration. Let the top sequent $S_{i+1}$ be of the form:

$\Gamma\vdash x_{1}:\forall r_{1}.C_{1},\ldots,x_{k}:\forall
r_{k}.C_{k},\Delta$

with all universal formulae displayed. For each $1\leq j\leq k$, repeatedly
apply the $(\forall r)$ rule bottom-up, extending $\mathcal{B}_{i+1}$, and so
the top sequent contains $r_{j}(x_{j},y)$ in the antecedent and
$y:C_{j},y:\dot{\neg}\mathcal{T}_{\mathcal{O}}$ in the consequent, where $y$
is fresh for each $j$. After all branches have been processed in this way, we
move onto the $({\leqslant}nr)$ case below.

$({\leqslant}nr)$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all
branches of the pseudo-proof $\pi$ currently under construction. Let
$S_{1},\ldots,S_{n}$ be the top sequents of each branch, respectively. We
consider each branch and its top sequent in turn. Let us suppose we have
already considered $\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that
$\mathcal{B}_{i+1}$ is currently under consideration. Let the top sequent
$S_{i+1}$ be of the form:

$\Gamma\vdash x_{1}:(\leqslant n_{1}r_{1}.C_{1}),\ldots,x_{k}:(\leqslant
n_{k}r_{k}.C_{k}),\Delta$

with all qualified number restrictions of the form $x_{j}:(\leqslant
n_{j}r_{j}.C_{j})$ displayed and where $1\leq j\leq k$. We repeatedly apply
the $({\leqslant}nr)$ rule bottom-up, extending $\mathcal{B}_{i+1}$ so that
the top sequent contains $\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n_{j}})$ and
$r(x_{j},y_{0}),\ldots,r(x_{j},y_{n_{j}})$ in the antecedent and
$y_{0}:\dot{\neg}C_{j},y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n_{j}}:\dot{\neg}C_{j},y_{n_{j}}:\dot{\neg}\mathcal{T}_{\mathcal{O}}$
in the consequent with $y_{0},\ldots,y_{n_{j}}$ fresh for each considered
qualified number restriction of the above form. After all branches have been
processed in this way, we move onto the $({\geqslant}nr)$ case below.

$({\geqslant}nr)$. Let $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ be all
branches of the pseudo-proof $\pi$ currently under construction. Let
$S_{1},\ldots,S_{n}$ be the top sequents of each branch, respectively. We
consider each branch and its top sequent in turn. Let us suppose we have
already considered $\mathcal{B}_{1},\ldots,\mathcal{B}_{i}$ so that
$\mathcal{B}_{i+1}$ is currently under consideration. Let the top sequent
$S_{i+1}$ be of the form:

$\Gamma\vdash x_{1}:(\geqslant n_{1}r_{1}.C_{1}),\ldots,x_{k}:(\geqslant
n_{k}r_{k}.C_{k}),\Delta$

with all qualified number restrictions of the form $x_{j}:(\geqslant
n_{j}r_{j}.C_{j})$ displayed and where $1\leq j\leq k$. For each collection
$\\{y_{1},\ldots,y_{n_{j}}\\}\subseteq\mathrm{Lab}(S_{i+1})$ of labels such
that $[x_{j}]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[y_{t}]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r_{j})$ and $1\leq
t\leq n_{j}$, we apply the $({\geqslant}nr)$ rule bottom-up, extending
$\mathcal{B}_{i+1}$. After all branches have been processed in this way, we
cycle back to the $(id)$ and $(id_{\dot{=}})$ case.

This concludes the description of $\mathtt{Prove}$.

We know that $\mathtt{Prove}$ cannot return $\mathtt{True}$ since then a proof
of $\vdash x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$ would exist, contrary to
our assumption. Therefore, $\mathtt{Prove}$ will not terminate, meaning that
it constructs an infinite pseudo-proof $\pi$ in the form of an infinite tree.
Since only finite branches occurs within this pseudo-proof, by König’s lemma
we know that an infinite branch of the following form exists in $\pi$:

$\mathcal{B}=(\Gamma_{0}\vdash\Delta_{0}),(\Gamma_{1}\vdash\Delta_{1}),\ldots,(\Gamma_{n}\vdash\Delta_{n}),\ldots$

such that $\Gamma_{0}=\emptyset$ and
$\Delta_{0}=x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$. Let us define
$\Gamma^{*}=\bigcup_{i\in\mathbb{N}}\Gamma_{i}$ and
$\Delta^{*}=\bigcup_{i\in\mathbb{N}}\Delta_{i}$. We use $\mathcal{B}$ to
construct an interpretation
$\mathcal{I}=(\Delta^{\mathcal{I}},{\cdot}^{\mathcal{I}})$ and define a label
assigment $\lambda$ such that $\mathcal{I}\vDash\mathcal{O}$,
$\mathcal{I},\lambda\vDash^{\forall}\Gamma^{*}$, but
$\mathcal{I},\lambda\not\vDash^{\exists}\Delta^{*}$, meaning
$\not\vDash_{\mathcal{O}}\emptyset\vdash x:C$. We define
$\Delta^{\mathcal{I}}=\\{[y]\ |\ y\in\mathrm{Lab}(\mathcal{B})\\}$, where we
use $[y]=[y]_{\Gamma^{*}}$ for simplicity. In other words,
$\Delta^{\mathcal{I}}$ contains all equivalence classes modulo the
$=^{*}_{\Gamma^{*}}$ relation on labels occurring in the sequents of the
branch $\mathcal{B}$. We define $\lambda$ and ${\cdot}^{\mathcal{I}}$
accordingly:

  * •

${y}^{\mathcal{I}}=[y]$ for $y\in\mathrm{Lab}(\mathcal{B})$;

  * •

$[y]\in{A}^{\mathcal{I}}$ iff $y:\neg A\in\Delta^{*}$;

  * •

$([y],[z])\in{r}^{\mathcal{I}}$ iff either (1) there exist $w\in[y]$ and
$u\in[z]$ such that $r(w,u)\in\Gamma^{*}$, or (2) $r_{1}\circ\cdots\circ
r_{n}\sqsubseteq r\in\mathcal{O}$ and
$([x]_{i-1},[x]_{i})\in{r}^{\mathcal{I}}_{i}$ for $1\leq i\leq n$ with
$y\in[x_{0}]$ and $z\in[x_{n}]$.

Based on the definition above and the definition of an $\mathbf{R}$-system
$\mathrm{G}(\mathcal{O})$, we note that if $([y],[z])\in{r}^{\mathcal{I}}$,
then there exist roles $r_{1},\ldots,r_{n}$ and $[z_{1}],\ldots,[z_{n-1}]$
such that

$\mathrm{PG}(\Gamma^{*})\vDash[y]\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r_{1}}}{\leadsto}$}\hskip
3.0pt[z_{1}]\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r_{2}}}{\leadsto}$}\hskip
3.0pt\cdots[z_{n-1}]\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{r_{n}}}{\leadsto}$}\hskip 3.0pt[z]$

and $r_{1}\cdots r_{n}\in L_{\mathrm{G}(\mathcal{O})}(r)$. It is
straightforward to show that $\mathcal{I}$ satisfies all RIAs
$r_{1}\circ\cdots\circ r_{n}\sqsubseteq r$ in $\mathcal{O}$. We now argue that
$\mathcal{I},\lambda\vDash^{\forall}\Gamma^{*}$. If $r(y,z)\in\Gamma^{*}$,
then $([y],[z])\in{r}^{\mathcal{I}}$ holds by the definition above, showing
that $(\lambda(y),\lambda(z))\in{r}^{\mathcal{I}}$. If
$y\,\dot{=}\,z\in\Gamma^{*}$, then by definition $[y]=[z]$, showing
$\lambda(y)=\lambda(z)$. Also, observe that if
$y\,{\not}{\dot{=}}\,z\in\Gamma^{*}$, then it cannot be the case that
$[y]=[z]$ since then the $(id_{\dot{=}})$ rule would be applied in
$\mathcal{B}$, implying that $\mathcal{B}$ is finite, which is a contradiction
as $\mathcal{B}$ is infinite; hence, $\lambda(y)\neq\lambda(z)$. We will now
show that $\mathcal{I},\lambda\not\vDash^{\exists}\Delta^{*}$, and afterward,
we will argue that $\mathcal{I}$ satisfies all GCIs in $\mathcal{O}$, thus
establishing that $\mathcal{I}\vDash\mathcal{O}$. We argue by induction on the
complexity of $D$ that if $y:D\in\Delta^{*}$, then
$\lambda(y)\not\in{D}^{\mathcal{I}}$.

$y:A\in\Delta^{*}.$

If $y:A\in\Delta^{*}$, then for every $z\in[y]$, $z:\neg A\not\in\Delta^{*}$
since otherwise $(s_{\dot{=}})$ would have been applied, eventually followed
by $(id)$ and $\mathcal{B}$ would be finite, contrary to our assumption.
Therefore, $y:\neg A\not\in\Delta^{*}$, implying that
$\lambda(y)\notin{A}^{\mathcal{I}}$ by the definition of $\mathcal{I}$.

$y:\neg A\in\Delta^{*}.$

Then, $\lambda(y)\in{A}^{\mathcal{I}}$, by the definition of $\mathcal{I}$.

$y:E\sqcup F\in\Delta^{*}.$

Then, eventually the $(\sqcup)$ rule will be applied in $\mathtt{Prove}$,
meaning $y:E,y:F\in\Delta^{*}$, showing that $\lambda(y)\in{E}^{\mathcal{I}}$
and $\lambda(y)\in{F}^{\mathcal{I}}$ by IH. Therefore, $\lambda(y)\in{(E\sqcup
F)}^{\mathcal{I}}$.

$y:E\sqcap F\in\Delta^{*}.$

If $y:E\sqcap F\in\Delta$, then eventually the $(\sqcap)$ rule will be applied
in $\mathtt{Prove}$, meaning either $y:E\in\Delta$ or $y:D\in\Delta$. Hence,
either $\lambda(y)\in{E}^{\mathcal{I}}$ or $\lambda(y)\in{F}^{\mathcal{I}}$ by
IH, implying $\lambda(y)\in{(E\sqcap F)}^{\mathcal{I}}$.

$y:\exists r.E\in\Delta^{*}.$

Suppose $(\lambda(y),\lambda(z))\in{r}^{\mathcal{I}}$, i.e.
$([y],[z])\in{r}^{\mathcal{I}}$. It follows that $[y]\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip 3.0pt[z]$
with $L=L_{\mathrm{G}(\mathcal{O})}(r)$, meaning at some step in
$\mathcal{B}$, we have that $[y]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[z]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$. Hence, the
$(\exists r)$ rule will be bottom-up applied, ensuring that
$z:E\in\Delta^{*}$. By IH, we have that $\lambda(z)\notin{E}^{\mathcal{I}}$,
so since $z$ was assumed arbitrary, we have that $\lambda(y)\notin{(\exists
r.E)}^{\mathcal{I}}$.

$y:\forall r.E\in\Delta^{*}.$

If $y:\forall r.E\in\Delta^{*}$, then eventually the $(\forall r)$ rule will
be bottom-up applied in $\mathtt{Prove}$, ensuring that for some label $z$,
$r(y,z)\in\Gamma^{*}$ and $z:E\in\Delta^{*}$. By the definition of
${r}^{\mathcal{I}}$, $([y],[z])\in{r}^{\mathcal{I}}$, and by IH
$\lambda(z)\notin{E}^{\mathcal{I}}$, thus $\lambda(y)\notin{\forall
r.E}^{\mathcal{I}}$.

$y:{\leqslant}nr.E\in\Delta^{*}.$

If $y:{\leqslant}nr.E\in\Delta$, then eventually the $({\leqslant}nr)$ rule
will be applied bottom-up in $\mathtt{Prove}$. It follows that
$\Gamma^{\not\dot{=}}(z_{0},\ldots,z_{n}),r(y,z_{0}),\ldots,r(y,z_{n})\in\Gamma^{*}$
and $y_{0}:\dot{\neg}E,\ldots,y_{n}:\dot{\neg}E\in\Delta^{*}$. Therefore,
there exist at least $n+1$ distinct elements in $\Delta^{\mathcal{I}}$, namely
$[y_{0}],\ldots,[y_{n}]$, such that for $0\leq i\leq n$,
$([y],[z_{i}])\in{r}^{\mathcal{I}}$ and where
$\lambda(z_{i})\notin{E_{i}}^{\mathcal{I}}$ by IH. Hence,
$\lambda(y)\notin{({\leqslant}nr.E)}^{\mathcal{I}}$.

$y:{\geqslant}nr.E\in\Delta^{*}.$

Assume that distinct $[z_{1}],\ldots,[z_{n}]\in\Delta^{\mathcal{I}}$ exist
such that for $1\leq i\leq n$, $([y],[z_{i}])\in{r}^{\mathcal{I}}$. It follows
that for $1\leq i\leq n$, $[y]\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip 3.0pt[z_{i}]$
with $L=L_{\mathrm{G}(\mathcal{O})}(r)$ and $z_{1},\ldots,z_{n}$ pairwise,
distinct labels. Hence, at some step in $\mathcal{B}$, we have that
$[y]_{\Gamma}\hskip
3.0pt\raise-3.0pt\hbox{$\overset{\mathclap{L}}{\leadsto}$}\hskip
3.0pt[z_{i}]_{\Gamma}$ with $L=L_{\mathrm{G}(\mathcal{O})}(r)$, and so, the
$({\geqslant}nr)$ rule will be applied bottom-up, ensuring that
$z_{i}:E\in\Delta^{*}$ for some $1\leq i\leq n$. By IH,
$\lambda(z_{i})\notin{E}^{\mathcal{I}}$. Since the elements
$[z_{1}],\ldots,[z_{n}]\in\Delta^{\mathcal{I}}$ were assumed to be arbitrary
and distinct, this shows that for any $n$ elements that $\lambda(y)$ relates
to via ${r}^{\mathcal{I}}$, at least one must not be an element of
${E}^{\mathcal{I}}$, i.e. $\lambda(y)\notin{({\geqslant}nr.E)}^{\mathcal{I}}$.

Let us now argue that $\mathcal{I}\models\mathcal{O}$ by arguing that all GCIs
in $\mathcal{O}$ are satisfied on $\mathcal{I}$ (note that all RIAs are
satisfied on $\mathcal{I}$ as stated above). Observe that our input is of the
form $\vdash x:\dot{\neg}\mathcal{T}_{\mathcal{O}},x:C$ and every time a fresh
label is added by the $(\forall r)$ or $({\leqslant}nr)$ step of
$\mathtt{Prove}$, the concepts in $\dot{\neg}\mathcal{T}_{\mathcal{O}}$ are
introduced at that label, meaning such concepts will occur at every label in
$\mathrm{Lab}(\Gamma^{*},\Delta^{*})$. Therefore, by the argument above, we
know that for every GCI $\top\sqsubseteq E\in\mathcal{O}$ and
$\lambda(y)=[y]\in\Delta^{\mathcal{I}}$,
$\lambda(y)\notin{\dot{\neg}E}^{\mathcal{I}}$, showing that
$\lambda(y)\in{E}^{\mathcal{I}}$, and hence, every GCI is satisfied on
$\mathcal{I}$. As $x:C\in\Delta^{*}$, all of the above implies that
$\vDash_{\mathcal{O}}\emptyset\vdash x:C$, completing the proof. ∎

##  Appendix C Proofs for Section 4

######  Lemma 5.

Let $\mathcal{O}=\mathcal{O}_{1}\cup\mathcal{O}_{2}$ be an ontology and
suppose that
$\Gamma,\Phi,\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}$
has a proof $\pi$ in $\mathsf{S}(\mathcal{O})$ with $\Phi\cap\Psi=\emptyset$.
Then, $\pi$ can be transformed into a proof in $\mathsf{SI}(\mathcal{O})$ of
$\Gamma;\Phi\ {}^{a}|^{b}\
\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta\ {}^{a}|^{b}\
\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}\ \|\ \mathcal{G}$ such that:

  * (1)

If $x\,\dot{=}\,y$ occurs in $\mathcal{G}$, then
$x\,{\not}{\dot{=}}\,y\in\Phi$ ;

  * (2)

If $x\,{\not}{\dot{=}}\,y$ occurs in $\mathcal{G}$, then
$x\,{\not}{\dot{=}}\,y\in\Psi$;

  * (3)

$\mathrm{Lab}(\mathcal{G})\subseteq\mathrm{Lab}(\Gamma,\Phi,\Psi,\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}})$;

  * (4)

$\mathrm{con}(\mathcal{G})\subseteq\mathrm{con}(\mathcal{O}_{a},\Delta)\cap\mathrm{con}(\Sigma,\mathcal{O}_{b})$.

###### Proof.

By induction on the height of the proof. The base cases are trivial, so we
focus on the inductive step. We argue one of the $({\leqslant}nr)$ cases as
the remaining cases are simple or similar. Suppose we have a proof in
$\mathsf{S}(\mathcal{O})$ ending with an application of $({\leqslant}nr)$, as
shown below, where $\Gamma^{\prime}=\Gamma,r(x,y_{0}),\ldots,r(x,y_{n})$ and
let $c\in\\{a,b\\}$.

$\Gamma^{\prime},\Phi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta,y_{0}:\dot{\neg}C,\ldots,y_{n}:\dot{\neg}C,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}$
$({\leqslant}nr)$
$\Gamma,\Phi,\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}}^{\prime},\Delta,x:{\leqslant}nr.C,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}^{\prime}$

By IH, the premise of the inference shown below has a proof in
$\mathsf{SI}(\mathcal{O})$, where
$\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}}=\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}}^{\prime},y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}},\ldots,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}}$
for $c\in\\{a,b\\}$. Since properties (1) and (2) hold for the premise below,
and $\Phi\cap(\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Psi)=\emptyset$ by
assumption, we know $y_{0},\ldots,y_{n}\not\in\mathrm{Lab}(\Phi,\Psi)$ since
otherwise the side condition of the $({\leqslant}nr)$ application above would
be violated. Hence, $\mathcal{G}$ will be in the form dictated by Definition
10, meaning we obtain a proof of the desired conclusion in
$\mathsf{SI}(\mathcal{O})$ by a single application of $({\leqslant}nr)$, as
shown below.

$\Gamma^{\prime};\Phi\ {}^{a}|^{b}\
\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}},\Delta\
{}^{a}|^{b}\
y_{0}:\dot{\neg}C,\ldots,y_{n}:\dot{\neg}C,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}\
\|\ \mathcal{G}$ $({\leqslant}nr)$ $\Gamma;\Phi\ {}^{a}|^{b}\
\Psi\vdash\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}}^{\prime},\Delta\
{}^{a}|^{b}\
x:{\leqslant}nr.C,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}^{\prime}\ \|\
{\leqslant}{n}r.\mathcal{G}$

$\mathrm{Lab}(\mathcal{G})\subseteq\mathrm{Lab}(\Gamma,\Phi,\Psi,\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}}^{\prime},\Delta,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}^{\prime}){\cup}\\{y_{0},\ldots,y_{n}\\}$
and
$\mathrm{con}(\mathcal{G}){\subseteq}\mathrm{con}(\mathcal{O}_{a},\Delta){\cap}\mathrm{con}(y_{0}{:}\dot{\neg}C_{0},\ldots,y_{n}{:}\dot{\neg}C_{n},\Sigma,\mathcal{O}_{b})$
follow from IH with the latter also following from the fact that
$\mathrm{con}(\dot{\neg}\mathcal{T}_{\mathcal{O}_{c}})\subseteq\mathrm{con}(\mathcal{O}_{c})$.
(1) and (2) easily hold, and as shown below, property (3) follows from the
former fact:

$\displaystyle\mathrm{Lab}({\leqslant}{n}r.\mathcal{G})$
$\displaystyle=\mathrm{Lab}(\mathcal{G})\setminus\\{y_{0},\ldots,y_{n}\\}$
$\displaystyle\subseteq\mathrm{Lab}(\Gamma,\Phi,\Psi,\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}}^{\prime},\Delta,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}^{\prime})$
$\displaystyle\subseteq\mathrm{Lab}(\Gamma,\Phi,\Psi,\dot{\neg}\mathcal{T}_{\mathcal{O}_{a}}^{\prime},\Delta,x:{\leqslant}{n}r.C,\Sigma,\dot{\neg}\mathcal{T}_{\mathcal{O}_{b}}^{\prime})$

while property (4) follows from the latter fact:

$\displaystyle\mathrm{con}({\leqslant}{n}r.\mathcal{G})=\
\mathrm{con}(\mathcal{G})$
$\displaystyle\subseteq\mathrm{con}(\mathcal{O}_{a},\Delta)\cap\mathrm{con}(y_{0}:\dot{\neg}C_{0},\ldots,y_{n}:\dot{\neg}C_{n},\Sigma,\mathcal{O}_{b})$
$\displaystyle=\mathrm{con}(\mathcal{O}_{a},\Delta)\cap\mathrm{con}(x:{\leqslant}nr.C,\Sigma,\mathcal{O}_{b})\qed$

######  Lemma 6.

If $(\Sigma\vdash\Pi)\in\overline{\overline{\mathcal{G}}}$, then there exists
a $(\Gamma\vdash\Delta)\in\mathcal{G}$ such that $\Gamma\subseteq\Sigma$ and
$\Delta\subseteq\Pi$.

###### Proof.

Let $(\Sigma\vdash\Pi)\in\overline{\overline{\mathcal{G}}}$ and suppose for a
contradiction that no $(\Gamma\vdash\Delta)\in\mathcal{G}$ exists such that
$\Gamma\subseteq\Sigma$ and $\Delta\subseteq\Pi$. Then, for each
$(\Gamma\vdash\Delta)\in\mathcal{G}$, either $\Gamma\not\subseteq\Sigma$ or
$\Delta\not\subseteq\Pi$. Let
$\mathcal{G}=\\{(\Gamma_{1}\vdash\Delta_{1}),\ldots,(\Gamma_{n}\vdash\Delta_{n})\\}$
and define $\Gamma^{\prime}\vdash\Delta^{\prime}$ such that for each $1\leq
i\leq n$, one and only one of the following holds: (1)
$x\,\dot{=}\,y\in\Gamma^{\prime}$ and
$x\,{\not}{\dot{=}}\,y\in\Gamma_{i}\setminus\Sigma$, (2)
$x\,{\not}{\dot{=}}\,y\in\Gamma^{\prime}$ and
$x\,\dot{=}\,y\in\Gamma_{i}\setminus\Sigma$, or (3)
$x:\dot{\neg}C\in\Delta^{\prime}$ and $x:C\in\Delta_{i}\setminus\Pi$. Observe
that $\Sigma\cap\Gamma^{\prime}=\emptyset$ and
$\Pi\cap\Delta^{\prime}=\emptyset$ by construction. However, since
$\Gamma^{\prime}\vdash\Delta^{\prime}\in\overline{\mathcal{G}}$ by Definition
9, we have that either $\Sigma\cap\Gamma^{\prime}\neq\emptyset$ or
$\Pi\cap\Delta^{\prime}\neq\emptyset$, which gives a contradiction and proves
the lemma. ∎

######  Lemma 7.

If $\mathsf{SI}(\mathcal{O})\Vdash\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\
{}^{a}|^{b}\ \Sigma\ \|\ \mathcal{G}$, then

  1. 1.

For each $(\Gamma^{\prime}\vdash\Pi_{i})\in\mathcal{G}$,
$\mathsf{S}(\mathcal{O})\Vdash\Gamma,\Gamma^{\prime},\Phi\vdash\Delta,\Pi_{i}$;

  2. 2.

For each $(\Gamma^{\prime}\vdash\Pi_{i})\in\overline{\mathcal{G}}$,
$\mathsf{S}(\mathcal{O})\Vdash\Gamma,\Gamma^{\prime},\Psi\vdash\Pi_{i},\Sigma$.

###### Proof.

We prove both claims simultaneously by induction on the height of the proof
and make a case distinction on the last rule applied.

_Base case._ Suppose we have a proof of height $1$, i.e. an instance of an
initial rule. Let us first consider the $(id^{I}_{2})$ case and then we will
consider the $(id_{\dot{=}}^{I})$ case, noting that the $(id^{I}_{1})$ case is
similar.

$(id^{I}_{2})$ $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\
x:A,x:\neg A,\Sigma\ \|\ \\{(\ \vdash x:\top)\\}$

Claim 1 is resolved as shown below left, and relies on Lemma 3, whereas claim
2 is resolved by applying the $(id)$ rule. Note that we use the interpolant
$\overline{\mathcal{G}}=\\{(\ \vdash x:\bot)\\}$ in claim 2 (see Definition 9
above) and $\Sigma^{\prime}=\Sigma,x:A,x:\neg A$.

$(\top)$ $\Gamma,\Phi\vdash\Delta,x:\top$ |  $(id)$ $\Gamma,\Psi\vdash\Sigma^{\prime},x:\bot$
---|---

For the $(id_{\dot{=}}^{I})$ case, suppose we have a proof consisting of a
single application of the $(id_{\dot{=}}^{I})$ rule, as shown below.

$(id_{\dot{=}}^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\
\Psi,x\,{\not}{\dot{=}}\,y\vdash\Delta\ {}^{a}|^{b}\ \Sigma\ \|\
\\{(x\,{\not}{\dot{=}}\,y\vdash\ )\\}$

By the side condition on the rule, we know that $x=^{*}_{\Gamma}y$ holds for
$(id_{\dot{=}}^{I})$ above. Therefore, the application of $(id_{\dot{=}})$
shown below left is warranted as is the application of $(id_{\dot{=}})$ shown
below right, thus resolving the case.

$(id_{\dot{=}}^{I})$ $\Gamma,\Phi,x\,{\not}{\dot{=}}\,y\vdash\Delta$ |  $(id_{\dot{=}}^{I})$ $\Gamma,\Psi,x\,{\not}{\dot{=}}\,y,x\,\dot{=}\,y\vdash\Sigma$
---|---

_Inductive step._ For the inductive step, we consider the $(O)$,
$(\sqcap^{I})$, $(\forall r^{I})$, and $({\leqslant}nr^{I})$ cases as the
remaining cases are similar.

$(O)$. Let our proof in $\mathsf{SI}(\mathcal{O})$ end with an $(O)$
application:

$\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ \Sigma\ \|\
\mathcal{G}$ $(O)$ $\Gamma;\Psi\ {}^{b}|^{a}\ \Phi\vdash\Sigma\ {}^{b}|^{a}\
\Delta\ \|\ \overline{\mathcal{G}}$

Observe that if $(\Gamma^{\prime}\vdash\Pi_{i})\in\overline{\mathcal{G}}$,
then $\Gamma,\Psi,\Gamma^{\prime}\vdash\Sigma,\Pi_{i}$ is provable in
$\mathsf{S}(\mathcal{O})$ by IH, which demonstrates claim (1). To prove claim
(2), let $(\Gamma^{\prime}\vdash\Pi_{i})\in\overline{\overline{\mathcal{G}}}$.
Then, by Lemma 6, there exists a
$(\Sigma^{\prime}\vdash\Pi_{i}^{\prime})\in\mathcal{G}$ such that
$\Sigma^{\prime}\subseteq\Gamma^{\prime}$ and
$\Pi_{i}^{\prime}\subseteq\Pi_{i}$. By IH,
$\mathsf{S}(\mathcal{O})\Vdash\Gamma,\Phi,\Sigma^{\prime}\vdash\Pi_{i}^{\prime},\Delta$,
implying
$\mathsf{S}(\mathcal{O})\Vdash\Gamma,\Phi,\Gamma^{\prime}\vdash\Pi_{i},\Delta$
by the hp-admissibility of $(w_{\,\dot{=}\,})$, $(w_{\,{\not}{\dot{=}}\,})$,
and $(w)$ (Lemma 3).

$(\sqcap^{I})$. Suppose we have a proof in $\mathsf{SI}(\mathcal{O})$ ending
with an application of $(\sqcap^{I})$, as shown below.

$\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ x:C,\Sigma\ \|\
\mathcal{G}_{1}$ $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\
x:D,\Sigma\ \|\ \mathcal{G}_{2}$ $(\sqcap^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\
\Psi\vdash\Delta\ {}^{a}|^{b}\ x:C\sqcup D,\Sigma\ \|\
\mathcal{G}_{1}\cup\mathcal{G}_{2}$

We prove claim (1) first. Let
$(\Gamma^{\prime}\vdash\Pi)\in\mathcal{G}_{1}\cup\mathcal{G}_{2}$. Regardless
of if $(\Gamma^{\prime}\vdash\Pi)\in\mathcal{G}_{1}$ or
$(\Gamma^{\prime}\vdash\Pi)\in\mathcal{G}_{2}$, we have a proof of
$\Gamma,\Phi,\Gamma^{\prime}\vdash\Delta,\Pi$ by IH, which proves the claim.
To prove claim (2), suppose that
$(\Gamma_{1},\Gamma_{2}\vdash\Pi_{1},\Pi_{2})\in\overline{\mathcal{G}_{1}\cup\mathcal{G}_{2}}$
such that $(\Gamma_{1}\vdash\Pi_{1})\in\overline{\mathcal{G}}_{1}$ and
$(\Gamma_{2}\vdash\Pi_{2})\in\overline{\mathcal{G}}_{2}$. By IH, the top two
sequents below are provable in $\mathsf{S}(\mathcal{O})$. We then apply the
hp-admissibility of $(w_{\,\dot{=}\,})$, $(w_{\,{\not}{\dot{=}}\,})$, and
$(w)$ (Lemma 3) a sufficient number of times (indicated by the asterisk) to
ensure the contexts match. Last, we apply the $(\sqcap)$ to obtain the desired
conclusion.

$\Gamma,\Gamma_{1},\Psi\vdash x:C,\Sigma,\Pi_{1}$
$(w_{\,\dot{=}\,})^{*},(w_{\,{\not}{\dot{=}}\,})^{*},(w)^{*}$
$\Gamma,\Gamma_{1},\Gamma_{2},\Psi\vdash x:C,\Sigma,\Pi_{1},\Pi_{2}$
$\Gamma,\Gamma_{2},\Psi\vdash x:D,\Sigma,\Pi_{2}$
$(w_{\,\dot{=}\,})^{*},(w_{\,{\not}{\dot{=}}\,})^{*},(w)^{*}$
$\Gamma,\Gamma_{1},\Gamma_{2},\Psi\vdash x:D,\Sigma,\Pi_{1},\Pi_{2}$
$(\sqcap)$ $\Gamma,\Gamma_{1},\Gamma_{2}\Psi\vdash x:C\sqcup
D,\Sigma,\Pi_{1},\Pi_{2}$

$(\forall r^{I})$. Suppose our proof ends with an $(\forall r^{I})$
application:

$\Gamma,r(x,y);\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\
y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Sigma\ \|\ \mathcal{G}$ $(\forall
r^{I})$ $\Gamma;\Phi\ {}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ x:\forall
r.C,\Sigma\ \|\ \forall r.\mathcal{G}$

We first argue claim (1). Let
$(\Gamma^{\prime}\vdash\Pi,y:C_{1},\ldots,y:C_{n})\in\mathcal{G}$ such that
all concepts labeled with $y$ are displayed and
$y\not\in\mathrm{Lab}(\Gamma^{\prime})$ by assumption, and let
$\vv{C}=C_{1},\ldots,C_{n}$. By IH, we obtain a proof in
$\mathsf{S}(\mathcal{O})$ ending as shown below:

$\Gamma,\Gamma^{\prime},r(x,y)\vdash\Delta,\Pi,y:C_{1},\ldots,y:C_{n}$
$(\sqcup)\times(n{-}1)$
$\Gamma,\Gamma^{\prime},r(x,y)\vdash\Delta,\Pi,y:\bigsqcup\vv{C}$ $(\forall
r)$ $\Gamma,\Gamma^{\prime}\vdash\Delta,\Pi,x:\forall r.\bigsqcup\vv{C}$

We now argue claim (2). Observe that for any
$(\Gamma^{\prime}\vdash\Pi)\in\overline{\mathcal{G}}$, the multiset $\Pi$
contains zero or more labeled concepts of the form $x:\exists
r.(\dot{\neg}C_{1}\sqcap\cdots\sqcap\dot{\neg}C_{n})$. We suppose $\Pi$
contains one such formula as the other cases are analogous, and let
$\Pi=\Pi^{\prime},x:\exists
r.(\dot{\neg}C_{1}\sqcap\cdots\sqcap\dot{\neg}C_{n})$. The case is resolved as
shown below, where $(\sqcap)^{*}$ denotes $n{-}1$ applications of $(\sqcap)$
between the $n$ premises obtained from IH and
$\Sigma^{\prime}=y:C,y:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Sigma$.

$\Gamma,\Gamma^{\prime},r(x,y)\vdash\Sigma^{\prime},\Pi^{\prime},y:\dot{\neg}C_{i}\
|\ 1\leq i\leq n$ $(\sqcap)^{*}$
$\Gamma,\Gamma^{\prime},r(x,y)\vdash\Sigma^{\prime},\Pi^{\prime},y:\bigsqcap\dot{\neg}\vv{C}$
$(w)$ $\Gamma,\Gamma^{\prime},r(x,y)\vdash x:\exists
r.\bigsqcap\dot{\neg}\vv{C},\Sigma^{\prime},\Pi^{\prime},y:\bigsqcap\dot{\neg}\vv{C}$
$(\exists r)$ $\Gamma,\Gamma^{\prime},r(x,y)\vdash x:\exists
r.\bigsqcap\dot{\neg}\vv{C},\Sigma^{\prime},\Pi^{\prime}$ $(\forall r)$
$\Gamma,\Gamma^{\prime}\vdash x:\exists r.\bigsqcap\dot{\neg}\vv{C},x:\forall
r.C,\Sigma,\Pi^{\prime}$

$({\leqslant}nr^{I})$. Let us suppose that we have a proof in
$\mathsf{SI}(\mathcal{O})$ ending with an application of $({\leqslant}nr^{I})$
as shown below such that $\Gamma^{\prime}=\Gamma,r(x,y_{0}),\ldots,r(x,y_{n})$
and where
$\Sigma^{\prime}=y_{0}:\dot{\neg}C,y_{0}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\ldots,y_{n}:\dot{\neg}C,y_{n}:\dot{\neg}\mathcal{T}_{\mathcal{O}},\Sigma$.

$\Gamma^{\prime};\Phi\ {}^{a}|^{b}\
\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})\vdash\Delta\ {}^{a}|^{b}\
\Sigma^{\prime}\ \|\ \mathcal{G}$ $({\leqslant}nr^{I})$ $\Gamma;\Phi\
{}^{a}|^{b}\ \Psi\vdash\Delta\ {}^{a}|^{b}\ x:(\leqslant nr.C),\Sigma\ \|\
{\leqslant}{n}r.\mathcal{G}$

We argue claim (1) first and suppose we have the following:
$(\Gamma_{1},\Gamma_{2}\vdash\Pi,y_{0}:\vv{C}_{0},\ldots,y_{n}:\vv{C}_{n})\in\mathcal{G}$
such that $\Gamma_{2}\subseteq\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})$,
$\mathrm{Lab}(\Gamma_{1})\cap\\{y_{0},\ldots,y_{n}\\}=\emptyset$, and we let
$\vv{C}=\vv{C}_{0},\ldots,\vv{C}_{n}$. By IH, the top sequent shown below has
a proof in $\mathsf{S}(\mathcal{O})$. We invoke Lemma 3 and apply the hp-
admissible $(w)$ and $(w_{\,{\not}{\dot{=}}\,})$ rules a sufficient number of
times to derive the second sequent from the first, and then apply the
$(\sqcup)$ rule a sufficient number of times to obtain the third sequent from
the second, using an asterisk $*$ to indicate these sequential rule
applications.

$\Gamma^{\prime},\Phi,\Gamma_{1},\Gamma_{2}\vdash\Delta,\Pi,y_{0}:\vv{C}_{0},\ldots,y_{n}:\vv{C}_{n}$
$(w)^{*},(w_{\,{\not}{\dot{=}}\,})^{*}$
$\Gamma^{\prime},\Phi,\Gamma_{1},\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})\vdash\Delta,\Pi,y_{0}:\vv{C},\ldots,y_{n}:\vv{C}$
$(\sqcup)^{*}$
$\Gamma^{\prime},\Phi,\Gamma_{1},\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})\vdash\Delta,\Pi,y_{0}:\bigsqcup\vv{C},\ldots,y_{n}:\bigsqcup\vv{C}$
$({\leqslant}nr)$
$\Gamma,\Phi,\Gamma_{1}\vdash\Delta,\Pi,x:{\leqslant}{n}r.\dot{\neg}\bigsqcup\vv{C}$

Let us now argue claim (2). Observe if
$(\Gamma^{\prime\prime}\vdash\Pi)\in\overline{{\leqslant}{n}r.\mathcal{G}}$,
then $\Pi$ contains zero or more labeled concepts of the form
$x:{\geqslant}{(n{+}1)}r.\bigsqcup\vv{C}$. We suppose $\Pi$ contains one such
formula and remark that the remaining cases are similar. Therefore,
$\Pi=\Pi^{\prime},x:{\geqslant}{(n{+}1)}r.\bigsqcup\vv{C}$. We let
$\vv{C}_{i}=C_{i,1},\ldots,C_{i,k_{i}}$ with $0\leq i\leq n$ and
$\vv{C}=\vv{C}_{0},\ldots,\vv{C}_{n}$. By IH, for each $0\leq i\leq n$, each
top sequent shown below is provable in $\mathsf{S}(\mathcal{O})$. We apply the
$(\sqcap)$ rule $k_{i}{-}1$ times, indicated by $(\sqcap)^{*}$, to derive the
second sequent from the first.

$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\dot{\neg}C_{i,j}\
|\ 1\leq j\leq k_{i}$ $(\sqcap)^{*}$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\bigsqcap\dot{\neg}\vv{C}_{i}$

We denote the concluding sequent in the proof above as $S_{i}^{\prime}$. Let
us pick an $1\leq i\leq n$ and let $1\leq\ell\neq i\leq n$. We then take
$S_{\ell}^{\prime}$ and apply the hp-admissible rules $(\ell^{z}_{y_{\ell}})$,
$(\ell^{y_{\ell}}_{y_{i}})$, and $(\ell^{y_{i}}_{z})$ with $z$ fresh to obtain
the sequent $S_{\ell}^{\prime\prime}$, shown below top, where the labels
$y_{i}$ and $y_{\ell}$ have been ‘swapped’. Observe that some inequalities of
the form $y_{t}\,{\not}{\dot{=}}\,y_{s}$ in
$\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})$ may have ‘flipped’ to
$y_{s}\,{\not}{\dot{=}}\,y_{t}$, yielding the set
$\Gamma^{\not\dot{=}}_{i,\ell}(y_{0},\ldots,y_{n})$. By applying
$(w_{\,{\not}{\dot{=}}\,})$ a sufficient number of times, one can weaken in
all inequalities from $\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})$ not occurring
in $\Gamma^{\not\dot{=}}_{i,\ell}(y_{0},\ldots,y_{n})$, and then apply
$(s_{\,{\not}{\dot{=}}\,})$ a sufficient number of times so that only
$\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n})$ occurs in the antecedent.

$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}_{i,\ell}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\bigsqcap\dot{\neg}\vv{C}_{\ell}$
$(w_{\,{\not}{\dot{=}}\,})^{*}$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}_{i,\ell}(y_{0},\ldots,y_{n}),\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\bigsqcap\dot{\neg}\vv{C}_{\ell}$
$(s_{\,{\not}{\dot{=}}\,})^{*}$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\bigsqcap\dot{\neg}\vv{C}_{\ell}$

For each $1\leq i\leq n$, we take $S_{i}^{\prime}$ and each sequent proven as
shown above, apply the $(\sqcap)$ rule $n{-}1$ times, and then $(w)$ to obtain
a proof of the sequent $S_{i}$ as shown in the proof below.

$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\bigsqcap\dot{\neg}\vv{C}_{\ell}\
|\ 1\leq\ell\leq n$ $(\sqcap)\times n{-}1$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},y_{i}:\bigsqcap\dot{\neg}\vv{C}$
$(w)$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},x:{\geqslant}{(n{+}1)}r.\dot{\neg}\bigsqcup\vv{C},y_{i}:\dot{\neg}\bigsqcup\vv{C}$

Note that the last inference inference above is warranted since
$\bigsqcap\dot{\neg}\vv{C}=\dot{\neg}\bigsqcup\vv{C}$ by definition, and
because $(w)$ is hp-admissible by Lemma 3. Next, observe that for each $i$ and
$j$ such that $0\leq i<j\leq n$, the following sequent $S_{i,j}$ is provable
by $(id_{\dot{=}})$.

$(id_{\dot{=}})$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime},y_{i}\,\dot{=}\,y_{j}\vdash\Sigma^{\prime},\Pi^{\prime},x:{\geqslant}{(n{+}1)}r.\dot{\neg}\bigsqcup\vv{C}$

We can finish the proof of claim (2) as follows:

$S_{0}\ \cdots\ S_{n}\ \ S_{0,1}\ \cdots\ S_{n,n+1}$ $({\geqslant}{(n{+}1)}r)$
$\Gamma^{\prime},\Psi,\Gamma^{\not\dot{=}}(y_{0},\ldots,y_{n}),\Gamma^{\prime\prime}\vdash\Sigma^{\prime},\Pi^{\prime},x:{\geqslant}{(n{+}1)}r.\dot{\neg}\bigsqcup\vv{C}$
$({\leqslant}nr)$ $\Gamma,\Psi,\Gamma^{\prime\prime}\vdash
x:{\leqslant}nr.C,\Sigma,\Pi^{\prime},x:{\geqslant}{(n{+}1)}r.\dot{\neg}\bigsqcup\vv{C}$

This completes the proof of the lemma. ∎