# On the difference between propositional proof system and polynomially-bounded proof system

For the definition of a propositional proof system we have:

An abstract proof system is a polynomial time function f whose range is equal to the set of tautologies. If τ is a tautology, then an f-proof of τ is any value π such that f(π)=τ.

In regards to a polynomially-bounded propositional proof system, we have:

If τ is a tautology, then an f-proof of τ is any value π such that f(π)=τ and |π| $\leq$ f(τ).

My question is in regards to a regular propositional proof system, does the function need to run in polynomial-time relative to any particular value? What is the polynomial in terms of?

Am I understanding it right, that the polynomial can in fact be in terms of any number, whereas a polynomial-bounded proof system would have the polynomial be in terms of the value of the size of the given tautology?

• Could you explain "if we have a proof verifier algorithm Q that does not run in polynomial time we can define a new proof verifier algorithm Q′ which accepts the accenting computations of that verifier Q on a given input π as proofs" a bit more, please? Or do you have any reading suggestions corresponding to that statement? – user37484 Feb 9 '16 at 7:50
• Think about Q as a Turing machine. It is straight forward to design a new Turing machine that given strings $\pi$ and $\pi'$ checks if $\pi'$ encodes a computation of Turing machine $Q$ on the input $\pi$ and halts and accepts. That is your $Q'$. In other words, a $Q'$-proof is simply an accepting computation of $Q$. – Kaveh Feb 9 '16 at 10:09

This is generally not a restriction: if we have a proof verifier algorithm $Q$ that does not run in polynomial time we can define a new proof verifier algorithm $Q'$ which accepts the accenting computations of that verifier $Q$ on a given input $\pi$ as proofs. The verifier $Q'$ is computable in polynomial time. The trade-off is that the proof in $Q'$ can be much larger than those in $Q$. E.g. if $Q$ was an exponential time algorithm and $\pi$ was a $Q$-proof for $\varphi$ then there is a $\pi'$ which is a $Q'$ proof for $\varphi$ which consists of the computation of $Q$ on $\pi$. Since the running of $Q$ is exponential the size of $\pi'$ is bounded by an exponential in the size of the original proof $\pi$.