0
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ So a proof system, B, whose WFFs are such that DNF is not permitted, yet whose tautologies--given in the system of B--are easily proven, would not constitute a polynomially bounded proof system? $\endgroup$ – Boolean_functions Mar 12 '16 at 23:20
  • $\begingroup$ From your answer, I believe that yes there is? The system needs to be able to represent formulas in DNF? I'm trying to understand to what specifically does this definition apply, Thanks $\endgroup$ – Boolean_functions Mar 12 '16 at 23:31
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I appreciate your response. However, I am asking in regards to a hypothetical system--one which would be vastly different from a typical Frege system. One which is functionally complete (in the sense that every boolean function can be expressed) and meets the definition of propositional-proof system, but does not p-simulate any other Frege system. Additionally, this system would be such that its tautologies can be efficiently proved within the system, yet representing these formulas in CNF/DNF would not constitute a WFF in the system. And converting them to such a system, is inefficient. $\endgroup$ – Boolean_functions Mar 12 '16 at 23:38
  • $\begingroup$ Would this system constitute a poloynmially-bounded proof system? In regards to the definition of the problem, I have always seen it posed as simply: given a system (which meets the definition of propositional proof system) if (informally) every tautology has a short proof, then it is polynomially-bounded. I appreciate you going over this, thanks $\endgroup$ – Boolean_functions Mar 12 '16 at 23:39
  • $\begingroup$ Ok, your edits and explicit definitions are starting to make sense. Thank you. Another question though. In regards to your def of a polynomially-bounded proof system $Q$: Assume that there is a propositional-proof-system $F$ such that any DNF formula $\phi$ (in some other system)--after being converted to a formula in the system $F$--has a short proof in $F$. Now assume that the conversion form the arbitray DNF formula to its equivalent formula in $F$ can not be done efficiently. Would F consitute a polynomially-bounded proof system? $\endgroup$ – Boolean_functions Mar 12 '16 at 23:49
  • $\begingroup$ Ok, so I'm just not clearly getting the definitions. But your post is helping. $\endgroup$ – Boolean_functions Mar 12 '16 at 23:50
  • $\begingroup$ OK, your answers make sense. Thanks for the time. So basically I had not understood what TAUT was meaning? TAUT is not just a class of tautologies for some propositional logic, but a class of tautologies for some logic, while represented in DNF form? $\endgroup$ – Boolean_functions Mar 13 '16 at 0:09

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.