arxiv: 2604.25251 · v1 · submitted 2026-04-28 · 🧮 math.LO · cs.CC

Recognition: unknown

From G\"odel incompleteness to the consistency of circuit lower bounds

Albert Atserias, Moritz M\"uller

Authors on Pith no claims yet

Pith reviewed 2026-05-07 14:28 UTC · model grok-4.3

classification 🧮 math.LO cs.CC

keywords bounded arithmeticcircuit lower boundsconsistencyGodel incompletenessEXPP/polyV^1_2S^1_2

0 comments

The pith

The bounded arithmetic theory S^1_2 is consistent with EXP not being contained in P/poly.

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

The paper shows that if V^1_2 is separated from a weaker theory T, then T cannot prove that every exponential-time problem has polynomial-size circuits. For the specific case of T equal to S^1_2, such a separation was already known from a variant of Godel's consistency statement. This matters to a sympathetic reader because it turns a foundational incompleteness result into a statement about the consistency of a major open question in circuit complexity. The same pattern applies to PSPACE not in P/poly once the needed separations are found, and the work also magnifies the difficulty of proving the lower bounds hold for almost all inputs.

Core claim

We prove that the bounded arithmetic theory S^1_2 is consistent with EXP notsubseteq P/poly. More generally, certain separations of V^1_2 from a theory T imply the consistency of T with EXP notsubseteq P/poly. For T = S^1_2, Takeuti established such a separation using a variant of Godel's consistency statement. Analogous results hold for PSPACE notsubseteq P/poly but the required separations of theories are yet unknown. Finally, we give magnification results for the hardness of proving almost-everywhere versions of these lower bounds.

What carries the argument

The implication that a separation of V^1_2 from T yields the consistency of T with EXP notsubseteq P/poly, built on Godel-style consistency statements to witness the separation.

If this is right

S^1_2 does not prove that EXP is contained in P/poly.
Any theory T separated from V^1_2 in the required way is consistent with the circuit lower bound EXP notsubseteq P/poly.
Proving almost-everywhere versions of the lower bounds is at least as hard as proving the basic versions, up to magnification.

Where Pith is reading between the lines

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

Proving the circuit lower bound inside S^1_2 is impossible if the consistency result holds.
Once theory separations are established for PSPACE, the same consistency statement would follow for PSPACE notsubseteq P/poly.
The technique might connect to independence phenomena for other complexity statements in still weaker or stronger arithmetical systems.

Load-bearing premise

That a separation between V^1_2 and the weaker theory T actually exists.

What would settle it

A formal derivation inside S^1_2 of the statement that every language in EXP has polynomial-size circuits.

read the original abstract

We prove that the bounded arithmetic theory $S^1_2$ is consistent with EXP $\not\subseteq$ P/poly. More generally, we show that certain separations of $V^1_2$ from a theory $T$ imply the consistency of $T$ with EXP $\not\subseteq$ P/poly. For $T=S^1_2$, Takeuti (1988) established such a separation using a variant of G\"odel's consistency statement. Analogous results hold for PSPACE $\not\subseteq$ P/poly but the required separations of theories are yet unknown. Finally, we give magnification results for the hardness of proving almost-everywhere versions of these lower bounds.

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

This paper shows S^1_2 is consistent with EXP not in P/poly by reducing from an existing V^1_2 separation, plus a general template and some magnification lemmas.

read the letter

The main point is that S^1_2 is consistent with EXP notsubseteq P/poly. The authors get this by proving that certain V^1_2 separations from a theory T imply the consistency of T with that circuit lower bound. For the S^1_2 case they simply plug in Takeuti's 1988 separation, which is a Gödel-style statement. They also give magnification results that lift the lower bounds to almost-everywhere versions. The consistency claim for S^1_2 and the general reduction are new; the rest rests on standard bounded arithmetic and the old separation result. The paper does a clean job of spelling out the transfer and adding the magnification step on top. This kind of link between incompleteness and the consistency of lower bounds is useful for anyone working on what can actually be proved about circuits inside weak theories. The soft spots are modest. The flagship result is essentially a transfer from Takeuti, so the novelty sits in the implication rather than a fresh separation. The PSPACE version stays conditional because the needed V^1_2 separation is still missing. The magnification lemmas look like a reasonable add-on but their practical payoff for the main theorem is not huge. Without the full derivations in front of me I cannot rule out small gaps in how the circuit classes are formalized inside the theories, though nothing in the setup suggests a problem. This is for people who already know bounded arithmetic and proof complexity. A reader who cares about independence results for circuit lower bounds will get something out of it. I would send it to peer review. The central implication is non-trivial, the argument is grounded in existing work, and the topic sits at a real intersection of logic and complexity.

Referee Report

0 major / 3 minor

Summary. The manuscript proves that the bounded arithmetic theory S^1_2 is consistent with EXP ⊈ P/poly. More generally, it establishes that certain separations of V^1_2 from a theory T imply the consistency of T with EXP ⊈ P/poly. For T = S^1_2 this follows directly from Takeuti's 1988 separation result (a Gödel-style consistency statement). Analogous implications are stated for PSPACE ⊈ P/poly, though the required V^1_2 separations remain unknown. The paper concludes with magnification results showing that proving almost-everywhere versions of these lower bounds is hard for the relevant theories.

Significance. If the central implication holds, the work supplies a clean bridge from known theory separations in bounded arithmetic to consistency statements about circuit lower bounds, without requiring new separations for the flagship case S^1_2. The reliance on the established Takeuti 1988 result and the standard formalization of EXP ⊈ P/poly in bounded arithmetic are strengths. The magnification theorems add a secondary contribution on proof hardness. The result is of interest to researchers working at the interface of proof theory and complexity.

minor comments (3)

[§2] §2, paragraph following Definition 2.3: the precise syntactic form of the separation statement (the exact Π_1 sentence or consistency statement) should be written explicitly rather than described as 'a variant of Gödel's consistency statement,' to allow direct verification of the plug-in into the general implication.
[§4] §4, Theorem 4.2: the magnification argument for almost-everywhere lower bounds would benefit from a short remark comparing the obtained hardness to existing magnification results in the bounded-arithmetic literature (e.g., those of Krajíček or Cook-Nguyen).
[Abstract] Notation: the symbol ⊈ is used without prior definition in the abstract and introduction; a single sentence clarifying that it denotes the standard formalization of 'not contained in P/poly' inside the language of bounded arithmetic would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of our manuscript, as well as for recommending minor revision. The referee correctly identifies the central results: the consistency of S^1_2 with EXP ⊈ P/poly via Takeuti's separation, the general implication from V^1_2 separations, the analogous (but open) case for PSPACE, and the magnification theorems on proof hardness.

Circularity Check

0 steps flagged

No significant circularity; derivation relies on external prior result

full rationale

The paper proves a general implication: separations of V^1_2 from a theory T imply the consistency of T with EXP notsubseteq P/poly (and analogously for PSPACE). For the specific case T = S^1_2, this plugs in the independent Takeuti 1988 separation theorem, which is not a self-citation and is externally established. No equation or step reduces the target consistency statement to a fitted parameter, self-definition, or a chain of results by the present authors. The magnification results for almost-everywhere lower bounds are likewise derived from standard bounded-arithmetic properties without circular reduction. The argument is therefore self-contained once the cited separation is granted.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof operates inside the standard axioms of bounded arithmetic S^1_2 and V^1_2 as defined in the literature; no new free parameters, invented entities, or ad-hoc axioms are introduced beyond those already present in the cited Takeuti separation.

axioms (1)

standard math Axioms of the bounded arithmetic theories S^1_2 and V^1_2
The paper works entirely within these theories and their standard properties as established in prior work.

pith-pipeline@v0.9.0 · 5409 in / 1378 out tokens · 100262 ms · 2026-05-07T14:28:40.536061+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

32 extracted references · 1 canonical work pages

[1]

M. Ajtai. The complexity of the pigeonhole principle. Proc. 29th Annual IEEE Sympo- sium on Foundations of Computer Science (FOCS’88), pp. 346-355, 1988

1988
[2]

Atserias and M

A. Atserias and M. M¨ uller. Partially definable forcing and bounded arithmetic. Archive for Mathematical Logic 54 (1): 1-33, 2015

2015
[3]

Atserias and I

A. Atserias and I. Tzameret. Feasibly constructive proof of Schwartz-Zippel lemma and the complexity of finding hitting sets. Proc. 57th ACM Symposium on the Theory of Computation (STOC’25), 2025

2025
[4]

Atserias, S

A. Atserias, S. Buss, M. M¨ uller. On the consistency of circuit lower bounds for non- deterministic time. Journal of Mathematical Logic 25 (3): 2450023, 2025

2025
[5]

Beckmann, S

A. Beckmann, S. Buss. Improved witnessing and local improvement principles for second-order bounded arithmetic. ACM Transactions on Computational Logic 15 (1): Article 2, 2014

2014
[6]

S. R. Buss. Bounded Arithmetic. Bibliopolis, Naples, 1986

1986
[7]

Bydˇ zovsk´ y, J

J. Bydˇ zovsk´ y, J. Kraj´ ıˇ cek and I. C. Oliveira. Consistency of circuit lower bounds with bounded theories. Logical Methods in Computer Science 16 (2): 12:1-12:16, 2020

2020
[8]

Bydˇ zovsk´ y and M

J. Bydˇ zovsk´ y and M. M¨ uller. Polynomial time ultrapowers and the consistency of circuit lower bounds. Archive for Mathematical Logic 59 (1): 127-147, 2020

2020
[9]

Carmosino, V

M. Carmosino, V. Kabanets, A. Kolokolova and I. C. Oliveira. LEARN-uniform circuit lower bounds and provability in bounded arithmetic. Proc. 62nd IEEE Symposium on Foundations of Computer Science (FOCS’21), pp. 770–780, 2021

2021
[10]

L. Chen, S. Hirahara, I. C. Oliveira, J. Pich, N. Rajgopal, R. Santhanam. Beyond natural proofs: hardness magnification and locality. Journal of the ACM 69 (4): Article 25, 2022. 30

2022
[11]

S. A. Cook. 1975. Feasibly constructive proofs and the propositional calculus (prelimi- nary version). Proc. 7th ACM Symposium on Theory of Computing (STOC’75), ACM, pp. 83–97, 1975

1975
[12]

S. A. Cook, J. Kraj´ ıˇ cek. Consequences of the provability ofNP⊆P/poly. Journal of Symbolic Logic 72 (4): 1353-1371, 2007

2007
[13]

H´ ajek, P

P. H´ ajek, P. Pudl´ ak. Metamathematics of First-Order Arithmetic. Perspectives in Math- ematical Logic, Springer, 1998

1998
[14]

R. M. Karp, R. J. Lipton. Some connections between nonuniform and uniform complex- ity classes. Proc. ACM Symposium on Theory of Computing (STOC’80), pp. 302-309, 1980

1980
[15]

Ko lodziejczyk, P

L. Ko lodziejczyk, P. Nguyen and N. Thapen. The provably total NP search problems of weak second order bounded arithmetic. Annals of Pure and Applied Logic 162 (6): 419-446, 2011

2011
[16]

Kraj´ ıˇ cek

J. Kraj´ ıˇ cek. Exponentiation and second order bounded arithmetic. Annals of Pure and Applied Logic 48 (3): 261-276, 1990

1990
[17]

Kraj´ ıˇ cek

J. Kraj´ ıˇ cek. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Ency- clopedia of Mathematics and Its Applications 60, Cambridge University Press, 1995

1995
[18]

Kraj´ ıˇ cek and I

J. Kraj´ ıˇ cek and I. C. Oliveira. Unprovability of circuit upper bounds in Cook’s theory PV. Logical Methods in Computer Science 13 (1:4), 2017

2017
[19]

Kraj´ ıˇ cek, P

J. Kraj´ ıˇ cek, P. Pudl´ ak and G. Takeuti. Bounded arithmetic and the polynomial hierar- chy. Annals of Pure and Applied Logic 52 (1-2): 143-153, 1991

1991
[20]

Kraj´ ıˇ cek, P

J. Kraj´ ıˇ cek, P. Pudl´ ak, A. Woods. Exponential lower bound to the size of bounded depth Frege proofs of the Pigeon Hole Principle. Random Structures and Algorithms 7 (1): 15-39, 1995

1995
[21]

M¨ uller

M. M¨ uller. Typical forcing, NP search problems and an extension of a theorem of Riis. Annals of Pure and Applied Logic 172 (4): Article 102930, 2021

2021
[22]

M¨ uller, J

M. M¨ uller, J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic 172 (2): Article 102735, 2020

2020
[23]

Pitassi, P

T. Pitassi, P. Beame, R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity 3: 97-140, 1993

1993
[24]

Pudl´ ak

P. Pudl´ ak. A bottom-up approach to foundations of mathematics. In: P. H´ ajek (ed.), G¨ odel ’96: Logical Foundations of Mathematics, Computer Science and Physics - Kurt G¨ odel’s Legacy. Lecture Notes in Logic. Cambridge University Press, pp. 81-97, 2017. 31

2017
[25]

Pudl´ ak

P. Pudl´ ak. Incompleteness in the finite domain. Bulletin of Symbolic Logic 23 (4): 405- 441, 2017

2017
[26]

A. A. Razborov. Bounded arithmetic and lower bounds in Boolean complexity. Feasible Mathematics II, pp. 344-386, 1995

1995
[27]

A. A. Razborov. Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic. Izvestiya of the Russian Academy of Science 59: 201-224, 1995

1995
[28]

A. A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus. Annals of Mathematics 181 (2): 415-472, 2015

2015
[29]

S. Riis. Making infinite structures finite in models of second order bounded arithmetic. In: Arithmetic, proof theory and computational complexity, Oxford University Press, pp. 289-319, 1993

1993
[30]

Santhanam and R

R. Santhanam and R. Williams. On uniformity and circuit lower bounds. Computational Complexity 23 (2): 177-205, 2014

2014
[31]

G. Takeuti. Bounded arithmetic and truth definition. Annals of Pure and Applied Logic 39: 75-104, 1988

1988
[32]

N. Thapen. On the consistency of stronger lower bounds for NEXP. Preprint arXiv:2504.03320 [cs.LO],https://arxiv.org/abs/2504.03320, 2025. 32

work page arXiv 2025