<p>In <a href="https://en.wikipedia.org/wiki/Propositional_proof_system">Cook-Reckhow propositional proof systems</a> 
proof checkers have to run in polynomial time 
w.r.t. the size of their input.
The size of the input is the size of the proof.</p>

<p>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 
<em>the accenting computations of that verifier $Q$ on a given input $\pi$</em> 
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$.</p>

<p>Note that without a restriction on the running time of the verifier 
the definition is not that useful: 
TAUT is in coNP and therefore 
has an exponential time deterministic algorithm 
which can directly check if a given propositional formula is a tautology.</p>

<p>The existence of a polynomially-bounded proof system is equivalent to
the existence of an NP algorithm for TAUT and therefore to NP=coNP.</p>

<p>Also note that in typical proof systems 
like those based on sequent calculus 
the proven formula is part of the proof 
so the size of the proof is an upper bound on the size of the proven formula.</p>

CC BY-SA 3.0
2016-02-09T07:05:33.667Z
2016-02-09T07:26:22.573Z
2016-02-09T07:26:22.573Z
Kaveh
<p>For the definition of a propositional proof system we have:</p>

<blockquote>
  <p>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(π)=τ.</p>
</blockquote>

<p>In regards to a polynomially-bounded propositional proof system, we have:</p>

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

<p>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?</p>

<p>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?</p>

CC BY-SA 3.0
2016-02-09T10:09:05.957Z
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
<cc.complexity-theory><lo.logic><proof-complexity>
On the difference between propositional proof system and polynomially-bounded proof system
Boolean_functions
# On the difference between propositional proof system and polynomially-bounded proof system

(Asked by: username_0 on 2016-02-09)

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?

**Tags:** cc.complexity-theory, lo.logic, proof-complexity

> **Comments:**
> **username_1**: 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$.  

---

## 1 answers

### Answer by username_1 on 2016-02-09. Score: 4

In [Cook-Reckhow propositional proof systems](https://en.wikipedia.org/wiki/Propositional_proof_system)
proof checkers have to run in polynomial time
w.r.t. the size of their input.
The size of the input is the size of the proof.

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$.

Note that without a restriction on the running time of the verifier
the definition is not that useful:
TAUT is in coNP and therefore
has an exponential time deterministic algorithm
which can directly check if a given propositional formula is a tautology.

The existence of a polynomially-bounded proof system is equivalent to
the existence of an NP algorithm for TAUT and therefore to NP=coNP.

Also note that in typical proof systems
like those based on sequent calculus
the proven formula is part of the proof
so the size of the proof is an upper bound on the size of the proven formula.


---

