Editing Descriptive complexity theory (section)

== Sub-polynomial time ==

=== FO without any operators ===

In [[circuit complexity]], first-order logic with arbitrary predicates can be shown to be equal to [[AC0|AC<sup>0</sup>]], the first class in the [[AC (complexity)|AC]] hierarchy. Indeed, there is a natural translation from FO's symbols to nodes of circuits, with <math>\forall, \exists</math> being <math>\land</math> and <math>\lor</math> of size {{mvar|n}}. First-order logic in a signature with arithmetical predicates characterises the restriction of  the AC<sup>0</sup> family of circuits to those constructible in [[LH (complexity)|alternating logarithmic time]].<ref name="Immerman 1999, p. 86"/> First-order logic in a signature with only the order relation corresponds to the set of [[star-free language]]s.<ref>{{Cite book|last=Robert.|first=McNaughton|url=http://worldcat.org/oclc/651199926|title=Counter-free automata|date=1971|publisher=M.I.T. Press|isbn=0-262-13076-9|oclc=651199926}}</ref><ref>Immerman 1999, p. 22</ref>

=== Transitive closure logic ===
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 [[NL (complexity)|non-deterministic logarithmic space (NL)]] on ordered structures. This was used by [[Neil Immerman|Immerman]] to show that NL is closed under complement (i. e. that NL = co-NL).<ref>{{Cite journal|last=Immerman|first=Neil|date=1988|title=Nondeterministic Space is Closed under Complementation|url=http://dx.doi.org/10.1137/0217058|journal=[[SIAM Journal on Computing]]|volume=17|issue=5|pages=935–938|doi=10.1137/0217058|issn=0097-5397}}</ref>

When restricting the transitive closure operator to [[Fixed-point logic#Deterministic transitive closure logic|deterministic transitive closure]], the resulting logic exactly characterises [[L (complexity)|logarithmic space]] on ordered structures.

=== Second-order Krom formulae ===
On structures that have a successor function, NL can also be characterised by second-order [[Krom formula]]e.

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. Every second-order Krom formula is equivalent to an existential second-order Krom formula.

SO-Krom characterises NL on structures with a successor function.<ref name=":2">Immerman 1999, p. 153{{Ndash}}4</ref>