Are Frege and extended Frege systems separated conclusively?

145 Views Asked by At

Buss in Propositional Proofs in Frege and Extended Frege Systems and Short Proofs of the Kneser-Lovasz Coloring Principle shows that propositional translations of Kneser-Lovasz Coloring Principle and truncated Tucker Lemma have extended Frege proofs with polynomial number of symbols and Frege proofs with only a quasi-polynomial number of symbols.

The first question is thus as follows.

Do these results rule out the possibility that a polynomial sized Frege proof exist or are quasi-polynomial proof sizes only an upper bound?

In the same papers (and earlier in Are there hard examples for Frege systems?) it is mentioned that Frege systems polynomially simulate extended Frege iff there are Frege proofs of $Con_{e\mathcal{F}}(n)$ formulas of polynomial size w.r.t. $n$.

The second question is, hence, as follows.

Have there been any attempts to assess the size of Frege proofs of $Con_{e\mathcal{F}}(n)$?