In regards to the tautologies of a polynomially-bounded propositional proof system

Question

In the book 'Logical Foundations of Proof Complexity', co-authored by Stephen Cook, the following definition is given:

A proof-system $F$ is said to be polynomially-bounded if there is a polynomial p(n) such that for all tautologies $A$, there is a proof $X$ of $A$ in $F$ such that |x| $\leq$ p(|A|). Informally, a proof system is polynomially-bounded if every tautology has a short proof in F.

My question is in regards to what "all tautologies" means. Is it in regards to every tautology in $F$ or any tuatology in in any adequate proof system, which first needs to be converted to an equivalent formula in $F$?

For example, let's say we are dealing with 2 very different proof-systems, A and B. Let's just assume for the moment that B is polynomially-bounded. Then every tautology in B has a short proof.

My question is: Given a tautology in system A--denoted as $\phi$--, is it necessary that the conversion from $\phi$ in A to its equivalent formula $\phi'$ in B happens in polynomial-time?

Or is the only thing that is necessary for B to be considered a polynomially-bounded proof system this: that once $\phi$ is represented in the system B (regardless of how long this conversion takes place), then this formula has a short proof in B?

So if it was inefficient to convert $\phi$ to $\phi'$, yet $\phi'$ nonetheless still had a short proof in system B, is B still considered a polynomially-bounded proof system?

Answer 1

Your question is like asking what is the class of formulas for the problem SAT? In the definition of SAT it is fixed to some fixed class, say those based on $\{\lnot, \land, \lor\}$ but it doesn't really matter usually whether we talk about formulas based on $\{\lnot, \land, \lor\}$ or $\{\bot, \to \}$ or any other complete set of Boolean connectives. Therefore it is often not explicitly stated. The reason is they can simulate each other with at most polynomial increase in the size of formulas. Therefore it is often not explicitly mentioned. If we pick an unusual one then things might be completely different. E.g. DNF-SAT is in P, but this does not mean SAT is in P. Similarly CNF-TAUT is in P and therefore if we define the concept of proof system for CNF-TAUT it has polynomially bounded proof system. But again this does not mean that TAUT has polynomially bounded proof system. The problem we are interested in is TAUT, not CNF-TAUT. We want a polynomially bounded proof system for TAUT.

For the definition of proof system we have to similarly fix the class of tautologies. If we pick different classes we get different definitions. TAUT being the dual to SAT it is natural to take the dual of the formulas for SAT (i.e. formulas based on connectives $\{\lnot, \land, \lor\}$). It is also common to use DNF-TAUT as a dual to CNF-SAT (there is a simple reduction from SAT to CNF-SAT using new extension variables such that the set of satisfying assignments of the original formula and resulting CNF are P-isomorphic). But as long as we can efficiently express DNF formulas it usually does not matter what we use. It can be linear equations, or any class of computational objects as long as they can express DNFs with at most a polynomial increase in size. If that is not the case then the system is trivially not polynomially bounded as it is not a proof system for TAUT (or DNF-TAUT). The book does not deal with cases where the class of formulas does not contain DNFs.

For the purpose of the book you can assume that the class of propositional formulas contains DNFs and every tautology means every DNF tautology.

A proof system $Q$ is polynomially bounded if there is a polynomial $p$ such that for every DNF tautology $\varphi$ there is a $Q$-proof $\pi$ such that $|\pi| \leq p(|\varphi|)$.

As you can see there is no mention of other proof systems.

If you want the more general definitions look at Reckhow's thesis. Reckhow looks at the more general definition with different set of connectives and classes of formulas. He shows that any two Frege systems polynomially simulate each other as long as we have a complete set of Boolean connectives. I think the simplest way to explain it is as follows:

If we have a complete set of connectives we can express in polynomial size the truth of formulas based on another finite set of Boolean connectives.

For more see the section in Reckhow's thesis discussing polynomial simulation between proof systems with different class of formulas.