# User:IssaRice/Computability and logic/Entscheidungsproblem

From Machinelearning

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

## Equivalent formulations

Some things to note:

- A relation is "decidable" means that there is some algorithm such that if is true, then the algorithm outputs "yes", and if is false, then the algorithm outputs "no".
- Deciding is different from semi-deciding (a.k.a. recognizing).

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 finite set of sentences and a sentence (both of first-order logic), and decide whether semantically implies (a.k.a. logically implies) . |

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

The question of decidability (i.e. is this thing decidable or undecidable?) can be asked of both logics/formal systems and of theories. This is similar to how both soundness and completeness can be asked of logics and theories (and why we have both the completeness theorem and the incompleteness theorems!).

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.