From Gödel incompleteness to the consistency of circuit lower bounds

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Atserias, Albert, Müller, Moritz
Format: Preprint
Published: 2026
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866917442921431040
author Atserias, Albert
Müller, Moritz
author_facet Atserias, Albert
Müller, Moritz
contents 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ödel'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.
format Preprint
id arxiv_https___arxiv_org_abs_2604_25251
institution arXiv
publishDate 2026
record_format arxiv
spellingShingle From Gödel incompleteness to the consistency of circuit lower bounds
Atserias, Albert
Müller, Moritz
Logic
Computational Complexity
03F20, 03F30, 68Q15
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ödel'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.
title From Gödel incompleteness to the consistency of circuit lower bounds
topic Logic
Computational Complexity
03F20, 03F30, 68Q15
url https://arxiv.org/abs/2604.25251