This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.
Specifically, each logical system produces a set of queries expressible in it.
The queries – when restricted to finite structures – correspond to the computational problems of traditional complexity theory.
It established that NP is precisely the set of languages expressible by sentences of existential second-order logic; that is, second-order logic excluding universal quantification over relations, functions, and subsets.
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.
If we restrict ourselves to ordered structures with a successor relation and basic arithmetical predicates, then we get the following characterisations: In circuit complexity, first-order logic with arbitrary predicates can be shown to be equal to AC0, the first class in the AC hierarchy.
Indeed, there is a natural translation from FO's symbols to nodes of circuits, with
of size n. First-order logic in a signature with arithmetical predicates characterises the restriction of the AC0 family of circuits to those constructible in alternating logarithmic time.
[1] First-order logic in a signature with only the order relation corresponds to the set of star-free languages.
[8][9] First-order logic gains substantially in expressive power when it is augmented with an operator that computes the transitive closure of a binary relation.
The resulting transitive closure logic is known to characterise non-deterministic logarithmic space (NL) on ordered structures.
On structures that have a successor function, NL can also be characterised by second-order Krom formulae.
SO-Krom is the set of Boolean queries definable with second-order formulae in conjunctive normal form such that the first-order quantifiers are universal and the quantifier-free part of the formula is in Krom form, which means that the first-order formula is a conjunction of disjunctions, and in each "disjunction" there are at most two variables.
SO-Krom characterises NL on structures with a successor function.
This augments first-order logic with the ability to express recursion.
The Immerman–Vardi theorem, shown independently by Immerman and Vardi, shows that FO[LFP] characterises PTIME on ordered structures.
[12][13] As of 2022, it is still open whether there is a natural logic characterising PTIME on unordered structures.
[14] In the presence of a successor function, PTIME can also be characterised by second-order Horn formulae.
SO-Horn is the set of Boolean queries definable with SO formulae in disjunctive normal form such that the first-order quantifiers are all universal and the quantifier-free part of the formula is in Horn form, which means that it is a big AND of OR, and in each "OR" every variable except possibly one are negated.
[11] Ronald Fagin's 1974 proof that the complexity class NP was characterised exactly by those classes of structures axiomatizable in existential second-order logic was the starting point of descriptive complexity theory.
[4] SO, unrestricted second-order logic, is equal to the Polynomial hierarchy PH.
More precisely, we have the following generalisation of Fagin's theorem: The set of formulae in prenex normal form where existential and universal quantifiers of second order alternate k times characterise the kth level of the polynomial hierarchy.
[17] Unlike most other characterisations of complexity classes, Fagin's theorem and its generalisation do not presuppose a total ordering on the structures.
[18] The class of all problems computable in polynomial space, PSPACE, can be characterised by augmenting first-order logic with a more expressive partial fixed-point operator.
Partial fixed-point logic characterises PSPACE on ordered structures.
[20] The time complexity class ELEMENTARY of elementary functions can be characterised by HO, the complexity class of structures that can be recognized by formulas of higher-order logic.
They are usually written in upper-case and with a natural number as exponent to indicate the order.
Higher-order logic is the set of first-order formulae where we add quantification over higher-order variables; hence we will use the terms defined in the FO article without defining them again.
th is equivalent to a formula in prenex normal form, where we first write quantification over variable of