Frege proof lower bounds

“If two statements are both true, the first is true” holds for every choice of true or false values. Such an always-true statement is a tautology. A Frege system proves these statements by writing a sequence of formulas, each justified by a fixed logical rule. For example, once that first statement is proved, it remains true even if we add “provided a third statement is true.” The question is whether we can specify a growing family of short tautologies for which every Frege proof needs far more writing than any fixed power of the statement length, such as a square or cube. The proof may use arbitrarily nested formulas.[1] [2] [3]

Can short, always-true statements inevitably require very long formal explanations in unrestricted Frege reasoning? Propositional variables take true or false values; a tautology is true under every assignment. To illustrate a legal derivation, use Buss’s stated axiom system, writing $\to$ for implication and $\land$ for “and.” It includes the templates $(A\land B)\to A$ and $A\to(B\to A)$, and modus ponens: from $A$ and $A\to B$, infer $B$. The following proof has two axiom instances followed by one application of that rule:$$\begin{aligned}(1)&\quad (p\land q)\to p\\(2)&\quad ((p\land q)\to p)\to\bigl(r\to((p\land q)\to p)\bigr)\\(3)&\quad r\to((p\land q)\to p).\end{aligned}$$The size includes all three written formulas, not just the number of inference steps. This easy example proves no lower bound. The target is an explicit family $\tau_n$ whose statement length is polynomial in $n$, but whose minimum total encoded Frege proof length has no polynomial bound. A polynomial bound is $O(n^k)$ for some fixed $k$; superpolynomial size rules out every such fixed exponent. Formula depth—the number of nested logical operations—may grow without a fixed cap.[1] [2] [3]

This remains open for unrestricted Frege proofs.[1]

The June 2026 algebraic bit-size lower bound concerns another proof system. Bounded-depth Frege results likewise leave arbitrary-depth Frege proof size unresolved.[1]

An exhaustive truth table establishes that a statement is always true by listing every setting of its variables. A formal proof can instead expose a short reason that covers them all. Proof length measures whether this explanation stays compact as the statement grows. A lower bound would reveal an unavoidable cost of justification in a powerful logical calculus, even when a researcher chooses the best possible deductions; a slow proof-search program alone cannot show that.[1] [2] [3]

Completeness ensures that every tautology has some Frege proof; it does not ensure a short one. The distinction asks how much information must be recorded to justify truth, rather than merely whether truth is decidable. General-purpose axiom presentations of Frege can simulate one another with polynomial growth in total proof size, so a superpolynomial obstruction would survive these conventional changes of notation and rules. It would still be a statement about Frege: neither a lower bound in a weaker calculus nor failure of one proof-search algorithm rules out short proofs in unrestricted Frege.[1] [2] [3]