The Undecidability of FO3 and the Calculus of Relations with Just One Binary Relation

Abstract

The validity problem for first-order logic is a well-known undecidable problem. The undecidability also holds even for $\mathsf {FO}3$ and (equational formulas of) the calculus of relations. In this paper we tighten these undecidability results to the following: (1) $\mathsf {FO}3$ with just one binary relation is undecidable even without equality; and (2) the calculus of relations with just one character and with only composition, union, and complement is undecidable. Additionally we prove that the finite validity problem is also undecidable for the above two classes.

Supported by JSPS KAKENHI Grant Number 16J08119.

1 Introduction

The validity problem for first-order logic (a.k.a. the Entscheidungsproblem) is the problem to decide whether a given formula of first-order logic ($\mathsf {FO}$) is valid or not. The problem is recursively enumerable by Gödel’s completeness theorem [6], but is undecidable shown by Church [4] and Turing [23]. In connection with the undecidability result, many decidable and undecidable variants of $\mathsf {FO}$ are studied (we refer to the book [3]).

One restriction is to consider the validity problem over a restricted signature. In 1915, Löwenheim [12] proved that monadic $\mathsf {FO}$ with equality is decidable (more precisely, $\mathsf {coNEXPTIME}$-complete [11, p. 318]). Monadic $\mathsf {FO}$ is $\mathsf {FO}$ with only unary relation symbols. In 1919, Skolem [19] extended the decidability result to monadic second-order logic (see also [24]). Subsequently Büchi [18] extended the decidability result to monadic second-order logic with the linear order (called $\mathsf {S1S}$). In contrast to this, $\mathsf {FO}$ with just one binary relation symbol is undecidable even without equality. Löwenheim [12] proved the undecidability of $\mathsf {FO}$ with only binary relation symbols, but the number of binary relation symbols is countably infinite. Subsequently the number was reduced to three by Herbrand [8] and to just one by Kalmár [10], see e.g., [3, p. 6] or [2, Theorem 21.4 (The Church-Herbrand theorem)]. Over finite models, $\mathsf {FO}$ with just one binary relation symbol is also undecidable by Trakhtenbrot’s Theorem [22] (moreover, the undecidability holds even over finite graphs of vertex-degree at most 3 [26]).

Another restriction is with respect to the number of variables occurring in formulas. $\mathsf {FO}k$ denotes the restriction of $\mathsf {FO}$ to formulas with at most k distinct variables. In these classes, it is known that $\mathsf {FO}3$ with countably infinitely many binary relation symbols and without equality is undecidable (because the $\forall \exists \forall$ case is undecidable [9]), whereas $\mathsf {FO}2$ (even with equality) is decidable [16] and $\mathsf {coNEXPTIME}$-complete [7, Corollary 5.4]. $\mathsf {FO}2$ has connection with modal logic in the sense of that some propositional modal logics can be embedded into $\mathsf {FO}2$ [25]. With respect to the expressive power of unary relations, $\mathsf {FO}2$ is equivalent to boolean modal logic with relational converse and the identity relation [13]. As for $\mathsf {FO}3$, it has connection with the calculus of (binary) relations [20]. We denote the full signature of the calculus of relations by , where $\varvec{\cdot }$ is relational composition, $\bullet ^-$ is set-theoretic complement, $\cup$ is set-theoretic union, is relational converse, and 1 is the identity relation. Actually, with respect to the expressive power of binary relations, $\mathsf {FO}3$ with equality is equivalent to terms of the calculus of relations [21] (see also [5]).

In this paper we prove that the intersection of the above two restrictions is also undecidable, i.e., the validity problem for $\mathsf {FO}3$ with just one binary relation symbol and without equality is undecidable. Moreover we prove the finite validity problem for the class is undecidable. The class is the minimal undecidable fragment with respect to the above two restrictions since both monadic $\mathsf {FO}$ and $\mathsf {FO}2$ are decidable. As for the calculus of relations, we prove that the validity problem and the finite validity problem for equational formulas of the calculus of relations with just one character over the signature $\langle \varvec{\cdot }, \bullet ^{-}, \cup \rangle$ are undecidable.

Outline

Figure 1 gives the outline of this paper. Every arrow denotes that there is a conservative reduction (a reduction preserving validity and finite validity) from the source to the target and A denotes a countably infinite set. In Sect. 2 we introduce first-order logic and the calculus of relations, and we show that $\mathsf {FO}3$ with equality and the calculus of relations are equivalent in the sense of expressive power of binary relations. In this section we prove that relational converse and the identity relation symbol 1 can be eliminated by using fresh variables preserving validity and finite validity. In Sect. 3 we give reductions for reducing the number of characters to one. Finally, in Sect. 4 we conclude this paper.

Fig. 1.

An overview of reductions

2 $\mathsf {FO}3$ and the Calculus of Relations

Let V be a countably infinite set of (first-order) variables. In this paper we assume that every signature of first-order logic is a set of binary relation symbols. Let A be a set denoting a signature. The set of formulas of first-order logic over A, written $\mathsf {FO}^=_{A}$, is defined by the following grammar (we omit parentheses and we use them in ambiguous situations when it is not clear how to parse):

We use the following abbreviations: (1) $\varphi \mathbin {\varvec{\wedge }}\psi :\equiv \varvec{\lnot }((\varvec{\lnot }\varphi ) \mathbin {\varvec{\vee }}(\varvec{\lnot }\psi ))$; (2) $\varphi \mathbin {\varvec{\rightarrow }}\psi :\equiv (\varvec{\lnot }\varphi ) \mathbin {\varvec{\vee }}\psi$; (3) $\varphi \mathbin {\varvec{\leftrightarrow }}\psi :\equiv (\varphi \mathbin {\varvec{\rightarrow }}\psi ) \mathbin {\varvec{\wedge }}(\psi \mathbin {\varvec{\rightarrow }}\varphi )$; (4) $\forall x. \varphi :\equiv \varvec{\lnot }\varvec{\exists }x. \varvec{\lnot }\varphi$. $\mathsf {FO}_{A}$ denotes the subset of $\mathsf {FO}^=_{A}$ whose formulas do not contain the symbol $=$. $\mathsf {FO}k^=_{A}$ (resp. $\mathsf {FO}k_{A}$) denotes the subset of $\mathsf {FO}^=_{A}$ (resp. $\mathsf {FO}_{A}$) whose formulas contain at most k distinct variables¹. $\mathsf {FO}^=$ denotes the set of all formulas in $\mathsf {FO}^=_{A}$ over a signature A.

A model over A is a tuple $M= \langle |M|, \mathcal {R}_{M}\rangle$, where $|M|$ is a nonempty set; and $\mathcal {R}_{M}:A \rightarrow \wp (|M|^2)$ is a function. Each $\mathcal {R}_{M}(a)$ denotes a binary relation on $|M|$. We may view every model as a graph, e.g., each element of $|M|$ is called a vertex and each element of $\mathcal {R}(a)$ is called an edge labelled with a. An interpretation I on $M$ is a function from V to $|M|$. The semantics of every formula $\varphi$ on $\langle M,I\rangle$ is a truth value. $\langle M,I\rangle \models \varphi$ (resp. $\langle M,I\rangle \not \models \varphi$) denotes that the value of $\varphi$ on $\langle M,I\rangle$ is true (resp. false). $\langle M,I\rangle \models \varphi$ is defined as follows: (1) $\langle M,I\rangle \models a(x,y) \;:\Longleftrightarrow \;\langle I(x),I(y)\rangle \in \mathcal {R}_{M}(a)$ for $a \in A$; (2) $\langle M,I\rangle \models x \mathbin {\varvec{=}}y \;:\Longleftrightarrow \;I(x) = I(y)$; (3) $\langle M,I\rangle \models \varphi \mathbin {\varvec{\vee }}\psi \;:\Longleftrightarrow \;\langle M,I\rangle \models \varphi \text { or } \langle M,I\rangle \models \psi$; (4) $\langle M,I\rangle \models \varvec{\exists }x.\varphi$ $\;:\Longleftrightarrow \;$ there is $v \in |M|$ s.t. $\langle M,[v/x]I\rangle \models \varphi$; (5) $\langle M,I\rangle \models \varvec{\lnot }\varphi \;:\Longleftrightarrow \;\langle M,I\rangle \not \models \varphi$, where [v / x]I denotes the function I in which I(x) has been replaced by the element v. Then the semantics of $\varphi$ on $M$ is defined by $\llbracket \varphi \rrbracket _{M} \mathbin {:=}\{I :V \rightarrow |M| \mid \langle M,I\rangle \models \varphi \}$. $M\models \varphi$ denotes that, for any interpretation I, $\langle M,I\rangle \models \varphi$ holds. $\llbracket \varphi \rrbracket _{M}^{\vec {x}}$ denotes the projection of $\llbracket \varphi \rrbracket _{M}$ with respect to $\vec {x}$, i.e., $\llbracket \varphi \rrbracket _{M}^{\vec {x}} \mathbin {:=}\{\langle I(x_1), \dots , I(x_n)\rangle \mid I \in \llbracket \varphi \rrbracket _{M}\}$, where $\vec {x} = \langle x_1, \dots , x_n\rangle$.

A formula $\varphi$ over the signature A is called valid (resp. finitely valid) if, for any model (resp. finite model) $M$ over A, $M\models \varphi$ holds. The validity problem (resp. the finite validity problem) is the problem to decide whether a given formula is valid (resp. finitely valid). In this paper we rely on the undecidability of the $\varvec{\forall }\varvec{\exists }\varvec{\forall }$ case [9] and modify the result for $\mathsf {FO}3$ and the calculus of relations. This class is a conservative reduction class [3, Definition 2.1.35] (i.e., there is a recursive function from every first-order logic formula over any signature to a formula of the class preserving validity and finite validity). From this, the following holds.

Lemma 1

(A corollary of [3, Theorem 3.1.1]). Let A be any countably infinite set. Then

• The validity problem for $\mathsf {FO}3_{A}$ is undecidable; and

• The finite validity problem for $\mathsf {FO}3_{A}$ is undecidable.

We now define the calculus of relations. Let X be a set and let R and $R'$ be binary relations. The identity relation $\triangle (Y)$ on a set Y is defined as $\{\langle v,v\rangle \mid v \in Y\}$. The relational composition $R \varvec{\cdot }R'$ is defined as $\{\langle v,v'\rangle \mid \exists v''.\langle v,v''\rangle \in R \wedge \langle v'',v'\rangle \in R'\}$. The relational converse is defined as $\{\langle v',v\rangle \mid \langle v,v'\rangle \in R\}$. The union $R \cup R'$ and the complement $R^{-}$ are defined as set-theoretic union and complement (in particular, $R^{-} \mathbin {:=}|X|^2 \setminus R$). Let A be a set of characters. The set of terms over A, written $\mathcal {T}_A$, is defined by the following grammar:

We use the following abbreviations: (1) $t \cap u :\equiv (t^- \cup u^-)^-$; (2) $\top :\equiv a \cup a^-$; (3) $0 :\equiv a \cap a^-$; (4) $t^{n+1} :\equiv t^n \cdot t$ and $t^1 :\equiv t$, where a is some character in A and $n \ge 1$. $\mathcal {T}_A^{\varsigma }$ denotes the set of terms over A and over the signature $\varsigma$, where $\varsigma$ is a subset of . Note that the symbols, and 1, are not used in these abbreviations.

Let $M$ be a model over A. The semantics of every term t on $M$, written $\llbracket t\rrbracket _{M}$, is a binary relation on $|M|$, defined as follows: (1) $\llbracket a\rrbracket _{M} \mathbin {:=}\mathcal {R}_{M}(a)$; (2) $\llbracket t \cdot u\rrbracket _{M} \mathbin {:=}\llbracket t\rrbracket _{M} \varvec{\cdot }\llbracket u\rrbracket _{M}$; (3) $\llbracket t^{-}\rrbracket _{M} \mathbin {:=}|M|^2 \setminus \llbracket t\rrbracket _{M}$; (4) $\llbracket t \cup u\rrbracket _{M} \mathbin {:=}\llbracket t\rrbracket _{M} \cup \llbracket u\rrbracket _{M}$; (5) ; (6) $\llbracket 1\rrbracket _{M} \mathbin {:=}\triangle (|M|)$. Note that $\llbracket t \cap u\rrbracket _{M} = \llbracket t\rrbracket _{M} \cap \llbracket u\rrbracket _{M}$, $\llbracket \top \rrbracket _{M} = |M|^2$, and $\llbracket 0\rrbracket _{M} = \varnothing$ hold. We also define the set of formulas of the calculus of the relations over a set $\mathcal {T}$, written $\Phi [\mathcal {T}]$, by the following grammar:

where $\mathcal {T}$ is a set of terms. The semantics of every formula $\varphi \in \Phi [\mathcal {T}]$ on $M$ is a truth value. $M\models \varphi$ (resp. $M\not \models \varphi$) denotes that the value of $\varphi$ on $M$ is true (resp. false) defined as follows: (1) $M\models t \mathbin {\varvec{=}}u \;:\Longleftrightarrow \;\llbracket t\rrbracket _{M} = \llbracket u\rrbracket _{M}$; (2) $M\models \varphi \mathbin {\varvec{\vee }}\psi \;:\Longleftrightarrow \;M\models \varphi \text { or } M\models \psi$; (3) $M\models \varvec{\lnot }\varphi \;:\Longleftrightarrow \;M\not \models \varphi$. A formula of the form $t \mathbin {\varvec{=}}u$ is called an equational formula. We denote the set of equational formulas over a set $\mathcal {T}$ by $\mathrm {Eq}[\mathcal {T}]$. Actually every formula is equivalent to an equational formula by the following lemma.

Lemma 2

(cf. [14, Theorem 1]). For any formula $\varphi$ in $\Phi [\mathcal {T}_{A}]$, there is an equational formula $\psi$ of the form $t \mathbin {\varvec{=}}0$ in $\mathrm {Eq}[\mathcal {T}_{A}]$ s.t. for any $M$ over A, $M\models \varphi \iff M\models \psi$.

Proof

(Sketch). It is proved by using the following equivalences: (1) $M\models t \mathbin {\varvec{=}}u \iff M\models (t \cap u^-) \cup (t^- \cap u) \mathbin {\varvec{=}}0$; (2) $M\models (t \mathbin {\varvec{=}}0) \mathbin {\varvec{\vee }}(u \mathbin {\varvec{=}}0) \iff M\models t \cdot \top \cdot u \mathbin {\varvec{=}}0$; (3) $M\models \lnot (t \mathbin {\varvec{=}}0) \iff M\models (\top \cdot t \cdot \top )^- \mathbin {\varvec{=}}0$.

By Lemma 2, every formula of the calculus of relations can be translated to an equational formula preserving validity and finite validity. For simplicity, we may use formulas of the calculus of relations (but it is not essential). Note that the symbols, and 1, are not used in the translation in Lemma 2.

$\mathsf {FO}3^=$ and the calculus of relations are equivalent in the sense of expressive power of binary relations. We use [n] to denote the set $\{1,\dots , n\}$ for every natural number $n \ge 0$. The following lemma shows that every term of the calculus of relations has an equivalent $\mathsf {FO}3^=$ formula.

Lemma 3

(e.g., [21, p. 28][5]). Let $x_1$, $x_2$, and $x_3$ are three distinct variables. There is a recursive function G from $\mathcal {T}_A \times [3]^2$ to $\mathsf {FO}3^=_{A}$ s.t., for any $\langle t,i,j\rangle$ and any model $M$ over A, $\llbracket t\rrbracket _{M} = \llbracket G(t,i,j)\rrbracket _{M}^{x_i,x_j}$ holds.

Proof

(Sketch). We define G(t, i, j) as follows: (1) $G(a, i, j) \mathbin {:=}a(x_i, x_j)$; (2) $G(t \cdot u, i, j) \mathbin {:=}\varvec{\exists }k. G(t, i, k) \mathbin {\varvec{\wedge }}G(u, k, j)$; (3) $G(t^-, i, j) \mathbin {:=}\varvec{\lnot }G(t, i, j)$; (4) $G(t \cup u, i, j) \mathbin {:=}G(t, i, j) \mathbin {\varvec{\vee }}G(u, i, j)$; (5) ; (6) $G(1, i, j) \mathbin {:=}x_i \mathbin {\varvec{=}}x_j$, where k is the minimum element in $[3] \setminus \{i, j\}$. Then $\llbracket t\rrbracket _{M} = \llbracket G(t,x_i,x_j)\rrbracket _{M}^{x_i, x_j}$ is proved by induction on the structure of t.

Actually the converse of Lemma 3 also holds, i.e., $\mathsf {FO}3^=$ and the calculus of relations are equivalent in the sense of expressive power of binary relations.

Lemma 4

(e.g., [21, Sect. 3.9][5]). There is a recursive function H from $\mathsf {FO}3^=_{A} \times V^2$ to $\mathcal {T}_A$ s.t., for any $\langle \varphi , v, w\rangle$ and any model $M$ over A, $\llbracket \varphi \rrbracket _{M}^{v,w} = \llbracket H(\varphi ,v,w)\rrbracket _{M}$.

By Lemmas 3 and 4, every equational formula of the calculus of relations can be translated to an $\mathsf {FO}3$ sentence, and vice versa, by the following:

where x is an arbitrary variable. Therefore the following also holds.

Lemma 5

Let A be any countably infinite set. Then both the validity problem and the finite validity problem for are undecidable.

2.1 Elimination of Relational Converse (Using the Identity Relation)

In this subsection, we show that relational converse can be eliminated by using fresh variables preserving validity and finite validity (Lemma 7). Let $\breve{A}$ be a countably infinite set that is disjoint with A. We use $\breve{a}$ to denote the character in $\breve{A}$ denoting the converse of the character a in A. The following two axioms force that $\breve{a}$ is the converse of a: ($\mathrm {C}{a}.1$) ; and ($\mathrm {C}{a}.2$) $(\breve{a} \cdot a^{-}) \cap 1 \mathbin {\varvec{=}}0$.

denotes the formula $(\mathrm {C}{a}.\mathrm {1}) \mathbin {\varvec{\wedge }}(\mathrm {C}{a}.\mathrm {2})$. In fact the following holds.

Proposition 6

For any model $M$ over the alphabet $A \cup \breve{A}$, the following hold: (1) ; (2) ; (3) ; (4) ; (5) ; (6) .

Proof

(2)–(6) are easily proved by the definition of $\llbracket t\rrbracket _{M}$. We only prove (1). ($\Rightarrow$): We assume that there is a pair $\langle v,w\rangle$ such that . Then, by $\langle w,v\rangle \in \llbracket a\rrbracket _{M}$ and $\langle v,w\rangle \in \llbracket \breve{a}^-\rrbracket _{M}$, $\langle w,w\rangle \in \llbracket (a \cdot \breve{a}^-) \cap 1\rrbracket _{M}$. However this contradicts to ($\mathrm {C}{a}.1$). Therefore . We assume that there is a pair $\langle v,w\rangle$ such that . Then, by $\langle v,w\rangle \in \llbracket \breve{a}\rrbracket _{M}$ and $\langle w,v\rangle \in \llbracket a^-\rrbracket _{M}$, $\langle v,v\rangle \in \llbracket (\breve{a} \cdot a^-) \cap 1\rrbracket _{M}$. However this contradicts to ($\mathrm {C}{a}.2$). Therefore , and thus . ($\Leftarrow$): We prove the contraposition. If $M\not \models (\mathrm {C}{a}.1)$, there are v and w such that $\langle v,w\rangle \in \llbracket a\rrbracket _{M}$ and $\langle w,v\rangle \in \llbracket \breve{a}^-\rrbracket _{M}$. Then by and $\langle w,v\rangle \not \in \llbracket \breve{a}\rrbracket _{M}$, . If $M\not \models (\mathrm {C}{a}.2)$, there are v and w such that $\langle v,w\rangle \in \llbracket \breve{a}\rrbracket _{M}$ and $\langle w,v\rangle \in \llbracket a^-\rrbracket _{M}$. Then by and $\langle v,w\rangle \in \llbracket \breve{a}\rrbracket _{M}$, .     $\square$

Let $\mathrm {CF}(t)$ be the normal form of a term t w.r.t. the following rewriting rule: (1) ; (2) ; (3) ; (4) ; (5) ; (6) . Note that, for any term t, $\mathrm {CF}(t)$ does not contain . We use $A_{\varphi }$ to denote the finite set of all characters occurring in $\varphi$.

Lemma 7

For any $t, u \in \mathcal {T}_{A}$, the following are equivalent: (1) $t \mathbin {\varvec{=}}u$ is valid (resp. finitely valid). (2) is valid (resp. finitely valid).

Proof

(2) $\Rightarrow$ (1): Let $M$ be a model over A such that $M\not \models t \mathbin {\varvec{=}}u$. We define the model $M'$ over $A \cup \breve{A}$ by $M' = (|M|,\mathcal {R}')$, where $\mathcal {R}'(a) = \mathcal {R}_{M}(a)$ for $a \in A$; and for $\breve{a} \in \breve{A}$. Then holds by Proposition 6 (1). Moreover, for any term $t \in \mathcal {T}_A$, $\llbracket t\rrbracket _{M} = \llbracket \mathrm {CF}(t)\rrbracket _{M'}$ holds by using Proposition 6. Therefore $M' \not \models \mathrm {CF}(t) \mathbin {\varvec{=}}\mathrm {CF}(u)$. (1) $\Rightarrow$ (2): Let $M$ be a model over A such that holds, but $M\not \models \mathrm {CF}(t) \mathbin {\varvec{=}}\mathrm {CF}(u)$. Then $\llbracket t\rrbracket _{M} = \llbracket \mathrm {CF}(t)\rrbracket _{M}$ holds for any term $t \in \mathcal {T}_A$ by using Proposition 6, and thus $M\not \models t = u$.     $\square$

By Lemma 2, Each formula can be translated to an equational formula without .

2.2 Elimination of the Identity Relation

In this subsection, we also eliminate the identity relation symbol 1 by using a fresh variable E. The key is to construct an equivalence relation denoting the identity relation not using 1 or . Let consider the following axioms: (${\mathrm {E}}.1$) $E \cdot \top \mathbin {\varvec{=}}\top$; (${\mathrm {E}}.2$) $(E^- \cdot E) \cap E \mathbin {\varvec{=}}0$; (${\mathrm {E}}.3$) $(E \cdot E^-) \cap E \mathbin {\varvec{=}}0$; and (${\mathrm {E}}.4$) $(E \cdot E) \cap E^- \mathbin {\varvec{=}}0$.

denotes the formula $(\mathrm {E}.\mathrm {1}) \mathbin {\varvec{\wedge }}\dots \mathbin {\varvec{\wedge }}(\mathrm {E}.\mathrm {4})$.

Proposition 8

$\iff$ $\llbracket E\rrbracket _{M}$ is an equivalence relation on $|M|$.

Proof

($\Leftarrow$): (E.1) is by the reflexivity. (E.4) is by the transitivity. (E.2) and (E.3) are by the symmetry and the transitivity. ($\Rightarrow$): The reflexivity is shown by (E.1) and (E.2). Let v be any vertex in $|M|$. Then let w be a vertex such that $\langle v,w\rangle \in \llbracket E\rrbracket _{M}$ holds (such w always exists by (E.1)). We assume that $\langle v,v\rangle \not \in \llbracket E\rrbracket _{M}$. Then, by $\langle v,v\rangle \in \llbracket E^-\rrbracket _{M}$, $\langle v,w\rangle \in \llbracket (E^- \cdot E) \cap E\rrbracket _{M}$ holds. However this contradicts to (E.2). Therefore $\langle v,v\rangle \in \llbracket E\rrbracket _{M}$. The symmetry is by the reflexivity and (E.3). Let $\langle v,w\rangle \in \llbracket E\rrbracket _{M}$. We assume $\langle w,v\rangle \not \in \llbracket E\rrbracket _{M}$. Then $\langle v,v\rangle \in \llbracket (E \cdot E^-) \cap E\rrbracket _{M}$ by the reflexivity. However this contradicts to (E.3). Therefore $\langle w,v\rangle \in \llbracket E\rrbracket _{M}$. The transitivity is by (E.4).     $\square$

For every term t, the term $\mathrm {IF}(t)$ is inductively defined as follows:(1) $\mathrm {IF}(a) \mathbin {:=}E \cdot a \cdot E$; (2) $\mathrm {IF}(t \cdot u) \mathbin {:=}\mathrm {IF}(t) \cdot \mathrm {IF}(u)$; (3) $\mathrm {IF}(t^-) \mathbin {:=}\mathrm {IF}(t)^-$; (4) $\mathrm {IF}(t \cup u) \mathbin {:=}\mathrm {IF}(t) \cup \mathrm {IF}(u)$; (5) ; (6) $\mathrm {IF}(1) \mathbin {:=}E$. Note that (i) $\mathrm {IF}(t)$ does not contain the symbol 1; and (ii) if t does not contain , then $\mathrm {IF}(t)$ also does not contain .

Lemma 9

For any , The following are equivalent: (1) $t \mathbin {\varvec{=}}u$ is valid (resp. finitely valid). (2) is valid (resp. finitely valid).

Proof

(2) $\Rightarrow$ (1): Let $M$ be a model over A such that $M\not \models t \mathbin {\varvec{=}}u$. We define the model $M'$ over $A \cup \{E\}$ by $M' \mathbin {:=}(|M|,\mathcal {R}')$, where $\mathcal {R}'(a) = \mathcal {R}_{M}(a)$ for $a \in A$ and $\mathcal {R}'(E) = \triangle (|M|)$. Then holds because $\llbracket E\rrbracket _{M'}$ is an equivalence relation. Also $M' \not \models \mathrm {IF}(t) \mathbin {\varvec{=}}\mathrm {IF}(u)$ holds because $\llbracket t\rrbracket _{M} = \llbracket \mathrm {IF}(t)\rrbracket _{M'}$ holds by the definition of $M'$. (1) $\Rightarrow$ (2): Let $M$ be a model over $A \cup \{E\}$ such that holds, but $M\not \models \mathrm {IF}(t) \mathbin {\varvec{=}}\mathrm {IF}(u)$. We define the model $M'$ over A by $M' \mathbin {:=}(|M|/{E},\mathcal {R}')$, where $|M|/{E}$ is the quotient set of $|M|$ by E; $[v]_E$ denotes the equivalence class of an element v with respect to E; and $\mathcal {R}'(a) = \{\langle [v]_{E},[w]_{E}\rangle \mid \langle v,w\rangle \in \mathcal {R}_{M}(a)\}$ for $a \in A$. Then $\{\langle [v]_{E},[w]_{E}\rangle \mid \langle v,w\rangle \in \llbracket \mathrm {IF}(t)\rrbracket _{M}\} = \llbracket t\rrbracket _{M'}$ holds for any term t. This is proved by induction on the structure of t. Therefore $M' \not \models t \mathbin {\varvec{=}}u$.     $\square$

We can eliminate both converse and the identity relation preserving validity and finite validity by Lemmas 7 and 9. Therefore the following holds.

Corollary 10

Let A be a countably infinite set. Then both the validity problem and the finite validity problem for $\mathrm {Eq}[\mathcal {T}_{A}^{\langle \cdot , \bullet ^-, \cup \rangle }]$ are undecidable.

3 Reductions to the One Binary Relation Case

In this section we consider to reduce the number of characters. Let A be an ordered set $\{a_1, a_2, \dots \}$. Without loss of generality, we can assume that every term is in $\mathcal {T}_{A}^{\langle \cdot , \bullet ^-, \cup \rangle }$ by Corollary 10. In this section we give two reductions to the one binary relation case. First we give a simple reduction, but this reduction uses the identity relation. The second reduction is a bit more complex than the first reduction, but the reduction does not use the identity relation.

3.1 A Conservative Reduction Using Identity

We first give a reduction $\mathrm {T}_1$ from $\mathcal {T}_{A}^{\langle \cdot , \bullet ^-, \cup , 1\rangle }$ to $\mathcal {T}_{\{a\}}^{\langle \cdot , \bullet ^-, \cup , 1\rangle }$. The term $\mathrm {T}_1(t)$ is inductively defined as follows: (1) $\mathrm {T}_1(a_i) \mathbin {:=}(a \cap 1) \cdot a \cdot ((a^- \cap 1) \cdot a)^{i} \cdot (a \cap 1)$; (2) $\mathrm {T}_1(t \cdot u) \mathbin {:=}\mathrm {T}_1(t) \cdot \mathrm {T}_1(u)$; (3) $\mathrm {T}_1(t^-) \mathbin {:=}(a \cap 1) \cdot \mathrm {T}_1(t)^- \cdot (a \cap 1)$; (4) $\mathrm {T}_1(t \cup u) \mathbin {:=}\mathrm {T}_1(t) \cup \mathrm {T}_1(u)$; (5) $\mathrm {T}_1(1) \mathbin {:=}(a \cap 1)$.

Figure 2 is an example of transforming from models over A to models over $\{a\}$ in Lemma 11. Each blue (resp. red, gray) colored edge denotes an edge labeled with $a_1$ (resp. $a_2$, a).

Fig. 2.

A transformation to the one binary relation case using identity (Color figure online)

Lemma 11

For any $t, u \in \mathcal {T}_{A}^{\langle \cdot , \bullet ^-, \cup , 1\rangle }$, The following are equivalent: (1) $t \mathbin {\varvec{=}}u$ is valid (resp. finitely valid). (2) $\mathrm {T}_1(t) \mathbin {\varvec{=}}\mathrm {T}_1(u)$ is valid (resp. finitely valid).

Proof

(2) $\Rightarrow$ (1): Let $M$ be a model over $A_{t \mathbin {\varvec{=}}u}$ such that $M\not \models t \mathbin {\varvec{=}}u$. We define the model $M'$ over $\{a\}$ by $M' \mathbin {:=}\langle |M'|,\mathcal {R}'\rangle$, where $|M'| \mathbin {:=}|M| \cup \{\langle v,w,i,j\rangle \mid \langle v,w\rangle \in \mathcal {R}_{M}(a_i), j \in [i] \}$ and $\mathcal {R}'(a) \mathbin {:=}\triangle (|M|) \cup \{\langle v,\langle v,w,i,1\rangle \rangle ,\langle \langle v,w,i,i\rangle ,w\rangle \mid \langle v,w\rangle \in \mathcal {R}_{M}(a_i)\} \cup \{\langle \langle v,w,i,j\rangle ,\langle v,w,i,j+1\rangle \rangle \mid \langle v,w\rangle \in \mathcal {R}_{M}(a_i), j \in [i-1] \}$. The right-hand side in Fig. 2 is an example of $M'$. Note that if $M$ is finite, $M'$ is also finite because $A_{t \mathbin {\varvec{=}}u}$ is finite. Then $\llbracket t\rrbracket _{M} = \llbracket \mathrm {T}_1(t)\rrbracket _{M'}$ holds. This is easily proved by induction on the structure of t. Therefore $M' \not \models \mathrm {T}_1(t) \mathbin {\varvec{=}}\mathrm {T}_1(u)$. (1) $\Rightarrow$ (2): Let $M$ be a model over $\{a\}$ such that $M\not \models \mathrm {T}_1(t) \mathbin {\varvec{=}}\mathrm {T}_1(u)$. Then we define the model $M'$ over A by $M' \mathbin {:=}\langle |M'|, \mathcal {R}'\rangle$, where $|M'| \mathbin {:=}\{v \mid \langle v,v\rangle \in \llbracket a\rrbracket _{M}\}$ and $\mathcal {R}'(a_i) \mathbin {:=}|M'|^2 \cap \llbracket \mathrm {T}_1(a_i)\rrbracket _{M}$. Then $\llbracket t\rrbracket _{M'} = \llbracket \mathrm {T}_1(t)\rrbracket _{M}$ holds. This is easily proved by induction on the structure of t. Therefore $M' \not \models t \mathbin {\varvec{=}}u$.     $\square$

By the above lemma, the following has been proved.

Theorem 12

Let a be a character. Then both the validity problem and the finite validity problem for $\mathrm {Eq}[\mathcal {T}_{\{a\}}^{\langle \cdot , \bullet ^-, \cup , 1\rangle }]$ are undecidable.

Remark 13

The undecidability of the validity problem for the calculus of relations with just one character over the signature had been shown by Maddux [15, p. 399]. More strongly, Theorem 12 shows that the validity problem is undecidable even without and shows that the finite validity problem is also undecidable. Furthermore, Theorem 12 will be strengthened to Theorem 17.

Combining Theorem 12 and Lemma 9, the following is also proved.

Corollary 14

Let $a_1, a_2$ be two distinct characters. Then both the validity problem and the finite validity problem for $\mathrm {Eq}[\mathcal {T}_{\{a_1,a_2\}}^{\langle \cdot , \bullet ^-, \cup \rangle }]$ are undecidable.

3.2 A Conservative Reduction Not Using Identity

In this subsection we give another reduction, which is not using the identity relation and relational converse. The key is how to distinguish the vertices of a given model and the other vertices on the transformed model, not relying on the identity relation. Without loss of generality we can assume that the size of character is 2 by Corollary 14. Now we consider the following axioms: ($\mathrm {Ax}.1$) $(a \cap a^2) \cdot \top \mathbin {\varvec{=}}(a \cap a^2) \cdot (a \cap a^3) \cdot \top$; and ($\mathrm {Ax}.2$) $\top \cdot (a \cap a^3) \mathbin {\varvec{=}}\top \cdot (a \cap a^2) \cdot (a \cap a^3)$. denotes the formula $(\mathrm {Ax.1}) \mathbin {\varvec{\wedge }}(\mathrm {Ax.2})$. These axioms are used to force ${\text {cod}}(\llbracket a \cap a^2\rrbracket _{M}) = {\text {dom}}(\llbracket a \cap a^3\rrbracket _{M})$, where ${\text {dom}}(R)$ (resp. ${\text {cod}}(R)$) denote the domain (resp. codomain) of a binary relation R, i.e., ${\text {dom}}(R) \mathbin {:=}\{v \mid \exists w.\langle v,w\rangle \in R\}$ and ${\text {cod}}(R) \mathbin {:=}\{w \mid \exists v.\langle v,w\rangle \in R\}$. In fact the following holds.

Proposition 15

$\iff$ ${\text {cod}}(\llbracket a \cap a^2\rrbracket _{M}) = {\text {dom}}(\llbracket a \cap a^3\rrbracket _{M})$.

Proof

By $M\models (\mathrm {Ax.1}) \iff {\text {cod}}(\llbracket a \cap a^2\rrbracket _{M}) \subseteq {\text {dom}}(\llbracket a \cap a^3\rrbracket _{M})$ and $M\models (\mathrm {Ax.2}) \iff {\text {cod}}(\llbracket a \cap a^2\rrbracket _{M}) \supseteq {\text {dom}}(\llbracket a \cap a^3\rrbracket _{M})$.     $\square$

We define a reduction $\mathrm {T}_2$ from $\mathcal {T}_{\{a_1,a_2\}}^{\langle \cdot , \bullet ^-, \cup \rangle }$ to $\mathcal {T}_{\{a\}}^{\langle \cdot , \bullet ^-, \cup \rangle }$ as follows: (1) $\mathrm {T}_2(a_i) \mathbin {:=}(a \cap a^3) \cdot a^{i+1} \cdot (a \cap a^2)$; (2) $\mathrm {T}_2(t \cdot u) \mathbin {:=}\mathrm {T}_2(t) \cdot \mathrm {T}_2(u)$; (3) $\mathrm {T}_2(t^-) \mathbin {:=}((a \cap a^3) \cdot \top ) \cap (\top \cdot (a \cap a^2)) \cap \mathrm {T}_2(t)^-$; (4) $\mathrm {T}_2(t \cup u) \mathbin {:=}\mathrm {T}_2(t) \cup \mathrm {T}_2(u)$. Intuitively, both the codomain of $a \cap a^2$ and the domain of $a \cap a^3$ denote the set of vertices in the pre-transformed model in the above reduction.

Figure 3 is an example of transforming models over $\{a_1,a_2\}$ to models over $\{a\}$ in Lemma 16. Each blue (resp. red, gray) colored edge denotes an edge labeled with $a_1$ (resp. $a_2$, a).

Fig. 3.

A transformation to the one binary relation case not using identity (Color figure online)

Lemma 16

For any $t, u \in \mathcal {T}_{\{a_1,a_2\}}^{\langle \cdot , \bullet ^-, \cup \rangle }$, the following are equivalent: (1) $t \mathbin {\varvec{=}}u$ is valid (resp. finitely valid). (2) is valid (resp. finitely valid).

Proof

(2) $\Rightarrow$ (1): Let $M$ be a model over $\{a_1,a_2\}$ such that $M\not \models t \mathbin {\varvec{=}}u$. We define the model $M'$ over $\{a\}$ by $M' \mathbin {:=}\langle |M'|,\mathcal {R}'\rangle$, where $|M'| \mathbin {:=}(|M| \times [6]) \cup \{\langle v,w,i,j\rangle \mid \langle v,w\rangle \in \mathcal {R}_{M}(a_i), j \in [i] \}$ and $\mathcal {R}'(a)$ is the union of the following:

• (i) $\bigcup _{v \in |M|} (\{\langle \langle v,i\rangle ,\langle v,i+1\rangle \rangle \mid i \in [5]\} \cup \{\langle \langle v,1\rangle ,\langle v,3\rangle \rangle ,\langle \langle v,3\rangle ,\langle v,6\rangle \rangle \})$;

• (ii) $\bigcup _{i \in \{1,2\}} \{\langle v,\langle v,w,i,1\rangle \rangle ,\langle \langle v,w,i,i\rangle ,w\rangle \mid (v,w) \in \mathcal {R}_{M}(a_i)\})$; and

• (iii) $\{\langle \langle v,w,2,1\rangle ,\langle v,w,2,2\rangle \rangle \mid (v,w) \in \mathcal {R}_{M}(a_2)\}$.

The right-hand side in Fig. 3 is an example of $M'$.

First holds by ${\text {cod}}(\llbracket a \cap a^2\rrbracket _{M'}) = \{\langle v,3\rangle \mid v \in |M|\} = {\text {dom}}(\llbracket a \cap a^3\rrbracket _{M'})$. Moreover the following holds: $\{\langle \langle v,3\rangle , \langle w,3\rangle \rangle \mid (v,w) \in \llbracket t\rrbracket _{M} \} = \llbracket \mathrm {T}_2(t)\rrbracket _{M'}$ $\cdots$ ($\heartsuit$). $M' \not \models \mathrm {T}_2(t) \mathbin {\varvec{=}}\mathrm {T}_2(u)$ is proved by ($\heartsuit$). We prove ($\heartsuit$) by induction on t.

If $t \equiv a_i$, let $\langle v,w\rangle$ be a pair such that $\langle v,w\rangle \in \llbracket a_i\rrbracket _{M}$. Then $\langle \langle v,3\rangle ,\langle w,3\rangle \rangle \in \llbracket (a \cap a^3) \cdot a^{i+1} \cdot (a \cap a^2)\rrbracket _{M'}$ is easily checked. Conversely, if $\langle v,w\rangle \in \llbracket (a \cap a^3) \cdot a^{i+1} \cdot (a \cap a^2)\rrbracket _{M'}$, then then there are $v',w'\in |M|$ such that $\langle v,w\rangle = \langle \langle v',3\rangle ,\langle w',3\rangle \rangle$ by ${\text {cod}}(\llbracket a \cap a^2\rrbracket _{M'}) = {\text {dom}}(\llbracket a \cap a^3\rrbracket _{M'}) = \{\langle v,3\rangle \mid v \in |M|\}$. Then $\{v \mid \langle \langle v',3\rangle , v\rangle \in \llbracket a \cap a^3\rrbracket _{M'}\} = \{\langle v',6\rangle \}$ and $\{w \mid \langle w,\langle w',3\rangle \rangle \in \llbracket a \cap a^2\rrbracket _{M'}\} = \{\langle w',1\rangle \}$ hold, and thus $\langle \langle v',6\rangle ,\langle w',1\rangle \rangle \in \llbracket a^{i+1}\rrbracket _{M'}$. If we assume $\langle v',w'\rangle \not \in \llbracket a_i\rrbracket _{M}$, then $\langle w',1\rangle$ is not reachable from $\langle v',6\rangle$ in $i + 1$ steps because $i + 1 \le 3$ and the length of paths from $\langle v',6\rangle$ to $\langle w',1\rangle$ via some $\langle w'',1\rangle$ is at least 6, where $w''$ is an element in $|M|$ not equal to $w'$. (More concretely, the following path is the shortest path from $\langle v',6\rangle$ to $\langle w',1\rangle$ via $\langle w'',1\rangle$: $\langle v',6\rangle \leadsto \langle v',w'',1, 1\rangle \leadsto \langle w'',1\rangle \leadsto \langle w'',3\rangle \leadsto \langle w'',6\rangle \leadsto \langle w'',w',1, 1\rangle \leadsto \langle w',1\rangle$.) However this contradicts to $\langle \langle v',6\rangle ,\langle w',1\rangle \rangle \in \llbracket a^{i+1}\rrbracket _{M'}$. Therefore $\langle v',w'\rangle \in \llbracket a_i\rrbracket _{M}$.

If $t \equiv t \cdot u$:

If $t \equiv t^-$:

If $t \equiv t \cup u$:

(1) $\Rightarrow$ (2): Let $M$ be a model over $\{a\}$ such that , but $M\not \models \mathrm {T}_2(t) \mathbin {\varvec{=}}\mathrm {T}_2(u)$. Then we define the model $M$ over A by $M' \mathbin {:=}\langle |M'|, \mathcal {R}'\rangle$, where $|M'| \mathbin {:=}{\text {dom}}(\llbracket a \cap a^3\rrbracket _{M})$ and $\mathcal {R}'(a_i) \mathbin {:=}\llbracket \mathrm {T}_2(a_i)\rrbracket _{M}$. Note that $\mathcal {R}'(a_i) \subseteq |M'|^2$ holds because ${\text {dom}}(\llbracket a \cap a^3\rrbracket _{M}) = {\text {cod}}(\llbracket a \cap a^2\rrbracket _{M})$ by Proposition 15. Then the following holds: $\llbracket t\rrbracket _{M'} = \llbracket \mathrm {T}_2(t)\rrbracket _{M}$ $\cdots$ ($\heartsuit$). $M' \not \models t \mathbin {\varvec{=}}u$ is proved by ($\heartsuit$). We now prove ($\heartsuit$) by induction on the structure of t.

If $t \equiv a_i$, $\llbracket a_i\rrbracket _{M'} = \llbracket \mathrm {T}_2(a_i)\rrbracket _{M}$ is shown by the definition of $M'$.

If $t \equiv t \cdot u$,

If $t \equiv t^-$,

If $t \equiv t \cup u$,

    $\square$

By Lemma 16, the next theorem has been proved.

Theorem 17

Let a be a character. Then both the validity problem and the finite validity problem for $\mathrm {Eq}[\mathcal {T}_{\{a\}}^{\langle \cdot , \bullet ^-, \cup \rangle }]$ are undecidable.

Combining Theorem 17 and Lemma 3, the following is also proved. Note that, if a term t does not contain 1, the formula G(t, i, j) does not contain $=$.

Theorem 18

Let a be a character. Then both the validity problem and the finite validity problem for $\mathsf {FO}3_{\{a\}}$ are undecidable.

4 Conclusion

In this paper we showed that the validity problem and the finite validity problem are undecidable for the following classes: (1) $\mathsf {FO}3$ with just one binary relation symbol and without equality; and (2) equational formulas of the calculus of relations with just one character over the signature $\langle \cdot ,\bullet ^-,\cup \rangle$. In connection with (2), the following decidable fragments are known.

Theorem 19

([1, Theorem 5] for (1)). The validity problem and the finite validity problem are decidable for the following classes: (1) the calculus of relations over the signature $\langle \cdot ,\cup \rangle$ (even with , and atomic negation); and (2) the calculus of relations over the signature $\langle \bullet ^-,\cup \rangle$ (even with ).

These decidability results are proved by the reduction to $\mathsf {FO}3$ (Lemma 3) and using the decidability of the satisfiability problem and the finite model property of the $\varvec{\exists }^* \varvec{\forall }^*$ case with equality (proved by Ramsey [17] in 1930, see also [3, Sect. 6.2.2]). To the best of our knowledge, the (un)decidability of the validity problem and the finite validity problem for equational formulas of the calculus of relations over the signature $\langle \cdot , \bullet ^{-}\rangle$ are open regardless of the number of characters.