# Putting perspective into OWL [sic]: complexity-neutral standpoint reasoning for ontology languages via monodic S5 over counting two-variable first-order logic

Lucía Gómez Álvarez, Sebastian Rudolph

<figure><img src="image_1.png" /></figure>

## To cite this version:

Lucía Gómez Álvarez, Sebastian Rudolph. Putting perspective into OWL [sic]: complexity-neutral standpoint reasoning for ontology languages via monodic S5 over counting two-variable first-order logic. KR 2025 - conference on International Conference on Principles of Knowledge Representation and Reasoning, Sep 2025, Melbourne, Australia. pp.366-375. hal-05463692

HAL Id: hal-05463692

https://hal.science/hal-05463692v1

Submitted on 17 Jan 2026

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Putting Perspective into OWL [sic]:
Complexity-Neutral Standpoint Reasoning for Ontology Languages
via Monodic S5 over Counting Two-Variable First-Order Logic

Lucía Gómez Álvarez<fnref n="1" />, Sebastian Rudolph²

¹INRIA, Université Grenoble Alpes

²TU Dresden and Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig
lucia.gomez-alvarez@inria.fr, sebastian.rudolph@tu-dresden.de

## Abstract

Standpoint extensions of KR formalisms have been recently introduced to incorporate multi-perspective modelling and reasoning capabilities. In such modal extensions, the integration of conceptual modelling and perspective annotations can be more or less tight, with monodic standpoint extensions striking a good balance as they enable advanced modelling while preserving good reasoning complexities.

We consider the extension of $C^2$– the counting two-variable fragment of first-order logic – by monodic standpoints. At the core of our treatise is a polytime translation of formulae in said formalism into standpoint-free $C^2$, requiring elaborate model-theoretic arguments. By virtue of this translation, the NEXPTIME-complete complexity of checking satisfiability in $C^2$ carries over to our formalism. As our formalism subsumes monodic S5 over $C^2$, our result also significantly advances the state of the art in research on first-order modal logics.

As a practical consequence, the very expressive description logics SHOIQB<sub>s</sub> and SROIQB<sub>s</sub> which subsume the popular W3C-standardized OWL 1 and OWL 2 ontology languages, are shown to allow for monodic standpoint extensions without any increase of standard reasoning complexity.

We prove that NEXPTIME-hardness already occurs in much less expressive DLs as long as they feature both nominals and monodic standpoints. We also show that, with inverses, functionality, and nominals present, minimally lifting the monodicity restriction leads to undecidability.

## 1 Introduction

Integrating knowledge from diverse, independently developed sources is a central problem in knowledge representation, particularly given the proliferation of available ontologies and other knowledge sources. Many of these ontologies – often expressed in W3C-standardized dialects of the Web Ontology Language (OWL) (Bao et al. 2009) – cover overlapping domains but embody varying conceptual frameworks and modelling choices. As an example scenario, imagine that some biomedical ontology ($O_{Process}$) might define Tumour as a dynamic biological process, whereas another ($O_{Tissue}$) might view it as a static abnormal tissue structure. While the description logics (DLs) (Baader et al. 2017; Rudolph 2011) underpinning OWL are well-suited to coherently model a domain, they lack mechanisms for managing heterogeneous or conflicting perspectives, leading to notoriouse challenges whenever such sources are to be integrated.

Standpoint logic (SL) (Gómez Álvarez and Rudolph 2021) is a recently proposed modal logic framework for multi-perspective reasoning and ontology integration. In a similar vein to epistemic logic, propositions with labelled modal operators $\Box_s \phi$ and $\Diamond_s \phi$ express information relative to the standpoint $s$ and read, respectively: “according to $s$, it is *unequivocal/conceivable* that $\phi$”. For instance, the formula $\Box_{Process}[\Diamond_{Tissue}[\text{Tumour}] \sqsubseteq \text{1TriggeredBy.Tumour}]$ expresses that, according to the Process standpoint, it is unequivocal that everything that is conceivably a Tumour from the Tissue standpoint has been triggered by exactly one Tumour (process). Similarly, $\Box_{Tissue}[\{\text{patient1}\} \sqsubseteq \exists\text{HasBodyPart.}(\text{Tumour} \sqcap \{\text{t1}\})]$ states that according to the Tissue standpoint, it is unequivocal that patient1 has the Tumour t1 as a body part. From both, we infer that according to the Process standpoint, t1 was triggered by one Tumour. Natural reasoning tasks over multi-standpoint specifications include gathering undisputed knowledge, determining knowledge that is relative to certain standpoints, and contrasting the knowledge from different standpoints.

The SL framework has promising applications in ontology integration, particularly in facilitating the interoperability of ontologies developed in isolation. For this reason, recent work has explored how it can be combined with logic-based formalisms underpinning the OWL family – most notably with the DLs $\mathcal{EL}$ (Gómez Álvarez, Rudolph, and Strass 2023b), $\mathcal{EL}^+$ (Gómez Álvarez, Rudolph, and Strass 2023a) and SHIQ (Gómez Álvarez and Rudolph 2024). It has been shown that monodic extensions<fnref n="1" /> of these languages with SL preserve the complexity of the standpoint-free DL, showing that joint reasoning over the integrated combination of possibly many ontologies is not fundamentally harder than reasoning with the ontologies in separation.

Hitherto, an open question has been whether the same holds for the very expressive side of modelling languages, in particular DLs that would fully cover high-end contemporary ontology languages such as OWL 2 DL. The results obtained so far for such languages only considered sentential fragments (Gómez Álvarez, Rudolph, and Strass 2022), which is an easier but much more restricted case with no interplay

<footnote n="1">¹Monodic extensions of first-order modal logic allow for one free variable in the scope of the modal operator, and for modalised axioms and concept expressions in the case of modal DLs.</footnote>
between quantification and modal operators (e.g., in DLs, the modal operators can only occur on the axiom-level).

In this paper, we address this open question by considering the extension of $C^2$– the counting two-variable fragment of first-order logic, which in fact has already gained some popularity for serving as a logic to embed very expressive DLs into – by monodic standpoints. After the preliminaries (in Section 2), we provide, in Section 3, a polytime translation of formulae in said formalism into plain $C^2$, using elaborate model-theoretic arguments. From this, we establish that the NEXPTIME-completeness of checking (finite) satisfiability in $C^2$ carries over to monodic standpoint $C^2$. As our formalism subsumes monodic S5 over $C^2$, our result also significantly advances the state of the art in first-order modal logic.

Section 4 exposes how, as a consequence, the very expressive DLs SHOIQB<sub>s</sub> and SROIQB<sub>s</sub> which subsume the OWL 1 and OWL 2 ontology languages, also allow for monodic standpoint extensions without any increase of standard reasoning complexity. Moreover, in Section 5 we prove that NEXPTIME-hardness already occurs in much less expressive DLs as long as they feature both nominals and monodic standpoints. What is more, we show that, with inverses, functionality, and nominals present, minimally lifting the monodicity restriction by allowing for one distinguished rigid binary predicate leads to undecidability. The full proofs for most proof sketches can be found in the extended version of this paper (Gómez Álvarez and Rudolph 2025).

# 2 Preliminaries

## 2.1 First-Order Standpoint Logic

We introduce syntax and semantics of first-order standpoint logic (FOSL, see Gómez Álvarez, Rudolph, and Strass 2022).

**Definition 1.** The syntax of any FOSL formula is based on a set **V** of variables, typically denoted with *x*, *y*, ..., and a signature $\langle \mathbf{P}, \mathbf{C}, \mathbf{S} \rangle$, consisting of predicates **P** (each associated with an arity *n* ∈ $\mathbb{N}$), constants **C** and standpoint symbols **S**, usually denoted *s*, *s'*. In particular, **S** also contains *, the universal standpoint. **V**, **P**, **C**, and **S** are assumed to be pairwise disjoint. The set **T** of terms contains all constants and variables, that is, $\mathbf{T} = \mathbf{C} \cup \mathbf{V}$.

The set $\mathbf{E_S}$ of standpoint expressions is defined by

$$e_1, e_2 ::= s | e_1 \cap e_2 | e_1 \cup e_2 | e_1 \setminus e_2,$$

with *s* ∈ **S**. The set $\mathcal{S}_{FO}$ of FOSL formulae is then given by
$\phi, \psi ::= \mathbf{P}(t_1, ..., t_k) | t_1 \doteq t_2 | \neg \phi | \phi \wedge \psi | \exists^{\Delta^n} x. \phi | \Diamond_e \phi,$
where $\mathbf{P} \in \mathbf{P}$ is a *k*-ary predicate; $t_1, ..., t_k \in \mathbf{T}$ are terms;
$\Delta$ is any of $\leq, =, \text{ or } \geq$; $n \in \mathbb{N}$; $x \in \mathbf{V}$; and $e \in \mathbf{E_S}$.
$\Diamond$

For a formula $\phi$, we denote the set of all of its subformulae by $Sub(\phi)$. The size of a formula is $|\phi| := |Sub(\phi)|$. The connectives and operators **t**, **f**, $\phi \lor \psi$, $\phi \rightarrow \psi$, $\phi \leftrightarrow \psi$, $\forall x.\phi$, and $\Box_e \phi$ are introduced as syntactic macros as usual – in particular, $\forall x.\phi$ is used to abbreviate $\exists^0 x.\neg\phi$. In line with intuition, we may just write $\exists x.\phi$ instead of $\exists^{\geq 1} x.\phi$. We note that in full first-order logic, the somewhat exotic counting quantifiers $\exists^{\Delta^n}$ do not add extra expressivity compared to the non-counting ones, but they do make a difference when the number of variables is restricted. As this is where we are heading, it is convenient to start from this syntax definition.

A first-order standpoint logic formula $\phi$ is called

* monodic if in each of its subformulae of the shape $\Diamond_e \psi$, the formula $\psi$ has at most one free variable,

* $C^2$ if it only uses the two variables *x* and *y* and predicates of arity $\leq 2$, and plain $C^2$ if it is $C^2$ and does not use $\Diamond$,

* S5 if the only standpoint expression used is *,

* nullary-free if it does not use predicates of arity zero,

* constant-free if it does not use constants.

Moreover, we will call formulae of the form $\Diamond_* \phi$ monodic modal formulae if they have exactly one free variable and sentential modal formulae if they have no free variables.

**Definition 2.** Given a signature $\langle \mathbf{P}, \mathbf{C}, \mathbf{S} \rangle$, a (first-order) standpoint structure $\mathfrak{M}$ is a tuple $\langle \Delta, \Pi, \sigma, \gamma \rangle$ where:

* $\Delta$ is a non-empty set, the domain of $\mathfrak{M}$;

* $\Pi$ is a non-empty set, called precisifications or worlds;

* $\sigma$ is a function mapping each standpoint symbol from $\mathbf{S}$ to a set of worlds (i.e., a subset of $\Pi$), with $\sigma(*) = \Pi$ fixed;

* $\gamma$ is a function mapping each precisification from $\Pi$ to an ordinary first-order structure $\mathcal{I}$ over the domain $\Delta$, whose interpretation function $\mathcal{I}^*$ maps:

- every predicate symbol $\mathbf{P} \in \mathbf{P}$ ofarity *k* to a *k*-ary relation $\mathbf{P}^* \subseteq \Delta^k$,

- each constant symbol $a \in \mathbf{C}$ to a domain element $a^* \in \Delta$.

For any two $\pi_1, \pi_2 \in \Pi$ and every $a \in \mathbf{C}$ we require $a^{\gamma(\pi_1)} = a^{\gamma(\pi_2)}$ (i.e., we enforce rigid constants). $\Diamond$

If in $\mathfrak{M}$, some predicate $\mathbf{P} \in \mathbf{P}$ satisfies $P^{\gamma(\pi_1)} = P^{\gamma(\pi_2)}$ for every $\pi_1, \pi_2 \in \Pi$, we say that $\mathbf{P}$ is rigid (in $\mathfrak{M}$) and allow ourselves to write $P^{\mathfrak{M}}$ instead of $P^{\gamma(\pi_1)}$.

**Definition 3.** Let $\mathfrak{M} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ be a first-order standpoint structure for the signature $\langle \mathbf{P}, \mathbf{C}, \mathbf{S} \rangle$ and $\mathbf{V}$ be a set of variables. A variable assignment is a function $v : \mathbf{V} \to \Delta$ mapping variables to domain elements. Given a variable assignment $v$, we denote by $v_{\{x \mapsto \delta\}}$ the function mapping $x$ to $\delta \in \Delta$ and any other variable $y$ to $v(y)$.

An interpretation function $\mathcal{I}^*$ together with a variable assignment $v$ specify how to interpret any term $t$ from **T** by a domain element from $\Delta$: We let $t^{\mathcal{I},v} = v(x)$ if $t = x \in \mathbf{V}$, and $t^{\mathcal{I},v} = a^*$ if $t = a \in \mathbf{C}$.

To interpret standpoint expressions, we lift $\sigma$ from $\mathbf{S}$ to all of $\mathbf{E_S}$ via $\sigma(e_1 \bowtie e_2) = \sigma(e_1) \bowtie \sigma(e_2)$ for $\bowtie \in \{\cup, \cap, \setminus\}$.

The satisfaction relation for formulae is defined in the usual way via structural induction. In what follows, let $\pi \in \Pi$ and let $v : \mathbf{V} \to \Delta$ be a variable assignment; we now establish the definition of the satisfaction relation $\models$ for FOSL using pointed first-order standpoint structures:

$$\mathfrak{M}, \pi, v \models \mathbf{P}(t_1, \dots, t_k) \quad \text{iff} \quad (t_1^{\gamma(\pi)}, v, \dots, t_k^{\gamma(\pi)}, v) \in \mathbf{P}^{\gamma(\pi)}$$

$$\mathfrak{M}, \pi, v \models t_1 \doteq t_2 \quad \text{iff} \quad t_1^{\gamma(\pi),v} = t_2^{\gamma(\pi),v}$$

$$\mathfrak{M}, \pi, v \models \neg \phi \quad \text{iff} \quad \mathfrak{M}, \pi, v \nvDash \phi$$

$$\mathfrak{M}, \pi, v \models \phi \wedge \psi \quad \text{iff} \quad \mathfrak{M}, \pi, v \models \phi \text{ and } \mathfrak{M}, \pi, v \models \psi$$

$$\mathfrak{M}, \pi, v \models \exists^{\Delta^n} x \phi \quad \text{iff} \quad \{\delta \mid \mathfrak{M}, \pi, v_{\{x \mapsto \delta\}} \models \phi\} \Delta^n$$

$$\mathfrak{M}, \pi, v \models \Diamond_e \phi \quad \text{iff} \quad \mathfrak{M}, \pi, v \models \phi \text{ for some } \pi' \in \sigma(\mathbf{e})$$

$$\mathfrak{M}, \pi \models \phi \quad \text{iff} \quad \mathfrak{M}, \pi, v \models \phi \text{ for all } v : \mathbf{V} \to \Delta$$

$$\mathfrak{M} \models \phi \quad \text{iff} \quad \mathfrak{M}, \pi \models \phi \text{ for all } \pi \in \Pi$$

As usual, $\mathfrak{M}$ is a *model* for a formula $\phi$ iff $\mathfrak{M} \models \phi$. $\Diamond$
**Lemma 4.** Let $\phi$ be an $\mathbb{S}_{\text{FO}}$ sentence and $\mathfrak{M} = (\Delta, \Pi, \sigma, \gamma)$ be a model of $\phi$. Then, for any $n \ge |\Pi|$, there exists a model $\mathfrak{M}' = (\Delta, \Pi', \sigma', \gamma')$ of $\phi$ with $|\Pi'| = n$.

*Proof Sketch.* We just pick one precisification from $\mathfrak{M}$ and add as many isomorphic copies of it to $\mathfrak{M}$ as required. $\square$

## 2.2 Transformations

The results obtained in the first part of this paper concern the fragment of all FOSL formulae that are monodic and $C^2$ - from here on, we will refer to this logical fragment as monodic standpoint $C^2$, short $\mathbb{S}_{C^2}^{\text{mon}}$. For technical reasons, we prefer to focus on formulae that additionally are S5, nullary-free, and constant-free; we will call these frugal for brevity. This section establishes that any $\mathbb{S}_{C^2}^{\text{mon}}$ formula can be efficiently transformed into an equisatisfiable frugal one.

**Theorem 5.** For any FOSL formula $\phi$, an equisatisfiable S5 FOSL formula S5($\phi$) can be computed in polynomial time. The transformation preserves $C^2$-ness and monodicity.

*Proof Sketch.* Let $\phi$ be a FOSL formula based on a signature $\langle \mathbf{P}, \mathbf{C}, \mathbf{S} \rangle$. We show that for any formula $\phi$, the formula $\text{trans}(\phi)$, based on the signature $\langle \mathbf{P} \cup \mathbf{S}, \mathbf{C}, \{ * \} \rangle$ is equisatisfiable and preserves $C^2$-ness and monodicity. For instance, the function trans replaces $\diamond_s \psi$ by $\diamond_*(s \land \psi)$, introducing one nullary predicate for every standpoint symbol $s \in \mathbf{S}$ and translating set expressions for standpoints into boolean expressions. The function trans is formally defined as follows:

$$ 
\begin{align*}
\text{trans}(\mathbf{P}(t_1, \dots, t_k)) &= \mathbf{P}(t_1, \dots, t_k) \\
\text{trans}(\neg \psi) &= \neg \text{trans}(\psi) \\
\text{trans}(\psi_1 \land \psi_2) &= \text{trans}(\psi_1) \land \text{trans}(\psi_2) \\
\text{trans}(\forall x \psi) &= \forall x (\text{trans}(\psi)) \\
\text{trans}(\diamond_* \psi) &= \diamond_*(\text{trans}(\psi)) \\
\text{trans}(\diamond_e \psi) &= \diamond_*(\text{trans}_E(e) \land \text{trans}(\psi))
\end{align*}
$$

Therein, $\text{trans}_E$ implements the semantics of standpoint expressions, providing for each expression $e \in \mathbf{E}_S \setminus \{ * \}$ a propositional formula $\text{trans}_E(e)$ as follows

$$ 
\begin{align*}
\text{trans}_E(s) &= s \\
\text{trans}_E(e_1 \cup e_2) &= \text{trans}_E(e_1) \lor \text{trans}_E(e_2) \\
\text{trans}_E(e_1 \cap e_2) &= \text{trans}_E(e_1) \land \text{trans}_E(e_2) \\
\text{trans}_E(e_1 \setminus e_2) &= \text{trans}_E(e_1) \land \neg \text{trans}_E(e_2)
\end{align*}
$$

Equisatisfiability follows by an easy induction. A routine check of the translation also yields that it preserves $C^2$-ness and monodicity, and it can be computed in polynomial time. Similar translations have been described before, for instance by Kurucz, Wolter, and Zakharyaschev (2023). $\square$

**Theorem 6.** For any FOSL formula $\phi$, one can compute an equisatisfiable nullary-free FOSL formula NF($\phi$) in polynomial time. The transformation preserves $C^2$-ness, S5-ness, and monodicity.

*Proof Sketch.* For any nullary predicate $\mathbf{N}$ occurring in $\phi$, introduce a fresh unary predicate $\mathbf{P}_\mathbf{N}$ and replace any occurrence of $\mathbf{N}$ inside $\phi$ by $\forall x.(\mathbf{P}_\mathbf{N}(x))$. $\square$

**Theorem 7.** For any $C^2$ FOSL formula $\phi$, one can compute in polynomial time an equisatisfiable constant-free $C^2$ FOSL formula CF($\phi$). If $\phi$ is S5 and nullary-free, then so is CF($\phi$).

*Proof Sketch.* For every constant a occurring in $\phi$, introduce a unary predicate $\mathbf{P}_a$. Let $\phi^{\text{consts}}$ be the conjunction over all $\exists^=1x.\mathbf{P}_a(x) \land \exists^=1x.\square_*\mathbf{P}_a(x)$ for all such a. Further, obtain $\phi'$ by replacing every atom using constants a, b as follows:

$$ 
\begin{align*}
\mathbf{P}(a) &\mapsto \exists x.(\mathbf{P}_a(x) \land \mathbf{P}(x)) \\
\mathbf{P}(a, x) &\mapsto \exists y.(\mathbf{P}_a(y) \land \mathbf{P}(y, x)) \\
\mathbf{P}(x, a) &\mapsto \exists y.(\mathbf{P}_a(y) \land \mathbf{P}(x, y)) \\
\mathbf{P}(a, y) &\mapsto \exists x.(\mathbf{P}_a(x) \land \mathbf{P}(x, y)) \\
\mathbf{P}(y, a) &\mapsto \exists x.(\mathbf{P}_a(x) \land \mathbf{P}(y, x)) \\
\mathbf{P}(a, b) &\mapsto \exists x.\exists y.(\mathbf{P}_a(x) \land \mathbf{P}_b(y) \land \mathbf{P}(x, y)) \\
x \doteq a &\mapsto \mathbf{P}_a(x) \quad (\text{same for } a \doteq x) \\
y \doteq a &\mapsto \mathbf{P}_a(y) \quad (\text{same for } a \doteq y) \\
a \doteq b &\mapsto \exists x.(\mathbf{P}_a(x) \land \mathbf{P}_b(x))
\end{align*}
$$

Then we let CF($\phi$) = $\phi^{\text{consts}} \land \phi'$. $\square$

Thus given an arbitrary $\mathbb{S}_{C^2}^{\text{mon}}$ formula $\phi$, consecutively applying the transformations of the above theorems yields the equisatisfiable frugal $\mathbb{S}_{C^2}^{\text{mon}}$ formula CF(NF(S5($\phi$))). The transformation is polytime and, in particular, the result is of polynomial size with respect to the input.

## 3 Satisfiability in Monodic Standpoint $C^2$

In this section, we study the satisfiability problem of frugal $\mathbb{S}_{C^2}^{\text{mon}}$ and prove NEXPTIME-completeness - which, by the previous section's results, carries over to full $\mathbb{S}_{C^2}^{\text{mon}}$. This finding constitutes the central result of our paper.

To get started, we provide an overview of the argument used to establish the result. In Section 3.1, we show that the satisfiability of a frugal $\mathbb{S}_{C^2}^{\text{mon}}$ formula $\phi$ coincides with the existence of a structure $\mathfrak{M}$ having exponentially many precisifications with respect to $\phi$'s size, from which a specific kind of model - called the $\mathbf{P}_E$-stable permutational closure of $\mathfrak{M}$ - can be constructed. In Section 3.2, we introduce stacked interpretations: these are plain first-order interpretations that closely reflect the form of standpoint structures for $\mathbb{S}_{C^2}^{\text{mon}}$. We also define stacked formulae $\phi_{\text{stack}}^m$, which enforce models to take the form of stacked interpretations corresponding to standpoint structures with $2^m$ precisifications. With these components in place, we present in Section 3.3 an equisatisfiable translation from frugal $\mathbb{S}_{C^2}^{\text{mon}}$ formulae into plain $C^2$, which is polynomial in the size of the input formula.

Throughout the section, we will use a running example to help the reader navigate through the technical details.

**Example 8.** Consider the monodic standpoint $C^2$ sentence $E$ in Figure 1(1), expressing that there is exactly one unequivocally good thing ($E_0$); that everything is either unequivocally good or conceivably the best (somewhere), with no two distinct things being the best simultaneously ($E_1$); and that it is conceivable that everything is good or the best ($E_2$).

Figure 1(2) shows a model of $E$. Notably, in models of $E$ with infinite domains - such as the one in Fig. 1(2) - there must also be infinitely many precisifications. This is because only one element satisfies Good everywhere, while every other element must be the Best in some precisification, with at most one such element per precisification. $\diamond$
<figure><img src="image_3.png" /><figcaption>Figure 1: (1) The formula $E$ from Example 8, and illustrations of (2) a model $\mathfrak{M}_o$ of $E$, (3) an interpretation $\mathfrak{M}$ with the signature $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \{*\} \rangle$, (4) the stacked interpretation $\mathcal{I}^{\mathfrak{M}}$ of $\mathfrak{M}$, and (5) $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$, the $\mathbf{P}_E$-stable permutational closure of $\mathfrak{M}$. In the graphics, all points within a coloured area labelled with a unary predicate are in the interpretation of that predicate.</figcaption></figure>

## 3.1 Permutational Representatives

Next, we show that for any satisfiable frugal $\mathbb{S}_{\mathbb{C}^2}^{\text{mon}}$ formula $\phi$, there is a structure $\mathfrak{M}$ with only exponentially many precisifications in $|\phi|$ from which a model of $\phi$ of a specific shape can be created (while $\mathfrak{M}$ may not be a model itself).

**Definition 9.** Let $\mathfrak{M} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ be a standpoint structure for the signature $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \{*\} \rangle$, where $\mathbf{P}$ contains only unary and binary predicates, and $\mathbf{P}_E = \{E_0, \dots, E_\ell\}$ is a set of special rigid unary predicates. Let $\mathbb{P}_E$ denote the set of all permutations (i.e., bijective functions) $f: \Delta \to \Delta$ which preserve (non)membership in every $E_i$, that is, we require $\delta \in E_i^{\mathfrak{M}} \Leftrightarrow f(\delta) \in E_i^{\mathfrak{M}}$ for every $i \in \{0, \dots, \ell\}$ and $\delta \in \Delta$.

Then, the $\mathbf{P}_E$-stable permutational closure of $\mathfrak{M}$, denoted $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ is the standpoint structure $\langle \Delta, \Pi', \sigma', \gamma' \rangle$ defined by

* $\Pi' = \Pi \times \mathbb{P}_E$,

* $\sigma' = \{* \mapsto \Pi'\}$,

* $\mathbf{P}^{\gamma'}((\pi, f)) = \{f(\delta) \mid \delta \in \mathbf{P}^{\gamma(\pi)}\}$ for unary predicates $\mathbf{P} \in \mathbf{P}$

* $\mathbf{P}^{\gamma'}((\pi, f)) = \{(f(\delta_1), f(\delta_2)) \mid (\delta_1, \delta_2) \in \mathbf{P}^{\gamma(\pi)}\}$ for binary predicates $\mathbf{P} \in \mathbf{P}$

As we can see, the structure $\mathfrak{M}$ contains a set of special rigid unary predicates $\mathbf{P}_E$. These predicates induce “E-types”, corresponding to the subsets $T \subseteq \mathbf{P}_E$, so a domain element is said to have the E-type $T$ if it belongs to the interpretation of each $E_i$ in $T$ and to none outside it. We say $T$ is realized (in $\mathfrak{M}$) if at least one domain element has it.

The $\mathbf{P}_E$-stable permutational closure of $\mathfrak{M}$ produces a much larger structure that contains, for each initial precisification in $\Pi$, the set of precisifications with all possible permutations between domain elements belonging to the same E-type. Locally, all permuted versions of any world $\pi \in \Pi$ in the closure are isomorphic to each other, they just have their elements “swapped around”, preserving the worlds’ internal structure. This intuition is materialised in the next lemma.

**Lemma 10.** Let $\phi$ be a frugal $\mathbb{S}_{\mathbb{C}^2}^{\text{mon}}$ formula and let $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ be the $\mathbf{P}_E$-stable permutational closure of some standpoint structure $\mathfrak{M}$. Let $(\pi, f)$ and $(\pi, f')$ be precisifications of $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ and let $v' = f' \circ f^{-1} \circ v$. Then,

$$ \langle \mathfrak{M} \rangle_{\mathbf{P}_E}, (\pi, f), v \models \phi \iff \langle \mathfrak{M} \rangle_{\mathbf{P}_E}, (\pi, f'), v' \models \phi. $$

At the global level, E-types of domain elements, which are preserved under the permutations (by construction), will be utilized to witness the elements’ “membership” in diamond-preceded subformulae in the following sense: we call some $\delta \in \Delta$ a member of a formula $\diamond_* \psi$ with one free variable $z$ if $\mathfrak{M}, \pi, \{z \mapsto \delta\} \models \diamond_* \psi$ for some/all $\pi \in \Pi$ (note that by the semantics, the choice of $\pi$ is irrelevant in this case). We will denote the set of members of $\diamond_* \psi$ in $\mathfrak{M}$ by $(\diamond_* \psi)^{\mathfrak{M}}$.

Let us now investigate what conditions $\mathfrak{M}$ must meet so that $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ is a model of $\phi$. First, for $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ to witness membership to the $\diamond_* \psi$ formulae, the number of E-types must be at least as large as the number of types induced by the monodic modal formulae – these we refer to as $\diamond$-types. The two sets of types will be aligned: all elements with the same E-type will also have the same $\diamond$-type. Moreover, for each formula $\diamond_* \psi$ in a given realised $\diamond$-type, $\mathfrak{M}$ must include at least one precisification in which some element of that type satisfies $\psi$. The $\mathbf{P}_E$-stable permutational closure then ensures that every other element of the same E-type also satisfies $\psi$ in some permutation of that precisification.

**Theorem 11.** Let $\phi$ be a satisfiable frugal $\mathbb{S}_{\mathbb{C}^2}^{\text{mon}}$ formula over the signature $\langle \mathbf{P}, \emptyset, \{*\} \rangle$. Let $\text{Dia}_\phi$ denote the diamond subformulae of $\phi$ and $\text{FreeDia}_\phi$ the diamond subformulae with one free variable. Then there is a standpoint structure $\mathfrak{M} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ over $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \{*\} \rangle$ with

* $|\mathbb{P}_E| = \ell = |\text{FreeDia}_\phi|$

* $|\Pi| \le |\text{Dia}_\phi| \cdot 2^{|\text{Dia}_\phi|}$

such that $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ is a model of $\phi$.
**Proof Sketch.** To prove Theorem 11, we start from an arbitrary model $\mathfrak{M}'$ of $\phi$ and let $\text{FreeDia}_\phi = \{\diamond_* \phi_1, \dots, \diamond_* \phi_\ell\}$ be the set of diamond subformulae of $\phi$ with one free variable. We enrich $\mathfrak{M}'$ by setting the extension of $E_i$ to $(\diamond_* \phi_i)^{\mathfrak{M}'}$ for every $i \in \{1, \dots, \ell\}$. Then we create a new structure $\mathfrak{M}$ by selecting at most exponentially many precisifications from the enriched $\mathfrak{M}'$ and removing the rest. Specifically,

* select an arbitrary $\pi$ in case there are no diamond subformulae of $\phi$ at all. Otherwise,

* for each $\diamond_* \psi$ with no free variables that is satisfied in $\mathfrak{M}'$, select some $\pi$ with $\mathfrak{M}'$, $\pi \models \psi$ and

* for each realised E-type $T \subseteq \mathbb{P}_E$, pick some $\delta$ having $T$, and select, for every $E_i \in T$, one $\pi$ with $\mathfrak{M}'$, $\pi$, $\{z \mapsto \delta\} \models \phi_i$. The first point ensures that $\Pi$ is nonempty. The second adds witnesses for sentential modal formulae. The third provides witnesses of all monodic modal formulae from $\text{FreeDia}_\phi$. The construction ensures that at least one domain element witnesses each $\diamond_* \phi_i$ formula of each $\diamond$-type occurring in $\mathfrak{M}'$. Once these seed witnesses are in $\mathfrak{M}$, the rest of the elements belonging to that type in $\mathfrak{M}'$ will be witnessed by a permutation in $\langle\mathfrak{M}\rangle_{\mathbb{P}_E}$. One can then show by induction on the structure of $\phi$ that $\langle\mathfrak{M}\rangle_{\mathbb{P}_E}$ is a model iff $\mathfrak{M}'$ is a model. $\square$

**Example 12.** Revisiting Example 8, note that $E$ contains two monodic modal subformulae, $E_0$ and $E_1$. From the model of $E$ shown in Fig. 1(2), we can extract a structure $\mathfrak{M}$ with $\mathbb{P}_E = \{E_0, E_1\}$ (depicted in Fig. 1(3)), such that the corresponding model $\langle\mathfrak{M}\rangle_{\mathbb{P}_E}$ (shown in Fig. 1(5)) also satisfies $E$. In constructing $\mathfrak{M}$, we proceed as follows:

* We use $\pi_0$ to witness the sentential modal subformula $E_2$.

* The type $\{\}$ is not realised.

* For type $\{E_0\}$, we use $\pi_0$ as witness since $\delta_0 \in \text{Good}^{\gamma_0(\pi_0)}$.

* For type $\{E_1\}$ we use $\pi_0$ as witness since $\delta_1 \in \text{Best}^{\gamma_0(\pi_0)}$.

* For type $\{E_0, E_1\}$ we use $\pi_0$ and $\pi_1$ as witnesses since $\delta_2 \in \text{Good}^{\gamma_0(\pi_0)}$ and $\delta_2 \in \text{Best}^{\gamma_0(\pi_1)}$. $\diamond$

Notice that the permutations of $\delta_2$ ensure that the membership to the formulae $E_0$ and $E_1$ in $\mathfrak{M}$ carries on to $\langle\mathfrak{M}\rangle_{\mathbb{P}_E}$.

## 3.2 Stacked Interpretations

We now define a specific kind of $C^2$ interpretation obtained from a given standpoint structure $\mathfrak{M}$ with $2^m$ precisifications, called the stacked interpretation of $\mathfrak{M}$ and denoted $\mathcal{I}^{\mathfrak{M}}$. This structure is designed to closely mirror the shape of $\mathfrak{M}$.

**Definition 13.** Let $\mathfrak{M} = (\Delta, \Pi, \sigma, \gamma)$ with $|\Pi|=2^m$ be a standpoint structure for the signature $\langle\mathbb{P}, \emptyset, \{*\}\rangle$ where $\mathbb{P}$ contains only unary and binary predicates. Assume $\Pi$ is linearly ordered with elements named $\pi_0, \pi_1, \dots, \pi_{2^m-1}$.

The stacked interpretation of $\mathfrak{M}$ is the FO-interpretation $\mathcal{I}^{\mathfrak{M}} = (\Delta', \mathcal{I})$ with signature $\langle\mathbb{P} \uplus \{\mathbb{F}, L_0, \dots, L_{m-1}\}, \emptyset\rangle$, where $\mathbb{F}$ is a fresh binary predicate and $L_0, \dots, L_{m-1}$ are fresh unary predicates, such that

$$ (S1) \quad \Delta' = \Delta \times \{0, \dots, 2^m - 1\} $$

$$ (S2) \quad \mathbb{L}_j^{\mathcal{I}} = \{(\delta, i) \mid \text{the } j^{\text{th}} \text{ bit of } i \text{ in binary encoding is } 1\} $$

$$ (S3) \quad \mathbb{F}^{\mathcal{I}} = \{((\delta, i), (\delta, i+1)) \mid \delta \in \Delta, 0 \le i < 2^m - 1\} $$

$$ (S4) \quad \mathbb{P}^{\mathcal{I}} = \bigcup_{0 \le i < 2^m} \mathbb{P}^{\gamma(\pi_i)} \times \{i\} \text{ for all unary } \mathbb{P} \in \mathbb{P}, $$

$$ (S5) \quad \mathbb{P}^{\mathcal{I}} = \{((\bar{\delta}_1, i), (\delta_2, i)) \mid 0 \le i < 2^m, (\delta_1, \delta_2) \in \mathbb{P}^{\gamma(\pi_i)}\} \\ \text{for all binary } \mathbb{P} \in \mathbb{P}. \quad \diamond $$

Our approach constructs a stacked domain by creating one copy of the original domain $\Delta$ for each precisification in $\mathfrak{M}$, so that each new element $(\delta, \pi)$ mimics $\delta$ at precisification $\pi$. A set of new unary predicates $L_0, \dots, L_{m-1}$ bit-encodes the index of the associated precisification (each $< 2^m$). Also, a new binary predicate $\mathbb{F}$ links each element $(\delta, \pi_i)$ to its “next-world-twin” $(\delta, \pi_{i+1})$. Thus, for every original element $\delta$, the stacked interpretation forms an $\mathbb{F}$-chain tracking $\delta$ across all precisifications in $\mathfrak{M}$. In Figure 1, (3) depicts the stacked interpretation of (2) with the $\mathbb{F}$-chains in purple.

**Definition 14.** For a given $m \in \mathbb{N}$, we define $\phi_{\text{stack}}^m$ as the conjunction of the following formulae

$$ (F1) \quad \forall x. (\bigvee_{0 \le j < m} \neg L_j(x)) \rightarrow \exists^= 1 y. \mathbb{F}(x, y) $$

$$ (F2) \quad \forall x. (\bigwedge_{0 \le j < m} L_j(x)) \rightarrow \exists^= 0 y. \mathbb{F}(x, y) $$

$$ (F3) \quad \forall x. (\bigvee_{0 \le j < m} L_j(x)) \rightarrow \exists^= 1 y. \mathbb{F}(y, x) $$

$$ (F4) \quad \forall x. (\bigwedge_{0 \le j < m} \neg L_j(x)) \rightarrow \exists^= 0 y. \mathbb{F}(y, x) $$

$$ (F5) \quad \forall xy. \mathbb{F}(x, y) \rightarrow \bigwedge_{0 \le j < m} ((L_j(x) \leftrightarrow L_j(y)) \leftrightarrow \bigvee_{0 \le j' < j} \neg L_{j'}(x)) $$

$$ (F6) \quad \forall xy. \mathbb{P}(x, y) \rightarrow \bigwedge_{0 \le j < m} L_j(x) \leftrightarrow L_j(y) \text{ for all binary } \mathbb{P} \in \mathbb{P}. \quad \diamond $$

The stacked formula of size $m$, denoted $\phi_{\text{stack}}^m$, is used to enforce that models are stacked models. Clause (F1) enforces that all elements except those with the highest index (as determined by the L predicates) have exactly one $\mathbb{F}$-successor. Conversely, (F2) ensures that elements with the highest index have none. Clauses (F3) and (F4) impose analogous constraints on $\mathbb{F}$-predecessors. Clause (F5) encodes that any two $\mathbb{F}$-connected elements have consecutive indexes, via a binary level-counter using the L predicates. Lastly, Clause (F6) enforces that all binary predicates (except $\mathbb{F}$) relate only elements with matching indices.

**Lemma 15.** Any stacked interpretation $\mathcal{I}^{\mathfrak{M}}$ satisfies $\phi_{\text{stack}}^m$.

*Proof sketch.* We verify that each clause of $\phi_{\text{stack}}^m$ is satisfied by the stacked interpretation $\mathcal{I}^{\mathfrak{M}}$ as defined. In particular, the structure of the domain, and the interpretation of the predicates $\mathbb{F}, L_0, \dots, L_{m-1}$, and $\mathbb{P} \in \mathbb{P}$ ensure that all required properties hold. $\square$

**Theorem 16.** A first-order interpretation $\mathcal{I}$ over the signature $\langle\mathbb{P} \uplus \{\mathbb{F}, L_0, \dots, L_{m-1}\}, \emptyset\rangle$ satisfies $\phi_{\text{stack}}^m$ if and only if it is isomorphic to a stacked interpretation $\mathcal{I}^{\mathfrak{M}}$ of some standpoint structure $\mathfrak{M}$ over signature $\langle\mathbb{P}, \emptyset, \{*\}\rangle$ with $2^m$ precisifications.

*Proof Sketch.* If $\mathcal{I}$ is isomorphic to a stacked model $\mathcal{I}^{\mathfrak{M}}$ then it satisfies $\phi_{\text{stack}}^m$ by Lemma 15. It remains to prove the other direction, i.e., for any $\mathcal{I}$ that satisfies $\phi_{\text{stack}}^m$, there exists a standpoint structure $\mathfrak{M}$ for which $\mathcal{I}^{\mathfrak{M}}$ is isomorphic to $\mathcal{I}$. We show how to construct $\mathfrak{M} = (\Delta, \Pi, \sigma, \gamma)$ given $\mathcal{I}$ with domain $\Delta'$: For any $\delta' \in \Delta'$ we let level($\delta'$) denote the unique number $i < 2^m$ that satisfies, for every $j < m$, that the $j^{\text{th}}$ bit in the binary encoding of $i$ is 1 if and only if $\delta' \in \mathbb{L}_j^{\mathcal{I}}$. Moreover, we let $\approx$ be the smallest equivalence relation containing $\mathbb{F}^{\mathcal{I}}$ and let $\Delta$ consist of the $\approx$-equivalence classes of $\Delta'$. As in Definition 13, let $\Pi = \{\pi_0, \dots, \pi_{2^m-1}\}$. Obviously, $\sigma = \{* \mapsto \Pi\}$. Finally, we set $\mathbb{P}^{\gamma(\pi_i)}$ to
• $\{[\delta'] \approx | \delta' \in P^I, \text{level}(\delta') = i\}$ for unary $P \in P$, and

• $\{([\delta'_1] \approx, [\delta'_2] \approx) | (\delta'_1, \delta'_2) \in P^I, \text{level}(\delta'_1) = \text{level}(\delta'_2) = i\}$ for binary $P \in P$.

Then, the bijection stacked : $\Delta' \to \Delta \times \{0, \dots, 2^m - 1\}$ defined via stacked($\delta') = ([\delta'] \approx, \text{level}(\delta'))$ can be shown to constitute an isomorphism from $\mathcal{I}$ to $\mathcal{I}^M$. $\square$

### 3.3 Translating Formulae

So far, we have shown that the satisfiability of a frugal $S_{C^2}^{\text{mon}}$ formula $\phi$ coincides with the existence of a structure $\mathfrak{M}$ of size exponential in $|\phi|$ from which a model can be extracted. Furthermore, we demonstrated that such structures can be characterized in plain $C^2$ through their corresponding stacked interpretations. In this subsection, we leverage these results to define a translation from frugal $S_{C^2}^{\text{mon}}$ into plain $C^2$, such that a frugal $S_{C^2}^{\text{mon}}$ formula $\phi$ is satisfiable if and only if its translation into $C^2$ is satisfiable. Together with the translation from $S_{C^2}^{\text{mon}}$ to frugal $S_{C^2}^{\text{mon}}$, this entails the upper complexity bound for all of $S_{C^2}^{\text{mon}}$.

**Definition 17.** Given some $m \in \mathbb{N}$, we define the function $\text{Trans}_m$ that maps frugal $S_{C^2}^{\text{mon}}$ sentences $\phi$ over the signature $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \{*\} \rangle$ with $\mathbf{P}_E = \{E_0, \dots, E_\ell\}$ into $C^2$ as follows: $\text{Trans}_m(\phi)$ is the sentence $\forall x. \forall y. (x \doteq y \to \text{tr}(\phi))$, where the function tr is recursively defined via

$$ \begin{array}{l} \psi \mapsto \psi \quad \text{if } \psi \text{ is of the form } \mathbf{P}(z), \mathbf{P}(z, z') \text{ or } z \doteq z' \\ \neg \psi \mapsto \neg (\text{tr}(\psi)) \\ \psi \wedge \psi' \mapsto \text{tr}(\psi) \wedge \text{tr}(\psi') \\ \exists^{\Delta^n} z. \psi \mapsto \exists^{\Delta^n} z. (\phi_L^\equiv(x, y) \wedge \text{tr}(\psi)) \\ \diamond_* \psi \mapsto \forall z_{nf}. x \doteq y \to \exists z_{nf}. \phi_E^\equiv(x, y) \wedge \text{tr}(\psi) \end{array} $$

where $z, z' \in \{x, y\}$ and

• $z_{nf}$ is a variable from $\{x, y\}$ that is not free in $\psi$ and $\{z_{nf}\} = \{x, y\} \setminus \{z_{nf}\}$,

• $\phi_L^\equiv(x, y)$ abbreviates $\bigwedge_{0 \le j < m} L_j(x) \leftrightarrow L_j(y)$, and

• $\phi_E^\equiv(x, y)$ abbreviates $\bigwedge_{0 \le i \le \ell} E_i(x) \leftrightarrow E_i(y)$. $\diamond$

<figure><img src="image_4.png" /></figure>

The key components of the translation are the handling of counting quantification and modal operators. The translation of a counting existential quantification employs the formula $\phi_L^\equiv(x, y)$ to ensure that quantification ranges only over elements belonging to the current layer of the stacked interpretation – namely, those whose counterparts correspond to the domain elements at the current precisification. In contrast, the translation of modal subformulae of the form $\diamond_* \psi$ makes use of $\phi_E^\equiv(x, y)$ to ensure that quantification ranges over the elements belonging to the current E-type. Recall that $\mathcal{I}^M$ is constructed to mirror the structure $\mathfrak{M}$, from which in turn we obtain the model $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$. Consequently, if any element of the same E-type satisfies $\psi$, then there exists some permutation within $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ that satisfies $\psi$ and thus the formula $\diamond_* \psi$ is satisfied. Notice that when $\diamond_* \psi$ is sentential, the variable assignment does not make a difference. The following Lemma formally establishes the discussed correspondence.

**Lemma 18.** Let $\phi$ be a frugal $S_{C^2}^{\text{mon}}$ sentence over the signature $\langle \mathbf{P}, \emptyset, \{*\} \rangle$. Let $\mathfrak{M} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ be a standpoint structure for the signature $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \{*\} \rangle$, with all predicates from $\mathbf{P}_E = \{E_0, \dots, E_\ell\}$ rigid, and $|\Pi| = 2^m$. Then,

$$ \langle \mathfrak{M} \rangle_{\mathbf{P}_E} \models \phi \iff \mathcal{I}^M \models \text{Trans}_m(\phi). $$

**Proof Sketch.** Toward the result, we first prove the claim that, for $\pi_i \in \Pi$, $f \in \mathbb{P}_E$ and a variable assignment $v$, we have $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}, (\pi_i, f), v \models \phi$ iff $\mathcal{I}^M, v' \models \text{tr}(\phi)$, where $v'(z) = (f(v(z)), i)$ for $z \in \{x, y\}$. Due to Lemma 10, it suffices to show that $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}, (\pi_i, f_{id}), v \models \phi$ iff $\mathcal{I}^M, v' \models \text{tr}(\phi)$ where $v'(z) = (v(z), i)$; this follows by structural induction on $\phi$.

Toward the statement of the Lemma, assume $\langle \mathfrak{M} \rangle_{\mathbf{P}_E} \models \phi$, thus $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}, (\pi_i, f), v \models \phi$ holds for all $\pi_i \in \Pi$, $f \in \mathbb{P}_E$ and assignments $v$. Then, $\mathcal{I}^M, v' \models \text{tr}(\phi)$ where $v'(z) = (v(z), i)$, thus $\mathcal{I}^M, v' \models \text{tr}(\phi)$ for all $v'$ where $x$ and $y$ have equal index, thus $\mathcal{I}^M \models \text{Trans}_m(\phi)$. The converse direction proceeds in a similar fashion. $\square$

**Example 19.** Revisiting Example 8, we compute $\text{Trans}_2(E)$. With some simplifications, we obtain the following:

$$ \begin{align*} \text{Trans}_2(E) &= \forall x. \forall y. x \doteq y \to \text{tr}(E) \\ \text{tr}(E) &= \exists^{=1} x. (\phi_L^\equiv(x, y) \wedge \text{tr}(E_0)) \\ &\phantom{=} \wedge \forall x. (\phi_L^\equiv(x, y) \to \text{tr}(E_1)) \wedge \text{tr}(E_2) \\ \text{tr}(E_0) &= \exists y. x \doteq y \wedge \forall x. \phi_E^\equiv(x, y) \to \text{Good}(x) \\ \text{tr}(E_1) &= \text{tr}(E_0) \vee \forall y. x \doteq y \to (\exists x. \phi_E^\equiv(x, y) \wedge \\ &\phantom{=} \text{Best}(x) \wedge \forall y. \phi_L^\equiv(x, y) \to (\text{Best}(y) \leftrightarrow x \doteq y)) \\ \text{tr}(E_2) &= \forall x. x \doteq y \to \exists y. (\phi_E^\equiv(x, y) \wedge \\ &\phantom{=} \forall x. \phi_L^\equiv(x, y) \to (\text{Good}(x) \vee \text{Best}(x))) \end{align*} $$

One may verify that the structure in Figure 1(4) indeed satisfies $\text{Trans}_2(E)$. Roughly, there exists $x$, e.g., $(\delta_0, 0)$, s.t. all elements of its E-Type, i.e. $(\delta_0, 0)$ and $(\delta_0, 1)$, are Good($E_0$), and for all elements, either they satisfy $E_0$ (like $(\delta_0, 0)$ and $(\delta_0, 1)$) or there is some element of their E-Type (e.g., $(\delta_1, 0)$ for $\{E_1\}$ and $(\delta_2, 1)$ for $\{E_0, E_1\}$) which is the only Best element on their layer ($E_1$). Finally there is some element (e.g., $(\delta_0, 0)$) such that all elements on its layer are Good($E_3$). $\diamond$

The last ingredient for our satisfiability translation is to ensure that the predicates in $\mathbf{P}_E$ are indeed rigid.

**Definition 20.** We let $\phi_{rigE}^\ell$ denote the $C^2$ sentence $\forall x. \forall y. F(x, y) \to \bigwedge_{0 \le i \le \ell} E_i(x) \leftrightarrow E_i(y)$.

**Lemma 21.** Let $\mathfrak{M} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ be a first-order standpoint structure for the signature $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \{*\} \rangle$. Then, all predicates from $\mathbf{P}_E = \{E_0, \dots, E_\ell\}$ are rigid iff $\mathcal{I}^M \models \phi_{rigE}^\ell$.

**Theorem 22.** Let $\phi$ be an arbitrary frugal $S_{C^2}^{\text{mon}}$ sentence. Let $\ell = |\text{FreeDia}_\phi|$ and $m = \lceil |\text{Dia}_\phi| + \log_2(|\text{Dia}_\phi|) \rceil$. Then $\phi$ is satisfiable iff $\phi_{\text{stack}}^m \wedge \phi_{\text{rigE}}^\ell \wedge \text{Trans}_m(\phi)$ is satisfiable.

**Proof.** Assume that $\phi$ is satisfiable. Then by Theorem 11 there is a standpoint structure $\mathfrak{M}$ over the signature $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \emptyset \rangle$ with $|\mathbf{P}_E| = \ell = |\text{FreeDia}_\phi|$ and $|\Pi| \le |\text{Dia}_\phi| \cdot 2^{|\text{Dia}_\phi|}$, such that $\langle \mathfrak{M} \rangle_{\mathbf{P}_E}$ is a model of $\phi$. Then, from Lemma 18, we have that $\mathcal{I}^M \models \text{Trans}_m(\phi)$. Moreover, from Lemma 15, $\mathcal{I}^M \models \phi_{\text{stack}}^m$. Finally, by Definition 9, all predicates from $\mathbf{P}_E$ are rigid and thus by Lemma 21 $\mathcal{I}^M \models \phi_{rigE}^\ell$.

For the other direction, assume that there is a model $\mathcal{I}$ over the signature $\langle \{\mathbf{F}, L_0, \dots, L_{m-1}\} \uplus \mathbf{P}_E \uplus \mathbf{P}, \emptyset \rangle$ such that $\mathcal{I} \models \phi_{\text{stack}}^m \wedge \phi_{\text{rigE}}^\ell \wedge \text{Trans}_m(\phi)$. Then, by Theorem 16, $\mathcal{I}$ is isomorphic to a stacked interpretation $\mathcal{I}^M$ of some standpoint structure $\mathfrak{M}$ over $\langle \mathbf{P} \uplus \mathbf{P}_E, \emptyset, \emptyset \rangle$ with $2^m$ precisifications. Moreover, since $\mathcal{I} \models \phi_{\text{rigE}}^\ell$ then by Lemma 21 the
predicates in P<sub>E</sub> are rigid. And since I<sup>∞</sup> |= Trans<sub>m</sub>(φ), then by Lemma 18, we have that ⟨I<sup>∞</sup>⟩<sub>P<sub>E</sub></sub> |= φ as desired. □

Therefore (and taking into account Section 2.2), there is a polytime equisatisfiable translation from S<sub>C<sup>2</sup></sub><sup>mon</sup> to plain C<sup>2</sup>. On the other hand, every plain C<sup>2</sup> formula is S<sub>C<sup>2</sup></sub><sup>mon</sup>, thus in view of the known NEXPTIME completeness of plain C<sup>2</sup> (Pratt-Hartmann 2005), we arrive at the below corollary.

**Corollary 23.** *Satisfiability in monodic standpoint C<sup>2</sup> is NEXPTIME-complete.*

Our equisatisfiable “standpoint removal” technique turns out to be robust under some variations. Let us call a monodic standpoint C<sup>2</sup> formula φ finitely satisfiable if it has a model M = ⟨Δ, Π, σ, γ⟩ where Δ is finite. It is easy to see that all equisatisfiable transformations in Section 2.2 are also “equi-finitely-satisfiable”, because the underlying model transformations do not alter the domain whatsoever; the same holds for the argument behind Theorem 11. Last not least, the domain Δ' of the stacked interpretation I<sup>∞</sup> = (Δ', I) corresponding to a structure M = ⟨Δ, Π, σ, γ⟩ is finite whenever Δ is (by the construction of Definition 13, we get |Δ'| = |Δ|·2<sup>m</sup>). Thus the correspondence established in Theorem 22 also holds for finite satisfiability. On the other hand, finite satisfiability of plain C<sup>2</sup> is also known to be NEXPTIME-complete (Pratt-Hartmann 2005), thus we obtain the following result.

**Corollary 24.** *Finite satisfiability in monodic standpoint C<sup>2</sup> is NEXPTIME-complete.*

Last not least, more recently Benedikt, Kostylev, and Tan (2020) introduced two-variable FO with a more expressive version of counting quantifiers, denoted ∃S, where S is any semilinear subset of N ∪ {∞}. For example, by means of such quantifiers one can express quantities like “evenly many x” or also “infinitely many x”, which go beyond what can be stated by the counting quantifiers of C<sup>2</sup>. Satisfiability of the ensuing logic, denoted FO<sub>Pres</sub><sup>2</sup> was established to be decidable in N2EXPTIME and NEXPTIME hard. We note that our definitions, constructions, and arguments seamlessly extend from C<sup>2</sup> to this logic, leading to the subsequent corollary.

**Corollary 25.** *Satisfiability and finite satisfiability in monodic standpoint FO<sub>Pres</sub><sup>2</sup> is in N2EXPTIME and hard for NEXPTIME.*

We believe that – beyond their applicability to ontology reasoning as demonstrated in the next sections – the results presented here also provide significant novel insights for the area of first-order modal logics (Gabbay et al. 2005). As indicated by our naming, the subcase of S<sub>C<sup>2</sup></sub><sup>mon</sup> where the only standpoint expression used is * coincides with the monodic fragment of modal counting two-variable FO with a S5 modal operator. While it has been observed earlier that restricting to the monodic setting is crucial for maintaining decidability in non-trivial combinations of FO fragments with modalities of varying kinds (Wolter and Zakharyaschev 2001), existing decidability results explicitly exclude FO fragments with equality or function symbols, which are notoriously harder, leaving such cases as an open question. We transcend this boundary, since C<sup>2</sup> supports equality and unary functions (via axiomatising binary predicates as functional), and beyond mere decidability, we establish tight complexity bounds.

# 4 Application to Ontology Languages

We now show that adding monodic standpoints to popular ontology languages does not negatively affect the computational complexity of standard reasoning tasks. To this end, we begin by adding monodic standpoints to the description logic ALCOIQB<sup>Self</sup> which is very closely related to C<sup>2</sup>, and then we show how we can also accommodate role chain axioms, thus obtaining monodic standpoint extensions of SHOIQB<sub>s</sub> and SROIQB<sub>s</sub>, which subsume the W3C ontology standards OWL 1 and OWL 2 DL respectively.<fnref n="2" /> For the following, some familiarity with description logics (Baader et al. 2017; Rudolph 2011) will be very helpful.

## 4.1 Monodic Standpoint ALCOIQB<sup>Self</sup>

We first introduce S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup> obtained by adding monodic standpoints to the description logic ALCOIQB<sup>Self</sup>. Just like C<sup>2</sup> FOSL, S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup> is based on a signature ⟨P, C, S⟩ where P only contains unary and binary predicates, also referred to as concept names and role names, respectively. Based on these, we define the set E<sub>rol</sub> of role expressions

$$R, R' ::= R | R^- | \neg R | R \cap R'$$

with R ∈ P binary, and the set E<sub>con</sub> of concept expressions

$$C, D ::= A | \neg C | \{o\} | C \sqcap D | \geq n R. C | \exists R. \text{Self} | \diamond_e C$$

with A ∈ P unary, o ∈ C, n ∈ N, e ∈ E<sub>S</sub> (see Definition 1). Finally the set of S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup> sentences is defined by

$$\phi, \psi ::= C \sqsubseteq D | \neg \phi | \phi \wedge \psi | \diamond_e \phi$$

We introduce S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup> with a minimalistic syntax, but note that all the usual description logic constructs can be introduced as syntactic sugar. For example, we obtain ⊥ as A □ ¬A and ⊤ as ¬⊥; we may write ∃R.C instead of ≥1R.C and also ∀R.C instead of ¬≥1R.¬C; last not least we may write □<sub>e</sub> C to denote ¬diamond<sub>e</sub> C. We also remind the reader that other usual axiom types can all be rewritten into statements of the form C ⊑ D (referred to as general concept inclusions, short: GCIs) in the presence of nominals (i.e., expressions of the form {o}) and role expressions. Following DL naming conventions, a S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup> sentence will be referred to as TBox if it is a conjunction of GCIs.

For later discussions, we single out some fragments of S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup>: We obtain S<sub>ALCOIQF</sub><sup>mon</sup> by excluding ¬ and ∩ from role expressions as well as disallowing concept expressions that use Self or ≥k for k ≥ 2, with the notable exception of axioms of the specific form ⊤ ⊑ ¬≥2F. ⊤ stating the functionality for binary predicates F, which are then often abbreviated by func(F). We obtain S<sub>ALCO</sub><sup>mon</sup> from S<sub>ALCOIQF</sub><sup>mon</sup> by disallowing role expressions of the form R<sup>-</sup> (known as inverses), and functionality axioms.

The semantics of standpoint-enhanced description logics is usually provided in a model-theoretic way using standpoint structures as in Definition 3 (Gómez Álvarez, Rudolph,

<footnote n="2">²The less mainstream letter *B* in the DL names refers to *boolean role constructors*, where *B*<sub>s</sub> denotes boolean role constructors over simple roles only (see, e.g., Rudolph, Krötsch, and Hitzler 2008). This modelling feature is not available in OWL 1 or OWL 2 DL.</footnote>
and Strass 2022). For space reasons, we will instead define the semantics by directly providing a translation into $S_{C2}^{\text{mon}}$. To justify this “shortcut” we point out that said translation truthfully reflects the model-theoretic semantics of all earlier described standpoint-enhanced DLs and that existing translations from standpoint-free DLs to plain $C^2$ (Kazakov 2008) naturally arise as a special case of ours.

The translation of a $S_{ALCOIQB^{\text{Self}}}^{\text{mon}}$ sentence $\phi$ into a $S_{C2}^{\text{mon}}$ sentence is obtained by replacing every GCI $C \sqsubseteq D$ inside $\phi$ by $\forall x.(\text{ctrans}(x, C) \to \text{ctrans}(x, D))$, where $\text{ctrans}: \{x, y\} \times \mathbf{E}_{\text{con}} \to S_{C2}$ is inductively defined:

$$
\begin{align*}
\text{ctrans}(z, \mathbf{A}) &= \mathbf{A}(z) \\
\text{ctrans}(z, \neg C) &= \neg \text{ctrans}(z, C) \\
\text{ctrans}(z, \{o\}) &= z \doteq o \\
\text{ctrans}(z, C \sqcap D) &= \text{ctrans}(z, C) \wedge \text{ctrans}(z, D) \\
\text{ctrans}(x, \ge n R.C) &= \exists^{\ge n} y. \text{rtrans}(x, y, R) \wedge \text{ctrans}(y, C) \\
\text{ctrans}(y, \ge n R.C) &= \exists^{\ge n} x. \text{rtrans}(y, x, R) \wedge \text{ctrans}(x, C) \\
\text{ctrans}(z, \exists R.\text{Self}) &= \text{rtrans}(z, z, R) \\
\text{ctrans}(z, \diamond_e C) &= \exists z. \diamond_e \text{ctrans}(z, C),
\end{align*}
$$

using $\text{rtrans}: \{x, y\} \times \{x, y\} \times \mathbf{E}_{\text{rol}} \to S_{C2}$ defined by

$$
\begin{align*}
\text{rtrans}(z, z', R) &= R(z, z') \\
\text{rtrans}(z, z', R^-) &= R(z', z) \\
\text{rtrans}(z, z', \neg R) &= \neg \text{rtrans}(z, z', R) \\
\text{rtrans}(z, R \cap R') &= \text{rtrans}(z, z', R) \wedge \text{rtrans}(z, z', R).
\end{align*}
$$

It can be readily checked that the translation described is
computable in polytime (hence polynomial in output) and
indeed yields a $S_{C2}^{\text{mon}}$ sentence. Therefore, and in view of
the fact that satisfiability is already NEXPTIME-hard for the
standpoint-free sublogic $\mathcal{ALCOIF}$ (Tobies 2000), we obtain
the following tight complexity bounds.

**Theorem 26.** *Checking satisfiability of* $S_{ALCOIQB^{\text{Self}}}^{\text{mon}}$ *sentences is NEXPTIME-complete.*

## 4.2 Adding Role Chain Axioms

In order to fully cover the web ontology languages OWL 1 and OWL 2 DL, we need to extend our formalism by so-called role chain axioms, arriving at the description logics SHOIQB<sub>s</sub> (when allowing just role chain axioms expressing transitivity such as FriendOf ◦ FriendOf ⊑ FriendOf) or SROIQB<sub>s</sub> (when admitting more complex forms like FriendOf ◦ EnemyOf ⊑ EnemyOf), respectively. Luckily, by combining known standpoint encoding tricks (Gómez Álvarez, Rudolph, and Strass 2022) and removal techniques for role-chain axioms (Kazakov 2008; Demri and de Nivelle 2005) with some novel ideas, it is possible to translate S<sub>SHOIQB<sub>s</sub></sub><sup>mon</sup> and S<sub>SROIQB<sub>s</sub></sub><sup>mon</sup> sentences back into S<sub>ALCOIQB<sup>Self</sup></sub><sup>mon</sup>. The translation is polynomial for S<sub>SHOIQB<sub>s</sub></sub><sup>mon</sup> and exponential for S<sub>SROIQB<sub>s</sub></sub><sup>mon</sup>.

**Theorem 27.** *Checking satisfiability of* $S_{SHOIQB_s}^{\text{mon}}$ *sentences is NEXPTIME-complete.* Checking satisfiability of $S_{SROIQB_s}^{\text{mon}}$ *sentences is N2EXPTIME-complete.*

Therein, the hardness part for $S_{SROIQB_s}^{\text{mon}}$ follows from the known N2EXPTIME hardness of its fragment SROIQ (Kazakov 2008). This concludes our argument that adding monodic standpoints to OWL 1 and OWL 2 does not increase complexity of standard reasoning tasks.

# 5 Nominals Cause Trouble

We finish our considerations by presenting two results that
provide some context for our main results and corroborate
the intuition (cf. Gómez Álvarez, Rudolph, and Strass 2023b
as well as Gómez Álvarez and Rudolph 2024) that the inter-
play of nominals and standpoint modalities is particularly
troublesome for reasoning. To this end, we will use the tiling
problem in two variations, which we introduce next.

A tiling system $\mathbb{T} = \langle k, H, V \rangle$ consists of a number $k \in \mathbb{N}$ indicating the number of tiles, and horzontal and vertical compatibility relations $H, V \subseteq \{1, \dots, k\} \times \{1, \dots, k\}$. For a downward-closed set $S \subseteq \mathbb{N}$ of natural numbers, a $\mathbb{T}$-tiling of $S \times S$ with initial condition $\langle t_0, \dots, t_n \rangle \in \{1, \dots, k\}^n$ for some $n \in S$ is a mapping tile : $S \times S \to \{1, \dots, k\}$ such that tile$(i, 0) = t_i$ for $i \in \{1, \dots, n\}$, and for all $i \in S$ with $i+1 \in S$ and all $j \in S$ holds (tile$(i, j)$, tile$(i+1, j)$) $\in H$ as well as (tile$(j, i)$, tile$(j, i+1)$) $\in V$. We recall the following:

* There is a tiling system $T_{\text{exp}}$ such that the following problem is NEXPTIME-hard: Given an initial condition of size $n$, does there exist a corresponding $T_{\text{exp}}$-tiling of $\{0, \dots, 2^n - 1\} \times \{0, \dots, 2^n - 1\}$?

* There is a tiling system $T_{\text{und}}$ such that the following problem is undecidable: Given an initial condition of size $n$, does there exist a corresponding $T_{\text{und}}$-tiling of $\mathbb{N} \times \mathbb{N}$?

## 5.1 NEXPTIME Hardness for ALCO TBoxes

From prior works, it is known that monodic standpoint SHIQ, a sublogic of $S_{SHOIQB_s}^{\text{mon}}$, has an EXPTIME-complete satisfiability problem (Gómez Álvarez and Rudolph 2024), which means that the complexity of SHIQ is unaltered if monodic standpoints are added. Two other popular EXPTIME-complete sub-DLs of SHOIQB<sub>s</sub> (incomparable to SHIQ) are SHIO and SHOQ (Hladik and Model 2004; Glimm, Horrocks, and Sattler 2008). This poses the question if adding monodic standpoints to these DLs preserves EXPTIME reasoning, like it does for SHIQ.

Interestingly, we can answer this question in the negative (unless NEXPTIME = EXPTIME), and identify nominals as the common culprit by showing that satisfiability even of monodic standpoint TBoxes in ALCO (a restricted sublogic of both SHIO and SHOQ) is already NEXPTIME-hard.

To this end, we provide a polynomial reduction from the first of the two above tiling problems to the satisfiability problem of a $S_{ALCO}^{\text{mon}}$ TBox of size polynomial in $n$, using just one nominal concept $\{o\}$. We use atomic concepts $T_1, \dots, T_k$ for the $k$ tiles and atomic concepts $X_1, \dots, X_n$ as well as $Y_1, \dots, Y_n$ to encode grid x- and y-coordinates in binary. First, we declare all these concepts as “almost rigid”: they hold uniformly across precisifications for all elements but $o$.

$$
\neg\{o\} \sqcap T_{\ell} \sqsubseteq \Box_{*} T_{\ell} \quad \neg\{o\} \sqcap X_{i} \sqsubseteq \Box_{*} X_{i} \quad \neg\{o\} \sqcap Y_{i} \sqsubseteq \Box_{*} Y_{i}
$$

Above and below, we let $i$ range from 1 to $n$ and let $\ell$ range from 1 to $k$. Next, we ensure that, in every precisification, every non-$o$ element with x-coordinate (y-coordinate) smaller than $2^n - 1$ has a horizontal (vertical) neighbour with that coordinate incremented and the same y-coordinate (x-
coordinate). We let $j$ range from 1 to $i-1$.

$$ 
\begin{aligned}
\neg\{o\} \sqcap \sqcup_i \neg\mathbf{X}_i &\sqsubseteq \exists\mathbf{H}.\neg\{o\} & \neg\{o\} \sqcap \sqcup_i \neg\mathbf{Y}_i &\sqsupseteq \exists\mathbf{V}.\neg\{o\} \\
\mathbf{X}_i \sqcap \neg\mathbf{X}_j &\sqsubseteq \forall\mathbf{H}.\mathbf{X}_i & \mathbf{Y}_i \sqcap \neg\mathbf{Y}_j &\sqsubseteq \forall\mathbf{V}.\mathbf{Y}_i \\
\neg\mathbf{X}_i \sqcap \neg\mathbf{X}_j &\sqsubseteq \forall\mathbf{H}.\neg\mathbf{X}_i & \neg\mathbf{Y}_i \sqcap \neg\mathbf{Y}_j &\sqsubseteq \forall\mathbf{V}.\neg\mathbf{Y}_i \\
\mathbf{X}_i \sqcap \sqcup_j \mathbf{Y}_j &\sqsubseteq \forall\mathbf{H}.\neg\mathbf{X}_i & \mathbf{Y}_i \sqcap \sqcup_j \mathbf{Y}_j &\sqsubseteq \forall\mathbf{V}.\neg\mathbf{Y}_i \\
\neg\mathbf{X}_i \sqcap \sqcup_j \mathbf{Y}_j &\sqsubseteq \forall\mathbf{H}.\mathbf{X}_i & \neg\mathbf{Y}_i \sqcap \sqcup_j \mathbf{Y}_j &\sqsubseteq \forall\mathbf{V}.\mathbf{Y}_i
\end{aligned}
$$

$$ \mathbf{Y}_i \sqsubseteq \forall \mathbf{H}. \mathbf{Y}_i \quad \neg \mathbf{Y}_i \sqsubseteq \forall \mathbf{H}. \neg \mathbf{Y}_i \quad \mathbf{X}_i \sqsubseteq \forall \mathbf{V}. \mathbf{X}_i \quad \neg \mathbf{X}_i \sqsubseteq \forall \mathbf{V}. \neg \mathbf{X}_i $$

We next ensure that there exists a non-o element with x and y set to zero, which together with its horizontal neighbours realises the initial condition $\langle t_0, \dots, t_n \rangle \in \{1, \dots, k\}^n$.

$$ \supset \exists \mathbf{R}. (\neg\{o\} \sqcap \neg\mathbf{X}_1 \sqcap \dots \sqcap \neg\mathbf{X}_n \sqcap \neg\mathbf{Y}_1 \sqcap \dots \sqcap \neg\mathbf{Y}_n \sqcap \\ \qquad \mathbf{T}_{t_1} \sqcap \forall \mathbf{H}. (\mathbf{T}_{t_2} \sqcap \forall \mathbf{H}. (\dots \sqcap \mathbf{T}_{t_{n-1}} \sqcap \forall \mathbf{H}. \mathbf{T}_{t_n}) \dots)) $$

For every non-o element, there exists some precisification wherein it is P-linked to o and propagates its x- and y-coordinate as well as its tile assignment via this link to o.

$$ \begin{array}{l} \neg\{o\} \sqsubseteq \diamond_* \exists \mathbf{P}.\{o\} & \mathbf{X}_i \sqsubseteq \forall \mathbf{P}.\mathbf{X}_i \\ \mathbf{T}_i \sqsubseteq \forall \mathbf{P}.\mathbf{T}_i & \neg\mathbf{X}_i \sqsubseteq \forall \mathbf{P}.\neg\mathbf{X}_i \quad \neg\mathbf{Y}_i \sqsubseteq \forall \mathbf{P}.\neg\mathbf{Y}_i \end{array} $$

In every precisification, every non-o element is P'-linked to o and, should its assigned x- and y-coordinate coincide with those assigned to o, then its tile-assignment will be made to coincide with the one of o as well.

$$ \begin{array}{l} \neg\{o\} \sqsubseteq \exists \mathbf{P}'.\{o\} \\ \exists \mathbf{P}'. \mathbf{T}_\ell \sqcap \sqcup_i ((\mathbf{X}_i \sqcap \exists \mathbf{P}'. \mathbf{X}_i) \sqcup (\neg \mathbf{X}_i \sqcap \exists \mathbf{P}'. \neg \mathbf{X}_i)) \\ \qquad \sqcap \sqcup_i ((\mathbf{Y}_i \sqcap \exists \mathbf{P}'. \mathbf{Y}_i) \sqcup (\neg \mathbf{Y}_i \sqcap \exists \mathbf{P}'. \neg \mathbf{Y}_i)) \sqsubseteq \mathbf{T}_\ell \end{array} $$

Note that this way, the tile assignments will be synchronized between all elements carrying the same coordinates. We finally make sure that in every precisification, every domain element must be assigned a tile. Moreover the H- and V-neighbouring pairs of elements must conform with the horizontal and vertical compatibility relation.

$$ \begin{array}{l} \supset \sqsubseteq \mathbf{T}_1 \sqcup \dots \sqcup \mathbf{T}_k \\ \mathbf{T}_\ell \sqsubseteq \forall \mathbf{H}. \neg \mathbf{T}_\ell' \quad \text{for } (\ell, \ell') \in \{1, \dots, k\} \times \{1, \dots, k\} \setminus \mathbf{H} \\ \mathbf{T}_\ell \sqsubseteq \forall \mathbf{V}. \neg \mathbf{T}_\ell' \quad \text{for } (\ell, \ell') \in \{1, \dots, k\} \times \{1, \dots, k\} \setminus \mathbf{V} \end{array} $$

This finishes the description of the TBox (obtained by taking the conjunction of all the introduced GCIs). We note that these axioms do not enforce the H and V relation to form a proper grid (in any precisification). Rather, the axioms ensure that for any two horizontally (vertically) neighbouring coordinate pairs, there exists a H-connected (V-connected) pair of domain elements carrying said coordinates. Since the tile assignments are rigid (except for o) and synchronized over all elements carrying equal coordinates, this suffices to ensure that satisfiability of our TBox coincides with the existence of a $\mathbf{T}_{\text{exp}}$-tiling, so we obtain the following theorem.

**Theorem 28.** In any sublogic of $\mathbb{S}_{\text{SHOIQB}_s}^{\text{mon}}$ that subsumes $\mathbb{S}_{\text{ALCO}}^{\text{mon}}$ TBoxes, satisfiability is NEXPTIME-complete.

## 5.2 Lifting Monodicity Causes Undecidability

A crucial restriction underlying all logical formalisms that we have considered so far is monodicity requiring that modal operators can only be put in front of subformulae with at most one free variable. The arguably mildest way of lifting monodicity is by imposing that one distinguished binary predicate, say E, must be rigidly interpreted. Note that rigidity of a binary predicate E could be expressed by the FOSL

formula $\forall x, y. (E(x, y) \rightarrow \square_* E(x, y))$, which is not monodic. By a reduction from the second of the above tiling problems, we show that allowing one rigid binary predicate causes undecidability even for a sublogic of $\mathbb{S}_{\text{SHOIQB}_s}^{\text{mon}}$.

**Theorem 29.** Satisfiability of $\mathbb{S}_{\text{ALCOIF}}^{\text{mon}}$ TBoxes with one rigid binary predicate is undecidable, even when using just one nominal and one functionality statement.

For space reasons, we only briefly provide a set of GCIs enforcing an $\mathbb{N} \times \mathbb{N}$ grid, noting that a $\mathbf{T}_{\text{und}}$-tiling on top can be obtained very similarly to the previous case. Let E be the distinguished rigid binary predicate, which we use to represent both horizontal and vertical grid connections (distinguishing them via extra unary rigid "markers" for even/odd grid rows). Let func(Point) specify that the binary "pointer predicate" Point is functional and put the following GCIs:

$$ \begin{array}{l} \supset \sqsubseteq \exists \mathbf{E}. \square_* \text{Even} \sqcap \exists \mathbf{E}. \square_* \text{Odd} \sqcap \diamond_* \text{Pick} \\ \qquad \text{Pick} \sqsubseteq \forall \mathbf{E}. (\neg \text{Even} \sqcup \forall \mathbf{E}. (\neg \text{Odd} \sqcup \exists \text{Point}^- . \{o\})) \\ \qquad \text{Pick} \sqsubseteq \forall \mathbf{E}. (\neg \text{Odd} \sqcup \forall \mathbf{E}. (\neg \text{Even} \sqcup \exists \text{Point}^- . \{o\})) \end{array} $$

In a nutshell, these GCIs ensure that every grid element $\delta$ will be Picked in some precisification, and in that precisification the upper neighbour of $\delta$'s right neighbour is forced to coincide with the right neighbour of $\delta$'s upper neighbour, by having both being "functionally Pointed to" from o.

We note that this finding contrasts with a positive result by Artale, Lutz, and Toman (2007), according to which – in our nomenclature – the satisfiability of TBoxes over $\mathcal{ALCIQ}$ with arbitrarily many rigid roles and one S5 modality allowed to occur in front of concept *and role expressions*, is decidable in $2\text{EXPTIME}$. Once more, this underlines the previous observation that while counting and inverses go reasonably well with standpoint modalities, nominals do not.

# 6 Conclusions and Future Work

We have shown that monodic standpoints can be added to $C^2$ without increasing the NEXPTIME reasoning complexity. We obtained this result by establishing a polynomial translation into plain $C^2$, whose justification required rather elaborate model-theoretic constructions and arguments. On one hand, this finding advances the research into first-order modal logics, since our result subsumes the case of monodic S5 over $C^2$ and even generalises to logics with more expressive counting. On the other hand, we leveraged the obtained result to prove that very expressive DLs subsuming popular W3C-standardized ontology languages can be endowed with monodic standpoints in a complexity-neutral way. We finally showed that in the presence of nominal concepts, NEXPTIME-hardness already arises for much less expressive DLs, and lifting monodicity even incurs undecidability.

For future work, it would be interesting to investigate the data complexity of our formalism. Also it would be advantageous to find translations from versions of monodic standpoint OWL into plain OWL rather than $C^2$, since this would allow to deploy existing highly optimized OWL reasoners for standpoint-aware ontological reasoning. While our results show that there are no complexity-theoretic barriers for this, our current translation approach heavily relies on features of $C^2$ that are beyond the capabilities of plain OWL.
Acknowledgements

We thank the anonymous reviewers for their constructive and useful comments, which helped us to improve the paper. This work is funded by the Agence Nationale de la Recherche, France (ANR) in project ANR-25-CE23-2478-01 (SPaRK), Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) grant 389792660 as part of TRR 248 – CPEC (Center for Perspicuous Systems), as well as the German Bundesministerium für Forschung, Technologie und Raumfahrt (BMFTR, Federal Ministry of Research, Technology and Space) and Deutscher Akademischer Austauschdienst (DAAD, German Academic Exchange Service) in project 57616814, SECAI (School of Embedded and Composite AI).

References

Artale, A.; Lutz, C.; and Toman, D. 2007. A description logic of change. In Veloso, M. M., ed., *Proc. 20th Int. Joint Conf. on Artificial Intelligence*, 218–223. AAAI Press.

Baader, F.; Horrocks, I.; Lutz, C.; and Sattler, U. 2017. *An Introduction to Description Logic*. Cambridge University Press.

Bao, J.; Calvanese, D.; Grau, B. C.; Dzbor, M.; Fokoue, A.; Golbreich, C.; Hawke, S.; Herman, I.; Hoekstra, R.; Horrocks, I.; Kendall, E.; Krötzsch, M.; Lutz, C.; McGuinness, D. L.; Motik, B.; Pan, J.; Parsia, B.; Patel-Schneider, P. F.; Rudolph, S.; Ruttenberg, A.; Sattler, U.; Schneider, M.; Smith, M.; Wallace, E.; Wu, Z.; and Zimmermann, A. 2009. OWL 2 Web Ontology Language: Document Overview. W3C Recommendation. http://www.w3.org/TR/owl2-overview/.

Benedikt, M.; Kostylev, E. V.; and Tan, T. 2020. Two variable logic with ultimately periodic counting. In Czumaj, A.; Dawar, A.; and Merelli, E., eds., *Proc. 47th Int. Colloquium on Automata, Languages and Programming*, volume 168 of LIPIcs, 112:1–112:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

Demri, S., and de Nivelle, H. 2005. Deciding regular grammar logics with converse through first-order logic. *Journal of Logic Language and Information* 14(3):289–329.

Gabbay, D. M.; Kurucz, A.; Wolter, F.; and Zakharyaschev, M. 2005. Many-dimensional modal logics: Theory and applications. *Studia Logica* 81(1):147–150.

Glimm, B.; Horrocks, I.; and Sattler, U. 2008. Unions of conjunctive queries in SHOQ. In Brewka, G., and Lang, J., eds., *Proc. 11th Int. Conf. on Principles of Knowledge Representation and Reasoning*, 252–262. AAAI Press.

Gómez Álvarez, L., and Rudolph, S. 2021. Standpoint logic: Multi-perspective knowledge representation. In Neuhaus, F., and Brodaric, B., eds., *Proc. 12th Int. Conf. on Formal Ontology in Information Systems*, volume 344 of *FAIA*, 3–17. IOS Press.

Gómez Álvarez, L., and Rudolph, S. 2025. Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monadic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix).

Gómez Álvarez, L., and Rudolph, S. 2024. Reasoning in SHIQ with axiom- and concept-level standpoint modalities. In Marquis, P.; Ortiz, M.; and Pagnucco, M., eds., *Proc. 21st Int. Conf. on Principles of Knowledge Representation and Reasoning*, 383–393. ijcai.org.

Gómez Álvarez, L.; Rudolph, S.; and Strass, H. 2022. How to agree to disagree - managing ontological perspectives using standpoint logic. In Sattler, U.; Hogan, A.; Keet, C. M.; Presutti, V.; Almeida, J. P. A.; Takeda, H.; Monnin, P.; Pirrò, G.; and d'Amato, C., eds., *Proc. 21st Int. Semantic Web Conf.*, volume 13489 of LNCS, 125–141. Springer.

Gómez Álvarez, L.; Rudolph, S.; and Strass, H. 2023a. Pushing the boundaries of tractable multiperspective reasoning: A deduction calculus for standpoint EL+. In Marquis, P.; Son, T. C.; and Kern-Isberner, G., eds., *Proc. 20th Int. Conf. on Principles of Knowledge Representation and Reasoning*, 333–343. ijcai.org.

Gómez Álvarez, L.; Rudolph, S.; and Strass, H. 2023b. Tractable diversity: Scalable multiperspective ontology management via standpoint EL. In Elkind, E., ed., *Proc. 32nd Int. Joint Conf. on Artificial Intelligence*, 3258–3267. ijcai.org.

Hladik, J., and Model, J. 2004. Tableau systems for SHIO and SHIQ. In Haarslev, V., and Möller, R., eds., *Proc. 2004 Int. Workshop on Description Logics*, volume 104 of CEUR Workshop Proceedings. CEUR-WS.org.

Kazakov, Y. 2008. RIQ and SROIQ are harder than SHOIQ. In Brewka, G., and Lang, J., eds., *Proc. 11th Int. Conf. on Principles of Knowledge Representation and Reasoning*, 274–284. AAAI Press.

Kurucz, A.; Wolter, F.; and Zakharyaschev, M. 2023. Definitions and (uniform) interpolants in first-order modal logic. In Marquis, P.; Son, T. C.; and Kern-Isberner, G., eds., *Proc. 20th Int. Conf. on Principles of Knowledge Representation and Reasoning*, 417–428. ijcai.org.

Pratt-Hartmann, I. 2005. Complexity of the two-variable fragment with counting quantifiers. *Journal of Logic, Language, and Information* 14(3):369–395.

Rudolph, S.; Krötzsch, M.; and Hitzler, P. 2008. Cheap Boolean role constructors for description logics. In Hölldobler, S.; Lutz, C.; and Wansing, H., eds., *Proc. 11th European Conf. on Logics in Artificial Intelligence*, volume 5293 of LNCS, 362–374. Springer.

Rudolph, S. 2011. Foundations of description logics. In Polleres, A.; d'Amato, C.; Arenas, M.; Handschuh, S.; Kroner, P.; Ossowski, S.; and Patel-Schneider, P. F., eds., *Reasoning Web. Semantic Technologies for the Web of Data - 7th International Summer School 2011, Tutorial Lectures*, volume 6848 of LNCS, 76–136. Springer.

Tobies, S. 2000. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. *Journal of Artificial Intelligence Research* 12:199–217.

Wolter, F., and Zakharyaschev, M. 2001. Decidable fragments of first-order modal logics. *Journal of Symbolic Logic* 66(3):1415–1438.