10
$\begingroup$

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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
15
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ Can't you define Extended Frege as Circuit Frege (in your APAL 2004 paper)? And thus tree like circuit Frege definition is immediate. $\endgroup$
    – Iddo Tzameret
    Commented Mar 10, 2016 at 14:11
  • 1
    $\begingroup$ @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). $\endgroup$
    – Emil Jeřábek
    Commented Mar 10, 2016 at 14:14
  • 2
    $\begingroup$ Also, I think that for extended Frege the size lower bound is only linear and not quadratic, right? $\endgroup$
    – Iddo Tzameret
    Commented Mar 10, 2016 at 14:15
  • 2
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Mar 10, 2016 at 14:16
  • 1
    $\begingroup$ 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... $\endgroup$
    – Iddo Tzameret
    Commented Mar 10, 2016 at 14:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.