User:IssaRice/Computability and logic/Entscheidungsproblem

Entscheidungsproblem, also called Hilbert's decision problem is a problem in mathematical logic.

Equivalent formulations

Some things to note:

• A relation $R$ is "decidable" means that there is some algorithm such that if $R(x)$ is true, then the algorithm outputs "yes", and if $R(x)$ is false, then the algorithm outputs "no".

Label	Syntactic or semantic	Statement	Notes
In terms of validity	Semantic	Take as input a sentence of first-order logic, and decide whether it is valid (a.k.a. universally valid, true-in-every-interpretation).
In terms of provability	Syntactic	Take as input a sentence of first-order logic, and decide whether it is provable (using only logical axioms).	By Godel's completeness theorem, validity and provability are equivalent.
In terms of satisfiability	Semantic	Take as input a sentence of first-order logic, and decide whether it is satisfiable.
In terms of semantic implication	Semantic	Take as input a set of sentences $\Gamma$ and a sentence $\phi$ (both of first-order logic), and decide whether $\Gamma$ semantically implies (a.k.a. logically implies) $\phi$.

Decidability for first-order logic versus decidability for a particular theory

Even though first-order logic is undecidable, a particular first-order theory (i.e. a theory specified in first-order logic via some non-logical axioms) may still be decidable.

See also

• wikipedia:Entscheidungsproblem