Editing Descriptive complexity theory (section)

=== 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>