Proofs in Computer Science (Optional) · Computability Theory
Lesson 2
A proof system for a language \(L\) is an algorithm \(S(x,w)\) that halts on every input and outputs “1” if and only if \(w\) is a proof that \(x \in L\). What exactly we call a proof here is explained by the following two requirements that we impose on the proof system:
- Completeness: for any \(x \in L\), there exists \(w\) such that \(S(x,w)=1\).
- Soundness: for any \(x \not \in L\) and any \(w\), it holds that \(S(x,w)=0\).
Languages for which there exist a proof systems are called recursively enumerable. In some case, it is convenient not to first describe a language, and then argue that it has a proof system, but to directly define a language by its proof system.