Editing Descriptive complexity theory (section)

== Polynomial time ==
On ordered structures, first-order [[least fixed-point logic]] captures [[PTIME]]:

=== First-order least fixed-point logic ===
FO[LFP] is the extension of first-order logic by a least fixed-point operator, which expresses the fixed-point of a monotone expression. This augments first-order logic with the ability to express recursion. The Immerman–Vardi theorem, shown independently by [[Neil Immerman|Immerman]] and [[Moshe Vardi|Vardi]], shows that FO[LFP] characterises PTIME on ordered structures.<ref>{{Cite journal|last=Immerman|first=Neil|year=1986|title=Relational queries computable in polynomial time|journal=[[Information and Control]]|language=en|volume=68|issue=1–3|pages=86–104|doi=10.1016/s0019-9958(86)80029-8|doi-access=free}}</ref><ref>{{Cite book|last=Vardi|first=Moshe Y.|chapter=The complexity of relational query languages (Extended Abstract) |title=Proceedings of the fourteenth annual ACM symposium on Theory of computing - STOC '82|date=1982|publisher=ACM|isbn=978-0897910705|location=New York, NY, USA|pages=137–146|citeseerx=10.1.1.331.6045|doi=10.1145/800070.802186|s2cid=7869248}}</ref>

As of 2022, it is still open whether there is a natural logic characterising PTIME on unordered structures.

The [[Abiteboul–Vianu theorem]] states that FO[LFP]=FO[PFP] on all structures if and only if FO[LFP]=FO[PFP]; hence if and only if P=PSPACE. This result has been extended to other fixpoints.<ref name="avv">Serge Abiteboul, [[Moshe Y. Vardi]], [[Victor Vianu]]: [http://portal.acm.org/citation.cfm?id=256295 Fixpoint logics, relational machines, and computational complexity] Journal of the ACM archive, Volume 44,  Issue 1  (January 1997), Pages: 30-56, {{ISSN|0004-5411}}</ref>

=== Second-order Horn formulae ===
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 clause|Horn]] form, which means that it is a big AND of OR, and in each "OR" every variable except possibly one are negated.

This class is equal to [[P (complexity)|P]] on structures with a successor function.<ref>{{Cite journal|last=Grädel|first=Erich|date=1992-07-13|title=Capturing complexity classes by fragments of second-order logic|journal=Theoretical Computer Science|language=en|volume=101|issue=1|pages=35–57|doi=10.1016/0304-3975(92)90149-A|issn=0304-3975|doi-access=free}}</ref>

Those formulae can be transformed to prenex formulas in existential second-order Horn logic.<ref name=":2" />