Whilst reading this: http://dtai.cs.kuleuven.be/krr/files/seminars/IntroToFMT-janvdbussche.pdf a seminar on finite model theory, I thought that something was wrong.
"Given a Graph G and a Binary Relation P on its vertices, check if P is the set of edges of a simple path in G".
I don't think it makes any real difference if we look at directed or simple paths.
The query he provides, I cannot see how it characterises paths. Basically he says, we have a unique source and a unique sink, and each other vertex has a directed edge to and from some unique vertex.
But how does that preclude having a disjoint union of connected components, one being a path and all the rest being cycles? This is not a path, but it seems to pass his query.
How then does one characterise paths in graph theory by a first order sentence?