# Define infinite path with a finite relation in a graph with Least Fixed Point logic

Least Fixed Point(LFP) logic (p. 37ff) is an extension of first order logic which enables the usage of the least fixed point of FO-definable operators. For example consider a graph $G=(V,E)$ and binary operator $T(x,y)$ defined by

$$x = y \lor \lor T(x,y) \lor \exists z (Exz \land Tzy).$$

The operator "updates" a binary relation $R \subseteq V \times V$ to $T(R)$. Now if we consider multiple application of $T$ onto a relation $R$

$$T(T(\dots T(R) \dots))$$

the operator reaches a fixed point such that

$$T^n(R) = T^{n+1}(R).$$

Then $T^n$ is a fixed point. The fixed point which is minimal with respect to $\subseteq$ is the least fixed point. LFP allows FO-defined operators to define new relations. The least fixed point of $E$ and the operator above is the binary transtive closure relation $TC(E)$ of $E$.

Given a directed (possibly not finite) graph $G = (V,E,P)$ with an unary relation symbol $P$. We want to define a LFP-formula $\varphi(v) \models G$ iff there is an infinite path starting in $v$ such that $P$ occurs only finitely often.

If have several problems with this exercise. First of all I do not now how to define paths because it is possible to define relations on $V \times V$ but if an edge on infinite path would occur twice then a fixed point is imitatively reached even though the path is not finished. Second, I know that it is possible to define "finite" in a structure with a successor function $S$ with $LFP$ logic. But I don't think that such a function is definable. Is it a good approach to divide the properties or is it easier to use a more holistic approach? Any hints?

-
I have only passing acquaintance with LFPL, but my thought would be to try to model the following statement: there is a node $u$ reachable from $v$ and there is an infinite path starting at $u$ with no occurrences of $P$. –  Arthur Fischer Jan 19 '13 at 16:14
Okay, the existence of a reachable node is similar to the transitive closure but how do I model an infinite path with a single formula without a set of formulas? –  joachim Jan 19 '13 at 17:12
If I had a better feel for the logic I would say more, but unfortunately I don't. I'll try to think about this more, however. –  Arthur Fischer Jan 20 '13 at 6:15