User:IssaRice/Computability and logic/Entscheidungsproblem
The Entscheidungsproblem, also called Hilbert's decision problem is a problem in mathematical logic.
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 of a finite set of sentences||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) .||This is version can be used (where is the set of axioms of Robinson arithmetic or the group axioms) 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 and a sentence (both of first-order logic), and decide whether there is a proof from to .||Again, this follows from Godel's completeness theorem applied to the previous row.|
Note: I don't think undecidability of semantic implication for arbitrary-sized sets is equivalent.
For equivalence of the problems of deciding satisfiability and validity, see exercises 1 and 2 in https://www.cs.nmsu.edu/historical-projects/Projects/FoLundecidability.pdf
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.
Decidability for a theory vs negation-completeness for a theory
Since there are many different equivalent formulations of the Entscheidungsproblem, we can prove any of them to get the result.
Main strategies for proofs:
- Prove the undecidability of a finitely axiomatized theory (e.g. Robinson arithmetic or group axioms); this proves the finite set implication version. Peter Smith's Godel book does this in theorem 40.3.
- Reduce it to the halting problem. This can prove several of the versions, including the finite set implication version and the satisfiability one. Boolos/Burgess/Jeffrey book does it this way.