Well so far you've only used first order logic. So you should try to quatify over predicates to express $Path$. I'm not exactly sure how to express $Path$. But I think you could replace it with $SimplePath(x,y)$ defined as "There is a simple path from $x$ to $y$", where a simple path is a path with no repeating vertex. $SimplePath$ is easier to express.

I know how to show it. But just giving you the answer would be pointless. Try to define $SimplePath(x,y) := \exists P, ...$ where in the $...$ you says that $P$ is a simple path from $x$ to $y$. If you look at it from an undirected point of view, being a path means that every vertex has exactly two neighbours (in the path) except the two endpoints that only have one. Now you can try to build the formula for $SimplePath$ that works for the directed case.

(Remark: The simple approach that I described above (saying that every node has two neighbours except the two endpoints) allows $P$ to be the union of a simple path from $x$ to $y$ and of several disjoint cycles. But that's not really a problem. This could be fixed by saying that $P$ is the smallest such set, but it's not necessary since you just want to know if a simple path exists)

How would you express being connected without using the notion of Path? It looks hard to me. The nice thing about paths is that you can just check locally that it's a path and it suffices to fully characterise a path. A connected set looks way harder to characterise locally.

Right. So you have a solution to your problem? And I initially missed that in your question, but as they say in the answer you linked, you only ever talk about finite paths, even in infinite graphs.

You should hard all the information you need in my previous comments. If there is something you don't understand, let me know.

The formula in your question works but is overly complicated. You're saying "If I can go to two distinct places, then I can go to some third place from those two places". But you don't need them to be distinct. In other words, you can remove the (b =/= c) hypothesis.

replace "a successor/predecessor" by "a unique successor/predecessor"

The only thing that can go wrong is if you have an infinite path starting at x and a coinfinite path going to y.

Which I kind of missed. Anyway, here's a fix: Define Reachable(x) the set of nodes reachable from x. You should be able to easily define a set that contains at least all nodes reachable from x. Then Reachable(x) is just the smallest such set. And once you have Reachable(x), testing the existence of a path is easy.