<p>1, 2, 4) The best known lower bounds on extended Frege are the same as for Frege: linear number of lines, and quadratic size. This applies e.g. to the tautologies $\neg^{2n}\top$ (basically, any tautology that is not a substitution instance of a shorter tautology, and whose sum of lengths of all subformulas is quadratic). This is proved in Krajíček’s <em>Bounded arithmetic, propositional logic, and complexity theory</em> for Frege systems, but the argument works for extended Frege systems as well.</p>

<p>3) It’s not entirely clear to me how exactly you define tree-like extended Frege (there has to be a mechanism allowing reuse of extension axioms), but I am not aware of any superlinear lower bounds on the number of lines in treelike Frege or extended Frege systems.</p>

CC BY-SA 3.0
2016-03-10T14:11:48.240Z
Can't you define Extended Frege as Circuit Frege (in your APAL 2004 paper)? And thus tree like circuit Frege definition is immediate.
Iddo Tzameret
CC BY-SA 3.0
2016-03-10T14:14:59.070Z
@Iddo: I can, but I can also define it in several other ways, and it’s not entirely clear their numbers of lines will be the same in this strict regime (linear).
Emil Jeřábek
CC BY-SA 3.0
2016-03-10T14:15:01.740Z
Also, I think that for extended Frege the size  lower bound is only linear and not quadratic, right?
Iddo Tzameret
CC BY-SA 3.0
2016-03-10T14:16:55.110Z
No, that’s the point I’m trying to get across. The quadratic  lower bound holds for extended Frege, even if it’s not commonly stated that way.
Emil Jeřábek
CC BY-SA 3.0
2016-03-10T14:19:52.220Z
I thought it is quadratic only if you define the size of extended Frege by counting the number of ( distinct) subformulas. But the actual size is linear. I will have to revisit the proof then...
Iddo Tzameret
CC BY-SA 3.0
2016-03-10T14:24:04.320Z
The size of a proof is defined as the sum of sizes of all lines (formulas or circuits, as applicable). You don’t a priori include the sizes of all their subformulas, nevertheless structural properties of the proof system imply that the size is in this case at least linear in the sum of the sizes of subformulas of the target formula.
Emil Jeřábek
CC BY-SA 3.0
2016-03-10T14:28:02.190Z
Basically, the result says that the optimal proof of the formula I gave as an example goes as $\top,\neg\neg\top,\neg^4\top,\dots,\neg^{2n}\top$ (with missing bits filled in if $\phi/\neg\neg\phi$ is not a basic rule of inference).
Emil Jeřábek
CC BY-SA 3.0
2016-03-09T19:45:06.453Z
2016-03-09T19:45:06.453Z
Emil Jeřábek
<p>Wikipedia [1] states that the best known lower bound for size of Frege proofs is quadratic, and that there is no known superlinear lower bounds for the number of lines of Frege proofs.</p>

<p>Questions: </p>

<p>1) What is the best known lower bound for the number of lines of extended Frege proofs? </p>

<p>2) What is the best known lower bound for the size of extended Frege proofs? Is it still quadratic as in Frege? </p>

<p>3) Tree-like Extended Frege can simulate DAG-like Extended Frege in a polynomial number of steps. Are there any superlinear lower bounds for size/number of lines on tree-like extended Frege? </p>

<p>4) What are the tautologies that lead to the linear lower bound for number of lines and to the quadratic lower bound for the size in Frege proofs as stated at wikipedia? </p>

<p>Obs: I'm aware of the fact that for constant depth Frege we have size lower bounds of the order of $2^{\Omega(n^{6^{-d}})}$. But I'm really interested in full power Frege and Extended Frege. </p>

<p>[1] <a href="https://en.wikipedia.org/wiki/Frege_system">https://en.wikipedia.org/wiki/Frege_system</a></p>

<proof-complexity>
Lower Bounds for Frege and Extended Frege
verifying
# Lower Bounds for Frege and Extended Frege

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

Wikipedia [1] states that the best known lower bound for size of Frege proofs is quadratic, and that there is no known superlinear lower bounds for the number of lines of Frege proofs.

Questions:

1) What is the best known lower bound for the number of lines of extended Frege proofs?

2) What is the best known lower bound for the size of extended Frege proofs? Is it still quadratic as in Frege?

3) Tree-like Extended Frege can simulate DAG-like Extended Frege in a polynomial number of steps. Are there any superlinear lower bounds for size/number of lines on tree-like extended Frege?

4) What are the tautologies that lead to the linear lower bound for number of lines and to the quadratic lower bound for the size in Frege proofs as stated at wikipedia?

Obs: I'm aware of the fact that for constant depth Frege we have size lower bounds of the order of $2^{\Omega(n^{6^{-d}})}$. But I'm really interested in full power Frege and Extended Frege.

[1] <https://en.wikipedia.org/wiki/Frege_system>

**Tags:** proof-complexity

---

## 1 answers

### Answer by username_1 on 2016-03-09. Score: 15 | Accepted answer

1, 2, 4) The best known lower bounds on extended Frege are the same as for Frege: linear number of lines, and quadratic size. This applies e.g. to the tautologies $\neg^{2n}\top$ (basically, any tautology that is not a substitution instance of a shorter tautology, and whose sum of lengths of all subformulas is quadratic). This is proved in Krajíček’s *Bounded arithmetic, propositional logic, and complexity theory* for Frege systems, but the argument works for extended Frege systems as well.

3) It’s not entirely clear to me how exactly you define tree-like extended Frege (there has to be a mechanism allowing reuse of extension axioms), but I am not aware of any superlinear lower bounds on the number of lines in treelike Frege or extended Frege systems.

> **Comments:**
> **username_2**: Can't you define Extended Frege as Circuit Frege (in your APAL 2004 paper)? And thus tree like circuit Frege definition is immediate.  
> **username_1**: @Iddo: I can, but I can also define it in several other ways, and it’s not entirely clear their numbers of lines will be the same in this strict regime (linear).  
> **username_2**: Also, I think that for extended Frege the size  lower bound is only linear and not quadratic, right?  
> **username_1**: No, that’s the point I’m trying to get across. The quadratic  lower bound holds for extended Frege, even if it’s not commonly stated that way.  
> **username_2**: I thought it is quadratic only if you define the size of extended Frege by counting the number of ( distinct) subformulas. But the actual size is linear. I will have to revisit the proof then...  
> **username_1**: The size of a proof is defined as the sum of sizes of all lines (formulas or circuits, as applicable). You don’t a priori include the sizes of all their subformulas, nevertheless structural properties of the proof system imply that the size is in this case at least linear in the sum of the sizes of subformulas of the target formula.  
> **username_1**: Basically, the result says that the optimal proof of the formula I gave as an example goes as $\top,\neg\neg\top,\neg^4\top,\dots,\neg^{2n}\top$ (with missing bits filled in if $\phi/\neg\neg\phi$ is not a basic rule of inference).  

---

