1735 LABEL:LastPageApr. 02, 2020Jul. 20, 2021

# Axiomatizing Hybrid XPath with Data

Carlos Areces  Universidad Nacional de Córdoba & CONICET, Argentina  and  Raul
Fervari<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

In this paper we introduce sound and strongly complete axiomatizations for
XPath with data constraints extended with hybrid operators. First, we present
$\text{HXPath}_{=}$, a multi-modal version of XPath with data, extended with
nominals and the hybrid operator $@$. Then, we introduce an axiomatic system
for $\text{HXPath}_{=}$, and we prove it is strongly complete with respect to
the class of abstract data models, i.e., data models in which data values are
abstracted as equivalence relations. We prove a general completeness result
similar to the one presented in, e.g., [BtC06], that ensures that certain
extensions of the axiomatic system we introduce are also complete. The
axiomatic systems that can be obtained in this way cover a large family of
hybrid XPath languages over different classes of frames, for which we present
concrete examples. In addition, we investigate axiomatizations over the class
of tree models, structures widely used in practice. We show that a strongly
complete, finitary, first-order axiomatization of hybrid XPath over trees does
not exist, and we propose two alternatives to deal with this issue. We finally
introduce filtrations to investigate the status of decidability of the
satisfiability problem for these languages.

###### Key words and phrases:

XPath, data graphs, axiomatizations, data trees, decidability

##  1\. XPath as a Modal Logic with Data Tests

XPath is, arguably, the most widely used query language for the eXtensible
Markup Language (XML). Indeed, XPath is implemented in XSLT [Wad00] and XQuery
[Wor02] and it is used in many specification and update languages (e.g.,
Saxon). It is, fundamentally, a general purpose language for addressing,
searching, and matching pieces of an XML document. It is an open standard and
constitutes a World Wide Web Consortium (W3C) Recommendation [CD99]. In
[KRV15] XPath is adapted to be used as a powerful query language over
knowledge bases. Core-XPath [GKP05] is the fragment of XPath 1.0 containing
the navigational behaviour of XPath. It can express properties of the
underlying tree structure of the XML document, such as the label (tag name) of
a node, but it cannot express conditions on the actual data contained in the
attributes. In other words, it is essentially a _classical modal logic_
[BdRV01, BvBW06]. For instance the path expressions child, parent and
descendant-or-self are basically the modal operators $\lozenge$,
$\lozenge^{-}$ and $\lozenge^{*}$ respectively.

Core-XPath has been well studied from a modal logic point of view. For
instance, its satisfiability problem is known to be decidable even in the
presence of Document Type Definitions (DTDs) [Mar04, BFG08]. Moreover, it is
known that it is equivalent, in terms of expressive power, to first-order
logic with two variables (FO2) over an appropriate signature on trees [MdR05],
and that it is strictly less expressive than Propositional Dynamic Logic (PDL)
with converse over trees [BK08]. Sound and complete axiomatizations for Core-
XPath have been introduced in [tCM09, tCLM10]. It has been argued that the
study of XPath from a modal logic point of view is not merely a theoretical
challenge but it has also concrete applications. For instance, by
investigating the _expressive power_ of XPath fragments it is possible to
determine if an integrity constraint can be simplified. Also, query
containment and query equivalence –two fundamental tasks in query
optimization– can be reduced to the _satisfiability problem_. In particular
these results have direct impact on, e.g., security [FCG04], type checking
[MN07] and consistency of XML specifications [AFL02].

However, from a database perspective, Core-XPath falls short to define the
most important construct in a query language: the _join_. Without the ability
to relate nodes based on the actual data values of the attributes, the logic’s
expressive power is inappropriate for many applications. The extension of
Core-XPath with (in)equality tests between attributes of elements in an XML
document is named Core-Data-XPath in [BMSS09]. Here, we will call this logic
$\text{XPath}_{=}$. Models of $\text{XPath}_{=}$ are usually data trees which
can be seen as XML documents. A data tree is a tree whose nodes contain a
label from a finite alphabet and a data value from an infinite domain. From a
modal logic perspective, these data trees are a particular class of
_relational models_. In recent years other data structures have been
considered, and $\text{XPath}_{=}$ has been used to query these structures. In
particular, in this article we consider arbitrary _data graphs_ as models for
$\text{XPath}_{=}$. Data graphs are the underlying mathematical structure in
_graph databases_ (see, e.g., [LV12, RWE13, AG08]) and it is important to
study the metalogical properties of languages to query this particular kind of
models (see, e.g., [LMV16, ABFF18]). In this respect, we focus on a variant of
$\text{XPath}_{=}$ which provides us with several interesting expressivity
features.

$\begin{array}[]{c}Person\\\
Name:Alice\end{array}$$\mathsf{A1}$$\begin{array}[]{c}Person\\\
Name:Bob\end{array}$$\begin{array}[]{c}Person\\\
Name:Alice\end{array}$$\mathsf{A2}$$\begin{array}[]{c}Person\\\
Name:Bob\end{array}$$\begin{array}[]{c}Date\\\
Value:7/7/1977\end{array}$$\begin{array}[]{c}Date\\\
Value:7/7/1977\end{array}$$\begin{array}[]{c}Date\\\
Value:5/5/1975\end{array}$$\begin{array}[]{c}Date\\\
Value:8/8/1988\end{array}$$\mathsf{friends}$$\mathsf{friends}$$\mathsf{born}$$\mathsf{born}$$\mathsf{born}$$\mathsf{born}$
Figure 1. Example of a graph-structured database.

Figure 1 shows an example of a data graph, where we can see that edges carry
labels from a finite alphabet (such as “friends”), and whose nodes carry data
values, usually presented as a “ _key: value_ ” pair, with _key_ being a label
from a finite alphabet (e.g., “Name”) and _value_ being a data value from an
infinite domain (e.g., “Alice”).

One of the characteristic advantages of graph databases is that they directly
exhibit the _topology_ of the data. Most of the approaches for querying these
databases have focused on exploring the topology of the underlying graph
exclusively. However, little attention has been paid to queries that check how
the actual data contained in the graph nodes relates with the topology.
$\text{XPath}_{=}$ allows comparison of data values by equality or inequality,
even though it does not grant access to the concrete data values themselves.

The main characteristic of $\text{XPath}_{=}$ is to allow formulas of the form
$\langle\alpha=\beta\rangle$ and $\langle\alpha\neq\beta\rangle$, where
$\alpha,\beta$ are path expressions that navigate the graph using
accessibility relations: successor, predecessor, and for the particular case
of tree-like models, descendant, next-sibling, etc.; and can make tests in
intermediate nodes. In addition, in this work we consider the novel ‘$@$’
navigation operator that allows us to jump to named nodes. The formula
$\langle\alpha=\beta\rangle$ (respectively $\langle\alpha\neq\beta\rangle$) is
true at a node $x$ of a data graph if there are nodes $y,z$ that can be
reached by paths satisfying the expressions $\alpha$ and $\beta$ respectively,
and such that the data value of $y$ is equal (respectively different) to the
data value of $z$.

The benefits of having data comparisons is described in the following example.
Consider a social network which stores the information about the friendship
relation between persons, and also stores the date of birth of each individual
in the network. This scene can be represented as in Figure 1. Topological
information is not sufficient to distinguish the Alice on the left, A1 from
the Alice on the right, A2 (formally, these two nodes are bisimilar for the
basic modal logic). However, the expression ‘the person that is friend of
someone born the same day” expressible in $\text{XPath}_{=}$, is true only at
A1.

Recent articles investigate $\text{XPath}_{=}$ from a modal perspective. For
example, satisfiability and evaluation are discussed in [Fig10, FS11, Fig12],
while model theory and expressivity are studied in [ADF14, FFA14, FFA15,
ADF17, ABFF16, ABFF18]. Query power and complexity of several
$\text{XPath}_{=}$ fragments are investigated in [LMV16, Fig18]. In [BLS16], a
Gentzen-style sequent calculus is given for a very restricted fragment of
$\text{XPath}_{=}$, named DataGL. In DataGL, data comparisons are allowed only
between the evaluation point and its successors. An extension of the
equational axiomatic system from [tCLM10] is introduced in [ADFF17], allowing
downward navigation and equality/inequality tests.

In this article, we will focus on the proof theory of $\text{XPath}_{=}$
extended with hybrid operators. It has been argued that the inclusion of
hybrid operators in a modal language leads to a better proof theory [Bra11].
In particular, it can lead to general completeness results for axiomatizations
by enabling Henkin style completeness proofs [BdRV01, BtC06]. Moreover, we
will focus on strong completeness results (i.e., the axiomatizations we
introduce characterize the consequence relation $\Gamma\vdash\varphi$ and not
only theoremhood $\vdash\varphi$).

First results using hybridization techniques were introduced in [AF16] for a
basic axiomatic system for $\text{XPath}_{=}$. In [AFS17] nominals are used as
labels in a tableaux system.

#### Contribution.

We will introduce a Hilbert-style axiomatization for $\text{XPath}_{=}$ with
forward navigation for multiple accessibility relations, multiple
equality/inequality comparisons, and where node expressions are extended with
nominals (special labels that are valid in only one node), and path
expressions are extended with the hybrid operator $@$ (allowing the navigation
to some particular named node). We call this logic Hybrid XPath with Data
(denoted $\text{HXPath}_{=}$). The language we consider is a variant of XPath
fragments for data graphs in the literature. It improves the expressive power
of the fragment $\text{XPath}_{=}$ from [ABFF16, ABFF18], e.g., by enabling us
to express global properties. On the other hand, it has similarities with the
fragment GXPathcore(eq) from [LMV16]. GXPathcore(eq) allows us to express data
properties of nodes that are reachable in a finite number of steps, due to the
reflexive-transitive navigation on atomic steps. However, the hybrid operator
$@$ in $\text{HXPath}_{=}$ is enough to capture some of its expressivity by
allowing us to ‘jump’ to nodes that are not accessible in one step, or that
are simply not connected with the current node. One of the advantages of our
approach, is that hybrid operators add only first-order behaviour, whereas
reflexive-transitive closure needs second-order expressivity.

We will take advantage of hybrid operators to prove completeness using a
Henkin-style model construction as presented in [Gol84, BdRV01, BtC06, SP10].
In fact, the use of the so-called unorthodox inference rules (i.e., inference
rules involving side conditions) will help us define an axiom system whose
completeness can be automatically extended to more expressive logics.

Summing up, our contributions in this article are the following:

  * •

We define a sound and strongly complete axiomatic system for multi-modal
$\text{HXPath}_{=}$, refining the axioms and rules first presented in [AF16].

  * •

We give a Henkin-style completeness proof, proving that the system is strongly
complete for any extension given by pure axioms (formulas involving only
nominals) and existential rules (instantiations of first-order formulas with
quantification pattern $\forall\exists$ followed by an
$\text{HXPath}_{=}$-formula). This gives us a strong completeness result with
respect to a wide variety of frame classes.

  * •

Even though the main focus of our work is axiomatizing node expressions, we
also provide as a by-product strong completeness results for path expressions.

  * •

We discuss concrete extensions of $\text{HXPath}_{=}$ in which completeness is
automatically obtained. In particular we explore backward and sibling
navigation, and equality inclusion.

  * •

We show that a strongly complete, finitary, first-order axiomatization of
hybrid XPath over trees does not exist. Then we introduce an infinite pure
axiomatic system that is strongly complete for a slightly larger class of tree
models. We also prove that this system is weakly complete over tree models. As
a corollary of the method we use, we conclude that the satisfiability problem
for $\text{HXPath}_{=}$ on trees is decidable in ExpSpace.

  * •

Finally, we prove that the satisfiability problem for the multi-modal logic
$\text{HXPath}_{=}$ and some of its pure extensions is decidable in NExpTime,
using filtrations to establish a bounded finite model property. To our
knowledge, the best known lower bound can be obtained by PSpace-hardness of
mono-modal hybrid XPath with forward navigation [AFS17].

#### Related Work.

It is argued in [BtC06] that hybrid logic is a natural setting for deductive
systems involving Kripke semantics. By having nominals in the language, it is
possible to imitate the role of first-order constants to obtain a Henkin-style
completeness proof. Moreover, hybrid operators provide all the necessary
machinery to get general completeness results for a wide variety of systems.
The claim is that allowing the use of _unorthodox rules_ , we can define a
basic axiomatic system that can be extended with _pure axioms_ and
_existential rules_ , which lets us obtain complete extensions with respect to
diverse classes of frames, automatically.

One of the first proof systems for data-aware fragments of XPath was
introduced in [BLS16]. It is a Gentzen-style system for a very restricted
language named _DataGL_ , interpreted on finite data trees. In _DataGL_
formulas of the form $\Diamond_{=}\varphi$ are read as: _“the current node has
the same data as a descendant where $\varphi$ holds”_. They introduced a sound
and weakly complete sequent calculus for _DataGL_ and established PSpace-
completeness for its validity problem.

An equational system which extends the one presented for navigational
fragments of XPath in [tCLM10] was introduced in [ADFF17]. The authors
consider first the fragment of $\text{XPath}_{=}$ without inequality tests,
over data trees. Therein, the proof of weak completeness relies on a normal
form theorem for both node and path expressions, and on a canonical model
construction for consistent formulas in normal form inspired by [Fin75]. When
inequality is also taken into account, similar ideas can be used but the
canonical model construction and the corresponding completeness proof become
quite complex.

A Hilbert-style axiomatization for $\text{XPath}_{=}$ extended with hybrid
operators and backward navigation was first introduced in [AF16], using ideas
from hybrid logic: nominals play the role of first-order constants in a
Henkin-style completeness proof. The system we present herein is a vast
extension of the work from [AF16], and it automatically encompasses a large
family of logics.

In [AFS17] nominals are used as labels in a tableaux system for a restricted
variant of $\text{HXPath}_{=}$ with only one accessibility relation and one
equality relation. The tableaux calculus is shown to be sound, complete and
terminating, and it is used to prove that the satisfiability problem for such
logic is PSpace-complete.

#### Organization.

The article is organized as follows. In Section 2 we introduce the syntax,
semantics and a notion of bisimulation for $\text{HXPath}_{=}$. We define the
axiomatic system $\mathsf{HXP}$ in Section 3 and we prove its completeness. We
finish that section by introducing extensions of $\mathsf{HXP}$ and their
complete axiomatizations with pure axioms and existential rules. In Section 4
we introduce an axiomatic system for XPath over the class of data trees. Then,
we use filtrations to show that the satisfiability problem of
$\text{HXPath}_{=}$ is decidable in Section 5. To conclude, in Section 6 we
discuss the results and introduce future lines of research.

##  2\. Hybrid XPath with Data

In this section we introduce the syntax and semantics for the logic we call
Hybrid XPath with Data ($\text{HXPath}_{=}$ for short). Then, we present a
notion of bisimulation for $\text{HXPath}_{=}$.

###  2.1. Syntax and Semantics of $\text{HXPath}_{=}$

Thoughout the text, let $\mathsf{Prop}$ be a countable set of propositional
symbols; let $\mathsf{Nom}$ be a countable set of nominals such that
$\mathsf{Prop}\cap\mathsf{Nom}=\emptyset$; and let $\mathsf{Mod}$ and
$\mathsf{Eq}$ be sets of modal and equality symbols, respectively.

######  Definition  (Syntax).

The sets $\mathsf{PExp}$ of path expressions (which we will note as $\alpha$,
$\beta$, $\gamma$, $\ldots$) and $\mathsf{NExp}$ of node expressions (which we
will note as $\varphi$, $\psi$, $\theta$, $\ldots$) of $\text{HXPath}_{=}$ are
defined by mutual recursion as follows:

$\displaystyle\mathsf{PExp}\;$
$\displaystyle\mathrel{{\mathop{:}}{\mathop{:}}}=\;{\mathsf{a}}\mathrel{\,\mid\,}@_{i}\mathrel{\,\mid\,}[\varphi]\mathrel{\,\mid\,}\alpha\beta$
$\displaystyle\mathsf{NExp}\;$
$\displaystyle\mathrel{{\mathop{:}}{\mathop{:}}}=\;p\mathrel{\,\mid\,}i\mathrel{\,\mid\,}\neg\varphi\mathrel{\,\mid\,}\varphi\wedge\psi\mathrel{\,\mid\,}\langle\alpha=_{e}\beta\rangle\mathrel{\,\mid\,}\langle\alpha\neq_{e}\beta\rangle,$

where $p\in\mathsf{Prop}$, $i\in\mathsf{Nom}$, $\mathsf{a}\in\mathsf{Mod}$,
$e\in\mathsf{Eq}$, $\varphi,\psi\in\mathsf{NExp}$, and
$\alpha,\beta\in\mathsf{PExp}$. We will refer to members of
$\mathsf{PExp}\cup\mathsf{NExp}$ as expressions. In what follows, when
referring to expressions of $\text{HXPath}_{=}$ we will reserve the term
_formula_ for members of $\mathsf{NExp}$. We say that an expression is _pure_
if it does not contain propositional symbols.

Notice that path expressions occur in node expressions in _data comparisons_
of the form $\langle\alpha=_{e}\beta\rangle$ and
$\langle\alpha\neq_{e}\beta\rangle$, while node expressions occur in path
expressions in _tests_ like $[\varphi]$.

In what follows we will always use $*$ for $=_{e}$ and $\not=_{e}$, when the
particular operator used is not relevant. Other Boolean operators are defined
as usual: $\varphi\vee\psi:=\neg(\neg\varphi\wedge\neg\psi)$, and
$\varphi\rightarrow\psi:=\neg\varphi\vee\psi$. Below we define other operators
as abbreviations.

######  Definition  (Abbreviations).

Let $\alpha,\beta,\delta$ be path expressions, $\gamma_{1},\gamma_{2}$ path
expressions or the empty string, $\varphi$ a node expression, $i$ a nominal,
and $p$ an arbitrary symbol in $\mathsf{Prop}$. We define the following
expressions:

$\top$ | $:=$ | $p\vee\neg p$
---|---|---
$\bot$ | $:=$ | $\neg\top$
$\epsilon$ | $:=$ | $[\top]$
$[\alpha=_{e}\beta]$ | $:=$ | $\neg\langle\alpha\neq_{e}\beta\rangle$
$[\alpha\neq_{e}\beta]$ | $:=$ | $\neg\langle\alpha=_{e}\beta\rangle$
$\langle\alpha\rangle\varphi$ | $:=$ | $\langle\alpha[\varphi]=_{e}\alpha[\varphi]\rangle$
$[\alpha]\varphi$ | $:=$ | $\neg\langle\alpha\rangle\neg\varphi$
$@_{i}\varphi$ | $:=$ | $\langle@_{i}\rangle\varphi$
$\langle\gamma_{1}(\alpha\cup\beta)\gamma_{2}*\delta\rangle$ | $:=$ | $\langle\gamma_{1}\alpha\gamma_{2}*\delta\rangle\vee\langle\gamma_{1}\beta\gamma_{2}*\delta\rangle$
$\langle\delta*\gamma_{1}(\alpha\cup\beta)\gamma_{2}\rangle$ | $:=$ | $\langle\delta*\gamma_{1}\alpha\gamma_{2}\rangle\vee\langle\delta*\gamma_{1}\beta\gamma_{2}\rangle$

As a corollary of the definition of the semantic relation below, the diamond
and box expressions $\langle\alpha\rangle\varphi$ and $[\alpha]\varphi$ will
have their classical meaning, and the same will be true for hybrid formulas of
the form $@_{i}\varphi$. Notice that we use $@_{i}$ both as a path expression
and as a modality; the intended meaning will always be clear in context.
Notice also that, following the standard notation in XPath logics and in modal
logics, the $[\ ]$ operation is overloaded: for $\varphi$ a node expression
and $\alpha$ a path expression, both $[\alpha]\varphi$ and $\alpha[\varphi]$
are well-formed expressions; the former is a node expression where $[\alpha]$
is a box modality, the latter is a path expression where $[\varphi]$ is a
test.

We now define the structures that will be used to evaluate formulas in the
language.

######  Definition  (Hybrid Data Models).

An _abstract hybrid data model_ is a tuple $\mathcal{M}=\langle M,$
$\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$,
where $M$ is a non-empty set of elements; for each $e\in\mathsf{Eq}$,
${\sim_{e}}\subseteq M\times M$ is an equivalence relation between elements of
$M$; for each $\mathsf{a}\in\mathsf{Mod}$, ${R_{\mathsf{a}}}\subseteq M\times
M$ is the associated accessibility relation; $\mathit{V}:M\rightarrow
2^{\mathsf{Prop}}$ is the valuation function; and
$\mathit{nom}:\mathsf{Nom}\rightarrow M$ is a function that assigns nominals
to certain elements. Given $m\in M$, $(\mathcal{M},m)$ is called a pointed
model (parentheses are usually dropped).

An abstract data frame (or just _frame_) is a tuple $\mathcal{F}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}}\rangle$.
Let $\mathfrak{F}$ be a class of frames, its _class of models_ is
$\mathsf{Mod}(\mathfrak{F})=\\{\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle\mid\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\rangle\in\mathfrak{F},\text{
for $\mathit{V},\mathit{nom}$ arbitrary}\\}$.

A concrete hybrid data model is a tuple $\mathcal{M}=\langle
M,D,\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom},data\rangle$,
where $M$ is a non-empty set of elements; $D$ is a non-empty set of data; for
each $\mathsf{a}\in\mathsf{Mod}$, ${R_{\mathsf{a}}}\subseteq M\times M$ is the
associated accessibility relation; $\mathit{V}:M\rightarrow 2^{\mathsf{Prop}}$
is the valuation function; $\mathit{nom}:\mathsf{Nom}\rightarrow M$ is a
function which names some nodes; and $data:\mathsf{Eq}\times M\rightarrow D$
is a function which assigns a data value to each node of the model (for each
type of equality considered in the model).

Concrete data models are most commonly used in applications, where we
encounter data from an infinite alphabet (e.g., alphabetic strings) associated
to the nodes in a semi-structured database, and different ways of comparing
this data. It is easy to see that to each concrete data model we can associate
an abstract data model where data is replaced by an equivalence relation that
links all nodes with the same data, for each equality symbol from
$\mathsf{Eq}$. Vice-versa, each abstract data model can be “concretized” by
assigning to each pair node and symbol from $\mathsf{Eq}$, its equivalence
data class as data. We will prove soundness and completeness over the class of
abstract data models and, as a corollary, obtain completeness over concrete
data models.

######  Definition  (Semantics).

Let $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be an abstract data model, and $m,n\in M$. We define the semantics of
$\text{HXPath}_{=}$ as follows:

$\begin{array}[]{r@{ \ \ \iff\ \ }l}\mathcal{M},m,n\models\mathsf{a}\ \
\mbox{iff}&mR_{\mathsf{a}}n\\\ \mathcal{M},m,n\models@_{i}\ \
\mbox{iff}&\mathit{nom}(i)=n\\\ \mathcal{M},m,n\models[\varphi]\ \
\mbox{iff}&m=n\mbox{ and }\mathcal{M},m\models\varphi\\\
\mathcal{M},m,n\models\alpha\beta\ \ \mbox{iff}&\mbox{there is $l\in M$ s.t.
}\mathcal{M},m,l\models\alpha\mbox{ and }\mathcal{M},l,n\models\beta\\\
\mathcal{M},m\models p\ \ \mbox{iff}&p\in\mathit{V}(m)\\\ \mathcal{M},m\models
i\ \ \mbox{iff}&\mathit{nom}(i)=m\\\ \mathcal{M},m\models\neg\varphi\ \
\mbox{iff}&\mathcal{M},m\not\models\varphi\\\
\mathcal{M},m\models\varphi\wedge\psi\ \
\mbox{iff}&\mathcal{M},m\models\varphi\mbox{ and }\mathcal{M},m\models\psi\\\
\mathcal{M},m\models\langle\alpha=_{e}\beta\rangle\ \ \mbox{iff}&\mbox{there
are $n,l\in M$ s.t.
}\mathcal{M},m,n\models\alpha,~{}\mathcal{M},m,l\models\beta\mbox{ and
}n\sim_{e}l\\\ \mathcal{M},m\models\langle\alpha\neq_{e}\beta\rangle\ \
\mbox{iff}&\mbox{there are $n,l\in M$ s.t.
}\mathcal{M},m,n\models\alpha,~{}\mathcal{M},m,l\models\beta\mbox{ and
}n\not\sim_{e}l.\end{array}$

We say a node expression $\varphi$ (path expression $\alpha$) is _satisfiable_
if there exists $\mathcal{M},m$ ($\mathcal{M},m,n$) such that
$\mathcal{M},m\models\varphi$ ($\mathcal{M},m,n\models\alpha$). Satisfiability
for sets of node and path expressions is defined in the obvious way. Let
$\Gamma\cup\\{\varphi\\}$ be a set of node expressions, $\Gamma\models\varphi$
if for all $\mathcal{M},m$, $\mathcal{M},m\models\Gamma$ implies
$\mathcal{M},m\models\varphi$. For a class $\mathfrak{C}$ of models,
$\Gamma\models_{\mathfrak{C}}\varphi$ if for all $\mathcal{M}\in\mathfrak{C}$
and $m$ in the domain of $\mathcal{M}$, $\mathcal{M},m\models\Gamma$ implies
$\mathcal{M},m\models\varphi$. When $\Gamma=\emptyset$ we write
$\models\varphi$ (respectively $\models_{\mathfrak{C}}\varphi$).

As mentioned, it is a straightforward exercise to show that modal and hybrid
operators have their intended meaning.

######  Proposition .

Let $\mathcal{M}$ be an abstract hybrid data model and $m$ a state in
$\mathcal{M}$. Then

$\begin{array}[]{r@{\,}l@{~~\iff~~}l}\mathcal{M},m&\models@_{i}\varphi\hfil~{}~{}\mbox{iff}~{}~{}&\mathcal{M},\mathit{nom}(i)\models\varphi\\\
\mathcal{M},m&\models\langle\mathsf{a}\rangle\varphi\hfil~{}~{}\mbox{iff}~{}~{}&\mbox{for
some $n\in M$ s.t. $mR_{\mathsf{a}}n$, }\mathcal{M},n\models\varphi\\\
\mathcal{M},m&\models[\mathsf{a}]\varphi\hfil~{}~{}\mbox{iff}~{}~{}&\mbox{for
all $n\in M$, $mR_{\mathsf{a}}n$ implies
}\mathcal{M},n\models\varphi.\end{array}$

The addition of the hybrid operators to XPath increases its expressive power.
The following examples should serve as illustration.

######  Example .

We list below some $\text{HXPath}_{=}$ expressions together with their
intuitive meaning:

$\alpha[i]$ | There exists an $\alpha$ path between the current points of evaluation; the
---|---
| second node is named $i$.
$@_{i}\alpha$ | There exists an $\alpha$ path between the node named $i$ and some other node.
$\langle@_{i}=_{e}@_{j}\rangle$ | The node named $i$ has the same data as the node named $j$, w.r.t. the
| data field $e$.
$\langle\alpha=_{e}@_{i}\beta\rangle$ | There exists a node accessible from the current point of evaluation by an
|  $\alpha$ path that has the same data than a node accessible from the point
| named $i$ by a $\beta$ path, w.r.t. the data field $e$.

The next example illustrates the expressivity gained by adding hybrid
operators into the language, in a concrete example.

######  Example .

Consider the following queries in the data graph from Figure 1 (we omit the
subdindex in the symbols $=$ and $\neq$, since we deal with only one equality
relation).

$\langle@_{\sf A1}{\sf born}[Value]=@_{\sf A1}{\sf friends}\ {\sf born}[Value]\rangle$ | The person with the id A1 is friend of
---|---
| someone born in the same day.
$[@_{\sf A2}{\sf born}[Value]\neq@_{\sf A2}{\sf friends}\ {\sf born}[Value]]$ | All friends of the person with id A2
| were born in a day different to hers.
$\langle@_{\sf A1}[Name]=@_{\sf A2}[Name]\rangle$ | The persons with id A1 and A2 have
$\ \ \ \ \wedge\langle@_{\sf A1}{\sf born}[Value]\neq@_{\sf A2}{\sf born}[Value]\rangle$ | the same value (both are named Alice)
| and they were born in different days.

In the last item, the conjunct $\langle@_{\sf A1}[Name]=@_{\sf
A2}[Name]\rangle$ states that the nodes named by the nominals A1 and A2
contain a data value corresponding to the key Name, expressed by the test
$[Name]$; also, these data values coincide, without referring to the actual
value.

It is worth noting that with classical $\text{XPath}_{=}$ navigation, the two
first properties can be expressed only if we are evaluating the formulas in
the node with id A1 and A2, respectively. This is due the fact that
$\text{XPath}_{=}$ only allows local navigation. Moreover, the third formula
is not expressible in $\text{XPath}_{=}$, even in the presence of transitive
closure operators, as it involves unconnected components of the graph.

Before concluding this section, we will introduce two classical notions that
will be useful in the rest of the paper: the _modal depth_ and the set of
_subformulas_ of a formula. These definitions are given on node and path
expressions seen as strings, in particular they consider the empty string
$\lambda$ which is not in the language. However, these definitions work as
intended.

######  Definition .

We define the _modal depth_ of an expression, by mutual recursion as follows.

$\begin{array}[]{l@{~ = ~}l@{\qquad}l@{~ = ~}l}{\sf
md}(\lambda)\hfil~{}=~{}&0&{\sf md}(p)\hfil~{}=~{}&0\\\ {\sf
md}(\mathsf{a}\alpha)\hfil~{}=~{}&1+{\sf md}(\alpha)&{\sf
md}(\neg\varphi)\hfil~{}=~{}&{\sf md}(\varphi)\\\ {\sf
md}([\varphi]\alpha)\hfil~{}=~{}&\max({\sf md}(\varphi),{\sf md}(\alpha))&{\sf
md}(\varphi\wedge\psi)\hfil~{}=~{}&\max({\sf md}(\varphi),{\sf md}(\psi))\\\
{\sf md}(@_{i}\alpha)\hfil~{}=~{}&{\sf md}(\alpha)&{\sf
md}(\langle\alpha*\beta\rangle)\hfil~{}=~{}&\max({\sf md}(\alpha),{\sf
md}(\beta)),\end{array}$

where $\lambda$ represents the empty string, $\mathsf{a}\in\mathsf{Mod}$,
$p\in\mathsf{Prop}\cup\mathsf{Nom}$, $i\in\mathsf{Nom}$,
$*\in\\{=_{e},\neq_{e}\\}$, $\varphi,\psi\in\mathsf{NExp}$ and
$\alpha,\beta\in\mathsf{PExp}$.

######  Definition .

We define the set of _subformulas_ of an expression, by mutual recursion as
follows.

$\begin{array}[]{@{~}l@{\,=\,}ll@{\,=\,}l@{~}}{}\lx@intercol\mathsf{Sub}(\lambda)&\emptyset&\mathsf{Sub}(p)&\\{p\\}\hfil~{}\\\
{}\lx@intercol\mathsf{Sub}(\mathsf{a}\alpha)&\\{\langle\mathsf{a}\alpha\rangle\top\\}\cup\mathsf{Sub}(\alpha)&\mathsf{Sub}(\neg\varphi)&\\{\neg\varphi\\}\cup\mathsf{Sub}(\varphi)\hfil~{}\\\
{}\lx@intercol\mathsf{Sub}([\varphi]\alpha)&\\{\langle[\varphi]\alpha\rangle\top\\}\cup\mathsf{Sub}(\varphi)\cup\mathsf{Sub}(\alpha)&\mathsf{Sub}(\varphi\wedge\psi)&\\{\varphi\wedge\psi\\}\cup\mathsf{Sub}(\varphi)\cup\mathsf{Sub}(\psi)\hfil~{}\\\
{}\lx@intercol\mathsf{Sub}(@_{i}\alpha)&\\{\langle@_{i}\alpha\rangle\top,i\\}\cup\mathsf{Sub}(\alpha)&\mathsf{Sub}(\langle\alpha*\beta\rangle)&\\{\langle\alpha*\beta\rangle\\}\cup\mathsf{Sub}(\alpha)\cup\mathsf{Sub}(\beta),\hfil~{}\end{array}$

where $\lambda$ represents the empty string, $\mathsf{a}\in\mathsf{Mod}$,
$p\in\mathsf{Prop}\cup\mathsf{Nom}$, $i\in\mathsf{Nom}$,
$*\in\\{=_{e},\neq_{e}\\}$, $\varphi,\psi\in\mathsf{NExp}$ and
$\alpha,\beta\in\mathsf{PExp}$.

###  2.2. A Note on Bisimulations

In the rest of the paper we will sometimes need the notion of bisimulation for
$\text{HXPath}_{=}$. Bisimulation for XPath on data trees was investigated in
[FFA14, FFA15]. In [ABFF16, ABFF18] it is shown that the same notion can be
used in arbitrary models. It is simple to extend these definitions to take
into account hybrid operators (see, e.g., [ABM01, BdRV01]).

######  Definition  (Bisimulations).

Let $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{{R_{\mathsf{a}}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
and $\mathcal{M}^{\prime}=\langle
M^{\prime},\\{\sim^{\prime}_{e}\\}_{e\in\mathsf{Eq}},\\{R^{\prime}_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V}^{\prime},\mathit{nom}^{\prime}\rangle$
be two abstract hybrid data models, $m\in M$, $m^{\prime}\in M^{\prime}$. An
_$\text{HXPath}_{=}$ -bisimulation_ between $\mathcal{M},m$ and
$\mathcal{M}^{\prime},m^{\prime}$ is a relation $Z\subseteq M\times
M^{\prime}$ such that $mZm^{\prime}$, and when $lZl^{\prime}$ we have:

  * •

$(\textbf{Harmony})$ $\mathit{V}(l)=\mathit{V}^{\prime}(l^{\prime})$ and
$l=\mathit{nom}(i)$ iff $l^{\prime}=\mathit{nom}^{\prime}(i)$ (for all
$i\in\mathsf{Nom}$).

  * •

$(\textbf{Zig}_{=})$ If there are paths
$\pi_{1}=lR_{\mathsf{a}_{1}}h_{1}R_{\mathsf{a}_{2}}\ldots
R_{\mathsf{a}_{n_{1}}}h_{n_{1}}$ and
$\pi_{2}=lR_{\mathsf{b}_{1}}k_{1}R_{\mathsf{b}_{2}}\ldots
R_{\mathsf{b}_{n_{2}}}k_{n_{2}}$ (for
$\mathsf{a}_{i},\mathsf{b}_{i}\in\mathsf{Mod}$), then there are paths
$\pi^{\prime}_{1}=l^{\prime}R^{\prime}_{\mathsf{a}_{1}}h^{\prime}_{1}R^{\prime}_{\mathsf{a}_{2}}\ldots
R^{\prime}_{\mathsf{a}_{n_{1}}}h^{\prime}_{n_{1}}$ and
$\pi^{\prime}_{2}=l^{\prime}R^{\prime}_{\mathsf{b}_{1}}k^{\prime}_{1}R^{\prime}_{\mathsf{b}_{2}}\ldots\linebreak
R^{\prime}_{\mathsf{b}_{n_{2}}}k^{\prime}_{n_{2}}$ such that

    1. (1)

$h_{i}Zh^{\prime}_{i}$ for $1\leq i\leq n_{1}$.

    2. (2)

$k_{i}Zk^{\prime}_{i}$ for $1\leq i\leq n_{2}$.

    3. (3)

$h_{n_{1}}\sim_{e}k_{n_{2}}~{}\mbox{iff}~{}h^{\prime}_{n_{1}}\sim^{\prime}_{e}k^{\prime}_{n_{2}}$,
for all $e\in\mathsf{Eq}$.

  * •

$(\textbf{Zag}_{=})$ If there are paths
$\pi^{\prime}_{1}=l^{\prime}R^{\prime}_{\mathsf{a}_{1}}h^{\prime}_{1}R^{\prime}_{\mathsf{a}_{2}}\ldots
R^{\prime}_{\mathsf{a}_{n_{1}}}h^{\prime}_{n_{1}}$ and
$\pi^{\prime}_{2}=l^{\prime}R^{\prime}_{\mathsf{b}_{1}}k^{\prime}_{1}R^{\prime}_{\mathsf{b}_{2}}\ldots\linebreak
R^{\prime}_{\mathsf{b}_{n_{2}}}k^{\prime}_{n_{2}}$ (for
$\mathsf{a}_{i},\mathsf{b}_{i}\in\mathsf{Mod}$), then there are paths
$\pi_{1}=lR_{\mathsf{a}_{1}}h_{1}R_{\mathsf{a}_{2}}\ldots
R_{\mathsf{a}_{n_{1}}}h_{n_{1}}$ and
$\pi_{2}=lR_{\mathsf{b}_{1}}k_{1}R_{\mathsf{b}_{2}}\ldots
R_{\mathsf{b}_{n_{2}}}k_{n_{2}}$ such that conditions 1, 2 and 3 above are
verified.

  * •

$(\textbf{Nom})$ For all $i\in\mathsf{Nom}$,
$\mathit{nom}(i)Z\mathit{nom}^{\prime}(i)$.

We write $\mathcal{M},m\leftrightarroweq\mathcal{M}^{\prime},m^{\prime}$ (and
say that $\mathcal{M},m$ and $\mathcal{M}^{\prime},m^{\prime}$ are
$\text{HXPath}_{=}$-bisimilar) if there is an $\text{HXPath}_{=}$-bisimulation
$Z$ such that $mZm^{\prime}$.

The notion of $\text{HXPath}_{=}$-bisimulation extends the one for basic modal
logic [BdRV01]. As usual, (Harmony) takes care of atomic information (both
propositional symbols and nominals). The standard (Zig) and (Zag) should be
strengthened to take into account that XPath modalities deal with two paths at
the same time, and moreover equality of data values can be checked at their
ending points. Finally (Nom) takes care of the $@$ operator.

It is straightforward to prove that $\text{HXPath}_{=}$-bisimilar models
satisfy the same $\text{HXPath}_{=}$-formulas (see [ABFF18]).

######  Proposition .

Let $\mathcal{M},m$ and $\mathcal{M}^{\prime},m^{\prime}$ be two pointed data
models. If $\mathcal{M},m\leftrightarroweq\mathcal{M}^{\prime},m^{\prime}$
then for any $\text{HXPath}_{=}$-formula $\varphi$,
$\mathcal{M},m\models\varphi$ if and only if
$\mathcal{M}^{\prime},m^{\prime}\models\varphi$.

We can extend the notion of $\ell$-bisimulation introduced in [FFA15] in a
similar way. An $\ell$-bisimulation checks model equivalence up to a certain
modal depth.

######  Definition  ($\ell$-bisimulations).

Let $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{{R_{\mathsf{a}}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
and $\mathcal{M}^{\prime}=\langle
M^{\prime},\\{\sim^{\prime}_{e}\\}_{e\in\mathsf{Eq}},\\{R^{\prime}_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V}^{\prime},\mathit{nom}^{\prime}\rangle$
be two abstract hybrid data models, $m\in M$, $m^{\prime}\in M^{\prime}$. We
say that $\mathcal{M},m$ and $\mathcal{M}^{\prime},m^{\prime}$ are _$\ell$
-bisimilar_ for $\text{HXPath}_{=}$ (written
$\mathcal{M},m\leftrightarroweq_{\ell}\mathcal{M}^{\prime},m^{\prime}$) if
there exists a family of relations $(Z_{j})_{j\leq\ell}$ in $M\times
M^{\prime}$ such that $mZ_{\ell}m^{\prime}$, and for all $j\leq\ell$, when
$lZ_{j}l^{\prime}$ we have:

  * •

$(\textbf{Harmony})$ $\mathit{V}(l)=\mathit{V}^{\prime}(l^{\prime})$ and
$l=\mathit{nom}(i)$ iff $l^{\prime}=\mathit{nom}^{\prime}(i)$ (for all
$i\in\mathsf{Nom}$).

  * •

$(\textbf{Zig}_{=})$ If there are paths
$\pi_{1}=lR_{\mathsf{a}_{1}}h_{1}R_{\mathsf{a}_{2}}\ldots
R_{\mathsf{a}_{n_{1}}}h_{n_{1}}$ and
$\pi_{2}=lR_{\mathsf{b}_{1}}k_{1}R_{\mathsf{b}_{2}}\ldots
R_{\mathsf{b}_{n_{2}}}k_{n_{2}}$ (for
$\mathsf{a}_{i},\mathsf{b}_{i}\in\mathsf{Mod}$), $n_{1},n_{2}\leq j$, then
there are paths
$\pi^{\prime}_{1}=l^{\prime}R^{\prime}_{\mathsf{a}_{1}}h^{\prime}_{1}R^{\prime}_{\mathsf{a}_{2}}\ldots
R^{\prime}_{\mathsf{a}_{n_{1}}}h^{\prime}_{n_{1}}$ and
$\pi^{\prime}_{2}=l^{\prime}R^{\prime}_{\mathsf{b}_{1}}k^{\prime}_{1}R^{\prime}_{\mathsf{b}_{2}}\ldots
R^{\prime}_{\mathsf{b}_{n_{2}}}k^{\prime}_{n_{2}}$ such that

    1. (1)

$h_{i}Z_{(j-n_{1})+i}h^{\prime}_{i}$ for $1\leq i\leq n_{1}$.

    2. (2)

$k_{i}Z_{(j-n_{2})+i}k^{\prime}_{i}$ for $1\leq i\leq n_{2}$.

    3. (3)

$h_{n_{1}}\sim_{e}k_{n_{2}}~{}\mbox{iff}~{}h^{\prime}_{n_{1}}\sim^{\prime}_{e}k^{\prime}_{n_{2}}$,
for all $e\in\mathsf{Eq}$.

  * •

$(\textbf{Zag}_{=})$ If there are paths
$\pi^{\prime}_{1}=l^{\prime}R^{\prime}_{\mathsf{a}_{1}}h^{\prime}_{1}R^{\prime}_{\mathsf{a}_{2}}\ldots
R^{\prime}_{\mathsf{a}_{n_{1}}}h^{\prime}_{n_{1}}$ and
$\pi^{\prime}_{2}=l^{\prime}R^{\prime}_{\mathsf{b}_{1}}k^{\prime}_{1}R^{\prime}_{\mathsf{b}_{2}}\ldots
R^{\prime}_{\mathsf{b}_{n_{2}}}k^{\prime}_{n_{2}}$ (for
$\mathsf{a}_{i},\mathsf{b}_{i}\in\mathsf{Mod}$), $n_{1},n_{2}\leq j$, then
there are paths $\pi_{1}=lR_{\mathsf{a}_{1}}h_{1}R_{\mathsf{a}_{2}}\ldots
R_{\mathsf{a}_{n_{1}}}h_{n_{1}}$ and
$\pi_{2}=lR_{\mathsf{b}_{1}}k_{1}R_{\mathsf{b}_{2}}\ldots
R_{\mathsf{b}_{n_{2}}}k_{n_{2}}$ such that conditions 1, 2 and 3 above are
verified.

  * •

$(\textbf{Nom})$ For all $i\in\mathsf{Nom}$,
$\mathit{nom}(i)Z_{\ell}\mathit{nom}^{\prime}(i)$.

Again, it is straightforward to prove the next proposition.

######  Proposition .

Let $\mathcal{M},m$ and $\mathcal{M}^{\prime},m^{\prime}$ be two pointed data
models. If
$\mathcal{M},m\leftrightarroweq_{\ell}\mathcal{M}^{\prime},m^{\prime}$ then
for any $\text{HXPath}_{=}$-formula $\varphi$ such that ${\sf
md}(\varphi)\leq\ell$, $\mathcal{M},m\models\varphi$ if and only if
$\mathcal{M}^{\prime},m^{\prime}\models\varphi$.

##  3\. Axiomatization

In this section we introduce the axiomatic system $\mathsf{HXP}$ for
$\text{HXPath}_{=}$. It is an extension of an axiomatic system for the hybrid
logic $\mathcal{HL}(@)$ which adds nominals and the $@$ operator to the basic
modal language (see [BdRV01]). In particular, we include axioms to handle data
equality and inequality. We will prove that $\mathsf{HXP}$ is sound and
strongly complete with respect to the class of abstract hybrid data models.
Moreover, we will show that the system is strongly complete for any extension
with some particular kind of axioms and inference rules. This result will be
helpful in order to automatically obtain complete axiomatic systems for
several natural extensions of the language $\text{HXPath}_{=}$. The system is
geared for inference over node expressions, but we will discuss path
expressions in Section 3.4. We remind the reader that when referring to
$\text{HXPath}_{=}$ we use the term _formula_ for node expressions. In what
follows, we use $*$ in axioms which hold for both $=_{e}$ and $\neq_{e}$.

###  3.1. The Basic Axiomatic System $\mathsf{HXP}$

We present axioms and rules step by step, providing brief comments to help the
reader understand their role. In all axioms and rules $\varphi$, $\psi$ and
$\theta$ are node expressions; $\alpha$, $\beta$, $\gamma$ and $\eta$ are path
expressions; and $i$, $j$ and $k$ are nominals. More precisely, we provide
_axiom and rule schemes_ , i.e., they can be instantiated with arbitrary path
and node expressions, respecting typing. Hence, $\varphi$, $\psi$ and $\theta$
can be instantiated with node expressions; $\alpha$, $\beta$, $\gamma$ and
$\eta$ with path expressions; and $i$, $j$ and $k$ with nominals.

######  Definition  (Theorems, Syntactic Consequence, Consistency).

For $\mathsf{A}$ an axiomatic system, _$\varphi$ is a theorem of $\mathsf{A}$_
(notation: $\vdash_{\mathsf{A}}\varphi$) if it is either an instantiation of
an axiom of $\mathsf{A}$, or it can be derived from an axiom of $\mathsf{A}$
in a finite number of steps by application of the rules of $\mathsf{A}$. Let
$\Gamma$ be a set of node expressions. We write
$\Gamma\vdash_{\mathsf{A}}\varphi$ and say that _$\varphi$ is a syntactic
consequence of $\Gamma$ in $\mathsf{A}$_ if there exists a finite set
$\Gamma^{\prime}\subseteq\Gamma$ such that
$\vdash_{\mathsf{A}}\bigwedge\Gamma^{\prime}\rightarrow\varphi$ (where
$\bigwedge\emptyset=\top$). We say that $\Gamma$ is _consistent (for
$\mathsf{A}$)_ if $\Gamma\not\vdash_{\mathsf{A}}\bot$. We write $\vdash$
instead of $\vdash_{\mathsf{A}}$ if $\mathsf{A}$ is clear from context.

In addition to a complete set of axioms and rules for propositional logic,
$\mathsf{HXP}$ includes generalizations of the K axiom and the Necessitation
rule for the basic modal logic to handle modalities with arbitrary path
expressions.

Axiom and rule for classical modal logic
---
| _K_ | $\vdash[\alpha](\varphi\rightarrow\psi)\rightarrow([\alpha]\varphi\rightarrow[\alpha]\psi)$
---|---
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
7.36516pt\hbox{$\displaystyle\penalty 1\vdash\varphi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=30.16081pt\hbox{\kern
3.00003pt$\emph{Nec}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash[\alpha]\varphi$}}}}\\\ $

Then we introduce generalizations of the inference rules for the hybrid logic
$\mathcal{HL}(@)$.

Hybrid rules
---
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\vdash@_{j}\varphi$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=25.83498pt\hbox{\kern 3.00003pt$name$}}}\hbox{\kern 3.81339pt\hbox{$\displaystyle\vdash\varphi$}}}}$ |  ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\vdash@_{i}\langle\mathsf{a}\rangle j\wedge\langle@_{j}\alpha*\beta\rangle\rightarrow\theta$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=97.10513pt\hbox{\kern 3.00003pt$paste$}}}\hbox{\kern 15.88081pt\hbox{$\displaystyle\vdash\langle@_{i}\mathsf{a}\alpha*\beta\rangle\rightarrow\theta$}}}}$
$j$ is a nominal different from $i$ that does not occur in
$\varphi,\alpha,\beta,\theta$.

Now we introduce axioms to handle $@$. Notice that $@_{i}$ is a path
expression and as a result, some of the standard hybrid axioms for $@$ have
been generalized. In particular, the $K$ axiom and _Nec_ rule above also apply
to $@_{i}$. In addition, we provide axioms to ensure that the relation induced
by $@$ is a congruence.

Axioms for $@$ | Congruence for $@$
---|---
| _$@$ -self-dual_ | $\vdash\neg@_{i}\varphi\leftrightarrow@_{i}\neg\varphi$
---|---
_$@$ -intro_ | $\vdash i\rightarrow(\varphi\leftrightarrow@_{i}\varphi)$
| _$@$ -refl_ | $\vdash@_{i}i$
---|---
_agree_ | $\vdash\langle@_{j}@_{i}\alpha*\beta\rangle\leftrightarrow\langle@_{i}\alpha*\beta\rangle$
_back_ | $\vdash\langle\gamma@_{i}\alpha*\beta\rangle\rightarrow\langle@_{i}\alpha*\beta\rangle$

Axioms involving the classical XPath operators can be found below. First we
introduce axioms to handle complex path expressions in data comparisons. Then
we introduce axioms to handle data tests.

Axioms for paths
---
| _comp-assoc_ | $\vdash\langle(\alpha\beta)\gamma*\eta\rangle\leftrightarrow\langle\alpha(\beta\gamma)*\eta\rangle$
---|---
_comp-neutral_ |  $\vdash\langle\alpha\beta*\gamma\rangle\leftrightarrow\langle\alpha\epsilon\beta*\gamma\rangle$ ($\alpha$ or $\beta$ can be empty)
_comp-dist_ | $\vdash\langle\alpha\beta\rangle\varphi\leftrightarrow\langle\alpha\rangle\langle\beta\rangle\varphi$
Axioms for data
| _equal_ | $\vdash\langle\epsilon=_{e}\epsilon\rangle$
---|---
_distinct_ | $\vdash\neg\langle\epsilon\neq_{e}\epsilon\rangle$
_$@$ -data_ | $\vdash\neg\langle@_{i}{=_{e}}@_{j}\rangle\leftrightarrow\langle@_{i}{\neq_{e}}@_{j}\rangle$
_$\epsilon$ -trans_ | $\vdash\langle\epsilon=_{e}\alpha\rangle\wedge\langle\epsilon=_{e}\beta\rangle\rightarrow\langle\alpha=_{e}\beta\rangle$
_$*$ -comm_ | $\vdash\langle\alpha*\beta\rangle\leftrightarrow\langle\beta*\alpha\rangle$
_$*$ -test_ | $\vdash\langle[\varphi]\alpha*\beta\rangle\leftrightarrow\varphi\wedge\langle\alpha*\beta\rangle$
_$@*$ -dist_ | $\vdash\langle@_{i}\alpha*@_{i}\beta\rangle\rightarrow@_{i}\langle\alpha*\beta\rangle$
_subpath_ | $\vdash\langle\alpha\beta*\gamma\rangle\rightarrow\langle\alpha\rangle\top$
_comp $*$-dist_ | $\vdash\langle\alpha\rangle\langle\beta*\gamma\rangle\rightarrow\langle\alpha\beta*\alpha\gamma\rangle$

It is a straightforward exercise to see that the axiomatic system
$\mathsf{HXP}$ is sound. However, we will provide a more general statement of
soundness later on.

Below we prove that some useful theorems and rules can be derived within
$\mathsf{HXP}$.

######  Proposition .

The following are theorems and derived rules of $\mathsf{HXP}$, and will be
used (explicitly or implicitly) in the rest of the paper.

test-dist | $\vdash\langle[\varphi]=_{e}[\psi]\rangle\leftrightarrow\varphi\wedge\psi$
---|---
test-$\bot$ | $\vdash\langle[\varphi]\neq_{e}[\psi]\rangle\leftrightarrow\bot$
$@$-swap | $\vdash@_{i}\langle\alpha*@_{j}\beta\rangle\leftrightarrow@_{j}\langle\beta*@_{i}\alpha\rangle$
$@$-intro’ | $\vdash(i\wedge\varphi)\rightarrow@_{i}\varphi$
$@$-sym. | $\vdash@_{i}j\rightarrow@_{j}i$
K${}_{@}^{-1}$ | $\vdash(@_{i}\varphi\rightarrow@_{i}\psi)\rightarrow@_{i}(\varphi\rightarrow\psi)$
nom | $\vdash@_{i}j\wedge\langle@_{i}\alpha*\beta\rangle\rightarrow\langle@_{j}\alpha*\beta\rangle$
bridge | $\vdash\langle\alpha\rangle i\wedge@_{i}\varphi\rightarrow\langle\alpha\rangle\varphi$
name’ |  If $\vdash i\rightarrow\varphi$ then $\vdash\varphi$, if $i$ does not appear in $\varphi$

###### Proof.

(test-dist and test-$\bot$). Let $*$ be $=_{e}$ or $\neq_{e}$. Then:

$\displaystyle\vdash\langle[\varphi]*[\psi]\rangle\leftrightarrow\langle[\varphi]\epsilon*[\psi]\rangle$
(_comp-neutral_)
$\displaystyle\vdash\langle[\varphi]\epsilon*[\psi]\rangle\leftrightarrow\varphi\wedge\langle\epsilon*[\psi]\rangle$
(_$*$ -test_)
$\displaystyle\vdash\varphi\wedge\langle\epsilon*[\psi]\rangle\leftrightarrow\varphi\wedge\langle[\psi]*\epsilon\rangle$
(_$*$ -comm_)
$\displaystyle\vdash\varphi\wedge\langle[\psi]*\epsilon\rangle\leftrightarrow\varphi\wedge\langle[\psi]\epsilon*\epsilon\rangle$
(_comp-neutral_)
$\displaystyle\vdash\varphi\wedge\langle[\psi]\epsilon*\epsilon\rangle\leftrightarrow\varphi\wedge\psi\wedge\langle\epsilon*\epsilon\rangle$
(_$*$ -test_)

Replacing $*$ by $=_{e}$ we get $\varphi\wedge\psi$ by _equal_. Replacing it
by $\neq_{e}$ we get $\langle\epsilon\neq_{e}\epsilon\rangle$, and given
_distinct_ we can derive $\bot$.

($@$-swap).

$\displaystyle\vdash@_{i}\langle\alpha=_{e}@_{j}\beta\rangle\leftrightarrow\langle@_{i}\alpha=_{e}@_{i}@_{j}\beta\rangle$
(_$@=$ -dist_)
$\displaystyle\vdash\langle@_{i}\alpha=_{e}@_{i}@_{j}\beta\rangle\leftrightarrow\langle@_{i}@_{j}\beta=_{e}@_{i}\alpha\rangle$
(_$=$ -comm_)
$\displaystyle\vdash\langle@_{i}@_{j}\beta=_{e}@_{i}\alpha\rangle\leftrightarrow\langle@_{j}\beta=_{e}@_{i}\alpha\rangle$
(_agree_)
$\displaystyle\vdash\langle@_{j}\beta=_{e}@_{i}\alpha\rangle\leftrightarrow\langle@_{i}\alpha=_{e}@_{j}\beta\rangle$
(_$=$ -comm_)
$\displaystyle\vdash\langle@_{i}\alpha=_{e}@_{j}\beta\rangle\leftrightarrow\langle@_{j}@_{i}\alpha=_{e}@_{j}\beta\rangle$
(_agree_)
$\displaystyle\vdash\langle@_{j}@_{i}\alpha=_{e}@_{j}\beta\rangle\leftrightarrow@_{j}\langle@_{i}\alpha=_{e}\beta\rangle$
(_agree_)
$\displaystyle\vdash@_{j}\langle@_{i}\alpha=_{e}\beta\rangle\leftrightarrow@_{j}\langle\beta=_{e}@_{i}\alpha\rangle$
(_$=$ -comm_)

($@$-intro’). Direct from $@$-intro.

($@$-sym.).

$\displaystyle\vdash(j\wedge i)\rightarrow@_{j}i$ (_$@$ -intro’_)
$\displaystyle\vdash(@_{i}j\wedge@_{i}i)\rightarrow@_{i}@_{j}i$ (_Nec, K_)
$\displaystyle\vdash@_{i}j\rightarrow@_{j}i$ (_$@$ -refl., back_)

(K${}_{@}^{-1}$).

$\displaystyle\vdash(@_{i}\neg(\varphi\rightarrow\psi)\rightarrow@_{i}\varphi)\wedge(@_{i}\neg(\varphi\rightarrow\psi)\rightarrow@_{i}\neg\psi)$
(_prop, Nec, K_)
$\displaystyle\vdash@_{i}\neg(\varphi\rightarrow\psi)\rightarrow(@_{i}\varphi\wedge@_{i}\neg\psi)$
(_prop_)
$\displaystyle\vdash\neg@_{i}(\varphi\rightarrow\psi)\rightarrow(@_{i}\varphi\wedge\neg@_{i}\psi)$
(_$@$ -self-dual_)
$\displaystyle\vdash(@_{i}\varphi\rightarrow@_{i}\psi)\rightarrow@_{i}(\varphi\rightarrow\psi)$
(_prop_)

(nom).

$\displaystyle\vdash(j\wedge\langle@_{j}\beta*\alpha\rangle)\rightarrow@_{j}\langle@_{j}\beta*\alpha\rangle$
(_$@$ -intro’_)
$\displaystyle\vdash(@_{i}j\wedge@_{i}\langle@_{j}\beta*\alpha\rangle)\rightarrow@_{i}@_{j}\langle@_{j}\beta*\alpha\rangle$
(_Nec, K_)
$\displaystyle\vdash(@_{i}j\wedge@_{j}\langle@_{i}\alpha*\beta\rangle)\rightarrow@_{i}@_{j}\langle@_{j}\alpha*\beta\rangle$
(_$@$ -swap, $*$-comm_)
$\displaystyle\vdash(@_{j}@_{i}j\wedge@_{j}\langle@_{i}\alpha*\beta\rangle)\rightarrow@_{j}\langle@_{j}\alpha*\beta\rangle$
(_agree_)
$\displaystyle\vdash@_{j}(@_{i}j\wedge\langle@_{i}\alpha*\beta\rangle\rightarrow\langle@_{j}\alpha*\beta\rangle)$
(_K ${}_{@}^{-1}$_)
$\displaystyle\vdash@_{i}j\wedge\langle@_{i}\alpha*\beta\rangle\rightarrow\langle@_{j}\alpha*\beta\rangle$
(_name_)

(bridge). Using contrapositive, bridge is equivalent to $\langle\alpha\rangle
i\wedge[\alpha]\varphi\rightarrow@_{i}\varphi$. Using the modal theorem
$\vdash\langle\alpha\rangle\varphi\wedge[\alpha]\psi\rightarrow\langle\alpha\rangle(\varphi\wedge\psi)$,
we reason:

$\displaystyle\vdash\langle\alpha\rangle
i\wedge[\alpha]\varphi\rightarrow\langle\alpha\rangle(i\wedge\varphi)$
$\displaystyle\vdash\langle\alpha\rangle(i\wedge\varphi)\rightarrow\langle\alpha\rangle(@_{i}\varphi)$
(_$@$ -intro’_)
$\displaystyle\vdash\langle\alpha\rangle(@_{i}\varphi)\rightarrow@_{i}\varphi$
(_back_)

(name’). Suppose $\vdash i\rightarrow\varphi$. Then:

$\displaystyle\vdash@_{i}(i\rightarrow\varphi)$ (_Nec_)
$\displaystyle\vdash@_{i}i\rightarrow@_{i}\varphi$ (_K_)
$\displaystyle\vdash@_{i}\varphi$ (_$@$ -refl._) $\displaystyle\vdash\varphi$
(name)

∎

###  3.2. Extended Axiomatic Systems

In the next section we will prove that not only $\mathsf{HXP}$ is complete
with respect to the class of all models, but that extensions of $\mathsf{HXP}$
with _pure axioms_ and _existential saturation rules_ preserve completeness
with respect to the corresponding class of models. In this section we present
such extensions.

The use of nominals, and in particular pure axioms and existential saturation
rules, allows us to characterize classes of models that are not definable
without them. For instance, the hybrid axiom
$@_{i}\neg\langle\mathsf{a}\rangle i$ forces the accessibility relation
related to $\mathsf{a}$ in the model to be _irreflexive_ , which cannot be
expressed in the basic modal logic. In this way, we can express properties
about the underlying topology of a data model and also impose restrictions
about the data fields. For instance, the axiom
$\langle@_{i}=_{e}@_{j}\rangle\rightarrow\langle@_{i}=_{d}@_{j}\rangle$ for
_data inclusion_ that will be discussed in Section 3.5, expresses that if two
nodes coincide in the data field $e$, then they must also coincide in the data
field $d$.

#### Standard Translation.

In order to establish frame conditions associated to pure axioms and
existential saturation rules we define the _standard translation_ of
$\text{HXPath}_{=}$ into first-order logic, by mutual recursion between NExp
and PExp.

######  Definition .

The correspondence language for expressions of $\text{HXPath}_{=}$ is a
relational language with a unary relation symbol $P_{i}$ for each
$p_{i}\in\mathsf{Prop}$, a binary relation symbol $R_{\mathsf{a}}$ for each
$\mathsf{a}\in\mathsf{Mod}$ and a binary relation symbol $D_{e}$ for each
$e\in\mathsf{Eq}$. Moreover, for each nominal $i\in\mathsf{Nom}$ we will
associate an indexed variable $x_{i}$. The function $\mathsf{ST}^{\prime}_{x}$
from $\text{HXPath}_{=}$-formulas into its correspondence language is defined
by

$\begin{array}[]{lcl}\mathsf{ST}^{\prime}_{x}(i)&=&x=x_{i}\\\
\mathsf{ST}^{\prime}_{x}(p)&=&P(x)\\\
\mathsf{ST}^{\prime}_{x}(\neg\varphi)&=&\neg\mathsf{ST}^{\prime}_{x}(\varphi)\\\
\mathsf{ST}^{\prime}_{x}(\varphi\wedge\psi)&=&\mathsf{ST}^{\prime}_{x}(\varphi)\wedge\mathsf{ST}^{\prime}_{x}(\psi)\\\
\mathsf{ST}^{\prime}_{x}(\langle\alpha=_{e}\beta\rangle)&=&\exists
y,z.~{}\mathsf{ST}^{\prime}_{x,y}(\alpha)\wedge\mathsf{ST}^{\prime}_{x,z}(\beta)\wedge
D_{e}(y,z)\\\
\mathsf{ST}^{\prime}_{x}(\langle\alpha\neq_{e}\beta\rangle)&=&\exists
y,z.~{}\mathsf{ST}^{\prime}_{x,y}(\alpha)\wedge\mathsf{ST}^{\prime}_{x,z}(\beta)\wedge\neg
D_{e}(y,z),\end{array}$

where $y,z$ are first-order variables which have not been used yet in the
translation, and where $\mathsf{ST}^{\prime}_{x,y}$ is defined as

$\begin{array}[]{lcl}\mathsf{ST}^{\prime}_{x,y}(\mathsf{a})&=&R_{\mathsf{a}}(x,y)\\\
\mathsf{ST}^{\prime}_{x,y}(@_{i})&=&y=x_{i}\\\
\mathsf{ST}^{\prime}_{x,y}([\varphi])&=&x=y\wedge\mathsf{ST}^{\prime}_{y}(\varphi)\\\
\mathsf{ST}^{\prime}_{x,y}(\alpha\beta)&=&\exists
z.~{}\mathsf{ST}^{\prime}_{x,z}(\alpha)\wedge\mathsf{ST}^{\prime}_{z,y}(\beta),\end{array}$

with $z$ not used yet in the translation. Finally, let $Eq(e)$ be the first-
order formula stating that the relation $D_{e}$ is an equivalence relation
(i.e., reflexive, symmetric and transitive), we define the _standard
translation_ $\mathsf{ST}_{x}$ of a formula $\varphi$ as

$\mathsf{ST}_{x}(\varphi)=\bigwedge\\{Eq(e)\mid{=}_{e}\mbox{ appearing in
}\varphi\\}\wedge\mathsf{ST}^{\prime}_{x}(\varphi).$

Since the standard translation mimics the semantic clauses for
$\text{HXPath}_{=}$-formulas, the following proposition holds.

######  Proposition .

Let $\varphi$ be an $\text{HXPath}_{=}$-formula, and let $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\\\
\mathit{nom}\rangle$ be an abstract hybrid data model with $m\in M$. Then
$\mathcal{M},m\models\varphi$ if and only if
$\mathcal{M},g\models\mathsf{ST}_{x}(\varphi)$, where $g$ is an arbitrary
first-order assignment such that $g(x_{i})=\mathit{nom}(i)$ and $g(x)=m$.

Notice, in the proposition above, that $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
is used to interpret $\mathsf{ST}_{x}(\varphi)$ with $\mathit{V}(p)$
interpreting the unary relation symbol $P$, each accessibility relation
$R_{\mathsf{a}}$ interpreting the binary relation symbol $R_{\mathsf{a}}$ and
each relation $\sim_{e}$ interpreting the binary relation $D_{e}$.

#### Pure Axioms and Existential Saturation Rules.

We have now all the ingredients needed to define pure axioms and existential
saturation rules, together with their associated frame conditions.

######  Definition  (Pure Axioms).

We say that a formula (or in particular, an axiom) is _pure_ if it does not
contain any occurrences of propositional symbols. Let $\Pi$ be a set of pure
axioms, we define $\textsf{FC}(\Pi)$, the _frame condition associated to
$\Pi$_ as the universal closure of the standard translation of the axioms in
$\Pi$, i.e.,

$\textsf{FC}(\Pi)=\bigwedge\\{\forall
x.\forall{x_{i_{1}}}\ldots\forall{x_{i_{n}}}.\mathsf{ST}_{x}(\varphi)\mid\varphi\in\Pi,i_{1},\ldots,i_{n}\text{
all the nominals in $\varphi$}\\}.$

######  Definition  (Existential Saturation Rules).

Let $\varphi(i_{1},\dots,i_{n},j_{1},\ldots,j_{m})$ be an $\text{HXPath}_{=}$
formula with no propositional symbols such that
$i_{1},\dots,i_{n},j_{1},\ldots,j_{m}$ is an enumeration of all nominals
appearing in $\varphi$. An existential saturation rule is a rule of the form

$\begin{array}[]{l@{\ \ \ }l}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash\varphi(i_{1},\dots,i_{n},j_{1},\ldots,j_{m})\rightarrow\psi$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=105.98251pt\hbox{}}}\hbox{\kern
43.90103pt\hbox{$\displaystyle\vdash\psi$}}}}&\begin{minipage}{199.16928pt}
\small provided that $j_{1},\ldots,j_{m}$ do not occur in $\psi$.
\end{minipage}\end{array}$

We will call $\varphi$ the _head_ of the rule, $i_{1},\ldots,i_{n}$ its
_universally quantified nominals_ (notation: $\varphi_{\forall}$), and
$j_{1},\ldots,j_{m}$ its _existentially quantified nominals_ (notation:
$\varphi_{\exists}$)111Notice that given a particular $\varphi$, different
existential saturation rules can be defined depending on which nominals are
listed in its side condition.. Let $\mathrm{P}$ be a set of existential
saturation rules, we define $\textsf{FC}(\mathrm{P})$, the _frame condition
associated to $\mathrm{P}$_ as follows:

$\begin{array}[]{l@{\ }l}\textsf{FC}(\mathrm{P})=\bigwedge\\{\forall x.\forall
x_{i_{1}}\ldots\forall x_{i_{n}}.\exists x_{j_{1}}\ldots\exists
x_{j_{m}}.\mathsf{ST}_{x}(\varphi)\mid&\text{$\varphi$ is the head of a rule
$\rho\in\mathrm{P}$,}\\\ &\text{$i_{k}\in\varphi_{\forall}$ and
$j_{l}\in\varphi_{\exists}$\\}}.\end{array}$

Let $\Pi$ be a set of pure formulas and let $\mathrm{P}$ be a set of
existential saturation rules, in what follows we write
$\mathsf{HXP}+\Pi+\mathrm{P}$ for the axiomatic system $\mathsf{HXP}$ extended
with $\Pi$ as additional axioms and $\mathrm{P}$ as additional inference
rules. In the coming sections we will show that this system is strongly
complete with respect to the class of models based on frames satisfying the
frame condition $\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$.

######  Example .

The axiom $p\rightarrow[\mathsf{a}]\langle\mathsf{b}\rangle p$ is not pure,
since it contains the propositional symbol $p$. On the other hand,
$\Pi=\\{i\rightarrow[\mathsf{a}]\langle\mathsf{b}\rangle
i,i\rightarrow[\mathsf{b}]\langle\mathsf{a}\rangle i\\}$ is a set of pure
axioms. Its corresponding frame condition $\textsf{FC}(\Pi)$ indicates that
$R_{\mathsf{b}}$ is the inverse of $R_{\mathsf{a}}$. Indeed,
$\textsf{FC}(\Pi)$ is equivalent to $\forall x.\forall
y.(R_{\mathsf{a}}(x,y)\leftrightarrow R_{\mathsf{b}}(y,x))$.

Consider the formula $@_{i}\langle\mathsf{a}\rangle i$. It can be used to
define two different existential saturation rules:

$\begin{array}[]{l@{\ \ \ \ }l}\rho_{1}={tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash@_{i}\langle\mathsf{a}\rangle i\rightarrow\psi$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=51.8882pt\hbox{}}}\hbox{\kern
16.85387pt\hbox{$\displaystyle\vdash\psi$}}}}&\mbox{\small(no side
condition)}\end{array}$

and

$\begin{array}[]{l@{\ \ \ \ }l}\rho_{2}={tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash@_{i}\langle\mathsf{a}\rangle i\rightarrow\psi$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=51.8882pt\hbox{}}}\hbox{\kern
16.85387pt\hbox{$\displaystyle\vdash\psi$}}}}&\mbox{\small where $i$ does not
occur in $\psi$.}\\\ \end{array}$

$\textsf{FC}(\\{\rho_{1}\\})$ is equivalent to $\forall x.R_{\mathsf{a}}(x,x)$
while $\textsf{FC}(\\{\rho_{2}\\})$ is equivalent to $\exists
x.R_{\mathsf{a}}(x,x)$.

Consider now the rule corresponding to the _Church-Rosser property_ discussed
in [BtC06]:

$\begin{array}[]{l@{\ \ \ \ }l}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\vdash(@_{i}\langle\mathsf{a}\rangle
j\wedge@_{i}\langle\mathsf{a}\rangle k\rightarrow@_{j}\langle\mathsf{a}\rangle
l\wedge@_{k}\langle\mathsf{a}\rangle l)\rightarrow\psi$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=174.8853pt\hbox{}}}\hbox{\kern
78.35242pt\hbox{$\displaystyle\vdash\psi$}}}}&\mbox{\small where $l$ does not
occur in $\psi$.}\end{array}$

The frame condition corresponding to this rule is:

$\forall x.\forall x_{i}.\forall x_{j}.\forall x_{k}.\exists
x_{l}.\mathsf{ST}_{x}(@_{i}\langle\mathsf{a}\rangle
j\wedge@_{i}\langle\mathsf{a}\rangle k\rightarrow@_{j}\langle\mathsf{a}\rangle
l\wedge@_{k}\langle\mathsf{a}\rangle l),$

which is equivalent to $\forall x_{i}.\forall x_{j}.\forall x_{k}.\exists
x_{l}.(R_{\mathsf{a}}(x_{i},x_{j})\wedge R_{\mathsf{a}}(x_{i},x_{k})\to
R_{\mathsf{a}}(x_{j},x_{l})\wedge R_{\mathsf{a}}(x_{k},x_{l}))$.

It is not difficult to see that any pure axiom $\pi$ is equivalent to the rule
that uses $\pi$ as head without side conditions (i.e., $\pi_{\exists}$ is
empty). In that sense, any axiomatic system $\mathsf{HXP}+\Pi+\mathrm{P}$ is
equivalent to some $\mathsf{HXP}+\mathrm{P}^{\prime}$, as pure axioms do not
introduce additional expressive power. On the other hand, properties that mix
both universal and existential quantification like the Church-Rosser property
mentioned above cannot be captured using only pure axioms. However, axioms are
simpler than rules with side conditions; and pure axioms are expressive enough
to characterize many interesting properties.

###  3.3. Soundness and Completeness

It is a fairly straightforward exercise to prove that the axioms and rules of
$\mathsf{HXP}$ are sound with respect to the class of all models. Similarly,
any set $\Pi$ of pure axioms is sound with respect to the class of models
obtained from frames satisfying $\textsf{FC}(\Pi)$, and any set $\mathrm{P}$
of existential saturation rules is sound with respect to the class of frames
satisfying $\textsf{FC}(\mathrm{P})$ (the proof is similar to the one provided
in [BtC06]).

######  Theorem  (Soundness).

Let $\Pi$ be a set of pure axioms and let $\mathrm{P}$ be a set of existential
saturation rules. All the axioms and rules from $\mathsf{HXP}$ are valid over
the class of abstract hybrid data models satisfying the frame condition
$\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$.

Now we will devote ourselves to show that the axiomatic system is also
strongly complete. The completeness argument follows the lines of the
completeness proof for $\mathcal{HL}(@)$ and similar approaches (see, e.g.,
[Gol84, BtC06, SP10]), which is a Henkin-style proof with nominals playing the
role of first-order constants.

We will prove in this section that the system $\mathsf{HXP}+\Pi+\mathrm{P}$ is
_strongly complete_ with respect to the class of abstract hybrid data models
obtained from frames satisfying
$\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$. More precisely, given a
particular extension $\mathsf{HXP}+\Pi+\mathrm{P}$, we will show that if
$\mathfrak{C}=\mathsf{Mod(\mathfrak{F})}$ for $\mathfrak{F}$ the class of
frames satisfying $\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$, then
$\Gamma\models_{\mathfrak{C}}\varphi$ implies
$\Gamma\vdash_{\mathsf{HXP}+\Pi+\mathrm{P}}\varphi$, where
$\Gamma\cup\\{\varphi\\}$ is a set of $\text{HXPath}_{=}$-formulas. Or,
equivalently, we need to show that every consistent set of formulas (for
$\mathsf{HXP}+\Pi+\mathrm{P}$) is satisfiable in some abstract hybrid data
model (in $\mathfrak{C}$). Recall that subscripts in relations $\vdash$ and
$\models$ are ommited when they are clear from the context.

######  Definition .

Let $\Gamma$ be a set of formulas, we say that $\Gamma$ is an
$\mathsf{HXP}+\Pi+\mathrm{P}$ _maximal consistent set_ (MCS for short) if and
only if $\Gamma\nvdash\bot$ and for all $\varphi\notin\Gamma$ we have
$\Gamma\cup\\{\varphi\\}\vdash\bot$.

######  Proposition .

Let $\Gamma$ be an MCS. Then, the following facts hold:

  1. (1)

If $\\{i,\varphi\\}\subseteq\Gamma$ then $@_{i}\varphi\in\Gamma$.

  2. (2)

If $@_{i}\langle\alpha=_{e}\beta\rangle\in\Gamma$ then
$\langle@_{i}\alpha=_{e}@_{i}\beta\rangle\in\Gamma$.

  3. (3)

If $\langle\alpha=_{e}@_{i}\beta\rangle\in\Gamma$ then
$\langle\alpha=_{e}@_{j}@_{i}\beta\rangle\in\Gamma$.

###### Proof.

Item 1 is a consequence of _$@$ -intro’_, 2 follows from _$@{=}$ -dist_ and 3
can be proved using agree and $=$-comm. ∎

The next fact follows from the definition of MCS, as expected:

######  Fact 1.

Let $\Gamma$ be an MCS. Then for all $\varphi$, either $\varphi\in\Gamma$ or
$\neg\varphi\in\Gamma$.

So far, we presented an axiom system together with the standard tools for
proving its completeness. We also introduced non-orthodox rules (i.e., rules
with side conditions), which will play a crucial role in the Henkin-style
model we will build for proving completeness. The _paste_ rule expresses that
path expressions can control what happens in accessible states from a named
state. The _name_ rule says that if $\varphi$ is provable to hold in an
arbitrary state named by $j$, then $\varphi$ is also provable. Now we
introduce some properties that will be required in the construction of the
Henkin-style model.

######  Definition 3.1 (Named, Pasted and $\rho$-saturated sets).

Let $\Sigma$ be a set of $\text{HXPath}_{=}$-formulas.

  * •

We say that $\Sigma$ is _named_ if for some nominal $i$ we have that
$i\in\Sigma$ (and we will say that $\Sigma$ is named by $i$).

  * •

We say that $\Sigma$ is pasted if the following holds:

    1. (1)

$\langle@_{i}\mathsf{a}\alpha=_{e}\beta\rangle\in\Sigma$ implies that for some
nominal $j$, $@_{i}\langle\mathsf{a}\rangle
j\wedge\langle@_{j}\alpha=_{e}\beta\rangle\in\Sigma$.

    2. (2)

$\langle@_{i}\mathsf{a}\alpha\not=_{e}\beta\rangle\in\Sigma$ implies that for
some nominal $j$, $@_{i}\langle\mathsf{a}\rangle
j\wedge\langle@_{j}\alpha\not=_{e}\beta\rangle\in\Sigma$.

  * •

For $\varphi$ a formula and
$i_{1},\ldots,i_{n},j_{1},\ldots,j_{n}\in\mathsf{Nom}$, let
$\varphi[i_{1}/j_{1},\ldots,j_{1}/j_{n}]$ be the simultaneous substitution of
$i_{k}$ by $j_{k}$, $1\leq k\leq n$ in $\varphi$. Let $\rho$ be an existential
saturation rule with head $\varphi$, $\varphi_{\forall}=i_{1},\ldots,i_{n}$
and $\varphi_{\exists}=j_{1},\ldots,j_{m}$. Then $\Sigma$ is _$\rho$
-saturated_ if for all nominals
$i^{\prime}_{1},\ldots,i^{\prime}_{n}\in\Sigma$,
$\varphi[i_{1}/i^{\prime}_{1},\ldots,i_{n}/i^{\prime}_{n},j_{i}/j^{\prime}_{n},\ldots,j_{m}/j^{\prime}_{m}]\in\Sigma$
for some $j^{\prime}_{1},\ldots,j^{\prime}_{m}\in\mathsf{Nom}$. For
$\mathrm{P}$ a set of existential saturation rules, _$\Sigma$ is
$\mathrm{P}$-saturated_ if it is $\rho$-saturated for all $\rho\in\mathrm{P}$.

Now we are going to prove a crucial property in our completeness proof: the
_Extended Lindenbaum Lemma_. Intuitively, it says that the rules of
$\mathsf{HXP}+\Pi+\mathrm{P}$ allow us to extend MCSs to _named and pasted_
MCSs, provided we enrich the language with new nominals. This lemma will be
useful to obtain the models we need from an MCS.

######  Lemma 3.2 (Extended Lindenbaum Lemma).

Let $\mathsf{Nom}^{\prime}$ be a (countably) infinite set of nominals disjoint
from $\mathsf{Nom}$, and let $\text{HXPath}_{=}^{\prime}$ be the language
obtained by adding these new nominals to $\text{HXPath}_{=}$. Then, every
consistent set of formulas in $\text{HXPath}_{=}$ can be extended to a named
and pasted MCS in $\text{HXPath}_{=}^{\prime}$.

######  Proof 3.3.

Enumerate $\mathsf{Nom}^{\prime}$ and let $k$ be the first nominal in the
enumeration. Given $\Sigma$ a consistent set in $\text{HXPath}_{=}$,
$\Sigma\cup\\{k\\}$ is consistent, otherwise for some conjunction $\theta$
from $\Sigma$, $\vdash k\rightarrow\neg\theta$. By the name’ rule,
$\vdash\neg\theta$, contradicting the consistency of $\Sigma$.

Now enumerate all formulas in $\text{HXPath}_{=}^{\prime}$. Define
$\Sigma^{0}=\Sigma\cup\\{k\\}$ and suppose we have defined $\Sigma^{n}$, for
$n\geq 0$. Let $\varphi_{n+1}$ be the $(n+1)^{th}$ formula in the enumeration
of $\text{HXPath}_{=}^{\prime}$. Define $\Sigma_{n+1}$ as follows. If
$\Sigma^{n}\cup\\{\varphi_{n+1}\\}$ is inconsistent, then
$\Sigma^{n+1}=\Sigma^{n}$. Otherwise:

  1. (1)

$\Sigma^{n+1}=\Sigma^{n}\cup\\{\varphi_{n+1}\\}$ if $\varphi_{n+1}$ is not of
the form $\langle@_{i}\mathsf{a}\alpha*\beta\rangle$.

  2. (2)

$\Sigma^{n+1}=\Sigma^{n}\cup\\{\varphi_{n+1}\\}\cup\\{@_{i}\langle\mathsf{a}\rangle
j\wedge\langle@_{j}\alpha*\beta\rangle\\}$, if $\varphi_{n+1}$ is of the form
$\langle@_{i}\mathsf{a}\alpha*\beta\rangle$. Here $j$ is the first nominal in
the enumeration that does not occur in any formula of $\Sigma^{n}$ or
$\langle@_{i}\mathsf{a}\alpha*\beta\rangle$.

Let $\Sigma^{\omega}=\bigcup_{n\geq 0}\Sigma^{n}$. This set is named (by $k$),
maximal and pasted. Furthermore, it is consistent as a direct consequence of
the paste rule.

######  Lemma 3.4 (Rule Saturation Lemma).

Let $\mathsf{Nom}^{\prime}$ be a (countably) infinite set of nominals disjoint
from $\mathsf{Nom}$, and let $\text{HXPath}_{=}^{\prime}$ be the language
obtained by adding these new nominals to $\text{HXPath}_{=}$. Let $\Pi$ be a
set of pure axioms, and $\mathrm{P}$ be a set of existential saturation rules.
Then, every consistent set of formulas in $\text{HXPath}_{=}$ can be extended
to a named, pasted and $\mathrm{P}$-saturated MCS in
$\text{HXPath}_{=}^{\prime}$.

######  Proof 3.5.

Let $\Sigma$ be a consistent set of formulas in $\text{HXPath}_{=}$. First, we
will show that $\Sigma$ can be extended to some $\Sigma^{+}$ such that for
every rule $\rho\in\mathrm{P}$ with head $\varphi$,
$\varphi_{\forall}=i_{1}\ldots i_{n}$, and $\varphi_{\exists}=j_{1}\ldots
j_{m}$, and for all $i^{\prime}_{1},\ldots,i^{\prime}_{n}\in\Sigma$, there are
nominals $j^{\prime}_{1},\ldots,j^{\prime}_{m}$ such that
$\varphi(i_{1}/i^{\prime}_{1},\ldots,i_{n}/i^{\prime}_{k},j_{1}/j^{\prime}_{1},\ldots,j^{\prime}_{m})\in\Sigma^{+}$.

Let $\mathsf{Nom}^{\prime}$ be a (countably) infinite set of nominals disjoint
from $\mathsf{Nom}$. Given $\Sigma$ and $\mathrm{P}$, say that a pair
$(\rho,\bar{i})$ is well-formed if $\rho\in\mathrm{P}$ with head $\varphi$,
and $\bar{i}$ is a sequence of nominals in $\Sigma$ with length equal to the
length of $\varphi_{\forall}$. For $\Sigma$ and $\mathrm{P}$ countable, the
set of well-formed pairs is countable and can be enumerated. Define
$\Sigma^{0}=\Sigma$. Let $(\rho_{n+1},i^{\prime}_{1}\ldots i^{\prime}_{k})$ be
the $(n+1)^{th}$ pair in the enumeration. Define $\Sigma^{n+1}$ as follows.

  * $\Sigma^{n+1}=\Sigma^{n}\cup\\{\varphi(i_{1}/i^{\prime}_{1},\ldots,i_{k}/i^{\prime}_{k},j_{1}/j^{\prime}_{1},\ldots,j_{m}/j^{\prime}_{m})\\}$ where $\varphi$ is the head of $\rho_{n+1}$, $\varphi_{\forall}=i_{1},\ldots,i_{k}$, $\varphi_{\exists}=j_{1},\ldots,j_{m}$, and $j^{\prime}_{1},\ldots,j^{\prime}_{m}$ are the first $m$ nominals in $\mathsf{Nom}^{\prime}$ that do not occur in any formula of $\Sigma^{n}$.

We define $\Sigma^{+}=\bigcup_{n\geq 0}\Sigma^{n}$, which is consistent and
extends $\Sigma$ as described above.

Now consider any consistent set of formulas $\Gamma$. Let $\Gamma^{0}=\Gamma$,
and for all $n\geq 0$ let $\Gamma^{n+1}$ be a named and pasted MCS extending
$(\Gamma^{n})^{+}$ (which exists by Lemma 3.2). Then we have the following
chain of inclusions:

$\Gamma=\Gamma^{0}\subseteq(\Gamma^{0})^{+}\subseteq\Gamma^{1}\subseteq(\Gamma^{1})^{+}\subseteq\ldots$

Let $\Gamma^{\omega}=\bigcup_{n\geq 0}\Gamma^{n}$. Then $\Gamma^{\omega}$ is a
named, pasted and $\mathrm{P}$-saturated MCS in $\text{HXPath}_{=}^{\prime}$.
As we used only countably many new nominals, this set is also countable.

From a named and pasted MCS we can extract a model:

######  Definition 3.6 (Extracted Model).

Let $\Gamma$ be a named and pasted MCS222For this definition, it is irrelevant
whether $\Gamma$ is $\mathrm{P}$-saturated.. Define
$\mathcal{M}_{\Gamma}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$,
the _extracted model_ from $\Gamma$, as

  * •

$M=\\{\Delta_{i}\mid\Delta_{i}=\\{j\mid@_{i}j\in\Gamma\\}\\}$

  * •

$\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ iff $@_{i}\langle\mathsf{a}\rangle
j\in\Gamma$

  * •

$p\in\mathit{V}(\Delta_{i})$ iff $@_{i}p\in\Gamma$

  * •

$\mathit{nom}(i)=\Delta_{i}$

  * •

$\Delta_{i}\sim_{e}\Delta_{j}$ iff
$@_{i}\langle\epsilon=_{e}@_{j}\rangle\in\Gamma$.

We need to prove that $\mathcal{M}_{\Gamma}$ is well defined, and that it is
actually an abstract hybrid data model.

######  Proposition 3.7.

  1. (1)

$\Delta_{i}=\Delta_{j}$ implies $@_{i}\varphi\in\Gamma$ iff
$@_{j}\varphi\in\Gamma$.

  2. (2)

For all $e\in\mathsf{Eq}$, $\sim_{e}$ is an equivalence relation.

######  Proof 3.8.

Item 1 ensures that the definition of $\mathcal{M}_{\Gamma}$ does not depend
of the particular nominal taken as representative of $\Delta_{i}$. The
property follows directly from _bridge_.

For item 2, we prove:

\- Reflexivity: We need to show that $\Delta_{i}\sim_{e}\Delta_{i}$, which by
definition is equivalent to $@_{i}\langle\epsilon=_{e}@_{i}\rangle\in\Gamma$.
By _equal_ we have $\langle\epsilon=_{e}\epsilon\rangle\in\Gamma$, and
applying _Nec_ we get $@_{i}\langle\epsilon=_{e}\epsilon\rangle\in\Gamma$.
Also, by _comp=-dist_ , $\langle@_{i}=@_{i}\rangle\in\Gamma$, and by _agree_
$\langle@_{i}=_{e}@_{i}@_{i}\rangle\in\Gamma$. Then, by _$@=$ -dist_,
$@_{i}\langle\epsilon=_{e}@_{i}\rangle\in\Gamma$, as wanted.

\- Symmetry: $\Delta_{i}\sim_{e}\Delta_{j}$ iff
$@_{i}\langle\epsilon=_{e}@_{j}\rangle\in\Gamma$. By neutral and $=$-comm we
get $@_{i}\langle\epsilon=_{e}@_{j}\epsilon\rangle\in\Gamma$. Then, by
$@$-swap $@_{j}\langle\epsilon=_{e}@_{i}\epsilon\rangle\in\Gamma$. Therefore
(by _neutral_) $@_{j}\langle\epsilon=_{e}@_{i}\rangle\in\Gamma$.

\- Transitivity: Suppose $\Delta_{i}\sim_{e}\Delta_{j}$ and
$\Delta_{j}\sim_{e}\Delta_{k}$, iff
$@_{i}\langle\epsilon=_{e}@_{j}\rangle\in\Gamma$ and
$@_{j}\langle\epsilon=_{e}@_{k}\rangle\in\Gamma$. This means that we have (by
_$@$ -swap_) $@_{j}\langle\epsilon=_{e}@_{i}\rangle\in\Gamma$, and
$@_{j}\langle\epsilon=_{e}@_{k}\rangle\in\Gamma$. Then
$@_{j}(\langle\epsilon=@_{i}\rangle\wedge\langle\epsilon=_{e}@_{k}\rangle)\in\Gamma$
(let us call this fact $(\dagger)$ for later use). On the other hand,
$\langle\epsilon=_{e}@_{i}\rangle\wedge\langle\epsilon=_{e}@_{k}\rangle\rightarrow\langle@_{i}=_{e}@_{k}\rangle\in\Gamma$
because of $\epsilon$-trans. Then (by Nec)
$@_{j}(\langle\epsilon=_{e}@_{i}\rangle\wedge\langle\epsilon=_{e}@_{k}\rangle\rightarrow\langle@_{i}=_{e}@_{k}\rangle)\in\Gamma$,
and by K and distributivity of $@$ with respect to $\wedge$,
$@_{j}\langle\epsilon=_{e}@_{i}\rangle\wedge@_{j}\langle\epsilon=_{e}@_{k}\rangle\rightarrow@_{j}\langle@_{i}=_{e}@_{k}\rangle\in\Gamma$.
By Modus Ponens with $(\dagger)$ we have
$@_{j}\langle@_{i}=_{e}@_{k}\rangle\in\Gamma$, and by comp=-dist
$\langle@_{j}@_{i}=_{e}@_{j}@_{k}\rangle\in\Gamma$. Using back and agree we
get $\langle@_{i}=_{e}@_{i}@_{k}\rangle\in\Gamma$. Hence by _$@{=}$ -dist_,
$@_{i}\langle\epsilon=_{e}@_{k}\rangle\in\Gamma$, which gives us
$\Delta_{i}\sim_{e}\Delta_{k}$.

######  Proposition 3.9.

Let $\mathcal{M}_{\Gamma}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be the extracted model, for some $\Gamma$. Then,

  1. (1)

$\Delta_{i}\not\sim_{e}\Delta_{j}$ if and only if
$@_{i}\langle\epsilon\neq_{e}@_{j}\rangle\in\Gamma$,

  2. (2)

if $\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ then for all $@_{j}\varphi\in\Gamma$,
$@_{i}\langle\mathsf{a}\rangle\varphi\in\Gamma$.

######  Proof 3.10.

Item $1$ follows from $@$-data; for item $2$ suppose
$\Delta_{i}R_{\mathsf{a}}\Delta_{j}$, then we have
$@_{i}\langle\mathsf{a}\rangle j\in\Delta_{i}$. Let $@_{j}\varphi\in\Gamma$,
then by _comp-dist_ we have $\langle@_{i}\mathsf{a}\rangle j\in\Gamma$, hence
by $bridge$ we get $\langle@_{i}\mathsf{a}\rangle\varphi\in\Gamma$. Therefore,
by $@*$-dist, $@_{i}\langle\mathsf{a}\rangle\varphi\in\Gamma$.

Now, given a named and pasted MCS $\Gamma$ we can prove the following lemma:

######  Lemma 3.11 (Existence Lemma).

Let $\Gamma$ be an MCS and $\mathcal{M}_{\Gamma}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V}$,
$\mathit{nom}\rangle$ be the extracted model from $\Gamma$. Let $\Delta_{i}\in
M$, then

  1. (1)

$@_{i}\langle\mathsf{a}\alpha=_{e}\beta\rangle\in\Gamma$ implies there exists
$\Delta_{j}\in M$ s.t. $\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ and
$@_{j}\langle\alpha=_{e}@_{i}\beta\rangle\in\Gamma$.

  2. (2)

$@_{i}\langle\mathsf{a}\alpha\neq_{e}\beta\rangle\in\Gamma$ implies there
exists $\Delta_{j}\in M$ s.t. $\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ and
$@_{j}\langle\alpha\neq_{e}@_{i}\beta\rangle\in\Gamma$.

  3. (3)

$@_{i}\langle@_{j}\alpha=_{e}@_{k}\beta\rangle\in\Gamma$ implies
$@_{j}\langle\alpha=_{e}@_{k}\beta\rangle\in\Gamma$.

  4. (4)

$@_{i}\langle@_{j}\alpha\not=_{e}@_{k}\beta\rangle\in\Gamma$ implies
$@_{j}\langle\alpha\not=_{e}@_{k}\beta\rangle\in\Gamma$.

######  Proof 3.12.

First, we discuss $1$ ($2$ is similar). We suppose
$@_{i}\langle\mathsf{a}\alpha=_{e}\beta\rangle\in\Gamma$. Then, by
$@{=}$-dist, $\langle@_{i}\mathsf{a}\alpha=_{e}@_{i}\beta\rangle\in\Gamma$.
Because $\Gamma$ is pasted, $@_{i}\langle\mathsf{a}\rangle
j\wedge\langle@_{j}\alpha=_{e}@_{i}\beta\rangle\in\Gamma$. As $\Gamma$ is an
MCS, $@_{i}\langle\mathsf{a}\rangle j\in\Gamma$ and
$\langle@_{j}\alpha=_{e}@_{i}\beta\rangle\in\Gamma$. By definition of
$\mathcal{M}_{\Gamma}$ we obtain $\Delta_{i}R_{\mathsf{a}}\Delta_{j}$, and by
agree, we have $\langle@_{j}\alpha=_{e}@_{j}@_{i}\beta\rangle\in\Gamma$. Then,
$@_{j}\langle\alpha=_{e}@_{i}\beta\rangle\in\Gamma$ by $@{=}$-dist.

For $3$ ($4$ is similar) assume
$@_{i}\langle@_{j}\alpha=_{e}@_{k}\beta\rangle\in\Gamma$, then by comp=-dist,
$\langle@_{i}@_{j}\alpha=_{e}@_{i}@_{k}\beta\rangle\in\Gamma$. Applying agree
twice, we have $\langle@_{j}\alpha=_{e}@_{j}@_{k}\beta\rangle\in\Gamma$, then
by $@{=}$-dist $@_{j}\langle\alpha=_{e}@_{k}\beta\rangle\in\Gamma$.

######  Corollary 3.13.

Let $\Gamma$ be an MCS and let $\mathcal{M}_{\Gamma}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be the extracted model, and $\Delta_{i}\in M$. If
$@_{i}\langle\mathsf{a}\alpha\rangle\varphi\in\Gamma$, then there exists
$\Delta_{j}\in M$ such that $\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ and
$@_{j}\langle\alpha\rangle\varphi\in\Gamma$.

######  Proof 3.14.

Let $\Delta_{i}\in M$. By hypothesis,
$@_{i}\langle\mathsf{a}\alpha[\varphi]=_{e}\mathsf{a}\alpha[\varphi]\rangle\in\Gamma$,
then by Lemma 3.11 there exists $\Delta_{j}\in M$ such that
$\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ and
$@_{j}\langle\alpha[\varphi]=_{e}@_{i}\alpha[\varphi]\rangle\in\Gamma$. By
comp=-dist,
$\langle@_{j}\alpha[\varphi]=_{e}@_{j}@_{i}\alpha[\varphi]\rangle\in\Gamma$,
and by comp-neutral and subpath we get
$\langle@_{j}\alpha[\varphi]\rangle\top\in\Gamma$. Then, using comp-dist,
comp-assoc and =-test, we have $@_{j}\langle\alpha\rangle\varphi\in\Gamma$.

Now we are ready to prove the Truth Lemma that states that membership in an
MCS generating an extracted model is equivalent to being true at a state in
the extracted model. First let us introduce a notion of size for node and path
expressions, which we will use in the inductive cases of the proof.

######  Definition 3.15.

We define inductively the size of a path and node expression (notation
${\mid}\cdot{\mid}$) as follows:

$\begin{array}[]{l@{~=~}l@{\quad\quad\quad}l@{~=~}l}{\mid}\mathsf{a}{\mid}\hfil~{}=~{}&2&{\mid}p{\mid}\hfil~{}=~{}&1,~{}p\in\mathsf{Prop}\cup\mathsf{Nom}\\\
{\mid}@_{i}{\mid}\hfil~{}=~{}&1&{\mid}\neg\varphi{\mid}\hfil~{}=~{}&{\mid}\varphi{\mid}\\\
{\mid}[\varphi]{\mid}\hfil~{}=~{}&1+{\mid}\varphi{\mid}&{\mid}\varphi\wedge\psi{\mid}\hfil~{}=~{}&{\mid}\varphi{\mid}+{\mid}\psi{\mid}\\\
{\mid}\alpha\beta{\mid}\hfil~{}=~{}&{\mid}\alpha{\mid}+{\mid}\beta{\mid}&{\mid}\langle\alpha*\beta\rangle{\mid}\hfil~{}=~{}&{\mid}\alpha{\mid}+{\mid}\beta{\mid},\end{array}$

where $\alpha,\beta$ are path expressions and $\varphi,\psi$ are node
expressions.

######  Lemma 3.16 (Truth Lemma).

Let $\mathcal{M}_{\Gamma}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be the extracted model from an MCS $\Gamma$, and let $\Delta_{i}\in M$. Then,
for any formula $\varphi$,

<EMAIL_ADDRESS>
######  Proof 3.17.

In fact we will prove a stronger result. Let $\Delta_{i},\Delta_{j}\in M$,
$\varphi$ be a node expression and $\alpha$ be a path expression.

(IH1):

<EMAIL_ADDRESS>
(IH2):

$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models\alpha~{}~{}\mbox{iff}~{}~{}@_{i}\langle\alpha\rangle
j\in\Gamma.$

The proof is a double induction argument, proceeding first on the structural
complexity of $\varphi$ and $\alpha$, and then on the size of path-formulas as
per Definition 3.15. First, we prove the base cases:

\- $\alpha=\mathsf{a}$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models\mathsf{a}$, iff
$\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ (by $\models$), iff
$@_{i}\langle\mathsf{a}\rangle j\in\Gamma$ (by definition of extracted model).

\- $\alpha=@_{k}$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models@_{k}$, iff
$\mathit{nom}(k)=\Delta_{j}$. But by definition of $\mathit{nom}$,
$\Delta_{j}=\Delta_{k}$, and because we know that $j\in\Delta_{j}$ we have
$j\in\Delta_{k}$. Then, we have $@_{k}j\in\Gamma$, and by agree,
$@_{i}@_{k}j\in\Gamma$.

\- $\varphi=p$: $\mathcal{M}_{\Gamma},\Delta_{i}\models p$ iff
$p\in\mathit{V}(\Delta_{i})$, iff $@_{i}p\in\Gamma$.

\- $\varphi=j$: $\mathcal{M}_{\Gamma},\Delta_{i}\models j$ iff
$\mathit{nom}(j)=\Delta_{i}$, iff $\Delta_{i}=\Delta_{j}$ iff
$j\in\Delta_{i}$, iff $@_{i}j\in\Gamma$.

Now we prove the inductive cases:

\- $\varphi=\psi\wedge\theta$ and $\varphi=\neg\psi$ are direct from (IH1).

\- $\alpha=[\psi]$: $\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models[\psi]$
iff $\Delta_{i}=\Delta_{j}$ and $\mathcal{M}_{\Gamma},\Delta_{i}\models\psi$.
By (IH1), we have $@_{i}\psi\in\Gamma$ and $j\in\Delta_{i}$, then
$@_{i}j\in\Gamma$. As $\Gamma$ is an MCS, we have $@_{i}(\psi\wedge
j)\in\Gamma$, and by idempotence of the conjunction we have
$@_{i}(\psi\wedge\psi\wedge j\wedge j)\in\Gamma$. Also,
$\langle\epsilon=_{e}\epsilon\rangle$ is a theorem, by Nec we have
$@_{i}\langle\epsilon=_{e}\epsilon\rangle\in\Gamma$, then
$@_{i}(\psi\wedge\psi\wedge j\wedge
j\wedge\langle\epsilon=_{e}\epsilon\rangle)\in\Gamma$. Using $=$-test and
$=$-comm we obtain $@_{i}\langle[\psi][j]=_{e}[\psi][j]\rangle\in\Gamma$
(which is the same as $@_{i}\langle[\psi]\rangle j$) as we wanted.

\- $\alpha=\mathsf{a}\beta$: For the left to right implication, let
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models\mathsf{a}\beta$ iff there
is some $\Delta_{k}\in M$ such that
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{k}\models\mathsf{a}$ and
$\mathcal{M}_{\Gamma},\Delta_{k},\Delta_{j},\models\beta$. By (IH2), we have
$@_{i}\langle\mathsf{a}\rangle k\in\Gamma$ and $@_{k}\langle\beta\rangle
j\in\Gamma$, then $@_{i}\langle\mathsf{a}\rangle
k\wedge@_{k}\langle\beta\rangle j\in\Gamma$. By agree, we have
$@_{i}\langle\mathsf{a}\rangle k\wedge@_{i}@_{k}\langle\beta\rangle
j\in\Gamma$, and with a simple hybrid logic argument, we get
$@_{i}(\langle\mathsf{a}\rangle k\wedge@_{k}\langle\beta\rangle j)\in\Gamma$.
By bridge, we have $@_{i}\langle\mathsf{a}\rangle\langle\beta\rangle
j\in\Gamma$, hence by comp-dist $@_{i}\langle\mathsf{a}\beta\rangle
j\in\Gamma$.

For the other direction, assume $@_{i}\langle\mathsf{a}\beta\rangle
j\in\Gamma$. Then, by Corollary 3.13 there exists some $k$ such that
$\Delta_{i}R_{\mathsf{a}}\Delta_{k}$ and $@_{k}\langle\beta\rangle
j\in\Gamma$. Then, applying (IH2) twice, we get
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{k}\models\mathsf{a}$ and
$\mathcal{M}_{\Gamma},\Delta_{k},\Delta_{j}\models\beta$. Therefore,
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models\mathsf{a}\beta$ as needed.

\- $\alpha=@_{k}\beta$ and $\alpha=[\psi]\beta$: these cases are similar to
the previous one.

For node expressions of the form $\langle\alpha*\beta\rangle$ we need to do
induction on the size of $\alpha$ and $\beta$. Notice that by $*$-comm,
$@_{i}\langle\alpha*\beta\rangle\in\Gamma$ iff
$@_{i}\langle\beta*\alpha\rangle\in\Gamma$. And by the semantic definition,
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle\alpha*\beta\rangle$ iff
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle\beta*\alpha\rangle$. So we need
only carry out the inductive steps for $\alpha$. Moreover, by comp-neutral,
$\vdash\langle\alpha*\beta\rangle\leftrightarrow\langle\alpha\epsilon*\beta\rangle$
which is also a validity. So we can assume that every path ends in a test. The
base case then is when ${\mid}\alpha{\mid}+{\mid}\beta{\mid}=2$, and both
$\alpha$ and $\beta$ are tests.

\- $\varphi=\langle[\psi]=_{e}[\theta]\rangle$: direct from test-dist.

\- $\varphi=\langle[\psi]\neq_{e}[\theta]\rangle$: By _test- $\bot$_ the
formula is equivalent to $\bot$, hence not in $\Gamma$. Moreover, by the
defined semantics the formula is unsatisfiable.

Now, let us consider ${\mid}\alpha{\mid}+{\mid}\beta{\mid}\geq 3$:

\- $\varphi=\langle\mathsf{a}\beta=_{e}\gamma\rangle$: Let us prove the right
to left direction. Suppose
$@_{i}\langle\mathsf{a}\beta=_{e}\gamma\rangle\in\Gamma$. By the Existence
Lemma, there is $\Delta_{j}\in M$ such that
$\Delta_{i}R_{\mathsf{a}}\Delta_{j}$, and
$@_{j}\langle\beta=_{e}@_{i}\gamma\rangle\in\Gamma$, for some
$j\in\mathsf{Nom}$. Notice that
${\mid}@_{j}\langle\beta=_{e}@_{i}\gamma\rangle{\mid}\leq{\mid}@_{i}\langle\mathsf{a}\beta=_{e}\gamma\rangle{\mid}$.
Applying (IH1) we obtain
$\mathcal{M}_{\Gamma},\Delta_{j}\models\langle\beta=_{e}@_{i}\gamma\rangle$,
so there exists $\Delta_{1},\Delta_{2}\in M$ such that

  1. (1)

$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{1}\models\beta$,

  2. (2)

$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{2}\models@_{i}\gamma$,

  3. (3)

$\Delta_{1}\sim_{e}\Delta_{2}$.

From $1$ and $\Delta_{i}R_{\mathsf{a}}\Delta_{j}$ we get
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{1}\models\mathsf{a}\beta$ and from
$2$ and the semantic interpretation of $@$ we get
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{2}\models\gamma$. Then, together with
$3$ we get
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle\mathsf{a}\beta=_{e}\gamma\rangle$,
as wanted.

For the other direction, suppose
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle\mathsf{a}\beta=_{e}\gamma\rangle$,
iff there are $\Delta_{j},\Delta_{k}$ such that
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models\mathsf{a}\beta$,
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{k}\models\gamma$ and
$\Delta_{j}\sim_{e}\Delta_{k}$. First notice that
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models\mathsf{a}\beta$ iff there
exists $\Delta_{t}\in M$ s.t.
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{t}\models\mathsf{a}$ and
$\mathcal{M}_{\Gamma},\Delta_{t},\Delta_{j}\models\beta$. Then we have,
$\Delta_{i}R_{\mathsf{a}}\Delta_{t}$, and by definition of
$\mathcal{M}_{\Gamma}$ we get $@_{i}\langle\mathsf{a}\rangle t\in\Gamma$. On
the other hand, by (IH2) on
$\mathcal{M}_{\Gamma},\Delta_{t},\Delta_{j}\models\beta$ we obtain
$@_{t}\langle\beta\rangle j\in\Gamma$. Since $\\{@_{i}\langle\mathsf{a}\rangle
t,@_{t}\langle\beta\rangle j\\}\subseteq\Gamma$, by comp-dist we have:

  1. (1)

$@_{i}\langle\mathsf{a}\beta\rangle j\in\Gamma$.

By (IH2) on $\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{k}\models\gamma$, and by
definition of $\mathcal{M}_{\Gamma}$ together with
$\Delta_{j}\sim_{e}\Delta_{k}$ we obtain, respectively:

  1. (2)

$@_{i}\langle\gamma\rangle k\in\Gamma$, and

  2. (3)

$@_{j}\langle\epsilon=_{e}@_{k}\rangle\in\Gamma$.

By $1$ and Corollary 3.13 there exists $\Delta_{l}$ such that

  1. (4)

$@_{l}\langle\beta\rangle j\in\Gamma$.

$(\ddagger)$ From $2$ we have $@_{i}\langle\gamma\rangle k\in\Gamma$ and from
$3$ we can obtain $@_{k}\langle\epsilon=_{e}@_{j}\rangle\in\Gamma$, then we
have $\langle@_{i}\gamma\rangle
k\wedge@_{k}\langle\epsilon=_{e}@_{j}\rangle\in\Gamma$, by comp-dist. By
bridge, $\langle@_{i}\gamma\rangle\langle\epsilon=_{e}@_{j}\rangle\in\Gamma$,
then by comp$=$-dist and back, we get
$\langle@_{i}\gamma=_{e}@_{j}\rangle\in\Gamma$. Applying $=$-comm, comp-
neutral, agree and $@$-dist,
$@_{j}\langle\epsilon=_{e}@_{i}\gamma\rangle\in\Gamma$.

Also, from $4$ we have $@_{l}\langle\beta\rangle j\in\Gamma$, then
$@_{j}\langle\epsilon=_{e}@_{i}\gamma\rangle\wedge\langle@_{l}\beta\rangle
j\in\Gamma$ (by MCS and comp-dist), and by bridge we get
$\langle@_{l}\beta\rangle\langle\epsilon=_{e}@_{i}\gamma\rangle\in\Gamma$. By
comp$=$-dist and comp-neutral,
$\langle@_{l}\beta=_{e}@_{l}\beta@_{i}\gamma\rangle\in\Gamma$, then by back,
agree and $@{=}$-dist we have
$@_{l}\langle\beta=_{e}@_{i}\gamma\rangle\in\Gamma$. Then we have

$\displaystyle@_{l}\langle\beta=_{e}@_{i}\gamma\rangle\in\Gamma$
$\displaystyle\Rightarrow~{}$
$\displaystyle@_{i}\langle\mathsf{a}\rangle\langle\beta=_{e}@_{i}\gamma\rangle\in\Gamma$
($\Delta_{i}R_{\mathsf{a}}\Delta_{l}$, Prop. 3.9 item 2)
$\displaystyle\Rightarrow~{}$
$\displaystyle@_{i}\langle\mathsf{a}\beta=_{e}\mathsf{a}@_{i}\gamma\rangle\in\Gamma$
(comp=-dist) $\displaystyle\Rightarrow~{}$
$\displaystyle@_{i}\langle\mathsf{a}\beta=_{e}@_{i}\gamma\rangle\in\Gamma$
(back) $\displaystyle\Rightarrow~{}$
$\displaystyle\langle@_{i}\mathsf{a}\beta=_{e}@_{i}@_{i}\gamma\rangle\in\Gamma$
(comp=-dist) $\displaystyle\Rightarrow~{}$
$\displaystyle\langle@_{i}\mathsf{a}\beta=_{e}@_{i}\gamma\rangle\in\Gamma$
(back) $\displaystyle\Rightarrow~{}$
$\displaystyle@_{i}\langle\mathsf{a}\beta=_{e}\gamma\rangle\in\Gamma$
($@$=-dist)

\- $\varphi=\langle[\psi]\beta=_{e}\gamma\rangle$: Let us prove the right to
left direction. Suppose $@_{i}\langle[\psi]\beta=_{e}\gamma\rangle\in\Gamma$.
By $=$-test, we have
$@_{i}(\psi\wedge\langle\beta=_{e}\gamma\rangle)\in\Gamma$, iff (by using an
argument purely based on modal reasoning), $@_{i}\psi\in\Gamma$ and
$@_{i}\langle\beta=_{e}\gamma\rangle\in\Gamma$. By (IH1) on both expressions
we get $\mathcal{M}_{\Gamma},\Delta_{i}\models\psi$ and
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle\beta=_{e}\gamma\rangle$. Then,
by the semantic interpretation of $\wedge$ and $[\psi]$, we get
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle[\psi]\beta=_{e}\gamma\rangle$,
as wanted.

For the other direction, suppose
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle[\psi]\beta=_{e}\gamma\rangle$,
iff there are $\Delta_{j},\Delta_{k}$ such that
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{j}\models[\psi]\beta$,
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{k}\models\gamma$ and
$\Delta_{j}\sim_{e}\Delta_{k}$. Then, by (IH2) and definition of
$\mathcal{M}_{\Gamma}$ we have:

  1. (1)

$@_{i}\langle\beta\rangle j\in\Gamma$,

  2. (2)

$@_{i}\langle\gamma\rangle k\in\Gamma$,

  3. (3)

$@_{j}\langle\epsilon=_{e}@_{k}\rangle\in\Gamma$, and

  4. (4)

$@_{i}\psi\in\Gamma$.

Using the same argument as in $(\ddagger)$ the proof that
$@_{i}\langle[\psi]\beta=_{e}\gamma\rangle\in\Gamma$ is straightforward.

\- $\varphi=\langle@_{j}\beta=_{e}\gamma\rangle$: For the left to right
direction suppose
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle@_{j}\beta=_{e}\gamma\rangle$,
iff there are $\Delta_{k},\Delta_{l}$ such that
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{k}\models@_{j}\beta$,
$\mathcal{M}_{\Gamma},\Delta_{i},\Delta_{l}\models\gamma$ and
$\Delta_{k}\sim_{e}\Delta_{l}$. Then, by (IH2) and definition of
$\mathcal{M}_{\Gamma}$ we have:

  1. (1)

$@_{i}\langle@_{j}\beta\rangle k\in\Gamma$ iff $@_{j}\langle\beta\rangle
k\in\Gamma$,

  2. (2)

$@_{i}\langle\gamma\rangle l\in\Gamma$, and

  3. (3)

$@_{l}\langle\epsilon=_{e}@_{k}\rangle\in\Gamma$, iff
$@_{k}\langle\epsilon=_{e}@_{l}\rangle\in\Gamma$.

By $1$ and $3$, applying bridge we get
$@_{j}\langle\beta\rangle\langle\epsilon=_{e}@_{l}\rangle\in\Gamma$, iff (by
comp$=$-dist) $@_{j}\langle\beta=_{e}\beta@_{l}\rangle\in\Gamma$. By back, we
get $@_{j}\langle\beta=_{e}@_{l}\rangle\in\Gamma$, which is equivalent to
$@_{l}\langle\epsilon=_{e}@_{j}\beta\rangle\in\Gamma$ (by agree and
comp=-dist). Together with $2$ and bridge we get
$@_{i}\langle\gamma\rangle\langle\epsilon=_{e}@_{j}\beta\rangle\in\Gamma$,
hence $@_{i}\langle\gamma=_{e}\gamma@_{j}\beta\rangle\in\Gamma$ iff (by back
and $=$-comm) $@_{i}\langle@_{j}\beta=_{e}\gamma\rangle\in\Gamma$.

For the other direction suppose
$@_{i}\langle@_{j}\beta=_{e}\gamma\rangle\in\Gamma$. First notice that, in all
the cases we considered so far, the induction is on the path expression
appearing on the left side of the $=$. However, an analogous argument can be
applied if we do induction in the path expression on the right side of the
$=$, by $=$-comm. Suppose we proceed as above for the node expression
$\langle@_{j}\beta=_{e}\gamma\rangle$. If we apply the exact same steps, we
will find out that this time we need to do induction on $\gamma$; but, as we
mentioned, the cases for $\mathsf{a}$ and $[\varphi]$ are symmetric in both
sides of the $=$. As a consequence, it all boils down to consider only the
case $\gamma=@_{k}\eta$.

Suppose $@_{i}\langle@_{j}\beta=_{e}@_{k}\eta\rangle\in\Gamma$. By Existence
Lemma we have $@_{j}\langle\beta=_{e}@_{k}\eta\rangle\in\Gamma$, hence by
(IH1)
$\mathcal{M}_{\Gamma},\Delta_{j}\models\langle\beta=_{e}@_{k}\eta\rangle$. By
semantics of $@$, and the fact that $\mathcal{M}_{\Gamma}$ is named,
$\mathcal{M}_{\Gamma},\Delta_{i}\models\langle@_{j}\beta=_{e}@_{k}\eta\rangle$.

\- The cases involving $\neq_{e}$ are analogous, using item $1$ from
Proposition 3.9 to obtain $@_{j}\langle\epsilon=_{e}@_{k}\rangle\notin\Gamma$
in item $3$ above.

######  Lemma 3.18 (Frame Lemma).

If $\Gamma$ is a named, pasted and $\mathrm{P}$-saturated MCS of
$\mathsf{HXP}+\Pi+\mathrm{P}$, then the underlying frame of
$\mathcal{M}_{\Gamma}$ satisfies
$\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$.

######  Proof 3.19.

Since $\mathcal{M}_{\Gamma}$ is a named model and $\Gamma$ contains all
instances of elements of $\Pi$, it follows that the underlying frame of
$\mathcal{M}_{\Gamma}$ satisfies $\textsf{FC}(\Pi)$. Since
$\mathcal{M}_{\Gamma}$ is a named model and $\Gamma$ is
$\mathrm{P}$-saturated, it follows that the underlying frame of
$\mathcal{M}_{\Gamma}$ satisfies $\textsf{FC}(\mathrm{P})$.

As a result we obtain the completeness result.

######  Theorem 3.19 (Strong Completeness).

Let $\Pi$ be a set of pure axioms and $\mathrm{P}$ a set of existential
saturation rules. Let $\mathfrak{C}=\mathsf{Mod}(\mathfrak{F})$ for
$\mathfrak{F}$ the class of all frames satisfying
$\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$. Then, the axiomatic system
$\mathsf{HXP}+\Pi+\mathrm{P}$ is strongly complete for $\mathfrak{C}$.

######  Proof 3.20.

We need to prove that every set of $\text{HXPath}_{=}$-formulas $\Sigma$ is
consistent if and only if $\Sigma$ is satisfiable in an abstract hybrid data
model satisfying the frame properties defined by $\Pi$ and $\mathrm{P}$.

For any consistent $\Sigma$, we can use the Rule Saturation Lemma to obtain
$\Sigma^{\omega}$, which is a named, pasted and $\mathrm{P}$-saturated MCS in
$\text{HXPath}_{=}$ extended by a set $\mathsf{Nom}^{\prime}$ of additional
nominals. Let $\mathcal{M}_{\Sigma^{\omega}}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be the extracted model from $\Sigma^{\omega}$. Let $i\in\Sigma^{\omega}$, for
all $\varphi\in\Sigma$, by _$@$ -intro_ we have
$@_{i}\varphi\in\Sigma^{\omega}$ since $\Sigma^{\omega}$ is MCS. Then by the
Truth Lemma, $\mathcal{M}_{\Sigma^{\omega}},\Delta_{i}\models\varphi$. By the
Frame Lemma, $\mathcal{M}_{\Sigma^{\omega}}$ satisfies all required frame
properties.

Because the class of abstract data models is a conservative abstraction of
concrete data models, we can conclude:

######  Corollary 3.21.

The axiomatic system $\mathsf{HXP}+\Pi+\mathrm{P}$ is strongly complete for
the class of concrete hybrid data models satisfying the frame conditions
$\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$.

###  3.4. Completeness for path formulas

The main contribution of this article is a characterization of (local)
semantic consequence between node formulas by means of an axiomatic system.
Given that soundness of an axiomatic system is usually granted, this is the
main outcome of the strong completeness result we just proved. In the setting
of XPath it also makes sense to discuss the issue of inference between path
formulas. Path inference can be traced back to [Pra91], in the context of
dynamic algebras. We will now show how Theorem 2 can also be used to
characterize path inference.

First, recall that previous work like [tCLM10, ADFF17] provided _equational_
axiomatizations that characterize theorems of the form
$\vdash\varphi\equiv\psi$ (for $\varphi,\psi$ node expressions) and
$\vdash\alpha\equiv\beta$ (for $\alpha,\beta$ path expressions). The first are
obviously covered by our results that characterize theoremhood for arbitrary
node expressions (in this case $\equiv$ is nothing more than
$\leftrightarrow$). For equivalence between path formulas the following
proposition suffices:

######  Proposition 3.22.

Let $\alpha,\beta$ be path expressions in $\text{HXPath}_{=}$, then
$\models\alpha\equiv\beta$ iff $\models@_{i}\langle\alpha\rangle
j\leftrightarrow@_{i}\langle\beta\rangle j$ for $i,j$ not appearing in
$\alpha,\beta$.

Hence, completeness for equivalence theorems between path formulas follow from
Theorem 2. More interesting is to consider whether a strong completeness
result for path consequence is also possible. We need first to introduce this
notion. There exists at least two natural possible definitions:

######  Definition 3.23.

Let $\Lambda\cup\\{\alpha\\}$ be a set of path formulas in
$\text{HXPath}_{=}$, and let $\mathfrak{C}$ be a class of models. Define

  * •

$\Lambda\models^{1}_{\mathfrak{C}}\alpha$ iff for any model
$\mathcal{M}\in\mathfrak{C}$, ($\forall m,n$, $\mathcal{M},m,n\models\Lambda$
implies $\mathcal{M},m,n\models\alpha$).

  * •

$\Lambda\models^{2}_{\mathfrak{C}}\alpha$ iff for any model
$\mathcal{M}\in\mathfrak{C}$, ($\forall m,n$, $\mathcal{M},m,n\models\Lambda$
implies $\forall m,n$, $\mathcal{M},m,n\models\alpha$).

As before we write $\models$ instead of $\models_{\mathfrak{C}}$ if the
intended class is clear from context. From the above definition it is easy to
show that $\models^{1}_{\mathfrak{C}}$ implies $\models^{2}_{\mathfrak{C}}$
but not vice versa. Now, both $\models^{1}$ and $\models^{2}$ can be captured
using Theorem 2.

######  Theorem 3.23.

Let $\Pi$ be a set of pure axioms and $\mathrm{P}$ be a set of existential
saturation rules. Let $\mathfrak{C}=\mathsf{Mod}(\mathfrak{F})$ for
$\mathfrak{F}$ the class of frames satisfying
$\textsf{FC}(\Pi)\wedge\textsf{FC}(\mathrm{P})$. Let $\Lambda\cup\\{\alpha\\}$
be a set of path expressions in $\text{HXPath}_{=}$ then

  1. (1)

$\Lambda\models^{1}_{\mathfrak{C}}\alpha$ implies $\\{@_{i}\langle\beta\rangle
j\mid\beta\in\Lambda\\}\vdash@_{i}\langle\alpha\rangle j$, for $i,j$ not in
$\Lambda\cup\\{\alpha\\}$.

  2. (2)

$\Lambda\models^{2}_{\mathfrak{C}}\alpha$ implies $\\{@_{i}\langle\beta\rangle
j\mid\beta\in\Lambda\\}\vdash@_{k}\langle\alpha\rangle l$, for $i,j,k,l$ not
in $\Lambda\cup\\{\alpha\\}$.

######  Proof 3.24.

The result is a corollary of Theorem 2 because the following hold:

  1. (1)

$\Lambda\models^{1}_{\mathfrak{C}}\alpha$ iff $\\{@_{i}\langle\beta\rangle
j\mid\beta\in\Lambda\\}\models_{\mathfrak{C}}@_{i}\langle\alpha\rangle j$, for
$i,j$ not in $\Lambda\cup\\{\alpha\\}$.

  2. (2)

$\Lambda\models^{2}_{\mathfrak{C}}\alpha$ iff $\\{@_{i}\langle\beta\rangle
j\mid\beta\in\Lambda\\}\models_{\mathfrak{C}}@_{k}\langle\alpha\rangle l$, for
$i,j,k,l$ not in $\Lambda\cup\\{\alpha\\}$.

###  3.5. Some Concrete Examples of Pure Extensions

In this section we introduce some extensions of $\text{HXPath}_{=}$, and their
corresponding extended axiomatic systems. In all cases, we can apply the
result from previous section and automatically obtain completeness, since we
only use pure axioms and/or existential saturation rules.

#### Backwards Navigation.

We start with the language $\text{HXPath}_{=}(\shortminus)$, i.e.,
$\text{HXPath}_{=}$ extended with the path expression $\mathsf{a}$ (backwards
navigation). The intuitive semantics for $\mathsf{a}$ is

$\mathcal{M},x,y\models\mathsf{a}~{}~{}\mbox{iff}~{}~{}xR_{\mathsf{a}}^{-1}y,$

i.e., $\mathsf{a}$ is interpreted on the inverse of the accessibility relation
associated to $\mathsf{a}$. Equivalently,

$\mathcal{M},x,y\models\mathsf{a}~{}~{}\mbox{iff}~{}~{}yR_{\mathsf{a}}x.$

In fact, following our presentation, $\mathsf{a}$ is an additional modal
operator from $\mathsf{Mod}$ (to which all rules and axioms of $\mathsf{HXP}$
apply), and in addition we will insist that in models of
$\text{HXPath}_{=}(\shortminus)$, this accessibility relation is always
interpreted as the inverse of the one for $\mathsf{a}$.

Formally, consider two modal symbols $\mathsf{a}$ and $\mathsf{a}$ in
$\mathsf{Mod}$ (and assume that their respective accessibility relations in a
model are $R_{\mathsf{a}}$ and $R_{\mathsf{a}}$). Define the set $\Pi_{1}$ of
pure axioms that characterizes the interaction between $\mathsf{a}$ and
$\mathsf{a}$ as

Axioms for $\mathsf{a},\mathsf{a}$-interaction
---
| down-up | $\vdash i\rightarrow[\mathsf{a}]\langle\mathsf{a}\rangle i$
---|---
up-down | $\vdash i\rightarrow[\mathsf{a}]\langle\mathsf{a}\rangle i$

Since the axioms presented above are pure, the axiom system we obtain is
complete for models obtained from frames satisfying $\textsf{FC}(\Pi_{1})$. It
is a simple exercise to verify that $\textsf{FC}(\Pi_{1})$ is equivalent to
$\forall x.\forall y.(R_{\mathsf{a}}(x,y)\leftrightarrow
R_{\mathsf{a}}(y,x))$.

######  Proposition 3.25.

$\mathsf{HXP}+\Pi_{1}$ is sound and strongly complete for
$\text{HXPath}_{=}(\shortminus)$.

#### Sibling Navigation.

We consider now the extension of $\text{HXPath}_{=}(\shortminus)$ with sibling
navigation $\mathsf{s}$, denoted $\text{HXPath}_{=}(\shortminus,\mathsf{s})$.
Intuitively,

$\mathcal{M},x,y\models\mathsf{s}~{}~{}\mbox{iff}~{}~{}x\neq y\mbox{ and there
is some $z$ s.t. $zR_{\mathsf{a}}x$ and $zR_{\mathsf{a}}y$,}$

where $\mathsf{a}\in\mathsf{Mod}$ is fixed.

Consider now three modal symbols $\mathsf{a}$, $\mathsf{a}$ and $\mathsf{s}$
in $\mathsf{Mod}$ (and their respective accessibility relations
$R_{\mathsf{a}}$, $R_{\mathsf{a}}$ and $R_{\mathsf{s}}$). Define the set
$\Pi_{2}$ of pure axioms that characterizes their interaction as the axioms in
$\Pi_{1}$ together with

Axioms for siblings
---
| is-sib | $\vdash\langle\mathsf{s}\rangle i\rightarrow\langle\mathsf{a}\rangle\langle\mathsf{a}\rangle i$
---|---
has-sib | $\vdash\neg i\wedge\langle\mathsf{a}\rangle\langle\mathsf{a}\rangle i\rightarrow\langle\mathsf{s}\rangle i$
irref-sib | $\vdash i\rightarrow\neg\langle\mathsf{s}\rangle i$

As $\Pi_{2}$ extends $\Pi_{1}$, $\textsf{FC}(\Pi_{2})$ ensures that
$R_{\mathsf{a}}$ and $R_{\mathsf{a}}$ are inverses, and in addition that
$\forall x.\forall
y.(R_{\mathsf{s}}(x,y)\leftrightarrow((x\not=y)\wedge(\exists
z.(R_{\mathsf{a}}(x,z)\wedge R_{\mathsf{a}}(z,y)))))$.

######  Proposition 3.26.

$\mathsf{HXP}+\Pi_{2}$ is sound and strongly complete for
$\text{HXPath}_{=}(\shortminus,\mathsf{s})$.

#### Data Equality Properties.

As a final, very simple, example let us consider pure axioms defining the
behaviour of equality tests. Consider a language with two equality test
operators $=_{e}$ and $=_{d}$ such that one defines finer equivalence classes
than the other (i.e., if $\sim_{e}$ and $\sim_{d}$ are their respective
accessibility relations we want to ensure that
${\sim_{e}}\subseteq{\sim_{d}}$). Let us call this logic
$\text{HXPath}_{=}(\subseteq)$. Let $\Pi_{3}$ be the singleton set containing
the axiom

Axioms for equality inclusion
---
| incl | $\vdash\langle@_{i}=_{e}@_{j}\rangle\rightarrow\langle@_{i}=_{d}@_{j}\rangle$
---|---

$\textsf{FC}(\Pi_{3})$ is equivalent to $\forall x.\forall y.(D_{e}(x,y)\to
D_{d}(x,y))$.

######  Proposition 3.27.

$\mathsf{HXP}+\Pi_{3}$ is sound and strongly complete for
$\text{HXPath}_{=}(\subseteq)$.

##  4\. Hybrid XPath on Trees

The Henkin-style model construction from Section 3.3 provides us with the
tools to obtain complete axiomatizations for a wide variety of extensions of
$\text{HXPath}_{=}$. However there are interesting cases in which completeness
is not a direct corollary of the results we already presented. One such case
is the class of tree models which we call $\mathfrak{C}_{tree}$.

We will devote this section to investigate hybrid XPath over the class of tree
models. First, in Section 4.1 we will show that it is not possible to get a
strongly complete finitary first-order axiomatization over trees. In Section
4.2 we show that it is possible to obtain a strongly complete infinite first-
order axiomatization over a slightly larger class of models, while in Section
4.3 we prove that this axiomatization is weakly complete for
$\mathfrak{C}_{tree}$.

Tree models are interesting in this context since XPath is commonly used as a
query language over XML documents; and mathematically, the relational
structure of an XML document is a tree. In our setting, this consists of
asking that the union of all relations in a model has a tree-shape.

Without loss of generality, in the rest of this section we will work in a
mono-modal setting, with a unique basic path expression $\mathsf{a}$, and with
single equality/inequality comparisons denoted $=$ and $\neq$. The path
expression $\mathsf{a}$ will be interpreted over an accessibility relation
$R_{\mathsf{a}}$, representing the union of all the accessibility relations in
the model. To achieve this, we need to work in a signature where the set
$\mathsf{Mod}$ is finite. Therefore, we can include the followig additional
axiom:

|  $\mathsf{a}$-definition |  $\langle\mathsf{a}\rangle\top\leftrightarrow\langle\mathsf{a}_{1}\cup\ldots\cup\mathsf{a}_{k}\rangle\top$ with $\mathsf{Mod}=\\{\mathsf{a}_{1},\ldots,\mathsf{a}_{k}\\}$
---|---

It is a straightforward exercise to show that this axiom characterizes
$R_{\mathsf{a}}$ as the union of all the relations of the model, in a
signature where $\mathsf{Mod}$ is finite. As a consequence, in this section we
will focus on axiomatizing $R_{\mathsf{a}}$ as the acessibility relation of a
tree. In this way, we obtain the intended meaning for XPath as a query
language for XML documents.

Hence, a model in this signature is a tuple $\mathcal{M}=\langle
M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$, in which we have a
unique data equality relation $\sim$ and the accessibility relation
$R_{\mathsf{a}}$.

###  4.1. Failure of Strong Completeness over Trees

Let us start by formally defining the structures we will consider.

######  Definition 4.1.

$\mathfrak{C}_{tree}$ is defined as the class of abstract hybrid data models
$\langle M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$ satisfying:

  * •

there is a unique point in $M$ without predecessors by $R_{\mathsf{a}}$, which
we call the _root_ ;

  * •

every node $n\in M$ is reachable from the root by $R_{\mathsf{a}}$ in zero or
more steps;

  * •

for all $n,l,l^{\prime}\in M$, if $lR_{\mathsf{a}}n$ and
$l^{\prime}R_{\mathsf{a}}n$, then $l=l^{\prime}$; and

  * •

there is no $n\in M$ such that $n$ is reachable by $R_{\mathsf{a}}$ from
itself in one or more steps.

Intuitively, a model $\langle
M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$ is in
$\mathfrak{C}_{tree}$ if $\langle M,R_{\mathsf{a}}\rangle$ is a tree.

In order to show that there is no finitary first-order axiomatization for
$\text{HXPath}_{=}$ over $\mathfrak{C}_{tree}$, we will use a standard tool
from first-order model theory: the _compacteness_ theorem. In particular, we
will show that $\text{HXPath}_{=}$ over $\mathfrak{C}_{tree}$ is not compact,
and consequently, a finitary axiomatization may not exist (see, e.g., [End01]
for details).

######  Proposition 4.2.

$\text{HXPath}_{=}$ is not compact over the class $\mathfrak{C}_{tree}$.

######  Proof 4.3.

We need to show that there exists an infinite set of
$\text{HXPath}_{=}$-formulas such that every finite subset
$\Gamma^{fin}\subset\Gamma$ is satisfiable in the class $\mathfrak{C}_{tree}$,
but $\Gamma$ is not.

Without loss of generality, we will use natural numbers as names for nominals,
i.e., $\mathsf{Nom}={\rm Nature}$. We start by defining the following formula
indicating that, at the given point, the nominal $k$ is the only one satisfied
from the set $\\{0,\ldots,n\\}$:

$\mathsf{Only}^{n}_{k}=@_{k}(\underset{0\leq j\neq k\leq n}{\bigwedge}\neg
j).$

We can define for $n\geq 0$:

$\mathsf{Lin}(n)=\bigwedge_{0<i\leq n}@_{i}(\langle\mathsf{a}\rangle
i-1)\wedge\bigwedge_{0\leq i\leq n}\mathsf{Only}^{n}_{i}.$

The formula $\mathsf{Lin}(n)$ states that there exists a linear chain of named
states of length $n$. Now let us define the set
$\Gamma_{\mathsf{Lin}}=\\{\mathsf{Lin}(n)\mid n\in{\rm Nature}\\}$. Notice
that $\Gamma_{\mathsf{Lin}}$ enforces structures with at least one infinite
branch of the shape

$\ldots$$3$$2$$1$$0$

$\Gamma_{\mathsf{Lin}}$ satisfies the following properties:

  1. (1)

$\Gamma_{\mathsf{Lin}}$ does not have a model in $\mathfrak{C}_{tree}$, since
it enforces an infinite chain without a root (since every node has a
predecessor), and

  2. (2)

for all finite sets $\Gamma_{\mathsf{Lin}}^{fin}\subset\Gamma_{\mathsf{Lin}}$,
$\Gamma_{\mathsf{Lin}}^{fin}$ has a model in $\mathfrak{C}_{tree}$.

Hence, the proposition follows.

######  Theorem 4.3.

There is no finitary first-order axiomatization which is strongly complete for
$\text{HXPath}_{=}$ over $\mathfrak{C}_{tree}$.

######  Proof 4.4.

Suppose there is some finitary first-order axiomatization $\mathsf{H}$ which
is sound and strongly complete for $\text{HXPath}_{=}$ over
$\mathfrak{C}_{tree}$, and let $\vdash$ be obtained from $\mathsf{H}$. For any
set of formulas $\Gamma$, we know:

  1. ($\dagger$)

if for all finite set $\Gamma^{fin}\subseteq\Gamma$, $\Gamma^{fin}$ is
consistent (i.e., $\Gamma^{fin}\not\vdash\bot$), then $\Gamma$ is consistent.

This follows from the fact that any proof is finite, so in order to make
$\Gamma$ inconsistent, only a finite set of its formulas is needed.

Since $\mathsf{H}$ is strongly complete, by item 2 in Proposition 4.2, each
set $\Gamma_{\mathsf{Lin}}^{fin}$ defined therein is consistent. Then, by item
($\dagger$) also $\Gamma_{\mathsf{Lin}}$ is consistent, and again by strong
completeness of $\mathsf{H}$ we can conclude that $\Gamma_{\mathsf{Lin}}$ has
a model in $\mathfrak{C}_{tree}$, contradicting item 1 in Proposition 4.2.
Therefore, there is no finitary first-order axiomatic system $\mathsf{H}$
strongly complete for $\mathfrak{C}_{tree}$.

######  Corollary 4.5.

There are no $\Pi$ and $\mathrm{P}$ such that $\mathsf{HXP}+\Pi+\mathrm{P}$ is
strongly complete for $\mathfrak{C}_{tree}$.

###  4.2. Axiomatizing the Class $\mathfrak{C}_{forest^{-}}$ with Pure Axioms

Define the class $\mathfrak{C}_{forest^{-}}$ as follows:

######  Definition 4.6.

Let $\mathfrak{C}_{forest^{-}}$ be the class of models $\langle
M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$ such that

  * •

there is no $n\in M$ such that $n$ is reachable by $R_{\mathsf{a}}$ from
itself in one or more steps;

  * •

for all $n\in M,n$ has at most one predecessor by $R_{\mathsf{a}}$.

Notice that the class $\mathfrak{C}_{forest^{-}}$ admits forests made of a
collection of models that consist of a tree, possibly extended with an
infinite chain attached to the root. Models from the class
$\mathfrak{C}_{forest^{-}}$ differ from those in $\mathfrak{C}_{tree}$, given
that we relaxed the first two conditions from Definition 4.1. We will
introduce a strongly complete axiomatization for $\mathfrak{C}_{forest^{-}}$.
Let $\Pi_{forest^{-}}$ be the set of axioms below. Define $\mathsf{a}^{1}$ as
$\mathsf{a}$, and $\mathsf{a}^{n+1}$ as $\mathsf{a}\mathsf{a}^{n}$.

Axioms for forests
---
|  _no-loops_ |  $\vdash@_{i}\neg\langle\mathsf{a}^{n}\rangle i$ for all $n>0$
---|---
_no-join_ | $\vdash@_{j}\langle\mathsf{a}\rangle i\wedge@_{k}\langle\mathsf{a}\rangle i\rightarrow@_{j}k$

In the table above, _no-loops_ is an infinite set of axioms preventing loops
of any size, whereas _no-join_ prevents the existence of more than one
predecesor. Since our axioms are pure and enforce the appropriate structures,
from Theorem 2 we get:

######  Theorem 4.6.

The axiomatic system $\mathsf{HXP}+\Pi_{forest^{-}}$ is strongly complete for
$\mathfrak{C}_{forest^{-}}$.

###  4.3. A Weakly Complete Axiomatization for Trees

In this section we will show that the axiom system
$\mathsf{HXP}+\Pi_{forest^{-}}$ introduced before, is weakly complete for
$\mathfrak{C}_{tree}$. Recall that for _weak completeness_ we need to show
that for any $\text{HXPath}_{=}$-formula $\varphi$, $\models\varphi$ implies
$\vdash\varphi$. In order to achieve this result we need to work on the
extracted model.

In what follows we use $mR_{\mathsf{a}}^{h}n$ to denote
$mR_{\mathsf{a}}u_{1}R_{\mathsf{a}}\ldots
R_{\mathsf{a}}u_{h-1}R_{\mathsf{a}}n$, for some sequence of states
$u_{1},\ldots,u_{h-1}$.

######  Definition 4.7.

Let $\mathcal{M}=\langle M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$
be a hybrid data model, $N\subseteq\mathsf{Nom}$, $N\neq\emptyset$, and $n\geq
0$. We define $\mathcal{M}_{\upharpoonright(n,N)}$ as

$\mathcal{M}_{\upharpoonright(n,N)}=\langle S,\sim_{\upharpoonright
S},{R_{\mathsf{a}}}_{\upharpoonright S},\mathit{V}_{\upharpoonright
S},\mathit{nom}_{\upharpoonright S}\rangle,$

where

  * •

$S=\\{m\mid\mbox{ there is some }i\in N\mbox{ such that
}\mathit{nom}(i)\rightarrow^{h}m,~{}\mbox{ with }h\leq n\\}$,

  * •

${\sim_{\upharpoonright S}}={\sim}\cap(S\times S)$;

  * •

${{R_{\mathsf{a}}}_{\upharpoonright S}}={R_{\mathsf{a}}}\cap(S\times S)$;

  * •

$\mathit{V}_{\upharpoonright S}(m)=~{}\mathit{V}(m)$, for all $m\in S$; and

  * •

$\mathit{nom}_{\upharpoonright
S}(i)=\left\\{\begin{array}[]{ll}\mathit{nom}(i)&\mbox{if }i\in N\\\
m&\mbox{if }i\notin N,~{}m\in S\mbox{ arbitrary}.\end{array}\right.$

Intuitively, $\mathcal{M}_{\upharpoonright(n,N)}$ is the restriction of
$\mathcal{M}$ to the states reached from a nominal in $N$, in at most $n$
steps. It is obvious that $\mathcal{M}_{\upharpoonright(n,N)}$ has finite
depth if $N$ is finite.

In what follows, we will write $\mathsf{Nom}(\varphi)$ to denote the set of
nominals appearing in the formula $\varphi$.

######  Proposition 4.8.

Let $\varphi$ be an $\text{HXPath}_{=}$-formula, and let
$\mathcal{M}_{\Gamma}=\langle
M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$ be the extracted model
from some $\mathsf{HXP}+\Pi_{forest^{-}}$ MCS $\Gamma$, such that
$\mathcal{M}_{\Gamma},\Delta_{i}\models\varphi$, for some $\Delta_{i}$. Let
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}=\langle
S,\sim_{\upharpoonright S},{R_{\mathsf{a}}}_{\upharpoonright
S},\mathit{V}_{\upharpoonright S},\mathit{nom}_{\upharpoonright S}\rangle$,
then,

  1. (1)

$\Delta_{i}\in(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$, and

  2. (2)

$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{i}\models\varphi$.

######  Proof 4.9.

Item $1$ follows from the definition of
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$, since $i\in\Delta_{i}$ by
MCS. For item $2$, we will prove a stronger result.

(IH1):

For all $\alpha\in\mathsf{PExp}$ such that ${\sf md}(\alpha)\leq{\sf
md}(\varphi)$ and $\mathsf{Nom}(\alpha)\subseteq\mathsf{Nom}(\varphi)$, if
$\Delta_{j},\Delta_{k}\in(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$ then

$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{k}\models\alpha~{}~{}\mbox{iff}~{}~{}(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{k}\models\alpha.$

(IH2):

For all $\psi\in\mathsf{NExp}$ such that ${\sf md}(\psi)\leq{\sf md}(\varphi)$
and $\mathsf{Nom}(\psi)\subseteq\mathsf{Nom}(\varphi)$, if
$\Delta_{j}\in(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$ then

$\mathcal{M}_{\Gamma},\Delta_{j}\models\psi~{}~{}\mbox{iff}~{}~{}(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j}\models\psi.$

The proof is by induction on $\alpha$ and $\psi$. Assume
$\Delta_{j},\Delta_{k}\in(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$. Let us start by the base
cases.

\- $\alpha=\mathsf{a}$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{k}\models\mathsf{a}$, iff
$\Delta_{j}R_{\mathsf{a}}\Delta_{k}$. Since
$\Delta_{j},\Delta_{k}\in(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$, by definition we have
$\Delta_{j}\rightarrow_{\upharpoonright S}\Delta_{k}$. Therefore,
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{k}\models\mathsf{a}$.
The other direction is straightforward, since
$\Delta_{j}{R_{\mathsf{a}}}_{\upharpoonright S}\Delta_{k}$ implies
$\Delta_{j}R_{\mathsf{a}}\Delta_{k}$.

\- $\alpha=@_{l}$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{k}\models@_{l}$, iff
$\mathit{nom}(l)=\Delta_{k}$. By assumption,
$\mathsf{Nom}(@_{l})\subseteq\mathsf{Nom}(\varphi)$, then
$\mathit{nom}_{\upharpoonright S}(l)=\mathit{nom}(l)=\Delta_{k}$, therefore
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{k}\models@_{l}$.
The other direction follows from the fact that
$\mathsf{Nom}(@_{l})=\\{l\\}\subseteq\mathsf{Nom}(\varphi)$, then
$\mathit{nom}(l)=\Delta_{k}$.

\- $\psi=p$: Suppose $\mathcal{M}_{\Gamma},\Delta_{j}\models p$, iff
$p\in\mathit{V}(\Delta_{j})$. By assumption $\Delta_{j}\in S$, then
$p\in\mathit{V}_{\upharpoonright S}(\Delta_{j})$. Hence,
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j}\models p$. The
other direction is similar.

\- $\psi=k\in\mathsf{Nom}(\varphi)$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{j}\models k$, iff $\mathit{nom}(k)=\Delta_{j}$.
By assumption $\Delta_{j}\in S$, then $\mathit{nom}_{\upharpoonright
S}=\Delta_{j}$. Hence, $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j}\models k$. The
other direction is similar.

Now we prove the inductive cases.

\- $\alpha=[\theta]$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{k}\models[\theta]$, iff
$\Delta_{j}=\Delta_{k}$ and $\mathcal{M}_{\Gamma},\Delta_{k}\models\theta$. By
$\Delta_{j}\in S$ and (IH2), we have
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j}\models\theta$, iff
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{k}\models[\theta]$.
For the other direction, use similar steps.

\- $\alpha=\beta\gamma$: Suppose
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{k}\models\beta\gamma$, iff there
exists $\Delta_{l}$ such that
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{l}\models\beta$ and
$\mathcal{M}_{\Gamma},\Delta_{l},\Delta_{k}\models\gamma$. Notice that since
$\Delta_{j},\Delta_{k}\in S$, and ${\sf md}(\alpha)\leq{\sf md}(\varphi)$, we
have $\Delta_{j}\rightarrow^{n}\Delta_{l}$, for some $n\leq{\sf md}(\varphi)$,
then $\Delta_{l}\in S$. By (IH1), we have
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{l}\models\beta$
and $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{l},\Delta_{k}\models\gamma$.
Therefore, $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{k}\models\beta\gamma$.
The other direction is direct from (IH1).

\- $\psi=\neg\theta$ and $\psi=\theta\wedge\theta^{\prime}$: are direct from
(IH2).

\- $\psi=\langle\beta=\gamma\rangle$:
$\mathcal{M}_{\Gamma},\Delta_{j}\models\langle\beta=\gamma\rangle$, iff there
exists $\Delta_{k},\Delta_{l}$ such that
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{k}\models\beta$,
$\mathcal{M}_{\Gamma},\Delta_{j},\Delta_{l}\models\gamma$ and
$\Delta_{k}\sim\Delta_{l}$. From the fact that ${\sf md}(\psi)\leq{\sf
md}(\varphi)$, we have ${\sf md}(\beta)\leq{\sf md}(\varphi)$ and ${\sf
md}(\gamma)\leq{\sf md}(\varphi)$. Then,
$\Delta_{j}\rightarrow^{n}\Delta_{k}$, and
$\Delta_{j}\rightarrow^{m}\Delta_{l}$, for some $n,m\leq{\sf md}(\varphi)$. As
a consequence, $\Delta_{k},\Delta_{l}\in S$, then by (IH1) we get
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{k}\models\beta$
and $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j},\Delta_{l}\models\gamma$.
On the other hand, since $\Delta_{k}\sim\Delta_{l}$, we also get
$\Delta_{k}\sim_{\upharpoonright S}\Delta_{l}$, therefore
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{j}\models\langle\beta=\gamma\rangle$.
The other direction follows from (IH1).

\- $\psi=\langle\beta\neq\gamma\rangle$: Analogous to the previous case.

With this construction at hand, we obtain almost the structure of the model we
are looking for.

######  Lemma 4.10.

Let $\mathcal{M}_{\Gamma}$ be the extracted model for some MCS $\Gamma$,
$n\in{\rm Nature}$ and $N\subseteq\mathsf{Nom}$ finite.
$(\mathcal{M}_{\Gamma})_{\upharpoonright(n,N)}$ is a forest composed by a
finite number of disjoint trees.

######  Proof 4.11.

It is a straightforward exercise to check that from each nominal $i\in N$, we
generate a tree (remember that by _no-loops_ there are no cycles in
$\mathcal{M}_{\Gamma}$, and by _no-join_ each node has at most one
precedessor). Since $N$ is finite, we generate only a finite number of trees.

######  Definition 4.12.

Let $\mathcal{M}_{\upharpoonright(n,N)}$ be a model as in Definition 4.7. We
define $\mathcal{M}_{\upharpoonright(n,N)}^{IT}$ as the tree resulting of
adding a new node $r$ to $\mathcal{M}_{\upharpoonright(n,N)}$, and edges from
$r$ to the root to each of its subtrees. Essentially,
$\mathcal{M}_{\upharpoonright(n,N)}^{IT}$ is of the form:

$r$$i_{1}$$i_{2}$$i_{4}$$i_{3}$⋮$i_{n}$

######  Proposition 4.13.

Let $\mathcal{M}_{\Gamma}$ be the extracted model for some
$\mathsf{HXP}+\Pi_{forest^{-}}$ MCS $\Gamma$ and let $\varphi$ be an
$\text{HXPath}_{=}$-formula such that
$\mathcal{M}_{\Gamma},\Delta_{i}\models\varphi$, for some $\Delta_{i}$. Then,

  1. (1)

$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT}$ is a tree of finite
height, and

  2. (2)

$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT},\Delta_{i}\models\varphi$.

######  Proof 4.14.

For $1$, by construction it is obvious that
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT}$ is a tree of finite
height. To prove $2$ we can use a bisimulation-based argument. Define $Z$ as
the identity relation between the states in
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}$ and
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT}$ (therefore $r$ is not in
the relation). It is a straightforward exercise to show that $Z$ is an
$\text{HXPath}_{=}$-bisimulation. Since
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})},\Delta_{i}\models\varphi$, by
Proposition 2.2 we get $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT},\Delta_{i}\models\varphi$.

Because we were able to transform the extracted model into a model in
$\mathfrak{C}_{tree}$ which still satisfies the intended formula, we obtain
the intended completeness result.

######  Theorem 4.14.

The system $\mathsf{HXP}+\Pi_{forest^{-}}$ is weakly complete for
$\mathfrak{C}_{tree}$.

Moreover, $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT}$ can be transformed into
a bounded finite model, and hence, also decidability of the validity problem
follows.

######  Definition 4.15.

Let $\varphi$ be an $\text{HXPath}_{=}$-formula, and let $\mathcal{M}=\langle
M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle\in\mathfrak{C}_{tree}$.
We write $m\equiv_{\Gamma}m^{\prime}$ if for all $n$, $nR_{\mathsf{a}}m$ if
and only if $nR_{\mathsf{a}}m^{\prime}$, and $\mathcal{M},m\models\varphi$ if
and only if $\mathcal{M},m^{\prime}\models\varphi$, for all
$\varphi\in\Gamma$. If $\Gamma$ is finite, $\equiv_{\Gamma}$ is an equivalence
relation of finite index.

Given an equivalence relation $\equiv$ over a set $M$, a _selection function
$s$ for $\equiv$_ is a function $s:M_{/{\equiv}}\to M$ such that
$s([m])=m^{\prime}$, for $m^{\prime}\in[m]$ arbitrary.

######  Definition 4.16.

Let $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT}=\langle
M,\sim,R_{\mathsf{a}},\mathit{V},\mathit{nom}\rangle$ be as in Definition
4.12, let $\varphi$ be an $\text{HXPath}_{=}$-formula, and let $s$ be a
selection function for $\equiv_{\mathsf{Sub}(\varphi)}$. We define
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{FT}=\langle
F,\sim_{\upharpoonright F},{R_{\mathsf{a}}}_{\upharpoonright
F},\mathit{V}_{\upharpoonright F},\mathit{nom}_{\upharpoonright F}\rangle$
where

  * •

$F=\\{s([m])\mid m\in M\\}$;

  * •

${\sim_{\upharpoonright F}}={\sim}\cap(F\times F)$;

  * •

${{R_{\mathsf{a}}}_{\upharpoonright F}}={R_{\mathsf{a}}}\cap(F\times F)$;

  * •

$\mathit{V}_{\upharpoonright F}(m)=~{}\mathit{V}(m)$, for all $m\in F$; and

  * •

$\mathit{nom}_{\upharpoonright
F}(i)=\left\\{\begin{array}[]{ll}\mathit{nom}(i)&\mbox{if
}i\in\mathsf{Nom}(\varphi)\\\ m&\mbox{if }i\notin\mathsf{Nom}(\varphi),m\in
F\text{ arbitrary}.\end{array}\right.$

######  Proposition 4.17.

Let $\mathcal{M}_{\Gamma}$ be the extracted model for some
$\mathsf{HXP}+\Pi_{forest^{-}}$ MCS $\Gamma$ and let $\varphi$ be an
$\text{HXPath}_{=}$-formula such that
$\mathcal{M}_{\Gamma},\Delta_{i}\models\varphi$, for some $\Delta_{i}$. Then,

  1. (1)

$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{FT}$ is a finite tree, and

  2. (2)

$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{FT},s([\Delta_{i}])\models\varphi$.

######  Proof 4.18.

$1$ follows from the fact that $(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT}$ is a tree of finite
height, and the selection function selects only one representant for each
equivalence class, which gives us finite width. In order to prove $2$, let
$d(m)$ be the distance from $m$ to the root, define: