Formalizing the notion of a finite number of steps.

Question

Suppose we have a (potentially infinite) graph $G$. Let $xRy$ denote the statement "there exists a directed edge from $x$ to $y$" for some two nodes $x, y$ of $G$. I'm interested in a formalization of the sentence

There exists a finite path from $a$ to $b$.

I have convinced myself this is impossible in first-order logic. How could we do this in some higher-order logic? I'm also curious as to how difficult it would be to prove that this statement isn't expressible in first-order logic.

I don't know much about this topic, so sorry if my question is vague. I couldn't find much on the internet about it. I'd be interested in any reading recommendations if this is too complicated to explain in a single thread. Thank you.

Answer 1

This is indeed impossible in first-order logic. The key is the compactness theorem: if $\varphi$ were a first-order formula characterizing finite distance, the set of sentences (in the language of graph theory + two constant symbols $a,b$) $$\varphi(a,b)\cup\{\delta_n: n\in\mathbb{N}\}$$ (where $\delta_n$ says "there is no length-$\le n$ path from $a$ to $b$" - this is clearly first-order-expressible) would be finitely satisfiable but not satisfiable. This, and similar questions, are treated in multiple places on this site; search "compactness + logic" and you should find a bunch.

In general, the way to show that first-order logic can't do something is to show that doing that thing would lead to a failure of some "tameness" property that FOL is known to have.

Second-order logic, meanwhile, is not compact (incidentally it's vastly easier to show that SOL is non-compact than it is to show that FOL is compact) so the above idea doesn't work. In fact, second-order logic can do the job. There are various ways to do this. My personal favorite approach is to shift from "There is a finite path from $a$ to $b$" to the equivalent "The connected component of $a$ contains $b$," which itself can be rephrased as "Every 'distance-$1$-closed' set containing $a$ also contains $b$." And this isn't hard to second-order-ify:

$$\forall X[a\in X\wedge\forall y, z(y\in X\wedge yRz\rightarrow z\in X)\rightarrow b\in X].$$

Note the similarity with induction - this sort of idea is extremely prevalent in applications of second-order logic.

Answer 2

What you are trying to formalize is something called the ancestor relation of $R$. We can prove that it is impossible to define this relation in first order logic using the compactness theorem. Here is a proof of that fact.

Let $R$ be a relation on $E$. Now, we want to define a relation $R^*$ such that $xR^*y$ if, and only if, there is a finite chain of $x_i$ such that $x_0=x$, $x_n=y$ and $x_iRx_{i+1}$. Suppose we can define such a relation with a first order formula $\phi$. That is, we have $xR^*y \leftrightarrow \phi(x,y)$. Now we seek to show that this $\phi$ cannot really define the relation we want.

Fix some $x$ and $y$ in the domain of discourse. For each $n\in \mathbb{N}$, we can define a formula $\psi_n$ in FOL that asserts that there is not an $R$-chain of length $n$ connecting $x$ and $y$. For $n=1$, this looks like $\neg\exists z(xRz\land zRy)$. I hope it is clear how to define the other $\psi_n$. Now we seek to show that $\{\psi_n\}_{n\in\mathbb{N}}\cup \{\phi\}$ has a model. By compactness, it suffices to show that each finite subset has a model. But for each finite subset, there is a largest $n$ such that the subset contains a $\psi_n$. Thus we can model the subset by interpreting $x$ and $y$ as two objects which have no $n$ length chain, but do have an $n+1$ length chain. It follows that there is a model for the whole set. But, by inspecting this model, it is clear that there is no finite length chain from $x$ to $y$. Thus $\phi$ cannot express the desired proposition. So the ancestor relation is not definable in FOL.

As I was writing this, Noah Schweber posted an answer in which they describe how to define the relation in second order logic, so I won't do that here.