Editing Entscheidungsproblem (section)

=== Quantifier prefix ===
Any first-order formula has a prenex normal form. For each possible quantifier prefix to the prenex normal form, we have a fragment of first-order logic. For example, the [[Bernays–Schönfinkel class]], <math>[\exists^*\forall^*]_=  </math>, is the class of first-order formulas with quantifier prefix <math>\exists\cdots\exists\forall\cdots \forall     </math>, equality symbols, and no [[Function symbol|function symbols]].

For example, Turing's 1936 paper (p. 263) observed that since the halting problem for each Turing machine is equivalent to a first-order logical formula of form  <math>\forall \exists \forall \exists^6 </math>, the problem <math>\rm{Sat}(\forall \exists \forall \exists^6)    </math> is undecidable.

The precise boundaries are known, sharply:

* <math>\rm{Sat}(\forall \exists \forall)  </math> and <math>\rm{Sat}([\forall \exists \forall]_{=} ) </math>are co-RE-complete, and the <math>\rm{FinSat}  </math> problems are RE-complete (Theorem 5.2).
* Same for <math>\forall^3 \exists  </math> (Theorem 5.3).
* <math>\exists^* \forall^2 \exists^* </math> is decidable, proved independently by Gödel, Schütte, and Kalmár. 
* <math>[\forall^2 \exists]_=  </math> is undecidable.
* For any <math>n \geq 0  </math>, both <math>\rm{Sat}(\exists^n \forall^*) </math> and <math>\rm{Sat}([\exists^n \forall^*]_=)  </math> are NEXPTIME-complete (Theorem 5.1).
** This implies that <math>\rm{Sat}( [\exists^*\forall^*]_= ) </math> is decidable, a result first published by Bernays and Schönfinkel.<ref>{{Cite journal |last1=Bernays |first1=Paul |last2=Schönfinkel |first2=Moses |date=December 1928 |title=Zum Entscheidungsproblem der mathematischen Logik |url=http://link.springer.com/10.1007/BF01459101 |journal=Mathematische Annalen |language=de |volume=99 |issue=1 |pages=342–372 |doi=10.1007/BF01459101 |s2cid=122312654 |issn=0025-5831}}</ref>
* For any <math>n \geq 0, m \geq 2   </math>, <math>\rm{Sat}(\exists^n \forall \exists^m )  </math> is EXPTIME-complete (Section 5.4.1).
* For any <math>n \geq 0 </math>, <math>\rm{Sat}([\exists^n \forall \exists^*]_=)   </math> is NEXPTIME-complete (Section 5.4.2).
** This implies that <math>\rm{Sat}(\exists^*\forall^*\exists^*) </math> is decidable, a result first published by Ackermann.<ref>{{Cite journal |last=Ackermann |first=Wilhelm |date=1928-12-01 |title=Über die Erfüllbarkeit gewisser Zählausdrücke |url=https://doi.org/10.1007/BF01448869 |journal=Mathematische Annalen |language=de |volume=100 |issue=1 |pages=638–649 |doi=10.1007/BF01448869 |s2cid=119646624 |issn=1432-1807}}</ref>
* For any <math>n \geq 0 </math>, <math>\rm{Sat}(\exists^n \forall \exists)   </math> and <math>\rm{Sat}([\exists^n \forall \exists]_=)   </math> are PSPACE-complete (Section 5.4.3).

Börger et al. (2001)<ref>{{Cite book |last1=Börger |first1=Egon |title=The classical decision problem |last2=Grädel |first2=Erich |last3=Gurevič |first3=Jurij |last4=Gurevich |first4=Yuri |date=2001 |publisher=Springer |isbn=978-3-540-42324-9 |edition=2. printing of the 1. |series=Universitext |location=Berlin}}</ref> describes the level of computational complexity for every possible fragment with every possible combination of quantifier prefix, functional arity, predicate arity, and equality/no-equality.