I am studying the lecture The Complexity of Propositional Proofs. ​Here there is a definition together with a discussion (page 3). I don't understand that discussion.

Let $F$ denote the set of propositional formulas over the connectives $\wedge$, $\vee$, $\rightarrow$ and $\lnot$, with a countably infinite supply of propositional variables. An abstract propositional proof system is a polynomial time function $V: F \times \{0,1\}^* \to \{0,1\}$ such that for every tautology $\tau$ there is a proof $P \in \{0,1\}^*$ with $V(\tau, P) = 1$ and for every non-tautology $\tau$, for every $P$, $V(\tau, P)=0$. The size of the proof is $|P|$.

Definition equates propositional proof systems with non-deterministic algorithms for the language of tautologies.

  • Why does the author conclude "Definition equates propositional proof systems with non-deterministic algorithms for the language of tautologies."?
  • 1
    $\begingroup$ This is already your second question on this rather long survey, and you're only on page 3. If there is anything else you don't understand I suggest you either skip it or try to find the answer yourself in other (offline) sources. Also, this survey is perhaps not the easiest first resource to use for studying the area, as its aim is more presenting the cutting edge rather than the basics. $\endgroup$ Oct 17, 2015 at 14:00
  • $\begingroup$ @YuvalFilmus thanks by your attention, Do you know an first resource for studying this area, I am looking in google, but the notations and terms are are confused. $\endgroup$
    – juaninf
    Oct 17, 2015 at 14:11
  • $\begingroup$ Notations and terms are not necessarily standard, so it might be best to stick to one source to start with. There should be some lecture notes around, keep looking. $\endgroup$ Oct 17, 2015 at 19:08

1 Answer 1


An algorithm computing $V$ can be thought of as a non-deterministic algorithm which gets only the first parameter $\tau$ and guesses $P$, verifying that $P$ is a proof of $\tau$.

If you've ever seen the definition of NP using witnesses, in this definition $V$ is accepts the language of all tautologies $\tau$ with proofs in a certain proof system. The witness that such a proof exists is the proof itself $P$, and the function $V$ verifies that the proof is valid for $\tau$.

Another equivalent way of defining a proof system is as a polynomial time function which accepts a proof $P$ and outputs a proposition $\tau$. The two properties satisfied by such a system $S$ is (i) for all $P$, $S(P)$ is a tautology, (ii) for every tautology $\tau$ there exists a proof $P$ such that $S(P) = \tau$. It is an easy exercise to convert between the two definitions.

If you want to learn more, look up Cook–Reckhow proof system.

  • $\begingroup$ I think so, that the defintion of $V$ is similar of equal to one definition of NP problems of wikipedia "Intuitively, NP is the set of all decision problems for which the instances where the answer is "yes" have efficiently verifiable proofs of the fact that the answer is indeed "yes"" $\endgroup$
    – juaninf
    Oct 17, 2015 at 21:16
  • $\begingroup$ One big difference is that the witness here is not constrained to be polynomial size. In fact, if there were a proof system in which every tautology had a polynomial size proof then NP=coNP; in fact the two conditions are equivalent! $\endgroup$ Oct 17, 2015 at 21:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.