Editing Entscheidungsproblem (section)

== Fragments ==
By default, the citations in the section are from Pratt-Hartmann (2023).<ref name=":0">{{Cite book |last=Pratt-Hartmann |first=Ian |url=https://academic.oup.com/book/46400 |title=Fragments of First-Order Logic |date=2023-03-30 |publisher=Oxford University Press |isbn=978-0-19-196006-2 |language=en}}</ref>

The classical ''Entscheidungsproblem'' asks that, given a first-order formula, whether it is true in all models. The finitary problem asks whether it is true in all finite models. [[Trakhtenbrot's theorem]] shows that this is also undecidable.<ref>B. Trakhtenbrot. ''The impossibility of an algorithm for the decision problem for finite models''. Doklady Akademii Nauk, 70:572–596, 1950. English translation: AMS Translations Series 2, vol. 33 (1963), pp. 1–6.</ref><ref name=":0" />

Some notations: <math>\rm{Sat} (\Phi) </math> means the problem of deciding whether there exists a model for a set of logical formulas <math>\Phi  </math>. <math>\rm{FinSat} (\Phi) </math> is the same problem, but for ''finite'' models. The <math>\rm{Sat}  </math>-problem for a [[logical fragment]] is called decidable if there exists a program that can decide, for each <math>\Phi  </math> finite set of logical formulas in the fragment, whether <math>\rm{Sat} (\Phi) </math> or not.

There is a hierarchy of decidabilities. On the top are the undecidable problems. Below it are the decidable problems. Furthermore, the decidable problems can be divided into a complexity hierarchy.

=== Aristotelian and relational ===
[[Term logic|Aristotelian logic]] considers 4 kinds of sentences: "All p are q", "All p are not q", "Some p is q", "Some p is not q". We can formalize these kinds of sentences as a fragment of first-order logic:<math display="block">\forall x, p(x) \to \pm  q(x), \quad \exists x, p(x) \wedge \pm  q(x) </math>where <math>p, q </math> are atomic predicates, and <math>+q := q, \; -q := \neg q </math>. Given a finite set of Aristotelean logic formulas, it is [[NL (complexity)|NLOGSPACE]]-complete to decide its <math>\rm{Sat}  </math>. It is also NLOGSPACE-complete to decide <math>\rm{Sat}  </math> for a slight extension (Theorem 2.7):<math display="block">\forall x, \pm p(x) \to \pm  q(x), \quad \exists x, \pm p(x) \wedge \pm  q(x) </math>[[Relational algebra|Relational logic]] extends Aristotelean logic by allowing a relational predicate. For example, "Everybody loves somebody" can be written as <math display="inline">\forall x, \rm{body}(x), \exists y, \rm{body}(y) \wedge \rm{love}(x, y)  </math>. Generally, we have 8 kinds of sentences:<math display="block">\begin{aligned}
\forall x, p(x) \to (\forall y, q(x) \to \pm r(x, y)), &\quad \forall x, p(x) \to (\exists y, q(x) \wedge \pm r(x, y))  \\
\exists x, p(x) \wedge (\forall y, q(x) \to \pm r(x, y)), &\quad \exists x, p(x) \wedge (\exists y, q(x) \wedge \pm r(x, y)) 
\end{aligned} </math>It is [[NL (complexity)|NLOGSPACE]]-complete to decide its <math>\rm{Sat}  </math> (Theorem 2.15). Relational logic can be extended to 32 kinds of sentences by allowing <math>\pm p, \pm q  </math>, but this extension is [[EXPTIME]]-complete (Theorem 2.24).

=== Arity ===
The first-order logic fragment where the only variable names are <math>x, y  </math> is [[NEXPTIME]]-complete (Theorem 3.18). With <math>x, y, z </math>, it is [[RE_(complexity)#co-RE-complete|co-RE]]-complete to decide its <math>\rm{Sat}  </math>, and [[RE_(complexity)|RE]]-complete to decide <math>\rm{FinSat}  </math> (Theorem 3.15), thus undecidable.

The [[monadic predicate calculus]] is the fragment where each formula contains only 1-ary predicates and no function symbols. Its  <math>\rm{Sat}  </math> is NEXPTIME-complete (Theorem 3.22).

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