User:IssaRice/Computability and logic/Entscheidungsproblem: Difference between revisions
No edit summary |
|||
| Line 19: | Line 19: | ||
| In terms of semantic implication || Semantic || Take as input a set of sentences <math>\Gamma</math> and a sentence <math>\phi</math> (both of first-order logic), and decide whether <math>\Gamma</math> semantically implies (a.k.a. logically implies) <math>\phi</math>. | | In terms of semantic implication || Semantic || Take as input a set of sentences <math>\Gamma</math> and a sentence <math>\phi</math> (both of first-order logic), and decide whether <math>\Gamma</math> semantically implies (a.k.a. logically implies) <math>\phi</math>. | ||
|} | |} | ||
==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== | ==See also== | ||
* [[wikipedia:Entscheidungsproblem]] | * [[wikipedia:Entscheidungsproblem]] | ||
Revision as of 00:47, 9 February 2019
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".
| 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 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
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.