Modeling reachability using entailment

Reachability in graphs can be modeled using entailment in first-order logic.

Let $G = \langle V_G, E_G\rangle$ be a directed graph, that is, $E_G \subseteq V_G \times V_G$. Let $v_0 \in V$. The reachability relation is defined inductively. It is the smallest binary relation over $V$ satisfying:

• $v_0$ belongs to this set,
• if $\langle v,v' \rangle \in E$ and $\langle v', v' '\rangle$ belongs to this set, then $\langle v, v' '\rangle \in E$ belongs to this set. This relation is denoted $R_G$.

There are two negative results on the reachability relation with regard to modeling it:

Theorem

1. Let $\mathcal S = \{E/2\}$. The reachability relation $R_G$ is not (!) definable in $\mathcal S$.
2. Let $\mathcal S = \{E/2, R/2\}$. The class of $\mathcal S$-structures $\mathcal A$ where $R^\mathcal A$ is the reachability relation for $E^\mathcal A$ is not (!) axiomatizable.

The positive result is that it can be modeled using entailment.

For a given graph as above, consider the set $\Phi_G$ of first-order formulas defined by \begin{align} \Phi_G & = \Psi_G \cup \Phi_R\enspace,\\ \Psi_G & = \{\dot E(v,v') \colon \langle v,v'\rangle \in E_G\}\enspace,\\ \Phi_R & = \{\forall x_0 R(x_0,x_0), \forall x_0 \forall x_1 \forall x_2 (E(x_0, x_1) \wedge R(x_1,x_2) \rightarrow R(x_0,x_2))\} \enspace. \end{align} Clearly, the signature is $V \cup \{E/2, R/2\}$.

Theorem For every graph $G$ and vertices $v,v' \in V_G$, the following are equivalent:

1. $\langle v,v'\rangle \in R_G$.
2. $\Phi_G \models R(v,v')$.

Proof For the implication from 1. to 2., let $\mathcal G$ be any structure such that $\mathcal G \mymodels \Phi_G$. What we show is that $\{\langle v^\mathcal G, {v'}^\mathcal G\rangle \colon \langle v,v'\rangle \in R_G \} \subseteq R^\mathcal G$, which is enough. To this end, we only need to show that $R^\mathcal G$ satisfies the two conditions from the inductive definition.

First, let $v \in V_G$. According to the semantics of first-order logic, we have $\langle v^\mathcal G, v^\mathcal G\rangle \in R^\mathcal G$ because of $\mathcal G \mymodels \forall x_0 R(x_0, x_0)$.

Second, let $v, v', v' ' \in V_G$ and assume $\langle v,v'\rangle \in E_G$ and $\langle v', v' ' \rangle \in R^\mathcal G$. From $\mathcal G \mymodels \Psi_E$ we obtain $\langle v,v' \rangle \in E^G$. From $\mathcal G \mymodels \forall x_0 \forall x_1 \forall x_2 (E(x_0,x_1) \wedge R(x_1,x_2) \rightarrow R(x_0,x_2))$ we can then conclude $\langle v,v' '\rangle \in R^\mathcal G$.

For the reverse implication, we first show that the structure $\mathcal G$ defined as follows is a model of $\Phi_G$:

• the universe of $\mathcal G$ is $V$,
• $v^\mathcal G = v$ for every $v \in V$,
• $E^\mathcal G = E_G$,
• $R^\mathcal G = R_G$.

Clearly, $\mathcal G \mymodels \Psi_G$. So it remains to be shown that $\mathcal G \mymodels \Phi_R$. First, $\mathcal G \models \forall x_0 R(x_0, x_0)$, because $\langle v, v\rangle$ is a base element of $R_G$ for every $v \in V_G$. Second, $\mathcal G \mymodels \forall x_0 \forall x_1 \forall x_2 (E(x_0, x_1) \wedge R(x_1, x_2) \rightarrow R(x_0, x_2))$ because of the inductive rule in the definition of $R_G$.—So, indeed, $\mathcal G \models \Phi_G$.

This means that if $\Phi_G \models R(v,v')$, then $\mathcal G \mymodels R(v,v')$, which means, by definition of $\mathcal G$: $\langle v,v'\rangle = \langle v^\mathcal G,{v'}^\mathcal G\rangle \in R^\mathcal G = R_G$, which is to be shown.