Extended Frege proofs, circuits and rewriting

Jan Krajicek

arxiv: 2606.13367 · v1 · pith:WEIYBABM · submitted 2026-06-11 · math.LO · cs.CC

Extended Frege proofs, circuits and rewriting

Jan Krajicek This is my paper

Reviewed by Pith2026-06-27 04:47 UTCgrok-4.3pith:WEIYBABM open to challenge →

classification math.LO cs.CC

keywords extended fregecircuit fregeproof complexitycircuit equivalencerewritingpolynomial time relationgate additionboolean circuits

0 comments

The pith

Equivalence proofs of size s in Extended Frege or Circuit Frege systems yield chains of length at most s to the O(1) under a local circuit rewrite relation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a polynomial-time decidable relation ≈ on Boolean circuits such that C ≈ D implies the two circuits compute identical functions. The same relation guarantees that one circuit can be transformed into the other by deleting arbitrary gates and inserting at most seven new gates. When two circuits are shown equivalent by a proof of size s in either the Extended Frege or the Circuit Frege system, the paper constructs an explicit sequence of circuits linked by ≈ steps whose length is bounded by a polynomial in s.

Core claim

If the equivalence C ≡ D has a size s proof in an Extended Frege or a Circuit Frege proof system then there is a chain of circuits E_i with C = E_0 ≈ … ≈ E_t = D where t ≤ s^{O(1)}, and the relation ≈ is polynomial-time and permits rewriting with at most seven added gates while preserving logical equivalence.

What carries the argument

The polynomial-time binary relation ≈ on circuits that implies logical equivalence and allows one circuit to be obtained from the other by deleting gates and adding at most seven new gates.

If this is right

Short proofs in these systems can be converted into polynomially long sequences of local circuit modifications.
The relation ≈ supplies a certificate for circuit equivalence that is checkable in polynomial time.
Any upper bound on the length of ≈-chains immediately yields an upper bound on the size of proofs in the corresponding Frege systems.
The seven-gate bound on local rewrites is preserved uniformly across the chain.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The existence of such short chains might be used to design heuristic algorithms that search for circuit equivalences by exploring bounded local changes rather than full proofs.
If circuit equivalence testing lies outside P, the construction still separates the length of ≈-chains from the existence of short proofs only if the relation itself is hard to decide.
The fixed seven-gate allowance could be tightened or relaxed in follow-up work to obtain sharper bounds on proof size versus rewrite length.

Load-bearing premise

The standard definitions of Extended Frege and Circuit Frege proof systems are taken to hold exactly as used in the cited background statements.

What would settle it

An explicit pair of circuits C and D whose logical equivalence has an Extended Frege proof of size s but for which every possible chain under the relation ≈ has length superpolynomial in s.

read the original abstract

Inspired by a statement about Extended Frege proof systems by Jain and Jin (FOCS 2022) we prove that: - there is a p-time binary relation $\approx$ between circuits that implies their logical equivalence, - the relation $\approx$ implies that each of the two circuits can be rewritten into the other one by possibly deleting some gates and adding at most seven new gates, - if the equivalence $C \equiv D$ has a size $s$ proof in an Extended Frege or a Circuit Frege proof system then there is a chain of circuits $E_i$ $$ C = E_0 \approx \dots \approx E_t = D $$ with $t \le s^{O(1)}$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Krajicek turns an EF/CF proof of size s into a polynomial-length chain of ≈ steps, each adding at most seven gates.

read the letter

The main takeaway is that an Extended Frege or Circuit Frege proof of size s for circuit equivalence C ≡ D yields a chain C = E0 ≈ … ≈ Et = D with t polynomial in s, where ≈ is a p-time relation that implies logical equivalence and allows each circuit to be rewritten into the other by deleting gates and adding at most seven new ones.

The three statements are new. They do not reduce to earlier published results and they make explicit a technical connection between proof size and bounded local rewriting that was only suggested before. The paper stays inside the standard definitions of EF and CF systems and uses the Jain-Jin observation as a starting point without adding extra machinery.

The argument chain is consistent: the p-time soundness of ≈ gives equivalence, the local rewrite bound follows from the definition of ≈, and the polynomial chain length follows from simulating each proof step by a bounded number of ≈ steps. No circularity or invented entities appear.

The only real limitation is that the abstract states the theorems without derivation steps, so the actual proofs need to be checked in the full text. The dependence on the cited FOCS 2022 statement is ordinary and not a flaw here. Nothing in the claimed implications looks shaky.

This is for specialists already working on proof complexity and circuit-based systems. Someone tracking EF lower bounds or circuit equivalence algorithms will find the link useful for organizing existing ideas.

Send it to peer review. The claims are precise enough and the subfield is active enough that a referee should see it.

Referee Report

1 major / 0 minor

Summary. Inspired by Jain and Jin (FOCS 2022), the paper proves three statements: there is a p-time binary relation ≈ between circuits that implies their logical equivalence; the relation ≈ implies that each of the two circuits can be rewritten into the other one by possibly deleting some gates and adding at most seven new gates; if the equivalence C ≡ D has a size s proof in an Extended Frege or a Circuit Frege proof system then there is a chain of circuits E_i with C = E_0 ≈ … ≈ E_t = D with t ≤ s^{O(1)}.

Significance. If these results hold, they establish a link between proof size in EF and CF systems and the length of chains under a local rewriting relation ≈, which could be significant for proof complexity theory. The p-time computability of ≈ and the constant bound of 7 on new gates are particular features that, if proved, would be noteworthy.

major comments (1)

[Abstract] The abstract states the three theorems cleanly but supplies no derivation steps; without the full manuscript the support for the central claims cannot be checked.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their comments on our manuscript. We address the single major comment below.

read point-by-point responses

Referee: [Abstract] The abstract states the three theorems cleanly but supplies no derivation steps; without the full manuscript the support for the central claims cannot be checked.

Authors: Abstracts are intended to state main results concisely without full derivations; the complete proofs and supporting arguments appear in the body of the manuscript (Sections 3--5). The arXiv version supplies the full text, so the claims can be verified directly from the provided derivations. revision: no

Circularity Check

0 steps flagged

Derivation self-contained from standard definitions; no circular reductions

full rationale

The three statements are derived from the standard formal definitions of Extended Frege and Circuit Frege proof systems together with the p-time relation ≈. No equations, parameters, or self-citations reduce any claimed implication to a fit or to a prior result by the same authors that is itself unverified. The chain from proof size s to polynomial-length ≈-chain is presented as a direct translation using bounded local rewrites, without self-definitional or fitted-input constructions. The citation to Jain and Jin is used only as inspiration for the relation, not as a load-bearing uniqueness theorem or ansatz. The result is therefore independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper introduces no new free parameters or invented entities; it relies on the standard axiomatic framework of proof complexity.

axioms (2)

standard math Standard definitions and properties of Extended Frege and Circuit Frege proof systems
Invoked throughout the abstract as the setting in which the size-s proofs are considered.
domain assumption The statement about Extended Frege systems from Jain and Jin (FOCS 2022)
Cited explicitly as the inspiration for the work.

pith-pipeline@v0.9.1-grok · 5641 in / 1278 out tokens · 34171 ms · 2026-06-27T04:47:32.302635+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

8 extracted references

[1]

Baader and T

F. Baader and T. Nipkow,Term Rewriting and All That, Cambridge University Press, (1998)

1998
[2]

Birkhoff, On the structure of abstract algebras,Proceedings Cam- bridge Phil

G. Birkhoff, On the structure of abstract algebras,Proceedings Cam- bridge Phil. Soc.,31, (1935), pp.433454

1935
[3]

S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems,J. Symbolic Logic,44(1), (1979), pp.36-50

1979
[4]

Jain and Z

A. Jain and Z. Jin, Indistinguishability Obfuscation via Mathematical Proofs of Equivalence, in63rd FOCS, IEEE Computer Society Press, (2022), pp.1023-1034

2022
[5]

Jeˇ r´ abek, Dual weak pigeonhole principle, Boolean complexity, and derandomization,Annals of Pure and Applied Logic,129, (2004), pp.1- 37

E. Jeˇ r´ abek, Dual weak pigeonhole principle, Boolean complexity, and derandomization,Annals of Pure and Applied Logic,129, (2004), pp.1- 37

2004
[6]

Kraj´ ıˇ cek, On Frege and Extended Frege Proof Systems

J. Kraj´ ıˇ cek, On Frege and Extended Frege Proof Systems. in:Feasi- ble Mathematics II., eds. P. Clote and J. Remmel, Birkhauser, (1995), pp.284-319

1995
[7]

Kraj´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Applications, Vol.170, Cambridge University Press, (2019)

J. Kraj´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Applications, Vol.170, Cambridge University Press, (2019)

2019
[8]

G. C. Tseitin, On the complexity of derivations in propositional cal- culus, in:Studies in mathematics and mathematical logic, Part II, ed. A.O.Slisenko, (1968), pp.115-125. 10

1968

[1] [1]

Baader and T

F. Baader and T. Nipkow,Term Rewriting and All That, Cambridge University Press, (1998)

1998

[2] [2]

Birkhoff, On the structure of abstract algebras,Proceedings Cam- bridge Phil

G. Birkhoff, On the structure of abstract algebras,Proceedings Cam- bridge Phil. Soc.,31, (1935), pp.433454

1935

[3] [3]

S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems,J. Symbolic Logic,44(1), (1979), pp.36-50

1979

[4] [4]

Jain and Z

A. Jain and Z. Jin, Indistinguishability Obfuscation via Mathematical Proofs of Equivalence, in63rd FOCS, IEEE Computer Society Press, (2022), pp.1023-1034

2022

[5] [5]

Jeˇ r´ abek, Dual weak pigeonhole principle, Boolean complexity, and derandomization,Annals of Pure and Applied Logic,129, (2004), pp.1- 37

E. Jeˇ r´ abek, Dual weak pigeonhole principle, Boolean complexity, and derandomization,Annals of Pure and Applied Logic,129, (2004), pp.1- 37

2004

[6] [6]

Kraj´ ıˇ cek, On Frege and Extended Frege Proof Systems

J. Kraj´ ıˇ cek, On Frege and Extended Frege Proof Systems. in:Feasi- ble Mathematics II., eds. P. Clote and J. Remmel, Birkhauser, (1995), pp.284-319

1995

[7] [7]

Kraj´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Applications, Vol.170, Cambridge University Press, (2019)

J. Kraj´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Applications, Vol.170, Cambridge University Press, (2019)

2019

[8] [8]

G. C. Tseitin, On the complexity of derivations in propositional cal- culus, in:Studies in mathematics and mathematical logic, Part II, ed. A.O.Slisenko, (1968), pp.115-125. 10

1968