1
$\begingroup$

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."?
$\endgroup$
  • 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$ – Yuval Filmus Oct 17 '15 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 '15 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$ – Yuval Filmus Oct 17 '15 at 19:08
1
$\begingroup$

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.

$\endgroup$
  • $\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 '15 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$ – Yuval Filmus Oct 17 '15 at 21:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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