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

From Machinelearning
Jump to: navigation, search
(Equivalent formulations)
Line 1: Line 1:
'''Entscheidungsproblem''', also called '''Hilbert's decision problem''' is a problem in mathematical logic.
+
The '''Entscheidungsproblem''', also called '''Hilbert's decision problem''' is a problem in mathematical logic.
  
 
==Equivalent formulations==
 
==Equivalent formulations==
Line 28: Line 28:
  
 
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.
 
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.
 +
 +
==Proofs==
 +
 +
Since there are many different equivalent formulations of the ''Entscheidungsproblem'', we can prove any of them to get the result.
  
 
==See also==
 
==See also==

Revision as of 04:24, 9 February 2019

The 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".
  • 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 of a finite set of sentences Semantic Take as input a finite 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. This is version can be used (where \Gamma is the set of axioms of Robinson arithmetic[1] or the group axioms)[2] to show that first-order logic is undecidable.
In terms of provability from a finite set of sentences Syntactic Take as input a finite set of sentences \Gamma and a sentence \phi (both of first-order logic), and decide whether there is a proof from \Gamma to \phi. Again, this follows from Godel's completeness theorem applied to the previous row.

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.

Proofs

Since there are many different equivalent formulations of the Entscheidungsproblem, we can prove any of them to get the result.

See also

References