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
Lower Bounds for Frege and Extended Frege
proof complexity
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 Krajeks Bounded arithmetic, propositional logic, and complexity theory for Frege systems, but the argument works for extended Frege systems as well.3) Its 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.