1 Preliminaries. Part 1.↩︎

We assume that the Reader is familiar with the standard notions regarding first-order logic (FOL) and its semantics. In particular, we use the terms signature, and atomic formula (or atom) in the standard sense. Fact is an atomic formula without variables (that is, only constants are allowed). We assume that there exists some fixed infinite set \(\mathcal{C}\) of constants.

1.1 Structures and Relations.↩︎

The signatures we consider only comprise unary and binary predicates, so we think of relational structures (for short just structures) over such signatures as (coloured and labelled) graphs and, in consequence, we call elements of their domains vertices and sometimes we call the binary atoms edges.

We find it notationally convenient to think that structures are just sets of facts. This means that the structures we consider never have isolated vertices and that only elements of \(\mathcal{C}\) can serve as verticies. This can be assumed, for the purpose of this paper, without loss of generality.

For a structure \({\mathcal{D}}\) by \(\operatorname{Dom}({\mathcal{D}})\) we denote the set of its vertices (that is the set of constants the facts of \({\mathcal{D}}\) mention). Structure \({\mathcal{D}}_1\) is called a substructure of \({\mathcal{D}}_2\) if \({\mathcal{D}}_1\subseteq{\mathcal{D}}_2\) (recall they are sets of facts). If \({\mathcal{D}}\) is a structure and \(C\subseteq \operatorname{Dom}({\mathcal{D}})\) then the set: \[{\mathcal{D}}[C] = \{E(c,d)\in {\mathcal{D}}: \; c,d\in C\} \cup \{A(c)\in {\mathcal{D}}: c\in C\}\] is called an induced by \(C\) substructure of \({\mathcal{D}}\).

1.2 Queries.↩︎

A conjunctive query (CQ) is a FOL formula which is a conjunction of atoms preceded by existential quantifiers. A conjunctive query with safe negation (\(\text{CQ}^{s\neg}\)) is a CQ where negated atoms are allowed. It is however assumed, that every variable that appears in such query, must appear in some positive (that is non-negated) atom. A CQ (or a \(\text{CQ}^{s\neg}\)) is Boolean if all its variables are bound by existential quantifiers. We use the notations \(\text{CQ}\) (or \(\text{CQ}^{s\neg}\)) also to denote the respective classes of queries.

For a Boolean \(\xi\in \text{CQ}\cup\text{CQ}^{s\neg}\) and a structure \({\mathcal{D}}\) by \({\mathcal{D}}\models \xi\) we mean that \(\xi\) is true in \({\mathcal{D}}\), in the usual FOL sense. Recall that if \(\xi\in \text{CQ}\) then \({\mathcal{D}}\models \xi\) is equivalent to the existence of a mapping from (the variables of) \(\xi\) to \({\mathcal{D}}\) which is a homomorphism. If \(\xi\in \text{CQ}^{s\neg}\) then, for \({\mathcal{D}}\models \xi\) to hold, this homomorphism must satisfy some additional natural constraint, namely the image of a negated atom in \(\xi\) must not be an atom in \({\mathcal{D}}\). We will call such mappings satisfying mappings.

1.3 The logic DL-Lite\(_{\text{\tiny \sc core}}\) and query entailment.↩︎

The DL-Lite family of logics, and the logic DL-Lite\(_{\text{\tiny \sc core}}\) in particular, were introduced in [1]. Since our work is technical in nature, we will not discuss DL-Lite family in the full generality here, focusing instead on presenting the minimal set of definitions allowing us to formulate our results.

A signature \(\Sigma\) comprising unary and binary predicates is assumed. A role is any binary relation over \(\Sigma\) or its inverse. A concept is any unary relation over \(\Sigma\) or any unary relation that can be defined as a projection of a role: for a role \(R\), the set \(\{x : \exists y\, R(x,y) \}\) is a concept, denoted as \(\exists R\).

A DL-Lite knowledge base \({\mathcal{O}}\) is a pair \(\langle \text{TBox}, \text{ABox} \rangle\), where \(\text{ABox}\) is a structure (i.e. a set of facts) and \(\text{TBox}\) is the “domain knowledge” – a set of expressions involving roles and concepts. DL-Lite\(_{\text{\tiny \sc core}}\) is the least expressive of the logics of family and only two forms of such expressions ale allowed in a DL-Lite\(_{\text{\tiny \sc core}}\), namely: \[(\usym{2660})\;\; B \sqsubseteq B' \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; (\usym{2665})\;\; B \sqsubseteq \neg B'\] where \(B\) and \(B'\) are concepts. The semantics of the expressions is natural, with \(\sqsubseteq\) meaning subset, and \(\neg\) meaning complementation. Notice that () means that two concepts are disjoint.

For a structure \({\mathcal{D}}\) and a knowledge base \({\mathcal{O}}=\langle \text{TBox}, \text{ABox} \rangle\) we say that \({\mathcal{D}}\) is a model of \({\mathcal{O}}\), denoted as \({\mathcal{D}}\models {\mathcal{O}}\) when \(\text{ABox}\subseteq {\mathcal{D}}\) and all the inclusions from \(\text{TBox}\) are satisfied in \({\mathcal{D}}\) in the usual FOL sense.

For a Boolean conjunctive query \(\xi\) (possibly with safe negation), and a knowledge base \({\mathcal{O}}\), by \({\mathcal{O}}\models \xi\) (“\({\mathcal{O}}\) entails \(\xi\)”) we mean that \(\xi\) is true in every structure \({\mathcal{D}}\) such that \({\mathcal{D}}\models {\mathcal{O}}\).

2 Our contribution↩︎

Our main technical result is:

3 Preliminaries. Part 2.↩︎

In this section, we present some non-standard notations, which will first let us equivalently restate Theorem 1 and then will be very useful in Sections 5 and 6 where our main technical result is proven.

3.1 CQs with one free variable.↩︎

For a conjunctive query \(\xi(x)\), possibly with safe negation, with one free variable, we denote by \(\xi^{\text{\scalebox{0.8}{\exists}}}\) the Boolean conjunctive query \(\exists x\,\xi(x)\). Variable \(x\) will be called the distinguished variable in \(\xi^{\text{\scalebox{0.8}{\exists}}}\).

To see what this notation can be good for imagine two queries \(\xi_1(x_1)\) and \(\xi_2(x_2)\), each with one free variable and a structure \({\mathcal{D}}\). Consider a new boolean conjunctive query: \[\xi \;\;\; = \; \;\; \exists x_1,x_2\;\;\; \neg H(x_1,x_2) \;\; \wedge \;\; \xi_1(x_1) \;\; \wedge \;\; \xi_2(x_2)\] Now, to satisfy \(\xi\) in \({\mathcal{D}}\), one needs to find two satisfying mappings \(h_1: \xi_1^{\text{\scalebox{0.8}{\exists}}} \rightarrow {\mathcal{D}}\) and \(h_2: \xi_2^{\text{\scalebox{0.8}{\exists}}} \rightarrow {\mathcal{D}}\) such that \(H(h_1(x_1),h_2(x_2))\not\in {\mathcal{D}}\). Apart from the last constraint, which concerns the distinguished variables of the two queries, the mappings are independent, because even if (syntactically) \(\xi_1^{\text{\scalebox{0.8}{\exists}}}\) and \(\xi_2^{\text{\scalebox{0.8}{\exists}}}\) shared some variables, the shared variables are local in \(\xi_1(x_1)\) and in \(\xi_2(x_2)\).

3.2 Types of vertices and the \(\text{\sc freeze}\) construct.↩︎

For a structure \({\mathcal{D}}\) over the signature \(\Sigma\) and for a vertex \(c\in \operatorname{Dom}({\mathcal{D}})\) we define the (unary) type \(type(c,{\mathcal{D}})\) of \(c\) in \({\mathcal{D}}\) in the natural way:

\[\begin{align} {3} \langle \;\;\{A&\in\Sigma \mid &&{\mathcal{D}}\models A(c)\},\\ \{R&\in\Sigma \mid \exists x\; &&{\mathcal{D}}\models R(c,x) \},\\ \{R&\in\Sigma \mid \exists x\; &&{\mathcal{D}}\models R(x,c)\} \;\; \rangle \end{align}\]

In words, \(type(c,{\mathcal{D}})\) tells us which unary predicates are true in \(c\), which binary predicates lead to \(c\), and which leave \(c\).

All DL-Lite\(_{\text{\tiny \sc core}}\) is able to say is about types. It is very easy to notice that:

So, as an example, suppose: \({\mathcal{D}}=\{E(a,b),E(b,c)\}\) and \({\mathcal{D}}'=\{E(a,b),E(b,c),E(a,c)\}\). Then no DL-Lite\(_{\text{\tiny \sc core}}\) \(\text{TBox}\) can distinguish between the two. This is a bit problematic from the point of view of proof of Theorem 1, because at some point in the proof we need to make sure that certain conjunctive query with safe negation is satisfied in every model. To this end we need to find a way to make sure that, in each model of the knowledge base we are going to construct, there is always enough of negativity to satisfy the negated atoms, that is there are enough atoms that are not true in the model.

But, as Observation 2 says we cannot prohibit the presence of atoms that do not change the types of the vertices. So let us at least prohibit the presence of atoms that do change the types of the vertices. And this is what the \(\text{\small \sc freeze}\) construct is about, which leads to the definition of a new logic, that we call DL-Lite\(_{\text{\tiny \sc core}}^+\):

Now, proving the following lemma is quite straighforward:

In view of Lemma 1 we equivalently restate Theorem 1 as:

And it is Theorem 3 that we prove in Sections 4 and 5.

4 High level proof of Theorem 3↩︎

In this section we present the high level part of our proof of Theorem 3. Some (or maybe even most) of the objects needed in the proof will remain undefined in this section. The list of such undefined notions includes:

1. a decision problem \({\mathbb{G}}\);

2. two finite sets \(\mathbb{S}\) of symbols and \(\mathbb{I}\) of names;

3. a conjunctive query with safe negation \({\mathbb{Q}}_i(x_i)\) with one free variable, for each \({i\in\mathbb{I}}\);

4. a finite structure \({\mathbb{A}}_i\), for each \(i \in \mathbb{I}\).

Instead of defining the above notions, in the current section we will just specify their properties.¹ Then we will prove that, if they all were indeed defined in a way satisfying the specifications, then the theorem would follow.

Let us insist that what we do here is not an “informal idea”, which will be followed by a precise proof. What we are doing here is totally rigorous, and — we hope — quite elegant. Then, in Sections 5 and 6 we show how to define the notions from the above list in a way satisfying the specifications. Definitions of the notions (ii)-(iv) will depend on the particular instance \({\mathcal{G}}\) of the problem \({\mathbb{G}}\) so, for example, instead of \(\mathbb{S}\) we should write \(\mathbb{S}_{\mathcal{G}}\). For the sake of readability, we omit this subscript. This should not cause any confusion, since we will always consider one fixed \({\mathcal{G}}\). Unlike the proof in the current section, the construction, and argument, in Sections 5 and 6 has a bit of a low-level programming flavour.

4.1 The source of undecidability↩︎

In order to prove Theorem 3 we are going to construct, for each instance \({\mathcal{G}}\) of the problem \({\mathbb{G}}\), a DL-Lite\(_{\text{\tiny \sc core}}^+\) knowledge base² \({\mathfrak K}\) and a Boolean conjunctive query with safe negations \({\mathfrak Q}\) such that the following equivalence will holds:

From now on, we consider an instance \({\mathcal{G}}\) to be fixed.

4.2 Towards the knowledge base \({\mathfrak K}\). Our \(\text{TBox}\).↩︎

We begin with the signature of the knowledge base \({\mathfrak K}\):

Now, recall that the \({\mathfrak K}\) we are going to construct is a DL-Lite\(_{\text{\tiny \sc core}}^+\) knowledge base, so it will be a triple \(\langle {\mathfrak T}, {\mathfrak A}, \text{\small \sc freeze}({\mathfrak A}_0) \rangle\) for some \(\text{TBox}\) \({\mathfrak T}\), some \(\text{ABox}\) \({\mathfrak A}\), and some \({\mathfrak A}_0 \subseteq {\mathfrak A}\).

We are now ready to define our \(\text{TBox}\) \({\mathfrak T}\) :

In human language this reads as:

• A vertex reached by some edge \(\mathsf{X}\in \mathbb{S}\) must produce an \(\mathsf{Y}\) for every \(\mathsf{Y}\in \mathbb{S}\);

• A vertex which is a \(Root\) must produce an \(\mathsf{Y}\) for every \(\mathsf{Y}\in \mathbb{S}\);

• A vertex reached by any \(\mathsf{X}\in \mathbb{S}\) (or one which is a \({\mathbf{A}}\)) is never too close to any other vertex.

4.3 Towards the \(\text{ABox}\).↩︎

Now let us concentrate on the structures \({\mathbb{A}}_i\), for \(i \in \mathbb{I}\). We like to think of them as beds in which our little bears will sleep, with their heads duly resting on the \(Pillows\). Their specification will come in two parts:

Notice, that our knowledge base is at this point defined: \[{\mathfrak K}\;\;=\;\;\langle {\mathfrak T}, {\mathfrak A}, \;\text{\small \sc freeze}({\mathfrak A}_0) \rangle\]

Now, suppose \({\mathcal{D}}\models {\mathbb{A}}\) for some structure \({\mathcal{D}}\). We define \({\Wintertree}({\mathcal{D}})\) as the set of all the vertices of \({\mathcal{D}}\) reachable from \(a\) by a path of \(\mathbb{S}\) symbols:

One can easily get tempted to imagine \({\mathcal{D}}_{\Wintertree}\) as an infinite tree, of out-degree equal to \(|\mathbb{S}|\) and with root in \(a\). But reality is more complicated, and many strange things³ may happen here. In the extreme case, \({\mathcal{D}}_{\Wintertree}\) could even be just the vertex \(a\) with all edges \(\mathsf{X}\), which origin from \(a\), looping back to it.

What we know for sure is that vertices of \({\Wintertree}({\mathcal{D}})\) are never too close to anything:

4.4 First step towards the query \({\mathfrak Q}\).↩︎

Now we are ready for:

The intuition is that the queries \({\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\), for \({i\in\mathbb{I}}\), collectively probe the structure \({\mathcal{D}}_{\Wintertree}\) in order to detect positivity of \({\mathcal{G}}\) there.

The queries (and also the set \(\mathbb{I}\)) will be defined in Section 5.2. But let us already reveal here that all of them but one will be conjunctive queries with safe negation, and one will be a CQ. Then, the idea is that the more \({\mathcal{D}}_{\Wintertree}\) will look like an infinite tree, the more the queries with safe negation will be likely to be satisfied in \({\mathcal{D}}_{\Wintertree}\). And the more \({\mathcal{D}}_{\Wintertree}\) will look like the aforementioned a self-looping \(a\), the more the single CQ will be likely to be satisfied.

Notice that if (as in (pos) above) there is \({\mathcal{D}}_{\Wintertree}\models {\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\) then also \({\mathcal{D}}\models {\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\), via the same mapping. This is true, despite the fact that queries \({\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\) may contain negated atoms, because \({\mathcal{D}}_{\Wintertree}\) is defined as the induced (by the set of vertices of \({\Wintertree}({\mathcal{D}})\)) substructure of \({\mathcal{D}}\).

There will be also one more very simple CQ needed in our construction: \({\mathbb{Q}}(x) = Pillow(x)\).

4.5 Little bears and their beds.↩︎

Imagine that queries \({\mathbb{Q}}_i\), for \(i\in \mathbb{I}\) are little bears, and the structures \({\mathbb{A}}_i\) as their designated beds. And imagine the query \({\mathbb{Q}}\) as Goldilocks, who does not really care where she sleeps, except that she needs a pillow.

The (c) above says that, whatever happens (that is, whatever model of \({\mathfrak T}\) we consider), each of the bears can sleep in his dedicated bed. The (d) says that (whatever happens) also Goldilocks can sleep in any of the beds.

The (e) and (f) say that there is only one right way, for each of our characters, to sleep in a bed: their head (the distinguished variable) must be mapped onto the pillow (the \(a_i\) vertex of the \({\mathbb{A}}_i\)).

A curious Reader could wonder here, how can we possibly define the structures in such a way that (c) is satisfied? However we defined \({\mathbb{A}}_i\), the \({\mathcal{D}}\) will be some unpredictable superstructure of \({\mathbb{A}}_i\), and how can we be sure that the negated atoms of \({\mathbb{Q}}_i\) are still satisfied in \({\mathcal{D}}\) (which means, that the relevant positive atoms remain false)? The answer is, that this requires all the objects here including the queries \({\mathbb{Q}}_i\) and the structures \({\mathbb{A}}_i\) to play as a one well-coordinated orchestra, with the \(\text{\small \sc freeze}\) operator playing the first violin in it.

The next lemma will be soon very useful, and it also gives us an opportunity to see the \(\freeze\) operator in action:

For the proof of the Lemma suppose \(k\neq i\). Then \(a_i\) is not involved in any atom of \(2Close_j\) in \({\mathbb{A}}_i\). So the statement \(\text{\small \sc freeze}(\bigcup_{i\in \mathbb{I}} {\mathbb{A}}_i)\) in \({\mathfrak K}\) guarantees that \(a_i\) is not involved in any atom of \(2Close_k\) also in \({\mathcal{D}}\). The case when \(k\neq j\) is analogous. 0◻

4.6 The query \({\mathfrak Q}\) and the main idea.↩︎

The idea here is that there are \(|\mathbb{I}|\)+1 characters that need to be put to bed. We have \(|\mathbb{I}|\) beds available, but there may also be an extra place for one of the bears to sleep, koala⁴ way, somewhere inside the “tree” \({\mathcal{D}}[{\Wintertree}({\mathcal{D}})]\) – the existence of this place is an undecidable property of \({\mathcal{G}}\) (recall Specification 6). And there is some mechanism in place (namely the part involving the \(2Close\) predicates) that is supposed to prohibit putting more than one character to the same bed.

Now, once we have both \({\mathfrak K}\) and \({\mathfrak Q}\) specified, we are able to prove the equivalence \(\bigpumpkin\) from Section 4.1.

4.7 The \(\Leftarrow\) direction.↩︎

Suppose \({\mathcal{G}}\) is a negative instance of \({\mathbb{G}}\). We just need to construct one structure \({\mathfrak D}\), such that \({\mathfrak D}\models{\mathfrak K}\) but \({\mathfrak D}\not\models{\mathfrak Q}\).

This \({\mathfrak D}\) will be defined as a disjoint union of structures: \[{\mathfrak D}\;\; = \;\; {\mathfrak D}_0\; \cupdot \; \bigcupdot_{i\in \mathbb{I}}\; {\mathbb{A}}_i\] Where \({\mathfrak D}_0\) is as in Specification 6 (neg).

First of all we need to show that \({\mathfrak D}\models{\mathfrak K}\). But clearly, all the facts from \({\mathbb{A}}\cup \bigcup_{i\in \mathbb{I}} {\mathbb{A}}_i\) are true in \({\mathfrak D}\) (recall that \({\mathfrak D}_0\models {\mathbb{A}}\)). Also the conditions imposed by \(\text{\small \sc freeze}(\bigcup_{i\in \mathbb{I}} {\mathbb{A}}_i)\) are obviously satisfied in \({\mathfrak D}\). This is because there are no new atoms in \({\mathfrak D}\), involving any of the constants from \(\operatorname{Dom}(\bigcup_{i\in \mathbb{I}} {\mathbb{A}}_i)\), compared to \(\bigcup_{i\in \mathbb{I}} {\mathbb{A}}_i\) itself. What concerns \({\mathfrak T}\), the structure \({\mathfrak D}\) is a disjoint union of several structures and it is enough to verify for each of these structures that it satisfies \({\mathfrak T}\). But we know that \({\mathfrak D}_0\models {\mathfrak T}\) (Specification 6 (neg)) and we also know that each \(i\in\mathbb{I}\) it holds that \({\mathfrak D}_0\models {\mathbb{A}}\) (Specification 7 (a)).

Now we need to prove that \({\mathfrak D}\not\models{\mathfrak Q}\). So suppose \({\mathfrak D}\models{\mathfrak Q}\). What would it mean exactly? It would mean that a set of mappings \(\{h\}\cup \{h_i\}_{i\in \mathbb{I}}\) could be found, such that:
• \(h_i\) satisfies \({\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\) in \({\mathfrak D}\) for each \(i\),
•  \(h\) satisfies \({\mathbb{Q}}^{\text{\scalebox{0.8}{\exists}}}\) in \({\mathfrak D}\),
and such that neither \(h(x)\) is too close to any of the \(h_i(x_i)\) nor \(h_i(x_i)\) is too close to any \(h_{i'}(x_{i'})\) for \(i\neq i'\).

Recall that each of \({\mathbb{Q}}_i\), for \(i\in \mathbb{I}\), is a connected query (by [spec:4] (con)). So the entire image of \(h_i\) must fall into one of the connected components of \({\mathfrak D}\). But it cannot fall into \({\mathfrak D}_0\) (by Specification 6 (neg)). Also the image of \(h\) cannot fall into \({\mathfrak D}_0\) (see Specification 6 (neg) again). Apart from \({\mathfrak D}_0\) the structure \({\mathfrak D}\) has \(|\mathbb{I}|\) connected components: the beds \({\mathbb{A}}_{i}\) for \(i\in \mathbb{I}\). So, by the bearhole principle, images of at least two of the aforementioned \(|\mathbb{I}|+1\) mappings must fall into some \({\mathbb{A}}_{k}\). In other words, two characters must be put to the same bed. But, by Specification 7 (e) and (f) this would mean that their heads (some \(x_i\) and \(x_j\), or \(x_i\) and \(x\)) are mapped to the same pillow \(a_k\). Which would mean that the constraint \(\neg2Close_k(x_i,x_j)\) (or \(\neg2Close_k(x_i,x)\)) would not be satisfied.

4.8 The \(\Rightarrow\) direction.↩︎

Now suppose that \({\mathcal{G}}\) is a positive instance of \({\mathbb{G}}\) and that \({\mathcal{D}}\models{\mathfrak K}\). We need to show that \({\mathcal{D}}\models{\mathfrak Q}\).

Again, this means that we need to find a set of mappings \(\{h\}\cup \{h_i\}_{i\in \mathbb{I}}\), such that \(h_i\) satisfies \({\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\) in \({\mathcal{D}}\) for each \(i\) (and \(h\) satisfies \({\mathbb{Q}}^{\text{\scalebox{0.8}{\exists}}}\) in \({\mathcal{D}}\)) and such that neither \(h(x)\) is too close to any of the \(h_i(x_i)\), nor \(h_i(x_i)\) is too close to \(h_{i'}(x_{i'})\) for any \(i\neq i\).

So let us first use the assumption that \({\mathcal{G}}\) is a positive instance. It implies (by Specification 6 (pos)) that there exists \(\Bbbk\in \mathbb{I}\) and a mapping \(h_\Bbbk\) which satisfies \({\mathbb{Q}}_\Bbbk^{\text{\scalebox{0.8}{\exists}}}\) in \({\mathcal{D}}\), and such that \(h_\Bbbk(x_\Bbbk)\in {\Wintertree}({\mathcal{D}})\) (in fact, \(h_\Bbbk\) maps all variables of \({\mathbb{Q}}_\Bbbk^{\text{\scalebox{0.8}{\exists}}}\) to \({\Wintertree}({\mathcal{D}})\), but it is only the image of \(x_\Bbbk\) that really matters to us).

Recall that (by Lemma 2) vertex \(h_\Bbbk(x_\Bbbk)\) is not too close to anything. So in particular \(h_\Bbbk(x_\Bbbk)\) may not happen to be equal to any \(a_j\), for \(j\in \mathbb{I}\), because each such \(a_j\) is too close to itself (by Specification 7 (b)).

Now we are ready to satisfy \({\mathbb{Q}}^{\text{\scalebox{0.8}{\exists}}}\). We put \(h(x)=a_\Bbbk\) (recall Specification 7 (d)). See, we do not need this \(a_\Bbbk\) any more for \(x_\Bbbk\), because \(x_\Bbbk\) is already happily mapped to some vertex from \({\Wintertree}({\mathcal{D}})\).

As the next step, we will satisfy all the queries \({\mathbb{Q}}_i^{\text{\scalebox{0.8}{\exists}}}\) for \(i\neq \Bbbk\). This is easy: just put \(h_i=g_i\) (recall Specification 7 (c)).

Now we need to notice that neither \(h_i(x_i)\) is too close to \(h_j(x_j)\), for some \(i\neq j\), nor any \(h_i(x_i)\) is too close to \(h(x)\). But, as we said above, \(h_\Bbbk(x_\Bbbk)\) is never too close. And in the remaining cases the two variables in question are mapped to two some \(a_i\) and \(a_j\), for \(i\neq j\) and we use Lemma 3. 0◻

This ends the proof of the equivalence \(\bigpumpkin\) and hence also the proof of Theorem 3. Modulo, of course, an implementation of the specifications.

5 Definitions↩︎

In this section we define the objects listed as (i)–(iv) at the beginning of Section 4

5.1 Source of Undecidability↩︎

Our source of undecidability will be, a specially tailored for this occasion, variant of the word problem for finitely generated semigroups⁵.

The following observation can be obtained via a standard reduction from the Turing Machines halting problem. Notice that \(\mathsf{B}\) is the blank symbol, and \(\mathsf{Z}\) and \(\mathsf{Z}'\) are two end-of-the-tape symbols, able to produce any number of blanks. Because of certain technical nuance we need two of them (see the proof of Lemma [lem:krolik]). The pairs from \(\Pi_{22}\) simulate the moves of the machine head. Notice that this means that, if \(\langle \mathsf{C}\mathsf{D},\mathsf{E}\mathsf{F} \rangle \in \Pi_{22}\) then exactly one of the symbols \(\mathsf{D}\), \(\mathsf{F}\) encodes the machine head, and in consequence we indeed have that \(\mathsf{D}\neq \mathsf{F}\).

From now on, we fix an instance \({\mathcal{G}}\) of \({\mathbb{G}}\). Note that this means that \(\mathbb{S}\) is also fixed.

Before we proceed towards definitions of the remaining objects let us recall the following well-known fact:

5.2 Our little bears: definition of queries \(\mathbb{Q}_i\).↩︎

For each name⁶ \(i\in \mathbb{I}\) we shall now define the query \(\mathbb{Q}_i\), with one free variable \(x_i\). Notice that there are four kinds of elements in \(\mathbb{I}\) and for this reason we will consider four cases (see 1 for visualization):

Case \(i={\textcolor{gray}{\vardiamondsuit}}\). Then \(\mathbb{Q}_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}(x_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}) =\)
\(\exists y_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}\!,y_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}'\!, z_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}\; Root(x_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}),\mathsf{L}(x_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}, y_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}), \mathsf{Z}(y_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}},z_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}), \mathsf{R}(x_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}, y_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}'), \mathsf{Z}(y_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}',z_{\vphantom{a}\!{\textcolor{gray}{\vardiamondsuit}}}).\)

Case \(i\in \Pi_{22}\). Then \(i\) is of the form \(\langle \mathsf{C}\mathsf{D},\mathsf{E}\mathsf{F} \rangle\) for some \(\mathsf{C},\mathsf{D},\mathsf{E},\mathsf{F}\in \mathbb{S}_0\), and:
\(\mathbb{Q}_i(x_i) = \exists y_i,y_i', z\;\; \mathsf{C}(x_i, y_i), \mathsf{D}(y_i,z_i), \mathsf{E}(x_i, y_i'), \neg \mathsf{F}(y_i',z_i).\)

Case \(i\in \Pi_{21}\). Then \(i\) is of the form \(\langle \mathsf{B}\mathsf{Y},\mathsf{Y}' \rangle\) for some \(\{\mathsf{Y}, \mathsf{Y}'\}=\{\mathsf{Z},\mathsf{Z}'\}\), and:
\(\mathbb{Q}_i(x_i) = \exists y_i, z_i\;\;\; \mathsf{B}(x_i,y_i), \mathsf{Y}(y_i,z_i),\neg \mathsf{Y}'(x_i,z_i)\)

Case \(i\in \Pi_{12}\). Then \(i\) is of the form \(\langle \mathsf{Y}', \mathsf{B}\mathsf{Y} \rangle\) for some \(\{\mathsf{Y}, \mathsf{Y}'\}=\{\mathsf{Z},\mathsf{Z}'\}\) and:
\(\mathbb{Q}_i(x_i) = \exists y_i, z_i\;\;\; \mathsf{B}(x_i,y_i), \neg \mathsf{Y}(y_i,z_i), \mathsf{Y}'(x,z)\)

We provide visualization for the queries below:

5.3 Specification [spec:4].↩︎

Having the queries \(\mathbb{Q}_i\) defined, for each \(i\in \mathbb{I}\), we need to prove that [spec:4] is indeed satisfied. It is clear that all the defined queries are connected. What remains to be proved are negative (neg) and positive (pos) parts of [spec:4]. This part is analogous to the respective part of the construction in [2]. For the sake of completeness however we present the argument in Appendix A.

5.4 Bears want to sleep. The structures \({\mathbb{A}}_i\).↩︎

Definitions of the structures \({\mathbb{A}}_i\), for \(i\in \mathbb{S}\), are best presented as a figure. From left to right \({\mathbb{A}}_i\) for: (1) \(i = \langle \mathsf{C}\mathsf{D},\mathsf{E}\mathsf{F} \rangle \in \Pi_{22}\), (2) \(i = \langle \mathsf{B}\mathsf{Y}',\mathsf{Y} \rangle \in \Pi_{21}\), (3) \(i = \langle \mathsf{Y}',\mathsf{Y}\mathsf{B} \rangle \in \Pi_{12}\) (for some \(\{\mathsf{Y},\mathsf{Y}'\}=\{\mathsf{Z},\mathsf{Z}'\})\), and (4) \(i = {\textcolor{gray}{\vardiamondsuit}}\). Unlabelled (rainbow) edges indicate the whole set \(\mathbb{S}\); predicate \(Pillow\) is indicated by a rhomboid outline. Notice that 5 is satisfied.

6 Specification 7↩︎

In this section we verify that Specification 7 is indeed satisfied by our queries and structures.

Regarding the conditions (b), (d) and and (f) of 7 there is nothing to prove. Let us now deal with (a):

The (c) of 7 comes next:

6.1 Tall Bears and Their Short Beds.↩︎

The last condition to be verified, from Specification 7, is (e):

Proof: If \(i={\textcolor{gray}{\vardiamondsuit}}\) then \({\mathbb{Q}}_{i}^{\text{\scalebox{0.8}{\exists}}}\) requires that \(Root(f(x_{\textcolor{gray}{\vardiamondsuit}}))\), and there is nothing to prove then, because \(a_{\textcolor{gray}{\vardiamondsuit}}\) is the only vertex in any \({\mathbb{A}}_j\) satisfying this requirement.

So fix \(i\in \Pi\) and \(j\in\mathbb{I}\), and \(f\), as in [lem:last-spec-lemma] and assume, towards contradiction, that \(f(x_i)\neq a_j\). Then, of course:

Let now \(\neg\mathsf{S}(u,z_i)\) be the negative atom in \({\mathbb{Q}}_{i}^{\text{\scalebox{0.8}{\exists}}}\). Notice that \(\mathsf{S}(f(u),d_j)\in{\mathbb{A}}_j\). This is because \(f(u)\neq a_j\), and because whatever \(j\) we took, there is a rainbow edge from each vertex of \({\mathbb{A}}_j\) (except possibly for \(a_j\)) to \(d_j\). We have just proved:

Now we will use the fact that \(f\) maps paths in \(\mathbb{Q}_i\) to paths in \({\mathbb{A}}_j\).

It is very easy to verify that:

Since, as we said, \(f\) maps paths in \(\mathbb{Q}_i\) to paths in \({\mathbb{A}}_j\) we get:

It follows immediately from Observations 13 and 14 that \(i\in \Pi_{12}\) and \(j\in \Pi_{12}\). So let \(i\) be \(\langle \mathsf{Y}', \mathsf{B}\mathsf{Y} \rangle\) and let \(j\) be \(\langle \mathsf{C}\mathsf{D}, \mathsf{E}\mathsf{F} \rangle\). Recall that \(f(z_i) \neq d_j\). Therefore \(f(x_i) = b_j\) and \(f(z_i) = c_j\). But \(\mathsf{Y}'\neq \mathsf{D}\) by definition of \(\Pi\). Contradiction. 0◻

7 Appendix A↩︎

7.1 Negative Part↩︎

We devote the rest of this subsection to the proof of [lem:spec-5-neg]. To this end we first define structure \({\mathfrak D}_0\) over \(\Sigma\).

By definition, we clearly get:

The remaining two conditions require simple proofs:

7.2 Positive Part↩︎

Assume \({\mathcal{G}}\) is positive, and fix a structure \({\mathcal{D}}\) such that \({\mathcal{D}}\models {\mathbb{A}}\) and \({\mathcal{D}}\models {\mathfrak T}\). Consider \({\mathcal{D}}_{\Wintertree}\), and recall that the set of vertices of \({\mathcal{D}}_{\Wintertree}\) is denoted with \({\Wintertree}({\mathcal{D}})\).

We introduce a useful notation for reachability in \({\mathcal{D}}_{\Wintertree}\).

The following lemma is natural:

References↩︎

---

1. We use the mathbb font for the objects that await definition.↩︎

2. We use the mathfrak font for the objects we construct in the reduction: the knowledge base, its elements, and the query.↩︎

3. As you soon will see, \({\mathcal{D}}_{\Wintertree}\) is where undecidability comes from.↩︎

4. The authors are perfectly aware of the fact that koalas are not bears.↩︎

5. This problem is also known as the word problem for Thue systems↩︎

6. We like to think of elements of \(\mathbb{I}\) as names of our bears.↩︎