Entscheidungsproblem: Difference between revisions
Jump to navigation
Jump to search
imported>OAbot m Open access bot: url-access updated in citation with #oabot. |
imported>Curlyquote m clean up, replaced: Aristotelean → Aristotelian (2) |
||
| Line 2: | Line 2: | ||
{{italic title}} | {{italic title}} | ||
{{Use dmy dates|date=August 2021}} | {{Use dmy dates|date=August 2021}} | ||
In [[mathematics]] and [[computer science]], the {{lang for|de|'''Entscheidungsproblem'''|decision problem|paren=left}}; {{IPA|de|ɛntˈʃaɪ̯dʊŋspʁoˌbleːm|pron}}) is a challenge posed by [[David Hilbert]] and [[Wilhelm Ackermann]] in 1928.<ref>David Hilbert and Wilhelm Ackermann. Grundzüge der Theoretischen Logik. Springer, Berlin, Germany, 1928. English translation: David Hilbert and Wilhelm Ackermann. Principles of Mathematical Logic. AMS Chelsea Publishing, Providence, Rhode Island, USA, 1950</ref> It asks for an [[algorithm]] that considers an inputted statement and answers "yes" or "no" according to whether it is universally valid, i.e., valid in every [[Structure (mathematical logic)|structure]]. Such an algorithm was proven to be impossible by [[Alonzo Church]] and [[Alan Turing]] in 1936. | In [[mathematics]] and [[computer science]], the {{lang for|de|'''Entscheidungsproblem'''|decision problem|paren=left}}; {{IPA|de|ɛntˈʃaɪ̯dʊŋspʁoˌbleːm|pron}}) is a challenge posed by [[David Hilbert]] and [[Wilhelm Ackermann]] in 1928.<ref>David Hilbert and Wilhelm Ackermann. Grundzüge der Theoretischen Logik. Springer, Berlin, Germany, 1928. English translation: David Hilbert and Wilhelm Ackermann. Principles of Mathematical Logic. AMS Chelsea Publishing, Providence, Rhode Island, USA, 1950</ref> It asks for an [[algorithm]] that considers an inputted statement and answers "yes" or "no" according to whether it is universally valid, i.e., valid in every [[Structure (mathematical logic)|structure]]. Such an algorithm was proven to be impossible by [[Alonzo Church]] and [[Alan Turing]] in 1936. | ||
| Line 19: | Line 20: | ||
Before the question could be answered, the notion of "algorithm" had to be formally defined. This was done by [[Alonzo Church]] in 1935 with the concept of "effective calculability" based on his [[lambda calculus|λ-calculus]], and by Alan Turing the next year with his concept of [[Turing machine]]s. Turing immediately recognized that these are equivalent [[model of computation|models of computation]]. | Before the question could be answered, the notion of "algorithm" had to be formally defined. This was done by [[Alonzo Church]] in 1935 with the concept of "effective calculability" based on his [[lambda calculus|λ-calculus]], and by Alan Turing the next year with his concept of [[Turing machine]]s. Turing immediately recognized that these are equivalent [[model of computation|models of computation]]. | ||
A negative answer to the {{lang|de|Entscheidungsproblem}} was then given by Alonzo Church in 1935–36 ('''Church's theorem'''<!--boldface per WP:R#PLA-->) and independently shortly thereafter by Alan Turing in 1936 ([[Turing's proof]]). Church proved that there is no [[computable function]] | A negative answer to the {{lang|de|Entscheidungsproblem}} was then given by Alonzo Church in 1935–36 ('''Church's theorem'''<!--boldface per WP:R#PLA-->) and independently shortly thereafter by Alan Turing in 1936 ([[Turing's proof]]). Church proved that there is no [[computable function]] that decides, for two given λ-calculus expressions, whether they are equivalent or not. He relied heavily on earlier work by [[Stephen Cole Kleene|Stephen Kleene]]. Turing reduced the question of the existence of an 'algorithm' or 'general method' able to solve the {{lang|de|Entscheidungsproblem}} to the question of the existence of a 'general method' that decides whether any given Turing machine halts or not (the [[halting problem]]). If 'algorithm' is understood as meaning a method that can be represented as a Turing machine, and with the answer to the latter question negative (in general), the question about the existence of an algorithm for the {{lang|de|Entscheidungsproblem}} also must be negative (in general). In his 1936 paper, Turing says: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0". | ||
The work of both Church and Turing was heavily influenced by [[Kurt Gödel]]'s earlier work on his [[Gödel's incompleteness theorem|incompleteness theorem]], especially by the method of assigning numbers (a [[Gödel numbering]]) to logical formulas in order to reduce logic to arithmetic. | The work of both Church and Turing was heavily influenced by [[Kurt Gödel]]'s earlier work on his [[Gödel's incompleteness theorem|incompleteness theorem]], especially by the method of assigning numbers (a [[Gödel numbering]]) to logical formulas in order to reduce logic to arithmetic. | ||
| Line 28: | Line 29: | ||
{{Main|Decidability (logic)#Decidability of a theory}} | {{Main|Decidability (logic)#Decidability of a theory}} | ||
Using the [[deduction theorem]], the Entscheidungsproblem encompasses the more general problem of deciding whether a given first-order sentence is | Using the [[deduction theorem]], the {{lang|de|Entscheidungsproblem}} encompasses the more general problem of deciding whether a given first-order sentence is a [[logical consequence]] of a given finite set of sentences, but validity in first-order theories with infinitely many axioms cannot be directly reduced to the {{lang|de|Entscheidungsproblem}}. Such more general decision problems are of practical interest. Some first-order theories are algorithmically [[decidability (logic)|decidable]]; examples of this include [[Presburger arithmetic]], [[real closed field]]s, and [[Type system#Static typing|static type systems]] of many [[programming language]]s. On the other hand, the first-order theory of the [[natural number]]s with addition and multiplication expressed by [[Peano axioms|Peano's axioms]] cannot be decided with an algorithm. | ||
== Fragments == | == 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> | 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 | The classical ''Entscheidungsproblem'' asks, 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. | 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. | ||
| Line 40: | Line 41: | ||
=== Aristotelian and relational === | === 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 | [[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 Aristotelian 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 Aristotelian 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)) \\ | \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)) | \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)) | ||
| Line 46: | Line 47: | ||
=== Arity === | === 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 [[ | 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). | 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 === | === 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 [[ | 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 and relation symbols, and no [[function symbol]]s. | ||
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. | 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: | The precise boundaries are known, sharply: | ||
| Line 59: | Line 60: | ||
* <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). | * <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). | * 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>\exists^* \forall^2 \exists^* </math> is decidable, proved independently by Gödel, [[Kurt Schütte|Schütte]], and [[László Kalmár|Kalmár]]. | ||
* <math>[\forall^2 \exists]_= </math> is undecidable. | * <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). | * 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= | ** 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=https://gdz.sub.uni-goettingen.de/id/PPN235181684_0099 |journal=[[Mathematische Annalen]] |language=de |volume=99 |issue=1 |pages=342–372 |doi=10.1007/BF01459101 |s2cid=122312654 |issn=0025-5831|url-access=subscription }}</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, 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). | * 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:// | ** 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://gdz.sub.uni-goettingen.de/id/PPN235181684_0100 |journal=Mathematische Annalen |language=de |volume=100 |issue=1 |pages=638–649 |doi=10.1007/BF01448869 |s2cid=119646624 |issn=1432-1807|url-access=subscription }}</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). | * 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). | ||
| Line 73: | Line 74: | ||
Having practical decision procedures for classes of logical formulas is of considerable interest for [[program verification]] and circuit verification. Pure Boolean logical formulas are usually decided using [[Boolean satisfiability problem|SAT-solving]] techniques based on the [[DPLL algorithm]]. | Having practical decision procedures for classes of logical formulas is of considerable interest for [[program verification]] and circuit verification. Pure Boolean logical formulas are usually decided using [[Boolean satisfiability problem|SAT-solving]] techniques based on the [[DPLL algorithm]]. | ||
For more general decision problems of first-order theories, conjunctive formulas over linear real or rational arithmetic can be decided using the [[simplex algorithm]], formulas in linear integer arithmetic ([[Presburger arithmetic]]) can be decided using [[Cooper's algorithm]] or [[William Pugh (computer scientist)|William Pugh]]'s [[Omega test]]. Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using [[satisfiability modulo theories|SMT-solving]] techniques, which combine SAT-solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of [[real closed field]]s, is decidable; this is the [[Tarski–Seidenberg theorem]], which has been implemented in computers by using the [[cylindrical algebraic decomposition]]. | For more general decision problems of first-order theories, conjunctive formulas over [[Linear function|linear]] real or rational arithmetic can be decided using the [[simplex algorithm]], formulas in linear integer arithmetic ([[Presburger arithmetic]]) can be decided using [[Cooper's algorithm]] or [[William Pugh (computer scientist)|William Pugh]]'s [[Omega test]]. Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using [[satisfiability modulo theories|SMT-solving]] techniques, which combine SAT-solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of [[real closed field]]s, is decidable; this is the [[Tarski–Seidenberg theorem]], which has been implemented in computers by using the [[cylindrical algebraic decomposition]]. | ||
== See also == | == See also == | ||
| Line 86: | Line 87: | ||
== References == | == References == | ||
* {{Cite book |last1=Hilbert |first1=David |title=Grundzüge der theoretischen Logik |last2=Ackermann |first2=Wilhelm |publisher=[[Springer-Verlag]] |year=1928 |isbn=0821820249 |language=de |trans-title=Principles of mathematical logic |author-link=David Hilbert |author-link2=Wilhelm Ackermann}} | * {{Cite book |last1=Hilbert |first1=David |title=Grundzüge der theoretischen Logik |last2=Ackermann |first2=Wilhelm |publisher=[[Springer-Verlag]] |year=1928 |isbn=0821820249 |language=de |trans-title=Principles of mathematical logic |author-link=David Hilbert |author-link2=Wilhelm Ackermann}} | ||
* [[Alonzo Church]], "An unsolvable problem of [[elementary number theory]]", American Journal of Mathematics, 58 (1936), pp 345–363 | * {{cite book | last=Ackermann |first=Wilhelm | location=Amsterdam | publisher=North-Holland | title=Solvable Cases of the Decision Problem | year=1954}} | ||
* [[Alonzo Church]], "An unsolvable problem of [[elementary number theory]]", [[American Journal of Mathematics]], 58 (1936), pp 345–363 | |||
* [[Alonzo Church]], "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), pp 40–41. | * [[Alonzo Church]], "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), pp 40–41. | ||
* {{Cite book |last=Davis |first=Martin |title=Engines of logic: mathematicians and the origin of the computer |date=2001 |publisher=Norton |isbn=978-0-393-32229-3 |edition=1. publ. as Norton paperback |series=Norton paperback |location=New York, NY London |author-link=Martin Davis (mathematician)}} | * {{Cite book |last=Davis |first=Martin |title=Engines of logic: mathematicians and the origin of the computer |date=2001 |publisher=Norton |isbn=978-0-393-32229-3 |edition=1. publ. as Norton paperback |series=Norton paperback |location=New York, NY London |author-link=Martin Davis (mathematician)}} | ||