3. The Entscheidungsproblem

The Entscheidungsproblem

The Entscheidungsproblem (The Decision Problem) is a machine that:

• Given an input of a Predicate formula $F$
• Gives an output of true if and only if $F$ is a tautology.

Link to original

Theorem: The Entscheidungsproblem is undecidable

Theorem: the Entscheidungsproblem is undecidable. Proof:

1. In the proof of the Cook-Levin Theorem, for a given machine $M$ and input word $W$, we constructed a propositional formula $F_{M,w}$ such that: $F_{M,w}\text{ is satisfiable}⟺M\text{ accepts }w\text{ within a polynomial number of steps}$
2. But, we cannot express global properties such as “the machine $M$ will eventually accept” without infinitely long disjunctions. (this would not be a well formed formula as they need to be finite)
3. However, with a suitable choice of symbols, lets take $S_q(t)=\text{machine is in state }q\text{ at time }t$. We can express this using a universal quantifier: $\exists t{S}_q(t)$.
4. Hence we can write down a formula $F_{M,w}$ in predicate logic such that: $F_{M,w}\text{ is satisfiable}\iff M\text{ eventually accepts input }w$
5. As there is no algorithm that can solve the accepting problem for Turing Machines, the Entscheidungsproblem is also undecidable as required.