Expressing complexity class P using first-order logic with LFP
In Neil Immerman's Descriptive Complexity the proof that P = FO + LFP uses alternating graphs: an alternating graph is a directed graph $G= \{ V, E, A, s, t\}$ where $A$ is the set of nodes marked as universal ($V \setminus A$ are existential). The accessibility relation is defined in this way:


$P_a^G(x,x)$
if $x \in V \setminus A$  $\land P_a^G(z,y)$ holds for some edge $(x,z)$ then $P_a^G(x,y)$
if $x \in A$ $\land \; outdeg(x)&gt;0 \land P_a^G(z,y)$ holds for all edges $(x,z)$ then $P_a^G(x,y)$


The reachability problem $REACH_a$ is defined as $\{G | P_a^G(s,t)\}$ and is complete for P via first-order reductions.

Using LFP one can give a FO + LFP definition of $REACH_a$ (i.e. $REACH_a \subseteq FO+LFP$):

$$\varphi_{as}(P,x,y)\equiv  x = y \lor [\exists z(E(x,z)\land P(z,y)) \land (A(x)\rightarrow \forall z(E(x,z)\rightarrow P(z,y)))]$$

and $REACH_a = (LFP_{P_{xy}\varphi_{ap}})(s,t)$

We have $P \subseteq REACH_a \subseteq FO+LFP$, the inverse $FO+LFP \subseteq P$ follows from the fact that a FO query can be evaluated in $L$ and at most $n^k$ evaluations of $\varphi(R,x_1,...,x_k)$ are needed for $(LFP_{R \varphi})$ ($R$ is a k-ary relation).

For further details you can see the proof on Immerman's book.