Proofs in Computer Science (Optional) · Computability Theory

Lesson 3

Nikolai Chukhin · Alexander S. Kulikov

It is not true that every language has a proof system. This is just because there are “more” languages than proof systems: the set of proof systems is countable, whereas the set of languages is not.

In the literature, a more commonly used definition of enumerability is: a language is enumerable if there exists an algorithm that prints all elements of this language and only them. It is easy to see that this definition is equivalent to the one introduced above. Indeed, if a language has a proof system \(S\), then there is also an enumerating algorithm: this algorithm iterates over pairs \((x,w)\) (say, in order of increasing input size) and prints those \(x\) for which \(S(x,w)=1\). Conversely, if there is an enumerating algorithm \(E\), then there is also a proof system \(S\): as a proof \(w\) for a string \(x \in L\), one can take, for example, the number of steps after which \(E\) prints \(x\); the algorithm \(S\) then simply runs the algorithm \(E\) for the required number of steps and verifies that the string \(x\) is printed. (Recall that the algorithm \(E\) may potentially never terminate. For this reason, we use the number of steps as a parameter above.)