# Immerman-Vardi theorem

(More discussion needed!)

Theorem (Immerman-Vardi). Over finite, ordered structures, the queries expressible in the logic FO(LFP) are precisely those that can be computed in polynomial time. Namely, FO(LFP) = P.

In this context, an order relation could be as simple as a succ binary predicate, such that the transitive closure of succ imply a total order on the structure. A quick definition of FO(FLP) can be found in the complexity zoo