A simultaneous induction over a vocabulary $L$ consists of a block of relation variables $R_1, \dots, R_m$, a step formula $\varphi_i(\bar x)$ for each variable, an arbitrary first-order formula over $L$ expanded by the block whose free variables are the arguments of $R_i$, and an output sentence over the same expanded vocabulary. On an $L$-structure, the inflationary iteration starts from the empty relations and at each stage adds to every $R_i$ the tuples satisfying $\varphi_i$ at the current stage: $R_i^0 = \emptyset$ and $R_i^{n+1} = R_i^n \cup \{\bar a \mid \varphi_i(\bar a) \text{ holds at stage } n\}$. Its limit is the union of the stages, and the induction holds on the structure, read inflationarily, when the output sentence is true at the limit. No positivity is required of the step formulas.

A decision problem $P$ over $L$ is FO($\le$, IFP) definable when some simultaneous induction over $L \cup \{\le\}$ holds inflationarily, for every nonempty finite $L$-structure $A$ and every linear order on $A$, exactly when $A$ is a yes-instance of $P$.