I'm wondering why we can't express graph reachability in first order logic in pretty much exactly the same way we express it in second order existential logic. For SOL, one definition is :

1 . L is a linear order on a subset of the vertices :

$$\begin{align} \psi_1 = &\forall u \neg L(u,u) \\ &\wedge \forall u\forall v (L(u,v) \Rightarrow \neg L(v,u)) \\ & \wedge \forall u\forall v \forall w(L(u,v) \wedge L(v,w) \Rightarrow L(u,w)) \end{align} $$

2 . Any two consecutive vertices in the order must be joined by an edge in G:

$$\begin{align} \psi_2 = &\forall u\forall v ((L(u,v) \ \wedge \forall w(\neg L(u,w) \vee \neg L(w,v))) \\ & \Rightarrow E(u,v)). \end{align} $$

3 . The first vertex in the order is x and the last is y and x, y are in the order:

$$\begin{align} \psi_3 = &(\forall u\ \neg L(u,x)) \wedge (\forall v\ \neg L(y,v)) \ \wedge L(x,y) \end{align} $$

and finally the expression for reachability is

4 . $\phi(x,y) =\exists L (x=y) \vee (\psi_1 \wedge \psi_2 \wedge \psi_3))$

But why can't we use the same thing in first order logic (i.e. no existential quantification over L) :

$\phi(x,y) =(x=y) \vee (\psi_1 \wedge \psi_2 \wedge \psi_3))$

This would be interpreted over the vocabulary with models M having two binary relations : E (edge) and L (reachable), and the universe of all nodes. Surely any model which satisfies the expression 5 above will have its L relation expressing a linear ordering of the nodes, with any two consecutive elements being adjacent in E - in other words, it will be the "Reachable" relation, (and the model will map the free variables x and y to nodes N1 and N2, with (N1,N2) in L, meaning N2 is reachable from N1).

Why doesn't this work? Specifically, would the proof of non expressibility of reachability fail for it?

The proof of non expressibility of reachability in FOL goes like this :

Assume that an FOL expression p, with free variables x and y exists, expressing reachability.

We have $s_1 \equiv \forall x \forall y \ p$ stating that all nodes are reachable from all nodes, i.e. the graph is strongly connected.

Then we add two sentences about E, $s_2$ (saying that every node of the graph has outdegree one), and $s_3$ (that every node has indegree one). The conjunction of the above three sentences

$s_4 = s_1 \wedge \ s_2 \wedge \ s_3$,

then states that the graph is strongly connected and all nodes have indegree and outdegree one - i.e. it's a cycle.

Since there are finite cycles with as many nodes as desired, s4 has arbitrary large finite models. Therefore by Lowenheim-Skolem theorem, it also has an infinite model. But infinite cycles do not exist, and so our assumption that there exists a p expressing reachability is contradicted.

If our FOL expression (5) is taken as the p expression in the proof, all the steps of the proof can be carried out the same, and we will be led to the same result, namely that (5) does not express reachability. But why not? It certainly has all the elements..

  • $\begingroup$ You would need new $L$ for (almost) every pair of vertices. If you had such $L_{(x,y)}$ in the language, then I don't see why this wouldn't work, after all this is similar to how existential quantifier works. $\endgroup$
    – dtldarek
    Dec 4, 2012 at 8:31

2 Answers 2


The issue here is with the terminology. You can express reachability in first-order logic; for example you can express it in the language of set theory by quantifying over paths in the graph, and set theory is a first-order theory.

You cannot express reachability in the particular language where the only relations available are the incidence relation on the graph and equality, and where quantification is only permitted over elements of the graph. So the issue actually has very little to do with "first order logic", and everything to do with the particular language that is being allowed. Tradition says that this situation is phrased as "reachability cannot be expressed in first order logic", even though that phrase could be interpreted in other ways.

Ignoring terminological issues, it can be genuinely useful to know that reachability cannot be expressed without quantifying over sets or paths in some way. For example, that fact means that if your graph is stored in an SQL database in a natural way then it will be more difficult to code an SQL query that tells whether an arbitrary pair of nodes has a path than it would be if that relation could be phrased in the limited language mentioned above.

By the way,here is how you show there is no formula $\phi(a,b)$ expressing reachability. Take the language of graph theory mentioned above and add two new constants $C$ and $D$. Take the infinite set of axioms "there is no path of length $1$ from $C$ to $D$", "there is no path of length two from $C$ to $D$", ... Then any finite set of these axioms is consistent with $\phi(a,b)$, as can be seen by looking at a graph with an infinitely long path and taking $C$ and $D$ to be far enough apart. Thus by the compactness theorem the set of all those axioms is consistent with $\phi(C,D)$. But if all those axioms are true in a graph, there is no path from $C$ to $D$ in that graph, so $\phi$ did not express that property correctly.

  • $\begingroup$ Ok, but where does your proof depend on the restriction that the only relations available in the language are graph and equality? If ϕ(a,b) is taken to be the first order expression for reachability that I gave in my original post (which is over a language that contains an additional relation symbol L), your proof would also seem to work for it. Or let's say you express reachability in FOL using set theory, which you said is possible. Then where would your proof break down for that expression? $\endgroup$
    – Int
    Dec 4, 2012 at 19:10
  • $\begingroup$ The compactness theorem does not hold for the semantics that are used to quantify over every possible interpretation of the relation $L$. On the other hand, if you just add $L$ to your language but don't quantify over $L$, then the proof does go through; no formula of that sort can define reachability. $\endgroup$ Dec 4, 2012 at 20:00
  • 1
    $\begingroup$ What if, like you said, you express reachability in first order logic in the language of set theory, by quantifying over the paths in the graph - won't that also be just a first order (no quantifications over relations) sentence ϕ(a,b) in the vocabulary of set theory? If so, the proof should go through for it as well! $\endgroup$
    – Int
    Dec 4, 2012 at 22:33
  • 1
    $\begingroup$ What happens is this: there is a formula $\phi(a,b,G)$ in the language of set theory such that, in the standard model of set theory, if $G$ is a graph and $a,b$ are nodes in it, $\phi(a,b,G)$ holds if and only if there is a path from $a$ to $b$. But for any such formula there will be nonstandard models of set theory in which there is a graph $G$ and two nodes $a,b$ in it that are not connected by a path, but such that $\phi(a,b,G)$ is still true in that nonstandard model. "Expression" in set theory is about the intended interpretation. ... $\endgroup$ Dec 5, 2012 at 11:46
  • 1
    $\begingroup$ The precise situation is that there is a single standard model of set theory, which contains every graph, and reachability is definable in that model with a single formula $\phi(a,b,G)$ that takes a graph as a parameter. But in the language of graph theory, different graphs correspond to different models, and there is no formula $\psi(a,b)$ in the language of graph theory that expresses reachability in all such models. There is no such thing as a "nonstandard model" in the language of graph theory; every model in that language really is a graph, and vice versa. $\endgroup$ Dec 5, 2012 at 11:50

"Surely any model which satisfies the expression 5 above will have its L relation expressing a linear ordering of the nodes, with any two consecutive elements being adjacent in E" - this is true, but the definition of first-order expressibility (w.r.t. some fixed language) is an equivalence, and not an implication. The other side of the implication, i.e. "$(\mathbb{G}, a,b)$ satisfies reachability => satisfies the expression 5" is false. Remember that if your language contains the relation $L$, then in any structure $\mathbb{G}$ for that language, the interpretation $L^\mathbb{G}$ is fixed. Now, to see the implication does not hold, take any connected graph $\mathbb{G}$ with $L^\mathbb{G} = \{(a,a): a \in G\}$. Now e.g. for any graph that is actually a cycle of size at least 2 that is connected the structure $(\mathbb{G}, L^\mathbb{G})$is obviously connected (as a graph), so every two nodes are reachable, yet for any $a \neq b$, the structure $(\mathbb{G}, L^\mathbb{G}, a, b)$ does not satisfy expression 5.

The cause of this problem is that you indeed need to quantify over binary relations to pick the right $L$ in order to exprerss reachability (or connectedeness for that matter).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .