Difference between revisions of "Entscheidungsproblem"
Karl Jones (Talk | contribs) (First) |
Karl Jones (Talk | contribs) |
||
| Line 1: | Line 1: | ||
In [[mathematics]] and [[computer science]], the '''''Entscheidungsproblem''''' (pronounced [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm], German for 'decision problem') is a challenge posed by [[David Hilbert]] in 1928. | In [[mathematics]] and [[computer science]], the '''''Entscheidungsproblem''''' (pronounced [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm], German for 'decision problem') is a challenge posed by [[David Hilbert]] in 1928. | ||
| − | The ''Entscheidungsproblem'' asks for an algorithm that takes as input a statement of a first-order logic (possibly with a finite number of axioms beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms. | + | The ''Entscheidungsproblem'' asks for an [[algorithm]] that takes as input a statement of a first-order logic (possibly with a finite number of axioms beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms. |
By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the ''Entscheidungsproblem'' can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic. | By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the ''Entscheidungsproblem'' can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic. | ||
| Line 11: | Line 11: | ||
== See also == | == See also == | ||
| + | * [[Algorithm]] | ||
* [[Alonzo Church|Church, Alonzo]] | * [[Alonzo Church|Church, Alonzo]] | ||
* [[Lambda calculus]] | * [[Lambda calculus]] | ||
Revision as of 17:21, 20 August 2015
In mathematics and computer science, the Entscheidungsproblem (pronounced [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm], German for 'decision problem') is a challenge posed by David Hilbert in 1928.
The Entscheidungsproblem asks for an algorithm that takes as input a statement of a first-order logic (possibly with a finite number of axioms beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms.
By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic.
In 1936, Alonzo Church and Alan Turing published independent papers showing that a general solution to the Entscheidungsproblem is impossible, assuming that the intuitive notion of "effectively calculable" is captured by the functions computable by a Turing machine (or equivalently, by those expressible in the lambda calculus).
This assumption is now known as the Church–Turing thesis.
See also
External links
- Entscheidungsproblem @ Wikipedia
