FO(LFP)
In descriptive complexity, a branch of computational complexity, FO is a complexity class of structures that can be recognized by formulas of first-order logic, and also equals the complexity class AC0. Descriptive complexity uses the formalism of logic, but does not use several key notions associated with logic such as proof theory or axiomatization.
Restricting predicates to be from a set X yields a smaller class FO[X]. For instance, FO[<] is the set of star-free languages. The two different definitions of FO[<], in terms of logic and in terms of regular expressions, suggests that this class may be mathematically interesting beyond its role in computational complexity, and that methods from both logic and regular expressions may be useful in its study.
Similarly, extensions of first-order logic formed by the addition of operators give rise to other well-known complexity classes. This allows the complexity of some problems to be established without reference to algorithms.
When we use the logic formalism to describe a computational problem, the input is a finite structure, and the elements of that structure are the domain of discourse. Usually the input is either a string (of bits or over an alphabet) and the elements of the logical structure represent positions of the string, or the input is a graph and the elements of the logical structure represent its vertices. The length of the input will be measured by the size of the respective structure. Whatever the structure is, we can assume that there are relations that can be tested, for example " is true iff there is an edge from x to y" (in case of the structure being a graph), or " is true iff the nth letter of the string is 1." These relations are the predicates for the first-order logic system. We also have constants, which are special elements of the respective structure, for example if we want to check reachability in a graph, we will have to choose two constants s (start) and t (terminal).
...
Wikipedia