cf. $C^{\prime}$ in (?, Proposition 3.32 (ii)). ∎

##  Appendix C Proofs for Section 4

See 10

###### Proof.

(1) We first consider the case of satisfiability under global ontology. Let
$A$ be a concept name and $\mathcal{O}$ an
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ ontology.
We assume that $A$ occurs in $\mathcal{O}$. Let $\mathsf{con}(\mathcal{O})$ be
the closure under single negation of the set of concepts occurring in
$\mathcal{O}$. A _type_ for $\mathcal{O}$ is a subset ${\boldsymbol{t}}$ of
$\mathsf{con}(\mathcal{O})$ such that $\neg C\in{\boldsymbol{t}}$ iff
$C\not\in{\boldsymbol{t}}$, for all $\neg C\in\mathsf{con}(\mathcal{O})$. A
_quasistate for $D$_ is a non-empty set $\boldsymbol{T}$ of types for
$\mathcal{O}$. The _description of $\boldsymbol{T}$_ is the
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept

$\Xi_{\boldsymbol{T}}=\forall
u.(\bigsqcup_{{\boldsymbol{t}}\in\boldsymbol{T}}{\boldsymbol{t}})\sqcap\bigsqcap_{{\boldsymbol{t}}\in\boldsymbol{T}}\exists
u.{\boldsymbol{t}}.$

Let $\mathcal{S}_{\mathcal{O}}$ denote the set of all quasistates
$\boldsymbol{T}$ for $\mathcal{O}$ that are _$\smash{\mathcal{ALCO}_{\\!u}}$
-satisfiable_, that is, such that $\Xi_{\boldsymbol{T}}^{t}$ is satisfiable,
where $\Xi_{\boldsymbol{T}}^{t}$ denotes the result of replacing every
outermost occurrence of $\Diamond_{i}C$ by $A_{\Diamond_{i}C}$, for a fresh
concept name $A_{\Diamond_{i}C}$. It should be clear that
$\mathcal{S}_{\mathcal{O}}$ can be computed in double exponential time as
satisfiabilty of $\smash{\mathcal{ALCO}_{\\!u}}$-concepts under
$\smash{\mathcal{ALCO}_{\\!u}}$ ontologies is in ExpTime.

We now reserve for any $C\in\mathsf{con}(\mathcal{O})$ of the form $\\{a\\}$
or $\exists r.C^{\prime}$ a fresh concept name $A_{C}$. Define a mapping
$\cdot^{\sharp}$ that associates with every
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept an
$\mathcal{ML}_{\text{{Diff}}}^{n}$-concept by replacing outermost occurrences
of concepts of the form $\exists r.C$ or concepts of the form $\\{a\\}$ by the
respective fresh concept name. Let $\mathcal{O}^{\prime}$ be the extension of
$\mathcal{O}^{\sharp}$ with the following CIs:

$\displaystyle\top$ $\displaystyle\sqsubseteq\exists
u.(\\{a\\}^{\sharp}\sqcap\neg\exists^{\neq}u.\\{a\\}^{\sharp}),\text{ for
every }a\in{\sf N_{I}}\text{ in }\mathcal{O},$ $\displaystyle\top$
$\displaystyle\sqsubseteq\bigsqcup_{\boldsymbol{T}\in\mathcal{S}_{\mathcal{O}}}\Xi_{\boldsymbol{T}}^{\sharp}.$

Then we have the following:

######  Lemma 21.

$A$ is $\mathcal{C}$-satisfiable under $\mathcal{O}$ iff there is a type
${\boldsymbol{t}}$ for $\mathcal{O}$ such that $A\in{\boldsymbol{t}}$ and
${\boldsymbol{t}}^{\sharp}$ is $\mathcal{C}$-satisfiable under
$\mathcal{O}^{\prime}$.

###### Proof.

Suppose $A$ is satisfied at $w\in W$ in an
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$
interpretation $\mathfrak{M}$ based on a frame from $\mathcal{C}$ and
$\mathcal{O}$ is satisfied in $\mathfrak{M}$. Then we can define the type
${\boldsymbol{t}}$ by reading it off from $e\in A^{\mathcal{I}_{w}}$:

${\boldsymbol{t}}=\bigl{\\{}C\in\mathsf{con}(\mathcal{O})\mid e\in
C^{\mathcal{I}_{w}}\bigr{\\}}.$

Then, we define an $\mathcal{ML}_{\text{{Diff}}}^{n}$ interpretation
$\mathfrak{M}^{\prime}$ from $\mathfrak{M}$ by providing the interpretation of
the additional concept names $A_{C}$ for
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ concepts
$C$ of the form $\\{a\\}$ and $\exists r.C^{\prime}$: we simply set
$A_{C}^{\mathcal{I}^{\prime}_{v}}=C^{\mathcal{I}_{v}}$, for all $v\in W$. It
should be clear that $\mathfrak{M}^{\prime}$ satisfies $\mathcal{O}^{\prime}$
and that $e\in({\boldsymbol{t}}^{\sharp})^{\mathcal{I}^{\prime}_{w}}$.

Conversely, suppose there is a type ${\boldsymbol{t}}$ for $\mathcal{O}$ such
that $A\in{\boldsymbol{t}}$ and ${\boldsymbol{t}}^{\sharp}$ is satisfied in an
$\mathcal{ML}_{\text{{Diff}}}^{n}$ interpretation $\mathfrak{M}^{\prime}$
based on a frame from $\mathcal{C}$ such that $\mathcal{O}^{\prime}$ is also
satisfied in $\mathfrak{M}^{\prime}$. We define $\mathfrak{M}$ by extending
$\mathfrak{M}^{\prime}$ by suitable interpretations of nominals and role
names. Let $v\in W^{\prime}$. Observe that for any nominal $a$ in
$\mathcal{O}$, $(a^{\sharp})^{\mathcal{I}^{\prime}_{v}}$ is a singleton, by
definition of $\mathcal{O}^{\sharp}$. Hence we define $a^{\mathcal{I}_{v}}$ as
its single element. For any role name $r$, we define $r^{\mathcal{I}_{v}}$ as
the maximal relation that is consistent with existential restrictions in the
types we aim to satisfy: for
$d\in({\boldsymbol{t}}^{\sharp})^{\mathcal{I}^{\prime}_{v}}$ and
$d^{\prime}\in({\boldsymbol{t}}^{\prime\sharp})^{\mathcal{I}^{\prime}_{v}}$,
let $(d,d^{\prime})\in r^{\mathcal{I}_{v}}$ if, for all $\exists
r.D\in\mathsf{con}(\mathcal{O})$, if $D\in{\boldsymbol{t}}^{\prime}$, then
$\exists r.D\in{\boldsymbol{t}}$. It is easy to see that $\mathfrak{M}$ is as
required. ∎

For the concept $\mathcal{C}$-satisfiability problem we adapt the proof in the
same way as in Proposition 2: the additional CIs of $\mathcal{O}^{\prime}$
need to be replaced by conjuncts with suitable prefixes of the box operators
and the universal role restrictions.

(2) ? (?) observed that the logic of the difference modality and nominals have
the same expressive power. Their technical result can be presented in our
setting in the following way. Let $C$ be an
$\mathcal{ML}_{\text{{Diff}}}^{n}$-concept and $\exists^{\neq}u.B$ its
subconcept. Denote by $C^{\ddagger_{B}}$ the result of replacing every
occurrence of $\exists^{\neq}u.B$ in $D$ with

$\exists u.B\sqcap(\\{a_{B}\\}\Rightarrow\exists u.(\neg\\{a_{B}\\}\sqcap
B)),$

where $a_{B}$ is a fresh nominal associated with concept $B$ (note that we
replace only a single subconcept here). Let $\mathcal{O}^{\textsf{wt}}_{B}$
consist of the following CI:

$B\sqsubseteq\exists u.(\\{a_{B}\\}\sqcap B).$

Then we can extend the proof of Lemmas 4.2 and 4.3 in (?) to the modal setting
(provided that interpretations do not satisfy the RDA, and so nominals can be
interpreted differently in different worlds) to obtain the following:

######  Lemma 22.

For any interpretation $\mathfrak{M}$ satisfying
$\mathcal{O}^{\textup{{wt}}}_{B}$, we have
$C^{\mathcal{I}(w)}=(C^{\ddagger_{B}})^{\mathcal{I}(w)}$, for all $w$ in
$\mathfrak{M}$.

This result gives us the reduction for the case of satisfiability under global
ontology. Let $\mathcal{O}$ be an $\mathcal{ML}_{\text{{Diff}}}^{n}$-ontology
and $A$ a concept name. By Lemma 4, we can assume that $\mathcal{O}$ is in
normal form. Denote by $\mathcal{O}^{\ddagger}$ the result of replacing every
CI $C_{1}\sqsubseteq C_{2}$ in $\mathcal{O}$ with $C_{1}^{\ddagger}\sqsubseteq
C_{2}^{\ddagger}$, where $C_{i}^{\ddagger}$ is the result of applying
$\cdot^{\ddagger_{B}}$ to $C_{i}$, for every subconcept of the form
$\exists^{\neq}u.B$; note that the order of applications of the
$\cdot^{\ddagger_{B}}$ does not matter as the ontology is in normal form. Let
$\mathcal{O}^{\prime}=\mathcal{O}^{\ddagger}\cup\mathcal{O}^{\textsf{wt}}$,
where $\mathcal{O}^{\textsf{wt}}$ is the union of all
$\mathcal{O}^{\textsf{wt}}_{B}$, for concepts $\exists^{\neq}u.B$ in
$\mathcal{O}$. It should be clear that, if $A$ is satisfied under
$\mathcal{O}$ at $w$ in an interpretation $\mathfrak{M}$ based on frame from
$\mathcal{C}$, then we can extend $\mathfrak{M}$ to $\mathfrak{M}^{\prime}$ by
interpreting the nominals $a_{B}$ for concepts of the form
$\exists^{\neq}u.B$: for each such nominal, if
$B^{\mathcal{I}_{v}}\neq\emptyset$, then we pick any $e\in
B^{\mathcal{I}_{v}}$ and assign $a_{B}^{\mathcal{I}_{v}}=e$; otherwise, we
leave $a_{B}^{\mathcal{I}_{v}}$ undefined. Clearly, $\mathfrak{M}^{\prime}$
satisfies $\mathcal{O}^{\textsf{wt}}$. Thus, by Lemma 22,
$\mathfrak{M}^{\prime}$ satisfies $\mathcal{O}^{\ddagger}$, and also $A$ is
satisfied at $w$ in $\mathfrak{M}^{\prime}$.

Conversely, if $A$ is satisfied under $\mathcal{O}^{\prime}$ at $w$ in an
interpretation $\mathfrak{M}^{\prime}$ based on a frame from $\mathcal{C}$,
then, by Lemma 22, $A$ is satisfied under $\mathcal{O}$ at $w$ in
$\mathfrak{M}^{\prime}$. We can now take the reduct $\mathfrak{M}$ of
$\mathfrak{M}^{\prime}$ by removing the interpretation of nominals: as
$\mathcal{O}$ does not contain nominals, $A$ is satisfied under $\mathcal{O}$
at $w$ in $\mathfrak{M}$.

Next, we consider the case of concept satisfiability. Let $D$ be an
$\mathcal{ML}_{\text{{Diff}}}^{n}$-concept. We repeatedly apply Lemma 5,
starting from the innermost occurrences of subconcepts of the form
$\exists^{\neq}u.C$, to transform $D$ into normal form $D^{\prime}$, where
each ‘elsewhere’ quantifier is applied only to concept names. We then
construct $D^{\ddagger}$ by applying the $\cdot^{\ddagger_{B}}$ to
$D^{\prime}$, for each $B$ such that $\exists^{\neq}u.B$ occurs in
$D^{\prime}$; again, the order of applications does not matter as $D^{\prime}$
is in normal form. Consider the conjunction of $D^{\ddagger}$ with all
concepts of the form

$\Box^{\pi}\forall u.(B\Rightarrow\exists u.(\\{a_{B}\\}\sqcap B)),$

for $\pi\in\mathsf{rp}(D^{\prime},\exists^{\neq}u.B)$ and concepts of the form
$\exists^{\neq}u.B$ in $D^{\prime}$ (note that, by Lemma 5,
$\mathsf{rp}(D^{\prime},\exists^{\neq}u.B)$ coincides with
$\mathsf{rp}(D,\exists^{\neq}u.C)$ for the respective $C$ in $D$). We can
easily modify the argument presented above (see the proof of Proposition 2) to
show that $D$ is satisfied in an interpretation $\mathfrak{M}$ iff
$D^{\prime}$ is satisfied in an interpretation $\mathfrak{M}^{\prime}$ that
additionally interprets nominals $a_{B}$ as ‘witnesses’ for concepts of the
form $\exists^{\neq}u.B$. ∎

##  Appendix D Proofs for Section 5

We first observe that for $\mathbf{S5}$, concept satisfiability under global
ontology can be reduced to concept satisfiability without ontology by using
the concept $C_{\mathcal{O}}\sqcap\Box C_{\mathcal{O}}$ with $C_{\mathcal{O}}$
the conjunction of all $C\Rightarrow D$ with $C\sqsubseteq D\in\mathcal{O}$.

See 11

###### Proof.

By Proposition 8, we can drop definite descriptions (hence consider
$L_{\smash{\mathcal{ALCO}_{\\!u}}}$) and by Proposition 3, it is sufficient to
consider total satisfiability. By Proposition 9, satisfiability with expanding
domains can be reduced in polytime to satisfiability with constant domain, so
we consider constant domain models. We give the proof for
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$. The proof for
$\mathbf{K}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ can then be derived in a
straightforward manner.

We show the exponential finite model property (every
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-concept that is satisfiable,
is satisfiable in a model of exponential size). The NExpTime upper bound then
follows directly. We proceed in a number of steps. First, we argue that tree-
shaped models are sufficient. Then, we introduce quasimodels as a surrogate
for models that is easier to manipulate and show the exponential finite model
property for tree-shaped quasimodels. Finite exponential-size models are then
easily constructed.

Recall that a frame $\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ is an
$\mathbf{S5}^{n}$-frame if all $R_{i}$ are equivalence relations. Then such an
$\mathbf{S5}^{n}$-frame $\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ is called a
_tree-shaped $\mathbf{S5}^{n}$-frames_ if there exists a $w_{0}\in W$ such
that the domain $W$ of $\mathfrak{F}$ is a prefix-closed set of words of the
form

$\vec{w}=w_{0}i_{0}w_{1}\cdots i_{m-1}w_{m},$ (7)

where $1\leq i_{j}\leq n$, $i_{j}\not=i_{j+1}$, and each $R_{i}$ is the
smallest equivalence relation containing all pairs of the form
$(\vec{w},\vec{w}iw)\in W\times W$. We call $w_{0}$ the root of
$\mathfrak{F}$. We define the _depth_ of $\mathfrak{F}$ as the maximal $m$
such that $W$ contains a word of the form (7). A _tree-shaped
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-model_ takes the form
$\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$ with $\mathfrak{F}$ a tree-
shaped $\mathbf{S5}^{n}$-frame.

######  Lemma 23.

$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ is determined by tree-shaped
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-models: an
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept $C$
is satisfiable in an $\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-model
iff it is satisfiable in the root of a tree-shaped
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-model of depth bounded by
the modal depth of $C$.

###### Proof.

Assume that $C$ has modal depth $K$ and assume
$\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$ with
$\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ and $w_{0}\in W$ with
$C^{\mathcal{I}_{w_{0}}}\not=\emptyset$ are given. Unfold $\mathfrak{F}$ into

$\mathfrak{F}^{\ast}=(W^{\ast},R_{1}^{\ast},\ldots,R_{n}^{\ast})$

where $W^{\ast}$ is the set of words $\vec{w}$ of the form (7) with
$(w_{j},w_{j+1})\in R_{i_{j}}$, $w_{j}\not=w_{j+1}$, $i_{j}\not=i_{j+1}$, and
$m\leq K$, and $R^{\ast}_{i}$ is the smallest equivalence relation containing
all pairs $(\vec{w},\vec{w}iw)\in W^{\ast}\times W^{\ast}$. Define a model
$\mathfrak{M}^{\ast}=(\mathfrak{F}^{\ast},\Delta^{\ast},\mathcal{I}^{\ast})$
by setting $\Delta^{\ast}=\Delta$ and
$\mathcal{I}^{\ast}_{\vec{w}}=\mathcal{I}_{w_{m}}$ for $\vec{w}\in W^{\ast}$
of the form (7). Clearly $\mathfrak{M}^{\ast}$ is tree-shaped. Moreover, for
all
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concepts
$D$ of modal depth not exceeding $K$, one can show by induction that
$D^{\mathcal{I}^{\ast}_{w_{0}}}=D^{\mathcal{I}_{w_{0}}}$. In particular,
$C^{\mathcal{I}^{\ast}_{w_{0}}}\neq\emptyset$. ∎

Given an $\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$
concept $C_{0}$, let $\mathsf{con}(C_{0})$ be the closure under single
negation of the set of concepts occurring in $C_{0}$. A _type_ for $C_{0}$ is
a subset ${\boldsymbol{t}}$ of $\mathsf{con}(C_{0})$ such that

  1. C1

$\neg C\in{\boldsymbol{t}}$ iff $C\not\in{\boldsymbol{t}}$, for all $\neg
C\in\mathsf{con}(C_{0})$;

  2. C2

$C\sqcap D\in{\boldsymbol{t}}$ iff $C,D\in{\boldsymbol{t}}$, for all $C\sqcap
D\in\mathsf{con}(C_{0})$.

Note that there are at most $2^{|\mathsf{con}(C_{0})|}$ types for $C_{0}$.

A _quasistate for $C_{0}$_ is a non-empty set $\boldsymbol{T}$ of types for
$C_{0}$ satisfying the following conditions:

  1. Q1

for every $\\{a\\}\in\mathsf{con}(C_{0})$, there exists exactly one
${\boldsymbol{t}}\in\boldsymbol{T}$ such that $\\{a\\}\in{\boldsymbol{t}}$;

  2. Q2

for every ${\boldsymbol{t}}\in\boldsymbol{T}$ and every $\exists
r.C\in{\boldsymbol{t}}$, there exists
${\boldsymbol{t}}^{\prime}\in\boldsymbol{T}$ such that $\\{\lnot
D\mid\lnot\exists
r.D\in{\boldsymbol{t}}\\}\cup\\{C\\}\subseteq{\boldsymbol{t}}^{\prime}$;

  3. Q3

for every ${\boldsymbol{t}}\in\boldsymbol{T}$, $\exists
u.C\in{\boldsymbol{t}}$ iff there exists
${\boldsymbol{t}}^{\prime}\in\boldsymbol{T}$ such that
$C\in{\boldsymbol{t}}^{\prime}$.

A _basic structure for $C_{0}$_ is a pair $(\mathfrak{F},\boldsymbol{q})$,
where $\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ is a tree-shaped
$\mathbf{S5}^{n}$-frame with root $w_{0}$ and $\boldsymbol{q}$ is a function
associating with every $w\in W$ a quasistate $\boldsymbol{q}(w)$ for $C_{0}$,
satisfying

  1. B1

there exists a type ${\boldsymbol{t}}\in\boldsymbol{q}(w_{0})$ such that
$C_{0}\in{\boldsymbol{t}}$.

A _run through $(\mathfrak{F},\boldsymbol{q})$_ is a function $\rho$ mapping
each world $w\in W$ into a type $\rho(w)\in\boldsymbol{q}(w)$ and satisfying
the following condition for every $\Diamond_{i}C\in\mathsf{con}(C_{0})$:

  1. R1

$\Diamond_{i}C\in\rho(w)$ if there exists $v\in W$ such that $wR_{i}v$ and
$C\in\rho(v)$.

  2. R2

if $\Diamond_{i}C\in\rho(w)$ then there exists $v\in W$ such that $wR_{i}v$
and $C\in\rho(v)$.

An _$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for $C_{0}$_
is a triple $\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$, where
$(\mathfrak{F},\boldsymbol{q})$ is a basic structure for $C_{0}$ and
$\mathfrak{R}$ is a set of runs through $(\mathfrak{M},\boldsymbol{q})$ such
that the following condition holds:

  1. M1

for every $w\in W$ and every ${\boldsymbol{t}}\in\boldsymbol{q}(w)$, there
exists $\rho\in\mathfrak{R}$ with $\rho(w)={\boldsymbol{t}}$;

  2. M2

for every $w\in W$ and for every ${\boldsymbol{t}}\in\boldsymbol{q}(w),\text{
with }\\{a\\}\in{\boldsymbol{t}}$, there exists exactly one
$\rho\in\mathfrak{R}$ such that $\\{a\\}\in\rho(w)$.

The next lemma provides a link between quasimodels and standard models.

######  Lemma 24.

An $\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept
$C_{0}$ is satisfiable in the root of a tree-shaped
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-model based on a frame
$\mathfrak{F}$ iff there exists a
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-quasimodel for $C_{0}$ based
on the same frame $\mathfrak{F}$.

###### Proof.

$(\Rightarrow)$ Let $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, with
$\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ be a tree-shaped
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-model of modal depth at most
md$(C_{0})$ with $C^{\mathcal{I}_{w_{0}}}\neq\emptyset$ for the root $w_{0}$
of $\mathfrak{F}$. Let
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)=\\{C\in\mathsf{con}(C_{0})\mid d\in
C^{\mathcal{I}_{w}}\\}$, for every $d\in\Delta$ and $w\in W$. Clearly,
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)$ is a concept type for $C_{0}$ since it
satisfies (C1)–(C2). We now define a triple
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$, where

  * •

$\boldsymbol{q}$ is the function from $W$ to the set of quasistates for
$C_{0}$ defined by setting
$\boldsymbol{q}(w)=\\{{\boldsymbol{t}}^{\mathcal{I}_{w}}(d)\mid
d\in\Delta\\}$, for every $w\in W$;

  * •

$\mathfrak{R}$ is the set of functions $\rho_{d}$ from $W$ to the set of types
for $C_{0}$ defined by setting
$\rho_{d}(w)={\boldsymbol{t}}^{\mathcal{I}_{w}}(d)$, for every $d\in\Delta$
and $w\in W$.

It is easy to show that $\mathfrak{Q}$ is a quasimodel for $C_{0}$. Indeed,
$\boldsymbol{q}$ is well-defined, as $\boldsymbol{q}(w)$ is a set of types for
$C_{0}$ satisfying (Q1)–(Q3), for every $w\in W$. Moreover,
$(\mathfrak{F},\boldsymbol{q})$ is a basic structure for $C_{0}$ since
$\mathfrak{M}$ satisfies $C_{0}$ in the root $w_{0}$ of $\mathfrak{F}$ and
thus $(\mathfrak{F},\boldsymbol{q})$ satisfies (B1). The set of runs,
$\mathfrak{R}$, by construction, satisfies (R1) and (R2). Finally, by
definition of $\boldsymbol{q}(w)$ and of $\rho$, $\mathfrak{Q}$ satisfies
(M1), and, since for every $w\in W$, if $\\{a\\}\in{\boldsymbol{t}}$, there is
exactly one $d\in\Delta$ such that $d=\\{a\\}^{\mathcal{I}_{w}}$, thus
$\mathfrak{Q}$ satisfies (M2).

$(\Leftarrow)$ Suppose there is a quasimodel
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$ for $C_{0}$. Define
a model $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, by setting
$\Delta=\mathfrak{R}$, and, for any $A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$ and
$a\in{\sf N_{I}}$:

  * •

$A^{\mathcal{I}_{w}}=\\{\rho\in\Delta\mid A\in\rho(w)\\}$;

  * •

$r^{\mathcal{I}_{w}}=\\{(\rho,\rho^{\prime})\in\Delta\times\Delta\mid\\{\lnot
C\mid\lnot\exists r.C\in\rho(w)\\}\subseteq\rho^{\prime}(w)\\}$;

  * •

$u^{\mathcal{I}_{w}}=\Delta\times\Delta$;

  * •

$a^{\mathcal{I}_{w}}=\rho$, for the unique $\rho\in\mathfrak{R}$ such that
$\\{a\\}\in\rho(w)$.

Observe that $\Delta$ is well-defined since $W$ is a non-empty set and
$\boldsymbol{q}(w)\neq\emptyset$, for all $w\in W$. Thus, by (M1),
$\mathfrak{R}\neq\emptyset$. Also, by (Q1) and (M2), $a^{\mathcal{I}_{w}}$ is
well-defined. We now require the following claim.

######  Claim 5.

For every $C\in\mathsf{con}(C_{0})$, $w\in W$ and $\rho\in\Delta$, $\rho\in
C^{\mathcal{I}_{w}}$ iff $C\in\rho(w)$.

###### Proof.

The proof is by induction on $C$. The base cases, $C=A$ and $C=\\{a\\}$,
follow immediately from the definition of $\mathfrak{M}$. We then consider the
inductive cases.
Let $C=\lnot D$. $\lnot D\in\rho(w)$ iff, by (C1), $D\not\in\rho(w)$. By
induction, $D\not\in\rho(w)$ iff $\rho\not\in D^{\mathcal{I}_{w}}$ iff
$\rho\in(\lnot D)^{\mathcal{I}_{w}}$.
Let $C=D\sqcap E$. Similar to the previous case, now by using (C2).
Let $C=\exists u.D$. $\rho\in(\exists u.D)^{\mathcal{I}_{w}}$ iff there exists
$\rho^{\prime}\in D^{\mathcal{I}_{w}}$. By inductive hypothesis,
$\rho^{\prime}\in D^{\mathcal{I}_{w}}$ iff $D\in\rho^{\prime}(w)$. By (Q3),
the previous step holds iff $\exists u.D\in\rho(w)$.
Let $C=\exists r.D$. $(\Rightarrow)$ Suppose that $\rho\in(\exists
r.D)^{\mathcal{I}_{w}}$. Then, there exists $\rho^{\prime}\in\Delta$ such that
$(\rho,\rho^{\prime})\in r^{\mathcal{I}_{w}}$ and $\rho^{\prime}\in
D^{\mathcal{I}_{w}}$. By inductive hypothesis, $\rho^{\prime}\in
D^{\mathcal{I}_{w}}$ iff $D\in\rho^{\prime}(w)$. By contradiction, assume that
$\exists r.D\not\in\rho(w)$, then, by (C1), $\lnot\exists r.D\in\rho(w)$. By
definition of $r^{\mathcal{I}_{w}}$, since $(\rho,\rho^{\prime})\in
r^{\mathcal{I}_{w}}$, then, $\lnot D\in\rho^{\prime}(w)$, thus contradicting,
by (C1), that $D\in\rho^{\prime}(w)$. $(\Leftarrow)$ Conversely, suppose that
$\exists r.D\in\rho(w)$. By (Q2) and (M1), there exists a
$\rho^{\prime}\in\Delta$ such that $\\{\lnot E\mid\lnot\exists
r.E\in\rho(w)\\}\cup\\{D\\}\subseteq\rho^{\prime}(w)$. By inductive hypothesis
and the definition of $r^{\mathcal{I}_{w}}$, $\rho^{\prime}\in
D^{\mathcal{I}_{w}}$ and $(\rho,\rho^{\prime})\in r^{\mathcal{I}_{w}}$. Thus,
$\rho\in(\exists r.D)^{\mathcal{I}_{w}}$.
Let $C=\Diamond_{i}D$. $\rho\in(\Diamond_{i}D)^{\mathcal{I}_{w}}$ iff there
exists $v\in W$ such that $(w,v)\in R_{i}$ and $\rho\in D^{\mathcal{I}_{v}}$.
By inductive hypothesis, $\rho\in D^{\mathcal{I}_{v}}$ iff $D\in\rho(v)$.
Hence, by (R1) and (R2), such a $v$ exists iff $\Diamond_{i}D\in\rho(w)$. ∎

Now we can easily finish the proof of Lemma 24 by observing that, by (B1),
there exists a world $w^{\prime}\in W$ and a type
${\boldsymbol{t}}\in\boldsymbol{q}(w^{\prime})$ such that
$C_{0}\in{\boldsymbol{t}}$. Thus, by (M1), there exists $\rho\in\mathfrak{R}$
with $\rho(w^{\prime})={\boldsymbol{t}}$ and, by Claim 5, $\rho\in
C_{0}^{\mathcal{I}_{w^{\prime}}}$. ∎

We now show the exponential finite model property in terms of quasimodels.

######  Lemma 25.

There exists an $\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel
for $C_{0}$ iff there exists an
$\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for $C_{0}$ of
exponential size in the length of $C_{0}$.

###### Proof.

Assume $\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$ with
$\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ is given such that $W$ is a prefix-
closed set of words of the form (7), where $1\leq i_{j}\leq m$,
$i_{j}\not=i_{j+1}$, and $m$ is bounded by md$(C_{0})$.

For each $\vec{w}\in W$ and ${\boldsymbol{t}}\in\boldsymbol{q}(\vec{w})$ we
fix a _proto-run, $\rho_{\vec{w},{\boldsymbol{t}}}\in\mathfrak{R}$, for
$\vec{w}$ and ${\boldsymbol{t}}$_ with
$\rho_{\vec{w},{\boldsymbol{t}}}(\vec{w})={\boldsymbol{t}}$. Let
$\mathcal{F}(\vec{w})$ denote the set of selected proto-runs through
$\boldsymbol{q}(\vec{w})$, that is
$\mathcal{F}(\vec{w})=\\{\rho_{\vec{w},{\boldsymbol{t}}}\mid{\boldsymbol{t}}\in\boldsymbol{q}(\vec{w})\\}$.
We also fix for any
$\Diamond_{i}C\in{\boldsymbol{t}}\in\boldsymbol{q}(\vec{w})$ a _proto-witness_
$\vec{w}^{\prime}=v_{\vec{w},i,C,{\boldsymbol{t}}}\in W$ such that
$\vec{w}^{\prime}$ takes the form $\vec{w}iv$ (and so
$(\vec{w},\vec{w}^{\prime})\in R_{i}$) and
$C\in\rho_{\vec{w},{\boldsymbol{t}}}(\vec{w}^{\prime})$, whenever such a
$\vec{w}^{\prime}$ exists. Note that such a $\vec{w}^{\prime}$ might not exist
since by the definition of $R_{i}$ as equivalence closure in tree-shaped
models the witness for $\Diamond_{i}C$ might also be ${\boldsymbol{t}}$ itself
if $C\in{\boldsymbol{t}}$ or $\vec{w}$ could take the form $\vec{w}_{0}iw$ for
some $\vec{w}_{0}$ and either
$C\in\rho_{\vec{w},{\boldsymbol{t}}}(\vec{w}_{0})$ or there is $w^{\prime}$
with $\vec{w}_{0}iw^{\prime}\in W$ and
$C\in\rho_{\vec{w},{\boldsymbol{t}}}(\vec{w}_{0}iw^{\prime})$.

We next define inductively sets $W_{0},W_{1},\ldots,W_{K}\subseteq W$ with $K$
the depth of $\mathfrak{F}$ by setting $W_{0}=\\{w_{0}\\}$ and
$W_{j+1}=W_{j+1}^{1}\cup\cdots\cup W_{j+1}^{n}$, where for $1\leq i\leq n$:

$W_{j+1}^{i}=\\{v_{\vec{w},i,C,{\boldsymbol{t}}}\mid\Diamond_{i}C\in{\boldsymbol{t}}\in\boldsymbol{q}(\vec{w}),\vec{w}\in
W_{j}\\}.$

Let $W^{\prime}=W_{0}\cup\cdots\cup W_{K}$ and let
$R_{1}^{\prime},\ldots,R_{n}^{\prime}$ and $\boldsymbol{q}^{\prime}$ be the
restrictions of $R_{1},\ldots,R_{n}$ and $\boldsymbol{q}$ to $W^{\prime}$:

$R_{i}^{\prime}=R_{i}\cap(W^{\prime}\times
W^{\prime}),\quad\boldsymbol{q}^{\prime}(\vec{w})=\boldsymbol{q}(\vec{w})\text{
for $\vec{w}\in W^{\prime}$}$

Also let $\mathfrak{R}^{\prime}$ denote the set of restrictions of the proto-
runs $\rho_{\vec{w},{\boldsymbol{t}}}$ with $\vec{w}\in W^{\prime}$ to
$W^{\prime}$. Let
$\mathfrak{F}^{\prime}=(W^{\prime},R_{1},^{\prime}\ldots,R_{n}^{\prime})$ and
$\mathfrak{Q}^{\prime}=(\mathfrak{F}^{\prime},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$.
Then $\mathfrak{Q}^{\prime}$ is a quasimodel except that the proto-runs in
$\mathfrak{R}^{\prime}$ might not all satisfy (R2). Note that (R2) holds for
every proto-run $\rho_{\vec{w},{\boldsymbol{t}}}$ at the world $\vec{w}$ for
those $\Diamond_{i}C$ for which $i_{m-1}\not=i$ (assuming that $\vec{w}$ takes
the form (7)) but that there might not be witnesses for $\Diamond_{i}C$ on
$\vec{w}^{\prime}\not=\vec{w}$ and if $i_{m-1}=i$. To ensure (R2) also in
these cases we introduce, in a careful way, copies of existing worlds that
provide the witnesses for such $\Diamond_{i}C$.

Denote the set of all bijections on $\mathfrak{R}^{\prime}$ by
$B(\mathfrak{R}^{\prime})$. The new domain is constructed using copies of the
original domain elements indexed by bijections in $B(\mathfrak{R}^{\prime})$.

Take for any $\vec{w}\in W^{\prime}$ and $\rho\in\mathfrak{R}^{\prime}$ the
bijection $\sigma_{\vec{w},\rho}\in B(\mathfrak{R}^{\prime})$ that swaps
$\rho$ with the proto-run $\rho_{\vec{w},{\boldsymbol{t}}}$ with
${\boldsymbol{t}}=\rho(\vec{w})$ and maps the remaining runs to themselves.
The _$\vec{w}$ -repair set_, Rep$(\vec{w})$, is the set of all
$\sigma_{\vec{w},\rho}$ with $\rho\in\mathfrak{R}^{\prime}$. Note that the
identity function, $id$, on $\mathfrak{R}^{\prime}$ is an element of
Rep$(\vec{w})$.

For any $(\vec{w},\sigma)\in W^{\prime}\times B(\mathfrak{R}^{\prime})$,
define

$Suc_{i}(\vec{w},\sigma)=\\{(\vec{w}^{\prime},\sigma^{\prime})\in
W^{\prime}\times B\mid\vec{w}^{\prime}=\vec{w}iw\in W^{\prime},\\\
\sigma^{\prime}=\tau\circ\sigma\text{ for some }\tau\in\text{Rep}(\vec{w})\\}$

and let $W^{\prime\prime}$ denote the set of all words

$\vec{u}=(\vec{w}_{0},\sigma_{0})i_{0}(\vec{w}_{1},\sigma_{1})i_{1}\cdots
i_{m-1}(\vec{w}_{m},\sigma_{m}),$ (8)

where $(\vec{w}_{0},\sigma_{0}):=(w_{0},id)$ and
$(\vec{w}_{i+1},\sigma_{i+1})\in Suc_{i}(\vec{w}_{i},\sigma_{i})$ for $0\leq
i<m$.

Define $\boldsymbol{q}^{\prime\prime}$ by setting
$\boldsymbol{q}^{\prime\prime}(\vec{u})=\boldsymbol{q}^{\prime}(\vec{w}_{m})$
for any $\vec{u}\in W^{\prime\prime}$ of the form (8). Associate with any run
$\rho\in\mathfrak{R}^{\prime}$ a unique run $\rho^{\uparrow}$ on
$W^{\prime\prime}$ by setting
$\rho^{\uparrow}(\vec{u}):=\sigma_{m}(\rho)(\vec{w}_{m})$ for any $\vec{u}\in
W^{\prime\prime}$ of the form (8) and let
$\mathfrak{R}^{\prime\prime}=\\{\rho^{\uparrow}\mid\rho\in\mathfrak{R}^{\prime}\\}$.

We show that
$(\mathfrak{F}^{\prime\prime},\boldsymbol{q}^{\prime\prime},\mathfrak{R}^{\prime\prime})$
with
$\mathfrak{F}^{\prime\prime}=(W^{\prime\prime},R_{1}^{\prime\prime},\ldots,R_{n}^{\prime\prime})$
the tree-shaped $\mathbf{S5}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ frame
defined by $W^{\prime\prime}$, is as required.

We show that conditions (B1), (R1), (R2), (M1), and (M2) are satisfied.

Observe first that $\rho\mapsto\rho^{\uparrow}$ is a bijection from
$\mathfrak{R}^{\prime}$ onto $\mathfrak{R}^{\prime\prime}$. To show this
observe that the mapping is surjective by definition. To show that it is
injective, assume that $\rho_{1}\not=\rho_{2}$. Take $\vec{w}_{m}\in
W^{\prime}$ of the form (7) with
$\rho_{1}(\vec{w}_{m})\not=\rho_{2}(\vec{w}_{m})$. Then let

$\vec{v}=(\vec{w}_{0},id)i_{0}(\vec{w}_{1},id)i_{1}\cdots
i_{m-1}(\vec{w}_{m},id)\in W^{\prime\prime},$

where $\vec{w}_{i+1}=\vec{w}_{i}iw_{i+1}$ for $i<m$. We have
$\rho_{1}^{\uparrow}(\vec{v})=id(\rho_{1})(\vec{w}_{m})\not=id(\rho_{2})(\vec{w}_{m})$,
as required.

(B1) is straightforward.

We prove (M1) and (M2) in one go by showing that for any $\vec{u}\in
W^{\prime\prime}$ of the form (8) and
${\boldsymbol{t}}\in\boldsymbol{q}^{\prime\prime}(\vec{u})$ there is a
bijection between
$V_{0}=\\{\rho\in\mathfrak{R}^{\prime\prime}\mid\rho(\vec{u})={\boldsymbol{t}}\\}$
and
$V_{1}=\\{\rho\in\mathfrak{R}^{\prime}\mid\rho(\vec{w}_{m})={\boldsymbol{t}}\\}$
(recall that
$\boldsymbol{q}^{\prime\prime}(\vec{u})=\boldsymbol{q}^{\prime}(\vec{w}_{m})$).

Indeed, we claim that $F\colon V_{0}\rightarrow V_{1}$ defined by setting
$F(\rho^{\uparrow})=\sigma_{m}(\rho)$ is a bijection. As
$\rho\mapsto\rho^{\uparrow}$ is bijective and
$\rho^{\uparrow}(\vec{u})=\sigma_{m}(\rho)(\vec{w}_{m})$, $F$ is a well
defined function into $V_{1}$. It is injective since $\sigma_{m}$ is also
bijective, by definition. It is surjective since for any
$\rho\in\mathfrak{R}^{\prime}$ with $\rho(\vec{w}_{m})={\boldsymbol{t}}$ we
have
$F((\sigma_{m}^{-1}(\rho))^{\uparrow})=\sigma_{m}\sigma_{m}^{-}(\rho)=\rho$
and $\sigma_{m}^{-1}(\rho)\in\mathfrak{R}^{\prime}$.

We next show (R1) and (R2). Assume that $\Diamond_{i}C\in\mathsf{con}(C_{0})$
and $\rho^{\uparrow}\in\mathfrak{R}^{\prime\prime}$. Consider $\vec{u}\in
W^{\prime\prime}$ of the form (8).

For (R1), assume there exists $\vec{v}\in W^{\prime\prime}$ such that
$\vec{u}R_{i}^{\prime\prime}\vec{v}$ and $C\in\rho^{\uparrow}(\vec{v})$. We
have to show that $\Diamond_{i}C\in\rho^{\uparrow}(\vec{u})$. Observe that the
runs in $\mathfrak{R}^{\prime}$ satisfy (R1) in $\mathfrak{Q}^{\prime}$ and
that, moreover,

  1. R3

if $\Diamond_{i}C\in\rho(\vec{w})$ with $\rho\in\mathfrak{R}^{\prime}$ and
$(\vec{w},\vec{w}^{\prime})\in R_{i}^{\prime}$, then
$\Diamond_{i}C\in\rho(\vec{w}^{\prime})$.

We distinguish the following four cases.

  1. 1.

$\vec{v}=\vec{u}$. Then $\Diamond_{i}C\in\rho^{\uparrow}(\vec{u})$ since we
have $\Diamond_{i}C\in{\boldsymbol{t}}$ whenever $C\in{\boldsymbol{t}}$ for
$\Diamond_{i}C\in\mathsf{con}(C_{0})$ for any ${\boldsymbol{t}}$.

  2. 2.

$\vec{v}=\vec{u}i(\vec{u}iw_{m+1},\sigma_{m+1})$ for some
$(w_{m+1},\sigma_{m+1})$ with $\vec{w}_{m}iw_{m+1}\in W^{\prime}$ with
$\sigma_{m+1}=\tau\circ\sigma_{n}$ and $\tau\in\text{Rep}(\vec{w}_{m})$.

We have $\rho^{\uparrow}(\vec{u})=\sigma_{m}(\rho)(\vec{w}_{m})$ and
$\rho^{\uparrow}(\vec{v})=\tau\circ\sigma_{m}(\rho)(\vec{w}_{m}iw_{m+1})$.
From $C\in\tau\circ\sigma_{m}(\rho)(\vec{w}_{m}iw_{m+1})$ it follows that
$\Diamond_{i}C\in\tau\circ\sigma_{m}(\rho)(\vec{w}_{m})$ since
$\tau\circ\sigma_{m}(\rho)$ satisfies condition (R1) for runs in
$\mathfrak{Q}^{\prime}$. Now $\tau\circ\sigma_{m}(\rho)$ coincides with
$\sigma_{m}(\rho)$ on $\vec{w}_{m}$. Hence
$\Diamond_{i}C\in\sigma_{m}(\rho)(\vec{w}_{m})$, as required.

  3. 3.

$\vec{v}=(\vec{w}_{0},\sigma_{0})i_{0}(\vec{w}_{1},\sigma_{1})i_{1}\cdots
i_{m-2}(\vec{w}_{m-1},\sigma_{m-1})$ and $i_{m-1}=i$.

We have $\sigma_{m}=\tau^{\prime}\circ\sigma_{m-1}$ for some
$\tau^{\prime}\in\text{Rep}(\vec{w}_{m-1})$. Note that
$\rho^{\uparrow}(\vec{u})=\tau^{\prime}\circ\sigma_{m-1}(\rho)(\vec{w}_{m-1}iw_{m})$
and $\rho^{\uparrow}(\vec{v})=\sigma_{m-1}(\rho)(\vec{w}_{m-1})$. Now
$\tau^{\prime}\circ\sigma_{m-1}(\rho)$ coincides with $\sigma_{m-1}(\rho)$ on
$\vec{w}_{m-1}$. Hence
$C\in\tau^{\prime}\circ\sigma_{m-1}(\rho)(\vec{w}_{m-1})$. Hence
$\Diamond_{i}C\in\tau^{\prime}\circ\sigma_{m-1}(\rho)(\vec{w}_{m-1}iw_{m})$
since $\tau^{\prime}\circ\sigma_{m-1}$ satisfies condition (R1) for runs in
$\mathfrak{Q}^{\prime}$, as required.

  4. 4.

for
$\vec{v}^{\prime}=(\vec{w}_{0},\sigma_{0})i_{0}(\vec{w}_{1},\sigma_{1})i_{1}\cdots
i_{m-2}(\vec{w}_{m-1},\sigma_{m-1})$ and $i_{m-1}=i$ we have
$\vec{v}=\vec{v}^{\prime}i(\vec{w}_{m-1}iw_{m}^{\prime},\sigma_{m}^{\prime})$
for some $(w_{m}^{\prime},\sigma_{m}^{\prime})$ with
$\vec{w}_{m-1}iw_{m}^{\prime}\in W^{\prime}$ and
$\sigma_{m}^{\prime}=\tau\circ\sigma_{m-1}$ for some
$\tau\in\text{Rep}(\vec{w}_{m-1})$. We can then first show that
$\Diamond_{i}C\in\rho^{\uparrow}(\vec{v}^{\prime})$ in exactly the same way as
in the proof of Point 2. Now we can argue in the same way as in the proof of
Point 3 and using (R3) that $\Diamond_{i}C\in\rho^{\uparrow}(\vec{u})$.

For (R2), assume $\Diamond_{i}C\in\rho^{\uparrow}(\vec{u})$. We have to show
that there exists $\vec{v}\in W^{\prime\prime}$ such that
$\vec{u}R_{i}^{\prime\prime}\vec{v}$ and $C\in\rho^{\uparrow}(\vec{v})$. We
have $\rho^{\uparrow}(\vec{u})=\sigma_{m}(\rho)(\vec{w}_{m})$ and distinguish
the following three cases:

  1. 1.

$C\in\sigma_{m}(\rho)(\vec{w}_{m})$. Then we are done since then for
$\vec{v}=\vec{u}$ we have $C\in\rho^{\uparrow}(\vec{v})$ and we have
$\vec{u}R_{i}^{\prime\prime}\vec{v}$.

  2. 2.

for ${\boldsymbol{t}}=\sigma_{m}(\rho)(\vec{w}_{m})$ we have for the proto-run
$\rho_{\vec{w}_{m},{\boldsymbol{t}}}\in\mathfrak{R}$ that there is a proto-
witness $\vec{w}_{m+1}=v_{\vec{w}_{m},i,C,{\boldsymbol{t}}}\in W^{\prime}$ of
the form $\vec{w}_{m}iw_{m+1}$. Then
$C\in\rho_{\vec{w}_{m},{\boldsymbol{t}}}(\vec{w}_{m+1})$.

Then let $\vec{v}=\vec{u}i(\vec{w}_{m+1},\tau\circ\sigma_{m})$ where $\tau$
swaps $\sigma_{m}(\rho)$ with $\rho_{\vec{w}_{m},{\boldsymbol{t}}}$. We have
$\vec{u}R_{i}^{\prime\prime}\vec{v}$ and
$\rho^{\uparrow}(\vec{v})=\tau\circ\sigma_{m}(\rho)(\vec{w}_{m+1})=\rho_{\vec{w}_{m},{\boldsymbol{t}}}(\vec{w}_{m+1})$.
So $C\in\rho^{\uparrow}(\vec{v})$, as required.

  3. 3.

$i_{m-1}=i$ and $\Diamond_{i}C\in\sigma_{m-1}(\rho)(\vec{w}_{m-1})$. If
$C\in\sigma_{m-1}(\rho)(\vec{w}_{m-1})$, then $C\in\rho^{\uparrow}(\vec{v})$
for $\vec{v}=(\vec{w}_{0},\sigma_{0})i_{0}(\vec{w}_{1},\sigma_{1})i_{1}\cdots
i_{m-2}(\vec{w}_{m-1},\sigma_{m-1})$ and we are done.

Otherwise we can proceed with $\sigma_{m-1}(\rho)(\vec{w}_{m-1})$ in the same
way as we did with $\sigma_{m}(\rho)(\vec{w}_{m})$ in Point 2 and find for
$\vec{v}^{\prime}=(\vec{w}_{0},\sigma_{0})i_{0}(\vec{w}_{1},\sigma_{1})i_{1}\cdots
i_{m-2}(\vec{w}_{m-1},\sigma_{m-1})$ a
$\vec{v}=\vec{v}^{\prime}i(\vec{w}_{m-1}iw_{m}^{\prime},\sigma_{m}^{\prime})$
for some $(w_{m}^{\prime},\sigma_{m}^{\prime})$ with
$\vec{w}_{m-1}iw_{m}^{\prime}\in W^{\prime}$ and
$\sigma_{m}^{\prime}=\tau\circ\sigma_{m-1}$ for some
$\tau\in\text{Rep}(\vec{w}_{m-1})$ such that $C\in\rho^{\uparrow}(\vec{v})$.

Clearly, the quasimodel
$(\mathfrak{F}^{\prime\prime},\boldsymbol{q}^{\prime\prime},\mathfrak{R}^{\prime\prime})$
is of at most exponential size, as required. ∎

The exponential finite model property now follows from Lemma 25 using Lemma
24. ∎

See 12

As before, it suffices to consider total concept satisfiability under
ontologies without definite descriptions. For
$\mathbf{K}\\!\boldsymbol{f}^{\ast n}_{\smash{\mathcal{ALCO}_{\\!u}}}$, the
decidability proof for concept satisfiability without ontologies is easily
extended to a proof with ontologies, so we consider concept satisfiability
without ontology. Call a finite frame $\mathfrak{F}=(W,R_{1},\ldots,R_{n},R)$
a _finite tree-shaped_ frame if $R$ is the transitive closure of
$R_{1}\cup\cdots\cup R_{n}$ and there exists a $w_{0}\in W$ such that the
domain $W$ of $\mathfrak{F}$ is a prefix closed set of words of the form

$\vec{w}=w_{0}i_{0}w_{1}\cdots i_{n-1}w_{m}$ (9)

where $1\leq i_{j}\leq n$, and

$R_{i}=\\{(\vec{w},\vec{w}iw)\mid\vec{w}iw\in W\\}.$

We call $w_{0}$ the root of $\mathfrak{F}$. A _finite tree-shaped model_ takes
the form $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$ with $\mathfrak{F}$
a finite tree-shaped frame. A straightforward unfolding argument shows that
any $\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept
that is satisfiable in a $\mathbf{K}\\!\boldsymbol{f}^{\ast
n}_{\smash{\mathcal{ALCO}_{\\!u}}}$-model is also satisfiable in a finite
tree-shaped model. So we start with finite tree-shaped models.

Given an
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept
$C_{0}$, let $\mathsf{con}(C_{0})$ be the closure under single negation of the
set of concepts occurring in $C_{0}$. A _type_ for $C_{0}$ is a subset
${\boldsymbol{t}}$ of $\mathsf{con}(C_{0})$ such that

  1. C1

$\neg C\in{\boldsymbol{t}}$ iff $C\not\in{\boldsymbol{t}}$, for all $\neg
C\in\mathsf{con}(C_{0})$;

  2. C2

$C\sqcap D\in{\boldsymbol{t}}$ iff $C,D\in{\boldsymbol{t}}$, for all $C\sqcap
D\in\mathsf{con}(C_{0})$.

Note that there are at most $2^{|\mathsf{con}(C_{0})|}$ types for $C_{0}$. We
fix an ordering ${\boldsymbol{t}}_{1},\ldots,{\boldsymbol{t}}_{k}$ of the set
of types for $C_{0}$. We use vectors
$\vec{x}=(x_{1},\ldots,x_{k})\in(\mathbb{N}\cup\\{\infty\\})^{k}$ to represent
that the type ${\boldsymbol{t}}_{i}$ is satisfied by $x_{i}$-many elements in
a world $w$, for $1\leq i\leq n$. Let $|\vec{x}|=\sum_{i=1}^{k}x_{i}$. A
_quasistate_ for $C_{0}$ is a vector
$\vec{x}=(x_{1},\ldots,x_{k})\in(\mathbb{N}\cup\\{\infty\\})^{k}$ with
$|\vec{x}|>0$ satisfying the following conditions:

  1. Q1

for every $\\{a\\}\in\mathsf{con}(C_{0})$,

$\sum_{\\{a\\}\in{\boldsymbol{t}}_{i}}x_{i}=1;$

  2. Q2

for every $x_{i}>0$ and every $\exists r.C\in{\boldsymbol{t}}_{i}$, there
exists $x_{j}>0$ such that $\\{\lnot D\mid\lnot\exists
r.D\in{\boldsymbol{t}}_{i}\\}\cup\\{C\\}\subseteq{\boldsymbol{t}}_{j}$;

  3. Q3

for every $x_{i}>0$ and $\exists u.C\in{\boldsymbol{t}}_{i}$ iff there exists
$x_{j}>0$ with such that $C\in{\boldsymbol{t}}_{j}$.

A _basic structure for $C_{0}$_ is a pair $(\mathfrak{F},\boldsymbol{q})$,
where $\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ is a finite tree-shaped frame with
root $w_{0}$ and $\boldsymbol{q}$ is a function associating with every $w\in
W$ a quasistate $\boldsymbol{q}(w)$ for $C_{0}$, satisfying

  1. B1

there exists $i\leq k$ with $\boldsymbol{q}(w_{0})_{i}>0$ such that
$C_{0}\in{\boldsymbol{t}}_{i}$.

Call a subset $V$ of $W$ _$R_{i}$ -closed_ if $v\in V$ whenever $w\in V$ and
$wR_{i}v$. Call $V$ _$R$ -closed_ if $V$ is $R_{i}$-closed for $1\leq i\leq
n$. A _run through $(\mathfrak{F},\boldsymbol{q})$_ is a partial function
$\rho$ mapping worlds $w\in W$ to natural numbers $\rho(w)\leq k$ with
$\boldsymbol{q}(w)_{\rho(w)}>0$ such that the domain of $\rho$ is $R$-closed
and satisfies the following condition for every
$\Diamond_{i}C\in\mathsf{con}(C_{0})$:

  1. R1

$\Diamond_{i}C\in{\boldsymbol{t}}_{\rho(w)}$ if there exists $v\in W$ such
that $wR_{i}v$ and $C\in{\boldsymbol{t}}_{\rho(v)}$;

  2. R2

if $\Diamond_{i}C\in{\boldsymbol{t}}_{\rho(w)}$ then there exists $v\in W$
such that $wR_{i}v$ and $C\in{\boldsymbol{t}}_{\rho(v)}$.

A _quasimodel for $C_{0}$_ is a triple
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$, where
$(\mathfrak{F},\boldsymbol{q})$ is a basic structure for $C_{0}$, and
$\mathfrak{R}$ is a set of runs through $(\mathfrak{M},\boldsymbol{q})$ such
that the following condition holds:

  1. M1

for every $w\in W$ and every $i\leq k$,

$|\\{\rho\in\mathfrak{R}\mid\rho(w)=i\\}|=\boldsymbol{q}(w)_{i}.$

The following lemma provides a link between quasimodels for $C_{0}$ and models
satisfying $C_{0}$.

######  Lemma 26.

An $\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept
$C_{0}$ is satisfiable in the root of a finite tree-shaped model iff there
exists a quasimodel for $C_{0}$ based on the same frame.

###### Proof.

$(\Rightarrow)$ Let $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, with
$\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ be a finite tree-shaped model with
$C^{\mathcal{I}_{w_{0}}}\not=\emptyset$ for the root $w_{0}$ of
$\mathfrak{F}$. Let
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)=\\{C\in\mathsf{con}(C_{0})\mid d\in
C^{\mathcal{I}_{w}}\\}$, for every $d\in\Delta$ and $w\in W$. Clearly,
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)$ is a type for $C_{0}$ since it
satisfies (C1)–(C2). We now define a triple
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$, where

  * •

$\boldsymbol{q}$ is the function from $W$ to the set of quasistates for
$C_{0}$ defined by setting $\boldsymbol{q}(w)=(x_{1},\ldots,x_{k})$ with

$x_{i}=|\\{d\in\Delta^{w}\mid{\boldsymbol{t}}^{\mathcal{I}_{w}}(d)={\boldsymbol{t}}_{i}\\}|$

for $1\leq i\leq k$ and every $w\in W$;

  * •

$\mathfrak{R}$ is the set of functions $\rho_{d}$ from $W$ to
$\\{1,\ldots,k\\}$ defined by setting $\rho_{d}(w)=i$ if
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)={\boldsymbol{t}}_{i}$, for every
$d\in\Delta$ and $w\in W$.

It is easy to show that $\mathfrak{Q}$ is a quasimodel for $C_{0}$.

$(\Leftarrow)$ Suppose there is a quasimodel
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$ for $C_{0}$. Define
a model $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, by setting
$\Delta^{w}=\\{\rho\in\mathfrak{R}\mid w\in\text{dom}(\rho)\\}$, and, for any
$A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$ and $a\in{\sf N_{I}}$:

  * •

$A^{\mathcal{I}_{w}}=\\{\rho\in\Delta^{w}\mid A\in\rho(w)\\}$;

  * •

$r^{\mathcal{I}_{w}}=\\{(\rho,\rho^{\prime})\in\Delta^{w}\times\Delta^{w}\mid\\{\lnot
C\mid\lnot\exists r.C\in\rho(w)\\}\subseteq\rho^{\prime}(w)\\}$;

  * •

$u^{\mathcal{I}_{w}}=\Delta^{w}\times\Delta^{w}$;

  * •

$a^{\mathcal{I}_{w}}=\rho$, for the unique $\rho\in\Delta^{w}$ such that
$\\{a\\}\in\rho(w)$.

Observe that $\Delta$ is well-defined and expanding since $|\vec{x}|>0$ for
every quasistate $\vec{x}$ and since the domain of each $\rho\in\mathfrak{R}$
is $R$-closed. The following claim is now straightforward from the definition
of quasimodels for $C_{0}$.

######  Claim 6.

For every $C\in\mathsf{con}(C_{0})$, $w\in W$ and $\rho\in\Delta$, $\rho\in
C^{\mathcal{I}_{w}}$ iff $C\in{\boldsymbol{t}}_{\rho(w)}$.

Now we can easily finish the proof of the proposition by observing that, by
(B1), there exists $i\leq k$ with $\boldsymbol{q}(w_{0})_{i}>0$ such that
$C_{0}\in{\boldsymbol{t}}_{i}$. Then there exists a $\rho\in\mathfrak{R}$ with
$\rho(w_{0})=i$. Hence, by the above claim, $\rho\in
C_{0}^{\mathcal{I}_{w_{0}}}$. ∎

The _size_ of a quasimodel
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$ with
$\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ is defined as

$|W|\times\max\\{|\boldsymbol{q}(w)|\mid w\in W\\}.$

Our next aim is to show that there exists a quasimodel for $C_{0}$ of size
bounded by a recursive function in $|C_{0}|$ (in particular with
$|\boldsymbol{q}(w)|<\infty$ for all $w$). We are going to apply Dickson’s
Lemma. For some $k>0$, let $(\mathbb{N}^{k},\leq)$ be the set of $k$-tuples of
natural numbers ordered by the natural product ordering: for
$\vec{x}=(x_{1},\ldots,x_{k})$ and $\vec{y}=(y_{1},\ldots,y_{k})$ we set
$\vec{x}\leq\vec{y}$ if $x_{i}\leq y_{i}$ for $1\leq i\leq k$. A pair
$\vec{x},\vec{y}$ with $\vec{x}\leq\vec{y}$ is called an _increasing pair_.
Dickson’s Lemma states every infinite sequence
$\vec{x}_{1},\vec{x}_{2},\ldots\in\mathbb{N}^{k}$ contains an increasing pair
$\vec{x}_{i_{1}},\vec{x}_{i_{2}}$ with $i_{1}<i_{2}$. In fact, assuming
$|\vec{x}_{i}|\leq|\vec{x}_{i+1}|$ for all $i\geq 0$ and given recursive
bounds on $|\vec{x}_{1}|$ and $|\vec{x}_{i+1}|-|\vec{x}_{i}|$ one can compute
a recursive bound on the length of the longest sequence without any increasing
pair (?).

Assume a finite tree-shaped frame $\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ with
root $w_{0}$ and worlds of the form (9) is given. Then we say that $\vec{w}$
is the _predecessor_ of $\vec{w}iw\in W$ in $\mathfrak{F}$ and that
$\vec{w}iw\in W$ is a _successor_ of $\vec{w}$ in $\mathfrak{F}$. Worlds
reachable along a path of predecessors from a world are called _ancestors_ and
worlds reachable along a path of successors from a world are called
_descendants_. We set $\vec{w}<\vec{w}^{\prime}$ if $\vec{w}$ is a predecessor
of $\vec{w}^{\prime}$ and $W_{\vec{w}}=\\{\vec{w}\\}\cup\\{\vec{v}\in
W\mid\vec{w}<\vec{v}\\}$.

We now show that one can reduce quasimodels for $C_{0}$ to quasimodels for
$C_{0}$ not having increasing pairs
$|\boldsymbol{q}(\vec{w})|,|\boldsymbol{q}(\vec{w}^{\prime})|$ with
$\vec{w}<\vec{w}^{\prime}$ and satisfying recursive bounds for
$|\boldsymbol{q}(w_{0})|$,
$|\boldsymbol{q}(\vec{w}iw)|-|\boldsymbol{q}(\vec{w})|$, and the outdegree of
each $\vec{w}$. We then obtain a recursive bound on the size of such
quasimodels from Dickson’s Lemma.

######  Lemma 27.

There exists a quasimodel for $C_{0}$ iff there exists a quasimodel
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$ for $C_{0}$ with

  1. 1.

$|\boldsymbol{q}(w_{0})|\leq 2^{|C_{0}|}$, for the root $w_{0}$ of
$\mathfrak{Q}$;

  2. 2.

if $v$ is a successor of $w$, then
$|\boldsymbol{q}(v)|\leq|\boldsymbol{q}(w)|+2^{|C_{0}|}$;

  3. 3.

if $w<v$, then $\boldsymbol{q}(w)\not\leq\boldsymbol{q}(v)$;

  4. 4.

the outdgree of $w$ in $\mathfrak{F}$ is bounded by
$|\boldsymbol{q}(w)|\times|C_{0}|$.

###### Proof.

Assume that a quasimodel $\mathfrak{Q}$ for $C_{0}$ with
$\mathfrak{Q}=(\mathfrak{F},\boldsymbol{q},\mathfrak{R})$ and
$\mathfrak{F}=(W,R_{1},\ldots,R_{n})$ with root $w_{0}$ is given. We may
assume that every run $\rho\in\mathfrak{R}$ has a _root_ $w\in W$ in the sense
that $W_{w}=\text{dom}(\rho)$. We let $\mathfrak{R}_{w}$ denote the set of
runs with root $w$. We introduce a few rules that allow us to modify
$\mathfrak{Q}$:

_Minimize root._ Assume $\boldsymbol{q}(w_{0})=(x_{1},\ldots,x_{k})$. Pick for
any $x_{i}>0$ a single $\rho_{i}\in\mathfrak{R}$ with $\rho_{i}(w_{0})=i$. Now
construct an updated
$\mathfrak{Q}^{\prime}=(\mathfrak{F}^{\prime},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$
by defining

  * •

$\mathfrak{F}^{\prime}=\mathfrak{F}$,

  * •

$\boldsymbol{q}^{\prime}(w_{0})=(\min\\{x_{1},1\\},\ldots,\min\\{x_{k},1\\})$
and $\boldsymbol{q}^{\prime}(w)=\boldsymbol{q}(w)$ for all $w\not=w_{0}$,

  * •

$\mathfrak{R}^{\prime}$ as the set of selected runs $\rho_{i}$, all runs in
$\mathfrak{R}\setminus\mathfrak{R}_{w_{0}}$, and the restrictions of all
remaining $\rho\in\mathfrak{R}_{w_{0}}$ to $W_{w}$ for $w$ a successor of
$w_{0}$.

It is easy to see that $\mathfrak{Q}^{\prime}$ is a quasimodel for $C_{0}$
satisfying Condition 1.

_Minimize non-root_ : Assume $v$ is a successor of $w$ and
$\boldsymbol{q}(v)=(x_{1},\ldots,x_{k})$. Call $i\leq k$ increasing at $v$ if
there exists $\rho_{i}\in\mathfrak{R}_{v}$ such that $\rho_{i}(v)=i$. Select
for any such $i$ such a $\rho_{i}\in\mathfrak{R}_{v}$. We construct an updated
$\mathfrak{Q}^{\prime}=(\mathfrak{F}^{\prime},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$
by defining

  * •

$\mathfrak{F}^{\prime}=\mathfrak{F}$,

  * •

$\boldsymbol{q}^{\prime}(v)=(x_{i}^{\prime},\ldots,x_{k}^{\prime})$ with

$x_{i}^{\prime}=|\\{\rho\in\mathfrak{R}\mid
w\in\text{dom}(\rho),\rho(v)=i\\}|+1$

if $i$ is increasing at $v$ and $x_{i}^{\prime}=x_{i}$ otherwise. Set
$\boldsymbol{q}^{\prime}(w^{\prime})=\boldsymbol{q}(w^{\prime})$ for all
$w^{\prime}\not=v$.

  * •

$\mathfrak{R}^{\prime}$ as the set of selected runs $\rho_{i}$, all runs in
$\mathfrak{R}\setminus\mathfrak{R}_{v}$, and the restrictions of all remaining
$\rho\in\mathfrak{R}_{v}$ to $W_{v^{\prime}}$ for $v^{\prime}$ a successor of
$v$.

It is easy to see that $\mathfrak{Q}^{\prime}$ is a quasimodel for $C_{0}$
satisfying Condition 2 for $w$ and $v$.

_Drop interval 1_ : Consider $\vec{w}=\vec{w}^{\prime}iw\in W$ and
$\vec{v}=\vec{v^{\prime}}jv\in W$ with $\vec{w}<\vec{v}$ and

  * •

$\boldsymbol{q}(\vec{w})=(x_{1},\ldots,x_{k})$;

  * •

$\boldsymbol{q}(\vec{v})=(y_{1},\ldots,y_{k})$;

  * •

$x_{i}\leq y_{i}$ for all $i\leq k$.

Now construct an updated
$\mathfrak{Q}^{\prime}=(\mathfrak{F}^{\prime},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$
by defining

  * •

$\mathfrak{F}^{\prime}$ is the frame determined by $W^{\prime}$ with

$W^{\prime}=(W\setminus
W_{\vec{w}})\cup\\{\vec{w}^{\prime}i\vec{r}\mid\vec{v}^{\prime}j\vec{r}\in
W_{\vec{v}}\\}.$

  * •

Set $\boldsymbol{q}^{\prime}(\vec{u})=\boldsymbol{q}(\vec{u})$ for all
$\vec{u}\in W\setminus W_{\vec{w}}$ and
$\boldsymbol{q}^{\prime}(\vec{w}^{\prime}i\vec{r})=\boldsymbol{q}(\vec{v}^{\prime}j\vec{r})$
for all $\vec{v}^{\prime}j\vec{r}\in W_{\vec{v}}$.

  * •

Take for any $\rho\in\mathfrak{R}$ with $\vec{w}^{\prime}\in\text{dom}(\rho)$
a $f(\rho)\in\mathfrak{R}$ with $\vec{v}\in\text{dom}(f(\rho))$ such that
$f(\rho)(\vec{v})=\rho(\vec{w})$. We can ensure that all $f(\rho)$ are
distinct since $x_{i}\leq y_{i}$ for all $i\leq k$. Then let
$\rho^{\prime}\in\mathfrak{R}^{\prime}$ with $\rho^{\prime}$ defined by
setting $\rho^{\prime}(\vec{u})=\rho(\vec{u})$ for $\vec{u}\in W\setminus
W_{\vec{w}}$ and
$\rho^{\prime}(\vec{w}^{\prime}i\vec{r})=f(\rho)(\vec{v}^{\prime}j\vec{r})$
for all $\vec{v}^{\prime}j\vec{r}\in W_{\vec{v}}$.

Also add all $\rho\in\mathfrak{R}$ with $\text{dom}(\rho)\cap
W_{\vec{w}}=\emptyset$ to $\mathfrak{R}^{\prime}$. Finally, for all $\rho$
with $\text{dom}(\rho)\subseteq W_{\vec{w}}$ which were not selected as an
$f(\rho)$, add the $\rho^{\prime}$ to $\mathfrak{R}^{\prime}$ defined by
setting
$\rho^{\prime}(\vec{w}^{\prime}i\vec{r})=\rho(\vec{v}^{\prime}j\vec{r})$ for
all $\vec{v}^{\prime}j\vec{r}\in W_{\vec{v}}$.

It is easy to see that $\mathfrak{Q}^{\prime}$ is a quasimodel for $C_{0}$.

_Drop interval 2_ : Consider the root $w_{0}$ and $v\in W$ with

  * •

$\boldsymbol{q}(w_{0})=(x_{1},\ldots,x_{k})$;

  * •

$\boldsymbol{q}(v)=(y_{1},\ldots,y_{k})$;

  * •

$x_{i}\leq y_{i}$ for all $i\leq k$.

Then construct an updated
$\mathfrak{Q}^{\prime}=(\mathfrak{F}^{\prime},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$
by restricting $\mathfrak{Q}$ to $W_{v}$ in the obvious way.

_Restrict outdegree_. Consider $\vec{w}\in W$ and assume
$\boldsymbol{q}(\vec{w})=(x_{1},\ldots,x_{k})$. To bound the number of
successors of $\vec{w}$ to $|\boldsymbol{q}(\vec{w})|\times|C_{0}|$ pick for
every $j\leq k$ with $x_{j}>0$ and every
$\Diamond_{i}C\in{\boldsymbol{t}}_{j}$ for every run $\rho\in\mathfrak{R}$
with $\rho(\vec{w})=j$ a successor $\vec{w}iw\in W$ with
$C\in{\boldsymbol{t}}_{\rho(\vec{w}iw)}$ or
$\Diamond_{i}C\in{\boldsymbol{t}}_{\rho(\vec{w}iw)}$. Let $V$ be the set of
successors of $W$ picked in this way. Then construct an updated
$\mathfrak{Q}^{\prime}=(\mathfrak{F}^{\prime},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$
by restricting $\mathfrak{Q}$ to

$W^{\prime}=(W\setminus W_{\vec{w}})\cup\\{\vec{w}\\}\cup\bigcup_{\vec{v}\in
V}W_{\vec{v}}.$

It is easy to see that $\mathfrak{Q}^{\prime}$ is a quasimodel for $C_{0}$
such that the outdegree of $\vec{w}$ is bounded by
$|\boldsymbol{q}(\vec{w})|\times|C_{0}|$.

By applying the rules above exhaustively, we obtain a quasimodel satisfying
the conditions of the lemma. ∎

As argued above, it follows from Lemma 27 that we have a recursive bound on
the size of a quasimodel for $C_{0}$. By Lemma 26, we then also have a
recursive bound on the size of a finite tree-shaped model satisfying $C_{0}$.
This shows the decidability of concept-satisfiability for
$\mathbf{K}\\!\boldsymbol{f}^{\ast n}_{\smash{\mathcal{ALCO}_{\\!u}}}$ in
expanding domain models.

We now discuss concept satisfiability for
$\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ and
$\mathbf{Grz}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ under expanding
domains. We focus on
$\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$,
$\mathbf{Grz}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ can be treated
similarly. Note that a straightforward selective filtration argument applied
to appropriate quasimodels shows that in
$\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ over expanding
domain models every satisfiable concept is satisfied in a finite model. This
observation implies that a
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$-concept
$C$ with a single modal operator is satisfiable in an expanding domain model
for $\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ iff it is
satisfiable in a model for $\mathbf{K}\\!\boldsymbol{f}^{\ast
n}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ with expanding domains,
where the modal operator in $C$ is interpreted by the transitive closure of
$R_{1}\cup\cdots\cup R_{n}$. Hence the decidability of concept-satisfiability
for $\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ over
expanding domain models is a consequence of the decidability of concept
satisfiability for $\mathbf{K}\\!\boldsymbol{f}^{\ast
n}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ over expanding domain
models.

The decidability of concept-satisfiability for
$\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ over expanding
domain models can also be derived from decidability results for expanding
domain product modal logics. We define the relevant modal logics using DL
syntax. Consider the modal DL with a single role, $o$, interpreted as a
Noetherian strict linear order. In DL syntax, concepts in
$\mathcal{ML}^{n}_{lin}$ are of the form

$C::=A\mid\lnot C\mid(C\sqcap C)\mid\exists o.C\mid\Diamond_{i}C,$

where $i\in I$.

######  Theorem 28.

Let $\mathcal{C}$ be a class of frames. Then $\mathcal{C}$-satisfiability of
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concepts
can be reduced in double exponential time to $\mathcal{C}$-satisfiability of
$\mathcal{ML}^{n}_{lin}$-concepts, both with constant and expanding domains.

###### Proof.

The proof is similar to the proof of Theorem 10 (1). Assume an
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept $C$
is given. Assume for simplicity that $C$ contains a single modal operator,
denoted by $\Box$. Let $m$ be the modal depth of $C$. Let $\mathsf{con}(C)$ be
the closure under single negation of the set of concepts occurring in $C$. A
_type_ for $C$ is a subset ${\boldsymbol{t}}$ of $\mathsf{con}(C)$ such that
$\neg C\in{\boldsymbol{t}}$ iff $C\not\in{\boldsymbol{t}}$, for all $\neg
C\in\mathsf{con}(\mathcal{O})$. A _quasistate for $D$_ is a non-empty set
$\boldsymbol{T}$ of types for $C$. The _description of $\boldsymbol{T}$_ is
the $\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept

$\Xi_{\boldsymbol{T}}=\forall
u.(\bigsqcup_{{\boldsymbol{t}}\in\boldsymbol{T}}{\boldsymbol{t}})\sqcap\bigsqcap_{{\boldsymbol{t}}\in\boldsymbol{T}}\exists
u.{\boldsymbol{t}}.$

Let $\mathcal{S}_{C}$ denote the set of all quasistates $\boldsymbol{T}$ for
$C$ that are _$\smash{\mathcal{ALCO}_{\\!u}}$ -satisfiable_, that is, such
that $\Xi_{\boldsymbol{T}}^{t}$ is satisfiable, where
$\Xi_{\boldsymbol{T}}^{t}$ denotes the result of replacing every outermost
occurrence of $\Diamond_{i}D$ by $A_{\Diamond_{i}D}$, for a fresh concept name
$A_{\Diamond_{i}D}$. We know that $\mathcal{S}_{C}$ can be computed in double
exponential time.

Let $\exists o^{+}.D=D\sqcup\exists o.D$ and $\forall o^{+}.D=D\sqcap\forall
o.D$. We reserve for any $D\in\mathsf{con}(C)$ of the form $\\{a\\}$ or
$\exists r.D^{\prime}$ or $\exists u.D^{\prime}$ a fresh concept name $A_{D}$.
Define a mapping $\cdot^{\sharp}$ that associates with every
$\smash{\smash{\mathcal{ML}}^{n}_{\smash{\mathcal{ALCO}_{\\!u}}}}$-concept an
$\mathcal{ML}^{n}_{lin}$-concept by replacing outermost occurrences of
concepts of the form $\\{a\\}$ or $\exists r.D^{\prime}$ or $\exists
u.D^{\prime}$ by the respective fresh concept name.

Let $C^{\ast}$ denote the conjunction of:

  1. 1.

$C^{\sharp}$;

  2. 2.

$\Box^{\leq m}\bigsqcup_{\boldsymbol{T}\in\mathcal{S}_{C}}(\forall
o^{+}.(\bigsqcup_{{\boldsymbol{t}}\in\boldsymbol{T}}{\boldsymbol{t}}^{\sharp})\sqcap\bigsqcap_{{\boldsymbol{t}}\in\boldsymbol{T}}\exists
o^{+}.{\boldsymbol{t}}^{\sharp})$;

  3. 3.

$\Box^{\leq m}\bigsqcap_{\exists u.D\in\mathsf{con}(C)}(A_{\exists
u.D}\Leftrightarrow\exists o^{+}.D^{\sharp})$;

  4. 4.

$\Box^{\leq m}\exists o^{+}.\\{a\\}^{\sharp}$, for every $a$ in $C$;

  5. 5.

$\Box^{\leq m}\forall o^{+}.(\\{a\\}^{\sharp}\Rightarrow\forall
o.\neg\\{a\\}^{\sharp})$, for every $a$ in $C$.

The following lemma completes the proof of the reduction.

######  Lemma 29.

$C$ is $\mathcal{C}$-satisfiable iff $C^{\ast}$ is $\mathcal{C}$-satisfiable
in a $\mathcal{ML}^{n}_{lin}$-model, with constant and expanding domains.

∎

Now decidability of concept satisfiability for
$\mathbf{GL}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ over expanding
domain models follows from decidability of satisfiability of
$\mathcal{ML}^{1}_{lin}$-concepts in models with expanding domains and
transitive Noetherian frames (?).

##  Appendix E Proofs for Section 6

The following two theorems share the same proof below.

See 14

See 15

###### Proof.

The proofs of these two theorems rely on the following results: the problem of
satisfiability of $\mathcal{TL}^{\Diamond}_{\text{Diff}}$ concepts is known
(?) to be

  1. 1.

$\Sigma_{1}^{1}$-complete in constant-domain interpretations over
$(\mathbb{N},<)$;

  2. 2.

recursively enumerable, but undecidable in constant-domain interpretations
over finite flows of time;

  3. 3.

undecidable (co-r.e.) in expanding-domains interpretations over
$(\mathbb{N},<)$;

  4. 4.

decidable, but Ackermann-hard in expanding-domains interpretations over finite
flows of time.

As a consequence of Theorem 10 (2) and results 1–3 above, we obtain the
following: in constant-domain interpretations, concept satisfiability is
$\Sigma_{1}^{1}$-hard for
$\mathbf{LTL}^{\Diamond}_{\smash{\mathcal{ALCO}_{\\!u}}}$ and undecidable for
$\mathbf{LTL}\\!{\text{$\boldsymbol{f}$}}^{\Diamond}_{\smash{\mathcal{ALCO}_{\\!u}}}$,
while in expanding-domains interpretations, the problem is undecidable for
$\mathbf{LTL}^{\Diamond}_{\smash{\mathcal{ALCO}_{\\!u}}}$. As a consequence of
result 4, concept satisfiability in expanding-domains interpretations is
Ackermann-hard for
$\mathbf{LTL}\\!{\text{$\boldsymbol{f}$}}^{\Diamond}_{\smash{\mathcal{ALCO}_{\\!u}}}$.

To prove the results for the languages without the universal modality, we
first replace the satisfiability problem for a given concept, say, $C$, with
the satisfiability problem for a concept name $A$ under the global ontology
$\mathcal{O}=\\{A\equiv C\\}$. Next, we transform global ontology
$\mathcal{O}$ into normal form; see Lemma 4. Next, the reduction in Lemma 6
allows us to obtain the undecidability (including $\Sigma_{1}^{1}$-hardness)
and Ackermann-hardness results for the problem of concept satisfiability under
global ontology in languages without the universal role.

The membership in $\Sigma^{1}_{1}$ follows from the fact that the problem can
be encoded in second-order arithmetic with existential quantifiers over binary
predicate symbols for concept names and ternary predicate symbols for role
names.

To show decidability of concept satisfiability (under global ontology) for
$\mathbf{LTL}\\!{\text{$\boldsymbol{f}$}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$,
we first eliminate definite descriptions; see Proposition 8. The result then
is a consequence of Theorem 28 and the decidability results proved for concept
satisfiability in the language with both ‘next’ and ‘eventually’ (?, Theorem
3); note that for
$\mathbf{LTL}\\!{\text{$\boldsymbol{f}$}}^{\Diamond}_{\smash{\mathcal{ALCO}_{\\!u}}}$
this follows more directly from Theorem 10 (1) and the result 4 above. ∎

See 16

###### Proof.

We prove these results by reduction from the satisfiability under global
ontology in the languages based on $\smash{\mathcal{ALC}}$. Let $A$ be a
concept name and $\mathcal{O}$ a
$\smash{\mathcal{TL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ ontology. By
Lemma 4, we assume that $\mathcal{O}$ is in normal form. First, we eliminate
occurrences of $\neg$: every CI of the form $B_{1}\sqsubseteq\neg B_{2}$ is
replaced by $B_{1}\sqcap B_{2}\sqsubseteq\bot$ and every CI of the form $\neg
B_{1}\sqsubseteq B_{2}$ is first replaced by $\top\sqsubseteq B_{1}\sqcup
B_{2}$. Then, we eliminate the disjunction from the C by using the method
suggested in (?): each CI of the form $\top\sqsubseteq B_{1}\sqcup B_{2}$ is
replaced with the following:

$\displaystyle\top$ $\displaystyle\sqsubseteq\exists q.(\Diamond
X_{1}\sqcap\Diamond X_{2}),$ $\displaystyle\exists
q.\Diamond(X_{1}\sqcap\Diamond X_{2})$ $\displaystyle\sqsubseteq B_{1},$
$\displaystyle\exists q.\Diamond(X_{1}\sqcap X_{2})$ $\displaystyle\sqsubseteq
B_{1},$ $\displaystyle\exists q.\Diamond(X_{2}\sqcap\Diamond X_{1})$
$\displaystyle\sqsubseteq B_{2},$

where $q$ is a fresh role name, and $X_{1}$ and $X_{2}$ are fresh concept
names. One can clearly see that every interpretation $\mathfrak{M}^{\prime}$
satisfying the four CI above also satisfies $\top\sqsubseteq B_{1}\sqcup
B_{2}$. Indeed, for every $t\in\mathbb{N}$ and every $d\in\Delta^{t}$, there
is a $d^{\prime}\in\Delta^{t}$ such that $d^{\prime}\in(\Diamond
X_{i})^{\mathcal{I}_{t}}$, for $i=1,2$. Thus, $d^{\prime}\in
X_{i}^{\mathcal{I}_{t_{i}}}$, for $t_{i}>t$ and $i=1,2$. Depending on whether
$t_{1}\geq t_{2}$ or not, we have $d\in B_{i}^{\mathcal{I}_{t}}$ for either
$i=1$ or $i=2$, thus satisfying $\top\sqsubseteq B_{1}\sqcup B_{2}$.

Conversely, if $\top\sqsubseteq B_{1}\sqcup B_{2}$ is satisfied at all $w\in
W$ in some $\mathfrak{M}$ over $(\mathbb{N},<)$ such that the $\Delta^{t}$ is
countably infinite, for each $t\in\mathbb{N}$, then $\mathfrak{M}$ can be
extended by interpreting the fresh symbols to satisfy the four CIs above: for
every $t\in\mathbb{N}$ and every $d\in\Delta^{t}$, we pick a unique element
$d^{\prime}\in\Delta^{t}$ and make it the $q^{\mathcal{I}_{t}}$-successor of
$d$; since the domains are countably infinite, we can choose these
$q^{\mathcal{I}_{t}}$-successor in such a way that no $d^{\prime}$ is the
$q^{\mathcal{I}_{t_{1}}}$-successor of $d_{1}$ and the
$q^{\mathcal{I}_{t_{2}}}$-successor of $d_{2}$ for distinct pairs
$(t_{1},d_{1})$ and $(t_{2},d_{2})$. It now remains to define the
interpretation of $X_{1}$ and $X_{2}$: for every $t\in\mathbb{N}$ and every
$d\in\Delta^{t}$, let $d^{\prime}$ be the $q^{\mathcal{I}_{t}}$-successor of
$d$; if $d\in B_{1}^{\mathcal{I}_{t}}$, then we include $d^{\prime}$ in
$X_{1}^{\mathcal{I}_{t+1}}$ and in $X_{2}^{\mathcal{I}_{t+2}}$; otherwise, we
include $d^{\prime}$ in $X_{1}^{\mathcal{I}_{t+2}}$ and in
$X_{2}^{\mathcal{I}_{t+1}}$. The interpretation of $X_{1}$ and $X_{2}$ is
well-defined due to our assumption on the interpretation of $q$.

A similar transformation works for the finite flows, but we need to reserve
two last instants for the interpretation of $X_{1}$ and $X_{2}$. To achieve
this, we ‘relativise’ all CIs in a given ontology $\mathcal{O}$: every CI of
the form $C_{1}\sqsubseteq C_{2}$ is replaced by $\Diamond\Diamond\top\sqcap
C_{1}\sqsubseteq C_{2}$ (alternatively,
${\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}\top$
can be used). It should be clear that $\mathcal{O}$ is satisfied in an
interpretation based on a flow $([0,n],<)$ iff the relativised ontology
$\mathcal{O}^{\prime}$ is satisfied in an interpretation based on a flow
$([0,n+2],<)$; the two interpretations coincide on the first $n$ instants, but
the additional two instants are simply ignored by the relativised CIs and so,
all concept and role names can be assumed to be empty there. Now, we can apply
the procedure for eliminating the negation described above (note that the two
additional time instants can now be used to interpret $X_{1}$ and $X_{2}$ in
any suitable way).

So, we now have a
$\smash{\mathcal{TL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ ontology
$\mathcal{O}^{\prime}$ in normal form without any occurrences of the $\neg$
operator. We have also shown that $A$ is satisfied under $\mathcal{O}$ in an
interpretation based on an infinite (respectively, finite) flow and having
countably infinite domains iff $A$ is satisfied under $\mathcal{O}^{\prime}$
in an interpretation based on an infinite (respectively, finite) flow and
having countably infinite domains. It remains to eliminate $\bot$. To this
end, we again use the method suggested in (?) and take a fresh concept name
$L$ and replace all occurrences of $\bot$ with $L$. In addition, we extend
$\mathcal{O}^{\prime}$ with the following CIs:

$\displaystyle\exists s.L$ $\displaystyle\sqsubseteq L,\text{ for all role
names }s\text{ in }\mathcal{O}^{\prime},$ $\displaystyle\Diamond L$
$\displaystyle\sqsubseteq L.$

Denote the resulting ontology by $\mathcal{O}^{\prime\prime}$. We can easily
show that $A$ is satisfied under $\mathcal{O}^{\prime}$ iff $A\sqsubseteq L$
is _not_ entailed by $\mathcal{O}^{\prime\prime}$. ∎

See 17

###### Proof.

Let $C_{0}$ be an
$\smash{\mathcal{TL}}^{\textstyle\circ}_{\smash{\mathcal{ALCO}_{\\!u}}}$
concept. By Proposition 3, it is sufficient to consider total satisfiability.
Set $d=\mathit{md}(C_{0})$. Observe that $C_{0}$ is satisfiable in an
interpretation of the form $(\Delta,(\mathcal{I}_{t})_{t\in[0,n]})$ with
$n\in\mathbb{N}$ iff it is satisfiable in an interpretation of the form
$(\Delta,(\mathcal{I}_{t})_{t\in[0,n]})$ with $n\leq d$. Fix $m_{0}\leq d$.
Below, we give an exponential-time subroutine that checks satisfiability in an
interpretation of the form $(\Delta,(\mathcal{I}_{t})_{t\in[0,m_{0}]})$. By
going through all $m_{0}\leq d$, we obtain an exponential-time algorithm that
checks satisfiability for
$\mathbf{LTL}\\!{\text{$\boldsymbol{f}$}}^{\textstyle\circ}_{\smash{\mathcal{ALCO}_{\\!u}}}$
in constant domains, which, by Proposition 9, also gives the same upper bound
for the problem in expanding domains. An algorithm for
$\mathbf{LTL}^{\textstyle\circ}_{\smash{\mathcal{ALCO}_{\\!u}}}$ in constant
domains simply checks satisfiability in an interpretation of the form
$(\Delta,(\mathcal{I}_{t})_{t\in[0,m_{0}]})$ for $m_{0}=d$; the case of
expanding domains is again due to Proposition 9.

As before, a _type_ for $C_{0}$ is a subset ${\boldsymbol{t}}$ of
$\mathsf{con}(C_{0})$ such that

  1. C1

$\neg C\in{\boldsymbol{t}}$ iff $C\not\in{\boldsymbol{t}}$, for all $\neg
C\in\mathsf{con}(C_{0})$;

  2. C2

$C\sqcap D\in{\boldsymbol{t}}$ iff $C,D\in{\boldsymbol{t}}$, for all $C\sqcap
D\in\mathsf{con}(C_{0})$.

Denote by $\boldsymbol{T}$ the set of types for $C_{0}$. We clearly have
$|\boldsymbol{T}|\leq 2^{|\mathsf{con}(C_{0})|}$. Given an interpretation
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in[0,m_{0}]})$, denote by
${\boldsymbol{t}}^{\mathcal{I}_{i}}(d)$ the type realised by $d\in\Delta$ in
$\mathcal{I}_{i}$, for $i\leq m_{0}$.

The subroutine is an elimination procedure on the set of all
$(m_{0}+1)$-tuples $\rho$ of types
$({\boldsymbol{t}}_{0},\cdots,{\boldsymbol{t}}_{m_{0}})$, called _runs_. Runs
can be thought of as elements in $\boldsymbol{T}^{m_{0}+1}$ and so the number
of runs is bounded by $2^{|\mathsf{con}(C_{0})|(m_{0}+1)}$. The components of
a run $\rho$ are denoted $\rho(0),\dots,\rho(m_{0})$. We write

$\rho\rightarrow_{r,i}\rho^{\prime}$

if $C\in\rho^{\prime}(i)$ implies $\exists r.C\in\rho(i)$ for all $\exists
r.C\in\mathsf{con}(C_{0})$. Given an interpretation
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in[0,m_{0}]})$, denote by
$\rho^{\mathfrak{M}}_{d}=({\boldsymbol{t}}^{\mathcal{I}_{0}}(d),\ldots,{\boldsymbol{t}}^{\mathcal{I}_{m_{0}}}(d))$
the run realised by $d\in\Delta$ in $\mathfrak{M}$.

Let $a_{1},\ldots,a_{n}$ be the nominals in $C_{0}$. To construct the initial
set $\mathfrak{R}_{0}$ of runs, we fix two parameters:

  * •

an $(m_{0}+1)$-tuple $(U^{0},\ldots,U^{m_{0}})$ of _$u$ -types_, where each
$U^{i}$ is a set containing either $\exists u.C$ or $\neg\exists u.C$, for
every $\exists u.C\in\mathsf{con}(C_{0})$;

  * •

a set $\mathfrak{N}$ of at most $n(m_{0}+1)$ _nominal runs_
$\rho\in\boldsymbol{T}^{m_{0}+1}$ such that

    * –

$U^{i}\subseteq\rho(i)$, for all $\rho\in\mathfrak{N}$ and $i\leq m_{0}$, and

    * –

for every $\rho\in\mathfrak{N}$, there is $i\leq m_{0}$ such that
$\\{a_{j}\\}\in\rho(i)$, for some $1\leq j\leq n$;

    * –

for every $i\leq m_{0}$ and every $1\leq j\leq n$, there is exactly one
nominal run $\rho\in\mathfrak{N}$ such that $\\{a_{j}\\}\in\rho(i)$.

Then we take $\mathfrak{R}_{0}=\mathfrak{N}\cup\mathfrak{O}$, where
$\mathfrak{O}$ is the set of _all_ runs without nominals consistent with the
fixed $u$-types, that is, all runs $\rho\in\boldsymbol{T}^{m_{0}+1}$ such that

  * •

$U^{i}\subseteq\rho(i)$, for all $i\leq m_{0}$, and

  * •

$\\{a_{j}\\}\notin\rho(i)$, for all $i\leq m_{0}$ and $1\leq j\leq n$.

We now exhaustively apply the run elimination procedure and to remove each run
$\rho$ from $\mathfrak{R}_{0}$ that satisfies one of the following:

  * •

there is $i\leq m_{0}$ and
${\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}C\in\rho(i)$ and either $i=m_{0}$
or $i<m_{0}$ but $C\notin\rho(i+1)$;

  * •

there is $i<m_{0}$ and $C\in\rho(i+1)$ but
${\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}C\notin\rho(i)$, for
${\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}C\in\mathsf{con}(C_{0})$;

  * •

there is $i\leq m_{0}$ and $\exists u.C\in\rho(i)$ but there is no
$\rho^{\prime}$ with $C\in\rho^{\prime}(i)$;

  * •

there is $i\leq m_{0}$ and $\exists r.C\in\rho(i)$ but there is no
$\rho^{\prime}$ with $C\in\rho^{\prime}(i)$ and
$\rho\rightarrow_{r,i}\rho^{\prime}$.

Assume that $\mathfrak{R}$ is the remaining set of runs.

######  Lemma 30.

The following conditions are equivalent:

(1) $C_{0}$ is satisfiable in a total interpretation
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in[0,m_{0}]})$ such that

  * •

$U^{i}=\\{\exists u.C\in\mathsf{con}(C_{0})\mid(\exists
u.C)^{\mathcal{I}_{i}}=\Delta\\}\cup$
$\hskip 25.00003pt\\{\neg\exists u.C\in\mathsf{con}(C_{0})\mid(\exists
u.C)^{\mathcal{I}_{i}}=\emptyset\\}$, for $i\leq m_{0}$;

  * •

$\mathfrak{N}=\\{\rho_{a_{j}^{\mathcal{I}_{i}}}^{\mathfrak{M}}\mid i\leq
m_{0},1\leq j\leq n\\}$.

(2) the set $\mathfrak{R}$ of runs satisfies the following conditions:

  * •

$\mathfrak{N}\subseteq\mathfrak{R}$;

  * •

$C_{0}\in\rho(0)$ for some $\rho\in\mathfrak{R}$.

###### Proof.

If (1) holds, then take a witness total interpretation $\mathfrak{M}$. Let
$\mathfrak{R}^{\prime}$ be the set of runs $\rho_{d}^{\mathfrak{M}}$ for
$d\in\Delta$. It is easy to see that
$\mathfrak{R}\supseteq\mathfrak{R}^{\prime}\supseteq\mathfrak{N}$. Moreover,
$\rho^{\mathfrak{M}}_{d_{0}}$, for some $d_{0}\in C_{0}^{\mathcal{I}_{0}}$,
provides the requited witness run for (2).

Conversely, assume that (2) holds. Construct a total interpretation
$\mathfrak{M}$ by setting:

  * •

$\Delta=\mathfrak{R}$;

  * •

$a^{\mathcal{I}_{i}}=\rho$ iff $\\{a\\}\in\rho(i)$, for $i\leq m_{0}$;

  * •

$\rho\in A^{\mathcal{I}_{i}}$ iff $A\in\rho(i)$, for $i\leq m_{0}$;

  * •

$(\rho,\rho^{\prime})\in r^{\mathcal{I}_{i}}$ iff
$\rho\rightarrow_{r,i}\rho^{\prime}$, for $i\leq m_{0}$.

It is now easy to show that $\mathfrak{M}$ is well-defined and as required for
(1). ∎

The exponential-time subroutine for satisfiability in interpretations of
length $m_{0}+1$ is obtained by going through all $u$-types and sets of
nominal runs (of which there are only exponentially many). ∎

See 18

###### Proof.

The result is obtained by a reduction of the (undecidable) halting problem for
(two-counter) Minsky machines starting with $0$ as initial counter values (?;
?).

A _(two-counter) Minsky machine_ is a pair $M=(Q,P)$, where
$Q=\\{q_{0},\ldots,q_{L}\\}$ is a set of _states_ and
$P=(I_{0},\ldots,I_{L\mbox{-}1})$ is a sequence of _instructions_. We assume
$q_{0}$ to be the _initial state_ , and $q_{L}$ to be the _halting state_.
Moreover, the instruction $I_{i}$ is executed at state $q_{i}$, for $0\leq
i<L$. Each instruction $I$ can have one of the following forms, where
$r\in\\{r_{1},r_{2}\\}$ is a _register_ that stores non-negative integers as
values, and $q,q^{\prime}$ are states:

  1. 1.

$I=+(r,q)$ – add $1$ to the value of register $r$ and go to state $q$;

  2. 2.

$I=-(r,q,q^{\prime})$ – if the value of register $r$ is (strictly) greater
than $0$, subtract $1$ from the value of $r$ and go to state $q$; otherwise,
go to state $q^{\prime}$.

Given a Minsky machine $M$, a _configuration of $M$_ is a triple
$(q,v_{1},v_{2})$, where $q$ is a state of $M$ and $v_{1},v_{2}\in\mathbb{N}$
are the _values_ of registers $r_{1},r_{2}$, respectively. In the following,
we denote $\overline{k}={3-k}$, for $k\in\\{1,2\\}$. Given $i,j\geq 0$, we
write
$(q_{i},v_{1},v_{2})\Rightarrow_{M}(q_{j},v^{\prime}_{1},v^{\prime}_{2})$ iff
one of the following conditions hold:

  * •

$I_{i}=+(r_{k},q_{j})$, $v^{\prime}_{k}=v_{k}+1$ and
$v^{\prime}_{\overline{k}}=v_{\overline{k}}$;

  * •

$I_{i}=-(r_{k},q_{j},q^{\prime})$, $v_{k}>0$, $v^{\prime}_{k}=v_{k}-1$, and
$v^{\prime}_{\overline{k}}=v_{\overline{k}}$;

  * •

$I_{i}=-(r_{k},q^{\prime},q_{j})$, $v_{k}=v^{\prime}_{k}=0$, and
$v^{\prime}_{\overline{k}}=v_{\overline{k}}$.

Given an _input_ $(v_{1},v_{2})\in\mathbb{N}\times\mathbb{N}$, the
_computation of $M$ on input $(v_{1},v_{2})$_ is the (unique) longest sequence
of configurations
$(q^{0},v^{0}_{1},v^{0}_{2})\Rightarrow_{M}(q^{1},v^{1}_{1},v^{1}_{2})\Rightarrow_{M}\ldots$,
such that $q^{0}=q_{0}$, $v^{0}_{1}=v_{1}$ and $v^{0}_{2}=v_{2}$. We say that
$M$ _halts_ _on input_ $(0,0)$ if the computation of $M$ on input $(0,0)$ is
finite: thus, its initial configuration takes the form $(q_{0},0,0)$, while
its last configuration has the form $(q_{L},v_{1},v_{2})$, for some
$v_{1},v_{2}\in\mathbb{N}$. The _halting problem for Minsky machines_ is the
problem of deciding, given a Minsky machine $M$, whether $M$ halts on input
$(0,0)$. This problem is known to be undecidable; see, e.g., (?; ?).

To represent the computation of a Minsky machine $M$ on input $(0,0)$, we use
the temporal dimension to model successive configurations in the computation.
We introduce a concept name $Q_{i}$, for each state $q_{i}$ of $M$. Concept
names $R_{1},R_{2}$ are used to represent registers $r_{1},r_{2}$,
respectively: the value of register $r_{k}$ at any computation step will
coincide with the cardinality of the extension of $R_{k}$ at the corresponding
moment of time. The incrementation of the value of register $r_{k}$ is
modelled by requiring that the extension of concept $\lnot
R_{k}\sqcap{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}R_{k}$ is included in
that of nominal $\\{a_{k}\\}$; dually, the decrementation of register $r_{k}$
is modelled by including the extension of
$R_{k}\sqcap{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}\lnot R_{k}$ in the
nominal $\\{b_{k}\\}$. Since the individual names $a_{k}$ and $b_{k}$ are
interpreted _non-rigidly_ , the (unique) element added or subtracted from the
extension of $R_{k}$ will vary over time.

We first construct a
$\smash{\mathcal{TL}^{\textstyle\circ}_{\mathcal{ALCO}_{\\!u}}}$ ontology
$\mathcal{O}_{M}$ such that

  * •

$Q_{0}$ is satisfiable under $\mathcal{O}_{M}$ over $(\mathbb{N},<)$ iff
machine $M$ never halts on $(0,0)$;

  * •

$Q_{0}$ is satisfiable under $\mathcal{O}_{M}$ over finite flows of time iff
machine $M$ halts on $(0,0)$;

Then, Lemmas 4 and 6 can be used to replace the ontology $\mathcal{O}_{M}$
with a $\smash{\mathcal{TL}^{\textstyle\circ}_{\mathcal{ALCO}}}$ ontology
$\mathcal{O}_{M}$ with the same property, thus establishing the required
results.

We use the following CIs to ensure that concepts $Q_{i}$ representing states
are either empty or coincide with the whole domain at any moment of time:

  1. $(\textbf{S1})$

$\exists u.Q_{i}\sqsubseteq Q_{i}$, for all $0\leq i\leq L$;

  2. $(\textbf{S2})$

$Q_{i}\sqcap Q_{j}\sqsubseteq\bot$, for all $0\leq i<j\leq L$.

Next, we encode instructions. We begin with incrementation. An instruction of
the form $I_{i}=+(r_{k},q_{j})$ is represented by the following CIs:

  1. $(\textbf{I1})$

$Q_{i}\sqsubseteq\exists u.(\\{a_{k}\\}\sqcap\neg R_{k})$;

  2. $(\textbf{I2})$

$Q_{i}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}R_{k}\Leftrightarrow(R_{k}\sqcup\\{a_{k}\\})$;

  3. $(\textbf{I3})$

$Q_{i}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}R_{\overline{k}}\Leftrightarrow
R_{\overline{k}}$;

  4. $(\textbf{I4})$

$Q_{i}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}Q_{j}$.

An instructions of the form $I_{i}=-(r_{k},q_{j},q_{h})$ is represented by the
following CIs:

  1. $(\textbf{D1})$

$Q_{i}\sqcap\exists u.R_{k}\sqsubseteq\exists u.(\\{b_{k}\\}\sqcap R_{k})$;

  2. $(\textbf{D2})$

$Q_{i}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}R_{k}\Leftrightarrow(R_{k}\sqcap\neg\\{b_{k}\\})$;

  3. $(\textbf{D3})$

$Q_{i}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}R_{\overline{k}}\Leftrightarrow
R_{\overline{k}}$;

  4. $(\textbf{D4})$

$Q_{i}\sqcap\exists
u.R_{k}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}Q_{j}$;

  5. $(\textbf{D5})$

$Q_{i}\sqcap\neg\exists
u.R_{k}\sqsubseteq{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}Q_{h}$.

Given $\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in\mathfrak{T}})$, we say
that an instant $t\in\mathfrak{T}$ _encodes_ a configuration
$(q_{i},v_{1},v_{2})$ whenever $Q_{i}^{\mathcal{I}_{t}}=\Delta$ and
$|R_{k}^{\mathcal{I}_{t}}|=v_{k}$, for $k=1,2$. We show the following:

######  Claim 7.

For any $\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in\mathfrak{T}})$ that
satisfies $(\textbf{S1})$–$(\textbf{D5})$, if $t\in\mathfrak{T}$ encodes
$(q_{i},v_{1},v_{2})$ and
$(q_{i},v_{1},v_{2})\Rightarrow_{M}(q^{\prime},v^{\prime}_{1},v^{\prime}_{2})$,
then $t+1$ encodes $(q^{\prime},v^{\prime}_{1},v^{\prime}_{2})$.

###### Proof of Claim.

We consider the following cases.

  * •

Suppose $I_{i}=+(r_{k},q_{j})$. By $(\textbf{I4})$ with $(\textbf{S1})$, we
have $Q_{j}^{\mathcal{I}_{t+1}}=\Delta$, and thus $q^{\prime}=q_{j}$. Note
that, by $(\textbf{S2})$, $Q_{j^{\prime}}^{\mathcal{I}_{t+1}}=\emptyset$ for
any $j^{\prime}\neq j$. Then, by $(\textbf{I1})$, $a_{k}^{\mathcal{I}_{t}}$ is
defined and $a_{k}^{\mathcal{I}_{t}}\notin R_{k}^{\mathcal{I}_{t}}$. By
$(\textbf{I2})$,
$R_{k}^{\mathcal{I}_{t+1}}=R_{k}^{\mathcal{I}_{t}}\cup\\{a_{k}^{\mathcal{I}_{t}}\\}$,
whence $|R_{k}^{\mathcal{I}_{t+1}}|=|R_{k}^{\mathcal{I}_{t}}|+1$, and so
$v^{\prime}_{k}=v_{k}+1$. For the other counter, by $(\textbf{I3})$,
$R_{\overline{k}}^{\mathcal{I}_{t+1}}=R_{\overline{k}}^{\mathcal{I}_{t}}$,
whence $v^{\prime}_{\overline{k}}=v_{\overline{k}}$.

  * •

Suppose $I_{i}=-(r_{k},q_{j},q_{h})$. By $(\textbf{D4})$ with $(\textbf{S1})$,
if $R_{k}^{\mathcal{I}_{t}}\neq\emptyset$, then
$Q_{j}^{\mathcal{I}_{t+1}}=\Delta$, and thus $q^{\prime}=q_{j}$. Otherwise, if
$R_{k}^{\mathcal{I}_{t}}=\emptyset$, then, by $(\textbf{D5})$ with
$(\textbf{S1})$, $Q_{h}^{\mathcal{I}_{t+1}}=\Delta$, and thus
$q^{\prime}=q_{h}$. Note that in either case, by $(\textbf{S2})$,
$Q_{j^{\prime}}^{\mathcal{I}_{t+1}}=\emptyset$ for any other $j^{\prime}$. We
next deal with the values of counters. If
$R_{k}^{\mathcal{I}_{t}}\neq\emptyset$, then, by $(\textbf{D1})$,
$b_{k}^{\mathcal{I}_{t}}$ is defined and $b_{k}^{\mathcal{I}_{t}}\in
R_{k}^{\mathcal{I}_{t}}$. Then, by $(\textbf{D2})$, we have
$R_{k}^{\mathcal{I}_{t+1}}=R_{k}^{\mathcal{I}_{t}}\setminus\\{b_{k}^{\mathcal{I}_{t}}\\}$.
It follows that $|R_{k}^{\mathcal{I}_{t+1}}|=|R_{k}^{\mathcal{I}_{t}}|-1$ and
so $v^{\prime}_{k}=v_{k}-1$. On the other hand, if
$R_{k}^{\mathcal{I}_{t}}=\emptyset$, then, by $(\textbf{D2})$,
$R_{k}^{\mathcal{I}_{t+1}}=\emptyset$ and so $v^{\prime}_{k}=v_{k}=0$. For the
other counter, by $(\textbf{D3})$,
$R_{\overline{k}}^{\mathcal{I}_{t+1}}=R_{\overline{k}}^{\mathcal{I}_{t}}$,
whence $v^{\prime}_{\overline{k}}=v_{\overline{k}}$.

So, in each case, $t+1$ encodes $(q^{\prime},v_{1}^{\prime},v_{2}^{\prime})$.
∎

It remains to encode the initial configuration and the acceptance condition.
For the initial configuration, we two CIs

  1. $(\textbf{O1})$

$Q_{0}\sqcap R_{k}\sqsubseteq\bot$, for $k=1,2$;

Clearly, these two CIs ensure that the value of both counters is $0$ whenever
the state is the initial state $q_{0}$. For the non-termination condition over
$(\mathbb{N},<)$ and the termination condition over finite flows of time, we
use the following CIs, respectively:

  1. $(\textbf{A1})$

$Q_{L}\sqsubseteq\bot$.

  2. $(\textbf{A2})$

$\neg{\raisebox{1.07639pt}{\text{{$\bigcirc$}}}}\top\sqsubseteq Q_{L}$.

We claim that $Q_{0}$ is satisfiable under $\mathcal{O}_{M}$ over
$(\mathbb{N},<)$ iff machine $M$ never halts on $(0,0)$. Indeed, if $Q_{0}$ is
satisfiable under $\mathcal{O}_{M}$, then by $(\textbf{O1})$, moment 0 encodes
configuration $(q_{0},0,0)$. By Claim 7, moments 0, 1, 2, etc. encode
configurations $(q^{t},v^{t}_{1},v_{2}^{t})$ such that
$(q^{t},v_{1}^{t},v_{2}^{t})\Rightarrow_{M}(q^{t+1},v^{t+1}_{1},v^{t+1}_{2})$,
for each $t$. By $(\textbf{A1})$, the halting state $q_{L}$ is never reached,
and so machine $M$ does not halt on $(0,0)$.

Conversely,
$(q^{0},v^{0}_{1},v^{0}_{2})\Rightarrow_{M}\ldots\Rightarrow_{M}(q^{t},v^{t}_{1},v^{t}_{2})\Rightarrow_{M}\ldots$
be the computation of $M$ on input $(0,0)$, where $q^{0}=q_{0}$ and
$v^{0}_{k}=0$, for $k=1,2$. We construct an interpretation
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in\mathbb{N}})$ that satisfies
$Q_{0}$ under $\mathcal{O}_{M}$. Let $\Delta$ be a fixed countable set. Given
$t\in\mathbb{N}$ and $q^{t}=q_{j}$, for some $0\leq i\leq L$, we set
$Q_{i}^{\mathcal{I}_{t}}=\Delta$ and $Q_{j}^{\mathcal{I}_{t}}=\emptyset$, for
all $j\neq i$. In addition, we set
$R_{1}^{\mathcal{I}_{0}}=R_{2}^{\mathcal{I}_{0}}=\emptyset$. Then, for every
instant $t\in\mathbb{N}$, we define the interpretations
$R_{1}^{\mathcal{I}_{t+1}}$, $R_{2}^{\mathcal{I}_{t+1}}$,
$a_{k}^{\mathcal{I}_{t}}$, and $b_{k}^{\mathcal{I}_{t}}$ inductively as
follows.

  * •

If $q^{t}=q_{i}$ and $I_{i}=+(r_{k},q_{j})$, then we choose some $d\notin
R_{k}^{\mathcal{I}_{t}}$ and set $a_{k}^{\mathcal{I}_{t}}=d$ and
$R_{k}^{\mathcal{I}_{t+1}}=R_{k}^{\mathcal{I}_{t}}\cup\\{d\\}$; we also choose
an arbitrary $b_{k}^{\mathcal{I}_{t}}$ and set
$R_{\overline{k}}^{\mathcal{I}_{t+1}}=R_{\overline{k}}^{\mathcal{I}_{t}}$.

  * •

If $q^{t}=q_{i}$ and $I_{i}=-(r_{k},q_{j},q_{h})$, then we have two options:

    * –

if $R_{k}^{\mathcal{I}_{t}}\neq\emptyset$, then we choose an arbitrary $e\in
R_{k}^{\mathcal{I}_{t}}$ and set $b_{k}^{\mathcal{I}_{t}}=e$ and
$R_{k}^{\mathcal{I}_{t+1}}=R_{k}^{\mathcal{I}_{t}}\setminus\\{e\\}$;

    * –

if $R_{k}^{\mathcal{I}_{t}}=\emptyset$, then we choose an arbitrary
$b_{k}^{\mathcal{I}_{t}}$ and set
$R_{k}^{\mathcal{I}_{t+1}}=R_{1}^{\mathcal{I}_{t}}$.

In either case, we also choose an arbitrary $a_{k}^{\mathcal{I}_{t}}$ and set
$R_{\overline{k}}^{\mathcal{I}_{t+1}}=R_{\overline{k}}^{\mathcal{I}_{t}}$.

It can be seen that $\mathfrak{M}$ satisfies $Q_{0}$ under $\mathcal{O}_{M}$.

Next, we claim that $Q_{0}$ is satisfiable under $\mathcal{O}_{M}$ over finite
flows of time iff machine $M$ halts on $(0,0)$. Indeed, if $Q_{0}$ is
satisfiable under $\mathcal{O}_{M}$ over some $([0,n],<)$, then by
$(\textbf{O1})$, moment 0 encodes configuration $(q_{0},0,0)$. By Claim 7,
moments $0,1,2,\dots,n$ etc. encode configurations
$(q^{t},v^{t}_{1},v_{2}^{t})$ such that
$(q^{t},v_{1}^{t},v_{2}^{t})\Rightarrow_{M}(q^{t+1},v^{t+1}_{1},v^{t+1}_{2})$,
for each $0\leq t<n$. By $(\textbf{A2})$, the state $q^{n}$ is the halting
state, $q_{L}$, as required. The converse direction is similar to the case of
$(\mathbb{N},<)$. ∎