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

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

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

<blockquote>
  <p>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|)$.</p>
</blockquote>

<p>As you can see there is no mention of other proof systems.</p>

<p>If you want the more general definitions look at <a href="https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf" rel="nofollow">Reckhow's thesis</a>.
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: </p>

<blockquote>
  <p>If we have a complete set of connectives 
  we can express in polynomial size the <em>truth</em> of formulas 
  based on another finite set of Boolean connectives.</p>
</blockquote>

<p>For more see the section in <a href="https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf" rel="nofollow">Reckhow's thesis</a> 
discussing polynomial simulation 
between proof systems with different class of formulas.</p>

CC BY-SA 3.0
2016-03-12T23:38:52.960Z
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.
Boolean_functions
CC BY-SA 3.0
2016-03-12T23:39:01.380Z
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
Boolean_functions
CC BY-SA 3.0
2016-03-12T23:49:18.147Z
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?
Boolean_functions
CC BY-SA 3.0
2016-03-12T23:50:17.367Z
Ok, so I'm just not clearly getting the definitions. But your post is helping.
Boolean_functions
CC BY-SA 3.0
2016-03-13T00:09:21.027Z
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?
Boolean_functions
CC BY-SA 3.0
2016-03-13T00:13:18.153Z
@Boolean_functions, that is correct.
Kaveh
CC BY-SA 3.0
2016-03-12T23:31:46.843Z
2016-03-14T05:30:11.617Z
2016-03-14T05:30:11.617Z
Kaveh
<p>In the book 'Logical Foundations of Proof Complexity', co-authored by Stephen Cook, the following definition is given:</p>

<p>A proof-system $F$ is said to be <em>polynomially-bounded</em> 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.</p>

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

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

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

<p>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 <em>this</em> formula has a short proof in B?</p>

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

CC BY-SA 3.0
2016-03-12T23:20:17.360Z
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?
Boolean_functions
CC BY-SA 3.0
2016-03-12T23:31:25.003Z
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
Boolean_functions
<cc.complexity-theory><lo.logic><computability><open-problem><proof-complexity>
In regards to the tautologies of a polynomially-bounded propositional proof system
Boolean_functions
# In regards to the tautologies of a polynomially-bounded propositional proof system

(Asked by: username_0 on 2016-03-12)

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?

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

> **Comments:**
> **username_0**: 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?  
> **username_0**: 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  

---

## 1 answers

### Answer by username_1 on 2016-03-12. Score: 2 | Accepted answer

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](https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf).
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](https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf)
discussing polynomial simulation
between proof systems with different class of formulas.

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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  
> **username_0**: 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?  
> **username_0**: Ok, so I'm just not clearly getting the definitions. But your post is helping.  
> **username_0**: 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?  
> **username_1**: @username_0, that is correct.  

---

