least-fixed point logic coincides exactly with the expressivity of the database querying language Datalog, showing that Datalog can express exactly those queries executable in polynomial time. Inflationary fixed-point logic Another way to ensure the monotonicity of the fixed-point construction is by only adding new tuples to at every stage of iteration, without removing tuples for which no longer holds. Formally, we define as where . This inflationary fixed-point agrees with the least-fixed point where the latter is defined. Although at first glance it seems as if inflationary fixed-point logic should be more expressive than least fixed-point logic since it supports a wider range of fixed-point arguments, in fact, every FO[IFP](X)-formula is equivalent to an FO[LFP](X)-formula. Simultaneous induction While all the fixed-point operators introduced so far iterated only on the definition of a single predicate, many computer programs are more naturally thought of as iterating over several predicates simultaneously. By either increasing the arity of the fixed-point operators or by nesting them, every simultaneous least, inflationary or partial fixed-point can in fact be expressed using the corresponding single-iteration constructions discussed above. Transitive closure logic Rather than allow induction over arbitrary predicates, transitive closure logic allows only transitive closures to be expressed directly. FO[TC](X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a transitive closure operator used to form formulas of the form , where and are tuples of pairwise distinct first-order variables, and tuples of terms and the lengths of , , and coincide. TC is defined as follows: Let be a positive integer and be vectors of variables. Then is true if there exist vectors of variables such that , and for all , is true. Here, is a formula written in FO(TC) and means that the variables and are replaced by and . Over ordered structures, FO[TC] characterises the complexity class NL. This characterisation is a crucial part of Immerman's proof that NL is closed under complement (NL = co-NL). Deterministic transitive closure logic FO[DTC](X) is defined as FO(TC,X) where the transitive closure operator is deterministic. This means that when we apply , we know that for all , there exists at most one such that . We can suppose that is syntactic sugar for where . Over ordered structures, FO[DTC] characterises the complexity class L. Iterations The fixed-point operations that we defined so far iterate the inductive definitions