Page "Entscheidungsproblem" Paragraph 0

In mathematics and computer science, the (, German for ' decision problem ') is a challenge posed by David Hilbert in 1928.

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