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.

翻译：我们证明有界算术理论 $S^1_2$ 与 EXP $\not\subseteq$ P/poly 是一致的。更一般地，我们表明 $V^1_2$ 与理论 $T$ 的某种分离蕴含了 $T$ 与 EXP $\not\subseteq$ P/poly 的一致性。对于 $T=S^1_2$，竹内（Takeuti, 1988）利用哥德尔一致性陈述的变体建立了这样的分离。类似结论对 PSPACE $\not\subseteq$ P/poly 也成立，但所需的理论分离尚不明确。最后，我们给出关于这些下界几乎处处版本的证明难度的放大结果。