0
$\begingroup$

I am trying to understand why directed graph reachability cannot be expressed in first-order logic.

In Papadimitriou's "Computational Complexity" book this is proven by contradiction. Assume that there is a first-order formula $\phi(x,y)$ that does express reachability between two vertices $x$ and $y$ in a directed graph represented by binary edge relation $G$. Then consider the following formula $\psi$ built out of $\phi(x,y)$:

$$ \forall x \forall y \; \phi(x,y) \\ \wedge \forall x \; \exists z \; \Bigl(G(x,z) \wedge ( \forall w \; G(x,z) \wedge G(x,w) \Rightarrow z = w )\Bigr) \\ \wedge \forall x \; \exists z \; \Bigl(G(z,x) \wedge ( \forall w \; G(z,x) \wedge G(w,x) \Rightarrow z = w )\Bigr), $$

In English, this says that every vertex is reachable from every other vertex and each vertex has both indegree and outdegree 1.

Papadimitriou argues that every finite interpretation of $G$ making it a cycle is a model of $\psi$, because every vertex is reachable from every other, and indegrees and outdegrees are always 1. Because there are arbitrarily large cycles (each being a model of $\psi$), by the Löwenheim–Skolem theorem we can affirm that there is an infinite model for $\psi$ as well. However, this is a contradiction because there are no infinite cycles. Therefore, there can be no such formula $\phi(x,y)$.

Now, it seems to me we can express graph reachability with first-order logic by writing the theory

$$R(x,y) \Leftrightarrow G(x,y) \vee \exists z \; G(x,z) \wedge R(z,y).$$

How can we reconcile this with Papadimitriou's proof?

PS: answer by Reese below shows that the above definition is not correct. However, it seems to me that Papadimitriou's definition of "cannot defined in first-order logic" as "there is no formula $\phi(x,y)$" is too restrictive, because it seems that in principle we could define concepts in FOL using a circularly-defined predicate like that, or at least we would need to prove that no circular definitions will work either.

$\endgroup$
2
$\begingroup$

Your definition of $R$ is circular. Consider, for example, the model consisting of four vertices, A, B, C, and D, in which we have edges AB and CD and we have $R(x,y)$ for every pair of vertices $x,y$. This model satisfies your proposed axiom; for example, we have $R(A,C) \iff G(A,C) \vee (\exists z)[G(A,z) \wedge R(z,C)]$; the witnessing $z$ in this case is $B$.

Circular definitions are dangerous in first-order logic; they usually permit tricks like this.

$\endgroup$
  • $\begingroup$ Thanks, that's great. Now, it seems to me that Papadimitriou's definition of "cannot defined in FOL" as "there is no $\phi(x,y)$" is too restrictive, because it does not allow for circular definitions; although this one does not work, can we prove that none will? $\endgroup$ – user118967 Nov 6 '16 at 8:18
  • $\begingroup$ Circular definitions are inherently bad - we don't want a notion of FOL in which circular definitions are allowed, because a circular definition defines nothing. Generally, we say a "definition" must uniquely specify the thing defined; a circular definition cannot do this, unless it reduces to a noncircular one. For example, "All ravens are ravens" is not a helpful definition in any circumstance; "all ravens are raven-colored" could conceivably be a useful description, but not a definition. Papadimitriou's definition of definability is the only one that makes sense for first-order logic. $\endgroup$ – Reese Nov 6 '16 at 23:57
  • $\begingroup$ Thanks. "All ravens are ravens" is obviously bad, but other circular definitions seem more sensical, such as $F(i) = f \Leftrightarrow (i = 1 \wedge f = 1) \vee f = i*F(i - 1)$. Of course, this one depends on arithmetic so it is not really FOL, but could we not include axioms declaring arithmetic-like functions that impose an order on objects (perhaps infinite axiomatizations for infinite domains) and then write useful circular definitions? I wonder if it is possible to impose an order an a graph's edge, for example, and only define R in terms of R for earlier edges? $\endgroup$ – user118967 Nov 7 '16 at 23:57
  • 1
    $\begingroup$ Definitions of the sort you suggest are only sensical in cases in which they are inductive, not circular. Even an inductive definition isn't sensical in a FOL sense - take, e.g., the inductive definition of "even" as $E(x) \iff \neg E(x - 1)$. There is a model of arithmetic which has infinite elements; fix such a $c$. It is consistent that $E(c)$ holds (so $E(c - 1)$ doesn't, and so on) or that it doesn't (in which case $E(c-1)$ does, and so on) without changing anything else about the model. So this isn't really a definition, just a general description of properties of "evenness". $\endgroup$ – Reese Nov 8 '16 at 0:05
  • 1
    $\begingroup$ To elaborate on my last comment (partly because I ran out of space): We might be able to impose an order on the graph; we might even be able to do it definably in FOL. But we wouldn't be able to do it well enough that the circular definition becomes necessarily inductive, because FOL isn't powerful enough to define an ordering that is necessarily a well-ordering (which is required for an inductive definition to make sense). $\endgroup$ – Reese Nov 8 '16 at 0:07
0
$\begingroup$

This can be reconciled by noting that the theory using $R$ is not providing a formula $\phi(x,y)$ as requested by Papadimitriou.

What are the options for using this theory and providing $\phi(x,y)$? We could make $\phi(x,y)$ be $R(x,y)$, but then we would not be providing $R$'s definition. We cannot define $\phi(x,y)$ to be the circularly-defined $G(x,y) \vee \exists z \; G(x,z) \wedge \phi(z,y)$, either.

Ultimately, the paradox can be clarified by noting that Papadimitriou's definition of the phrase "expressing graph reachability with first-order logic" is a narrower one than a definition that allows the use of a first-order theory to do so.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.