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?
