A definition in FO(LFP), in clausal normal form, over a vocabulary $L$ consists of a block of relation variables, a finite list of rules, which are Horn clauses over $L \cup \{\le\}$ and the block with a head, and an output sentence, an arbitrary first-order sentence over $L \cup \{\le\}$ expanded by the relation variables. On a linearly ordered $L$-structure the rules define the least relations closed under them: a tuple is derived when some rule, at some valuation satisfying its guard and whose body atoms are already derived, has it as head. The definition holds on the structure when the output sentence is true with the relation variables interpreted by these least fixed points. The output may negate the fixed-point atoms.

A decision problem $P$ over $L$ is FO(LFP) definable when some definition holds, for every nonempty finite $L$-structure $A$ and every linear order on $A$, exactly when $A$ is a yes-instance of $P$. This is the logic FO(LFP) of Immerman and Vardi on ordered structures, in the normal form of one simultaneous induction under a first-order formula.