Proofs in Computer Science (Optional) · Computability Theory
Lesson 4
Enumerability is a natural property of languages. Another natural and stronger property is decidability. A language \(L\) is called decidable if there is an algorithm that outputs 1 for \(x \in L\), and outputs 0 for \(x \not \in L\). Thus, we require that the algorithm halts on any input and outputs either one or zero. The property is indeed stronger: if there is a deciding algorithm \(C\) for the language \(L\), then there is also a proof system \(S\) in which each \(x \in L\) has an empty proof \(w=\varepsilon\): \(S(x,\varepsilon)\) simply runs the algorithm \(C\).
It is natural to ask: are there languages that are enumerable but not decidable? One of the classic examples of such a language is the halting problem: given an algorithm \(A\) and input \(x\), determine whether \(A\) halts on \(x\). The corresponding language is defined as follows: \[H=\{(A,x) \colon A(x)\text{ halts}\} \ .\] It is easy to see that \(H\) is enumerable: one iterates over all triples \((A,x,i)\) (for example, in order of increasing total length) and runs \(A\) on \(x\) for \(i\) steps; if the algorithm halts, one prints \((A,x)\). At the same time, this language is undecidable, as proven by Alan Turing in 1937.