Proofs in Computer Science (Optional) · Computability Theory

Lesson 2

Nikolai Chukhin · Alexander S. Kulikov

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.