Superpolynomial Lower Bounds for Frege Propositional Proof Systems

Superpolynomial Lower Bounds for Frege Propositional Proof Systems

Definitions and mathematical statement

A Frege system is a fixed sound and complete finite propositional axiom-and-rule calculus with substitution instances; proof size counts all written symbols. For a tautology $\tau$, let $s_F(\tau)$ be the minimum size of an $F$-proof. Seek an explicit growing family $\tau_n$, conventionally efficiently generated from $n$, for which \[ s_F(\tau_n)\text{ is not bounded by any polynomial in }|\tau_n|. \] A corresponding line-count lower bound is another allowed target in the catalogue. The family must consist of tautologies, and the system is a standard unrestricted Frege system, not merely a depth-restricted or otherwise weakened proof calculus.

Formulation and concept references: [S1].

Short English statement

Can one explicitly exhibit tautologies requiring superpolynomially long proofs in ordinary Frege reasoning systems?

Research attempt

Current frontier.

The target is unrestricted Frege with symbol-count size. Bounds for a restricted proof-line language or for bounded-size lines do not establish it. Two recent examples make this distinction concrete: Elbaz--Govindasamy--Lu--Tzameret obtain lower bounds for specified multilinear and branching-program fragments of algebraic IPS over finite fields, while the 2026 manuscript of de Rezende--Engström--Ghannane--Risse imposes both tree-likeness and a line-size restriction. Neither result supplies the target here. [E2][E3]

The route used below starts with the established polynomial simulation of Frege by noncommutative formula IPS, not a conjectural simulation of Frege by a weaker calculus. In this model there are elementary coefficient-matrix rank lower bounds, but a refutation is not a uniquely specified polynomial: one must lower-bound every permitted certificate. [E1] Literature was checked on 27 September 2026. The deductions below are worked out here; no claim of priority for their component lemmas is made.

Attack route.

There are three possibilities worth separating. A restriction argument would need a complexity measure stable under all unrestricted Frege rules; the cited restricted-system results do not furnish one. A counting argument would still have to produce an efficiently generated family and prove that its members are tautologies. The algebraic route instead asks for a uniform rank obstruction over an affine space of certificates. I pursue the third route, first testing whether the certificates can be normalized without an exponential formula-size cost. This normalization is important: simply retaining terms of degree one in the axiom placeholders does not work.

Attempt.

1. Fixing the algebraic model. Work over $K=\mathbb F_2$ in the free algebra $K\langle x_1,\ldots,x_n\rangle$. For an unsatisfiable CNF $A$, use the $0/1$ convention in which $1$ means true. The falsity polynomial of a clause is the ordered product of $1-x_i$ for a positive literal and $x_i$ for a negative literal. Fix the literal order once and for all. Include, in addition, all Boolean equations $x_i^2-x_i$ and all commutators $x_ix_j-x_jx_i$. Denote the resulting list by $F_1,\ldots,F_m$. Changing from the truth-value convention in [E1] only complements the variables; it does not alter the simulation or add a proof restriction.

A certificate is a noncommutative formula $C(x,y)$ satisfying the two formal identities \begin{equation}\label{wsref-0-33-30-30-30-36-37-33-30-3a-69-70-73} C(x,0)=0,\qquad C(x,F_1(x),\ldots,F_m(x))=1. \end{equation} These are identities in a free algebra, not merely identities on Boolean assignments. The commutator axioms must not be discarded. To connect the single-formula translation in Theorem 1.4 of [E1] to the clause list here, if $A$ has $q$ clauses put \[ G(x)=1-\prod_{i=1}^{q}(1-F_i(x)). \] After complementing the variables, this is its translated CNF polynomial. In a certificate using $G$ as an axiom, replace its placeholder by $1-\prod_{i=1}^{q}(1-y_i)$. This polynomial vanishes at $y=0$ and becomes $G$ after substitution. Replacing each occurrence costs only a factor polynomial in $|A|$. Thus the cited simulation supplies a polynomial-size certificate for the clause list above from a polynomial-size Frege proof of $\neg A$; no converse simulation is being presumed.

2. A formula-preserving two-sided linearization lemma. Suppose each $F_i$ has a formula of size at most $L$, and $C$ has formula size $s$, where leaves and gates are counted. There is a certificate $D$ with size $O((L+1)s^2)$ in which every nonzero monomial contains exactly one placeholder $y_i$. Thus it has the algebraic form \begin{equation}\label{wsref-0-33-30-30-30-36-37-33-30-3a-74-77-6f-2d-73-69-64-65-64} D(x,y)=\sum_{i,w} A_{i,w}(x)y_iB_{i,w}(x). \end{equation} The expanded sum need not be small; the asserted size bound is on its unexpanded formula.

Proof. For a subformula $H$, put $H^0=H(x,0)$ and $H^F=H(x,F)$. Construct a formula $D_H$ recursively. For a constant or an $x$-leaf set $D_H=0$; for the leaf $y_i$ set $D_H=y_i$. Set \begin{align} D_{U+V}&=D_U+D_V,\ D_{UV}&=D_U V^F+U^0D_V. \label{wsref-0-33-30-30-30-36-37-33-30-3a-70-72-6f-64-75-63-74} \end{align} Every coefficient formula in the second line contains only $x$'s. Induction therefore shows that every monomial of $D_H$ has exactly one $y$, unless it cancels. The same induction gives \[ D_H(x,F)=H^F-H^0, \] since \[ (U^F-U^0)V^F+U^0(V^F-V^0)=U^FV^F-U^0V^0. \] No factor has been commuted. Applying this to $H=C$ proves (30006730:ips) for $D_C$.

At a product gate the construction copies two ordinary subformulas, each of size at most $O((L+1)s)$. There are at most $s$ gates. Each recursively constructed $D_U$ or $D_V$ is used only once at its parent, so these copies do not cause exponential duplication. This gives the claimed quadratic bound. In particular, if the original input and proof sizes are polynomial, so are the size and degree of $D_C$. $\square$

This is genuinely a two-sided normalization. Replacing (30006730:two-sided) by $\sum_i A_i(x)y_i$ would assert an additional, unproved restriction. As a test of the tempting shortcut, take $F_1=x$, $F_2=x-1$ and $C=(y_1-y_2)^2$. Then $C(x,F)=1$ and $C(x,0)=0$, but its component of placeholder degree one is zero. The telescoping construction, unlike that shortcut, remains valid.

3. A precise rank objective and its quantifiers. For a homogeneous noncommutative polynomial $P_d$ of degree $d$, define $M_k(P_d)$, for $0\leq k\leq d$, to have rows indexed by words of length $k$ and columns by words of length $d-k$, with entry \[ M_k(P_d)_{u,v}=[uv]P_d. \] The alphabet here includes both the $x$'s and the $y$'s. A formula of size $S$ computing $P$ implies a polynomial bound on the ranks of these matrices for all homogeneous components $P_d$ with $d\leq S$.

For completeness, a sufficient version of the bound is \begin{equation}\label{wsref-0-33-30-30-30-36-37-33-30-3a-72-61-6e-6b-2d-75-70-70-65-72} \operatorname{rank}M_k(P_d)\leq O(S(d+1)^2). \end{equation} Convert the formula to its series-parallel algebraic branching program by parallel composition at addition gates and concatenation at multiplication gates. It has $O(S)$ vertices and edges. Track accumulated word degree from $0$ to $d$ to extract the homogeneous component. Scalar edges do not increase the degree. For $0<k<d$, split each source-to-sink path immediately before its $(k+1)$st variable edge. Summing over these crossing edges expresses $M_k(P_d)$ as a sum of rank-one outer products, with a polynomial number of summands. End cuts have rank at most one. This proves the deliberately loose bound (30006730:rank-upper); it is the usual noncommutative branching-program rank argument described in [E1].

Now fix a degree cutoff $D_0$. The coefficients of all polynomials of the form (30006730:two-sided) of degree at most $D_0$ form a finite-dimensional vector space. Requiring $D(x,F)=1$ imposes linear coefficient equations on that space. Thus the next proposed attack is a rank lower bound throughout an explicitly specified affine solution space, not a lower bound for one arbitrarily chosen lift.

Here is a sufficient, still unproved, statement. Find a polynomial-time constructed unsatisfiable CNF family $A_n$, of lengths $N_n\to\infty$, such that for every fixed $a,b>0$ there are arbitrarily large $n$ for which \begin{equation}\label{wsref-0-33-30-30-30-36-37-33-30-3a-6d-69-73-73-69-6e-67} \max_{d,k}\operatorname{rank}M_k(D_d)>N_n^b \quad\text{for every two-sided certificate $D$ of degree at most $N_n^a$.} \end{equation} The minimum over an empty certificate set is interpreted as $+\infty$. A polynomial Frege proof bound would, by the established simulation and the proved linearization, supply certificates of polynomial size and degree for every $n$. Bound (30006730:rank-upper) would then contradict (30006730:missing), with $a,b$ chosen larger than the corresponding fixed polynomial exponents. Hence this statement would resolve the selected symbol-size target. No such family satisfying (30006730:missing) is established below.

4. Testing a candidate: cyclic parity collapses. Consider equations $x_i+x_{i+1}=b_i$ over $\mathbb F_2$, with indices modulo $m\geq3$ and $\sum_i b_i=1$. Encode each constraint by its two forbidden Boolean assignments. When $b_i=0$, the two clause-falsity polynomials sum to \[ x_i(1-x_{i+1})+(1-x_i)x_{i+1}=x_i+x_{i+1}. \] When $b_i=1$, they sum to \[ (1-x_i)(1-x_{i+1})+x_ix_{i+1}=1+x_i+x_{i+1}. \] Summing over the cycle gives the formal identity $\sum_{j=1}^{2m}F_j=1$. Consequently $D=\sum_{j=1}^{2m}y_j$ is a linear-size certificate. Its only nonzero homogeneous component has degree one and coefficient-matrix rank one. An apparently global parity inconsistency therefore supplies no rank obstruction at all. This calculation does not use a Boolean evaluation or silently commute any variables.

Stress test.

A high-rank lift need not be the cheapest lift. For an alphabet $\{a,b\}$, consider \[ P_m=\sum_{w\in\{a,b\}^m}ww,\qquad Q_m=(a^2+b^2)^m. \] The middle coefficient matrix of $P_m$ is the $2^m$-by-$2^m$ identity, so (30006730:rank-upper) gives an exponential formula lower bound for $P_m$. In contrast, writing $Q_m$ as a product of $m$ copies gives a formula of size $O(m)$. Nevertheless their commutative images are identical: for each number $i$ of letters $a$, both have coefficient $\binom mi$ on $a^{2i}b^{2m-2i}$, interpreted in the chosen field. Adjacent swaps express $P_m-Q_m$ in the two-sided commutator ideal. Thus a proof that one attractive lift has large rank cannot establish (30006730:missing). This is a concrete failure of an intermediate strategy, not a counterexample to the Frege conjecture.

The size model and the dependency warning. All bounds above count symbols/formula gates, not just proof lines. They therefore pursue the size option in the catalogue; no line-count lower bound is inferred. Nor does a lower bound for this particular Frege system by itself establish $\mathsf{NP}\ne\mathsf{coNP}$: the latter requires excluding every polynomially bounded Cook--Reckhow proof system. [E3] Separately, over ${\mathbb{Q}}$, superpolynomial lower bounds for unrestricted commutative circuit IPS imply a permanent circuit lower bound by Grochow--Pitassi. [E4] That stronger route is not assumed here. The field qualification matters: in characteristic two the permanent coincides with the determinant, so that formulation of the consequence must not be transferred to the present $\mathbb F_2$ calculation.

The companion script checks telescoping on finite noncommutative formula examples, the parity identities, and the ranks in the lift example. These are tests of the stated calculations, not evidence that all certificates for an unconstructed family satisfy (30006730:missing).

Outcome.

Outcome: Exploratory approach with unresolved gap.

The completed deductions are a polynomial-overhead two-sided linearization, an explicit finite-dimensional rank objective, and two concrete obstructions to overly simple rank attacks. The missing result is an explicit tautology family with a lower bound uniform over all normalized certificates. No such lower bound, no hard explicit family, and no resolution of the unrestricted Frege target is claimed. The normalization lemma is useful for organizing that search, but its novelty is not asserted.

Sources

• S1 J. Krajicek, Proof Complexity, Cambridge University Press, 2019. https://doi.org/10.1017/9781108643818. Catalogue formulation source.
• E1 F. Li, I. Tzameret, and Z. Wang, Characterizing Propositional Proofs as Non-Commutative Formulas, arXiv:1412.8746v4 (11 September 2015), Definition 1.2, Theorem 1.4, Sections 1.2--1.3, 3, and 4.7. https://arxiv.org/html/1412.8746v4. Consulted 27 September 2026; simulation direction and size model checked.
• E2 T. Elbaz, N. Govindasamy, J. Lu, and I. Tzameret, Lower Bounds against the Ideal Proof System in Finite Fields, arXiv:2506.17210v1 (20 June 2025), Theorem 1 (informal), Section 1.4.3, and Section 6. https://arxiv.org/html/2506.17210v1. Consulted 27 September 2026; restricted algebraic models are not unrestricted Frege.
• E3 S. F. de Rezende, D. Engström, Y. Ghannane, and K. Risse, Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size, arXiv:2604.28172v1 (30 April 2026), Introduction and Corollary 1.6. https://arxiv.org/html/2604.28172v1. Consulted 27 September 2026; recent preprint, with its tree-like and line-size hypotheses retained.

• E4 Joshua A. Grochow and Toniann Pitassi, Circuit complexity, proof complexity, and polynomial identity testing, arXiv:1404.3820v1 $2014$, abstract. https://arxiv.org/abs/1404.3820.