Difference between revisions of "User:IssaRice/Computability and logic/Entscheidungsproblem"

From Machinelearning
Jump to: navigation, search
(Equivalent formulations)
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 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