Editing Descriptive complexity theory (section)

== Beyond NP ==

=== Partial fixed point is PSPACE ===
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]], FO[PFP], is the extension of first-order logic with a partial fixed-point operator, which expresses the fixed-point of a formula if there is one and returns 'false' otherwise.

Partial fixed-point logic characterises [[PSPACE]] on ordered structures.<ref>{{Cite book|last1=Abiteboul|first1=S.|last2=Vianu|first2=V.|title=&#91;1989&#93; Proceedings. Fourth Annual Symposium on Logic in Computer Science |chapter=Fixpoint extensions of first-order logic and datalog-like languages |chapter-url=http://dx.doi.org/10.1109/lics.1989.39160|year=1989|pages=71–79|publisher=IEEE Comput. Soc. Press|doi=10.1109/lics.1989.39160|isbn=0-8186-1954-6|s2cid=206437693}}</ref>

=== Transitive closure is PSPACE ===
Second-order logic can be extended by a transitive closure operator in the same way as first-order logic, resulting in SO[TC]. The TC operator can now also take second-order variables as argument. SO[TC] characterises [[PSPACE]]. Since ordering can be referenced in second-order logic, this characterisation does not presuppose ordered structures.<ref>{{Cite journal|last1=Harel|first1=D.|last2=Peleg|first2=D.|date=1984-01-01|title=On static logics, dynamic logics, and complexity classes|journal=Information and Control|language=en|volume=60|issue=1|pages=86–102|doi=10.1016/S0019-9958(84)80023-6|issn=0019-9958|doi-access=free}}</ref>