Consistency of circuit lower bounds with bounded theories

TL;DR

This paper explores the limitations of formal theories in proving circuit lower bounds for complexity classes like NP and P^NP, showing that certain bounds cannot be established within these theories, even with sophisticated arguments.

Contribution

It demonstrates that specific logical theories cannot prove infinitely often circuit upper bounds for key complexity classes, extending previous results and highlighting fundamental proof limitations.

Findings

Certain theories cannot prove infinitely often circuit upper bounds for NP and P^NP.

Consistency of these limitations is unconditional and improves previous results.

We formalize the interaction between logical proof systems and computational complexity.

Abstract

Proving that there are problems in $\mathsf{P}^\mathsf{NP}$ that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are known for larger complexity classes, existing results only show that the corresponding problems are hard on infinitely many input lengths. For instance, proving almost-everywhere circuit lower bounds is open even for problems in $\mathsf{MAEXP}$. Giving the notorious difficulty of proving lower bounds that hold for all large input lengths, we ask the following question: Can we show that a large set of techniques cannot prove that $\mathsf{NP}$ is easy infinitely often? Motivated by this and related questions about the interaction between mathematical proofs and computations, we investigate circuit complexity from the perspective of logic. Among other results, we prove that for any parameter $k \geq 1$ it is consistent with theory $T$ that computational class ${\mathcal C} \not \subseteq \textit{i.o.}\mathrm{SIZE}(n^k)$, where $(T, \mathcal{C})$ is one of the pairs: $T = \mathsf{T}^1_2$ and ${\mathcal C} = \mathsf{P}^\mathsf{NP}$, $T = \mathsf{S}^1_2$ and ${\mathcal C} = \mathsf{NP}$, $T = \mathsf{PV}$ and ${\mathcal C} = \mathsf{P}$. In other words, these theories cannot establish infinitely often circuit upper bounds for the corresponding problems. This is of interest because the weaker theory $\mathsf{PV}$ already formalizes sophisticated arguments, such as a proof of the PCP Theorem. These consistency statements are unconditional and improve on earlier theorems of [KO17] and [BM18] on the consistency of lower bounds with $\mathsf{PV}$.

Equations

$$\exists y_1\le t_1(\overline{x})\dots \exists y_k\le t_k(\overline{x})A(\overline{x},\overline{y}),$$

$$\forall 1^{(n)}\exists 1^{(m)}(m\ge n)\exists C_m(|C_m|\le m^k)\forall x(|x|=m),\phi (x)\equiv (C_m(x)=1).$$

$$T_2^1(\mathsf{PV})$$

$$S_2^1(\mathsf{PV})$$

$$\mathsf{PV}$$

$${\mathsf{S}}_2^1(\mathsf{PV})\cup \mathsf{sWPHP}(\mathsf{PV})⊬{\mathsf{UB}}_k^{i.o.}(\phi ),$$

$$m,|C_m|\le n^{O(1)}.$$

$$D_n(a,\stackrel{j}{1},\stackrel{\vec{b}}{\overbrace{1,\star ,\dots ,\star }},1^{(t)},\stackrel{c}{0}),$$

$$D_n(a,\stackrel{j}{2},\stackrel{\vec{b}}{\overbrace{d_1,1,\star ,\dots ,\star }},1^{(t)},\stackrel{c}{0}),$$

$$\begin{aligned} &\big{[}f_{1}({1^{(n)}})=(1^{(n_{1})},C_{n_{1}}^{1})\wedge|C^{1}_{n_{1}}|\leq n_{1}^{k}\wedge(|x_{1}|=n_{1}\rightarrow C^{1}_{n_{1}}(x_{1})=g_{k^{\prime}}(x_{1}))\big{]}\\ \vee&\big{[}f_{2}({1^{(n)}},x_{1})=(1^{(n_{2})},C_{n_{2}}^{2})\wedge|C^{2}_{n_{2}}|\leq n_{2}^{k}\wedge(|x_{2}|=n_{2}\rightarrow C^{2}_{n_{2}}(x_{2})=g_{k^{\prime}}(x_{2}))\big{]}\vee\ldots\\ \vee&\big{[}f_{r}({1^{(n)}},x_{1},\ldots,x_{r-1})=(1^{(n_{r})},C_{n_{r}}^{r})\wedge|C^{r}_{n_{r}}|\leq n_{r}^{k}\wedge(|x_{r}|=n_{r}\rightarrow C^{r}_{n_{r}}(x_{r})=g_{k^{\prime}}(x_{r}))\big{]}.\end{aligned}$$

$$⟨\mathsf{Bin}(n),1^{(n^{1/10k})},u,v,w,1^t⟩,$$

$$\mathsf{PV}⊢\forall 1^{(\ell )}\exists 1^{(n)}(n\ge \ell )\exists x(|x|=n_1(1^{(n)})),g_{k^{\prime }}(x)\ne C_{|x|}^1(x).$$

$$\forall 1^{(n)}\in S_1,\text{“KPT disjunct for}j\in [2,r]\text{under the counter-example}{x}_1\stackrel{\mathrm{def}}{=}{e}_1(1^{(\ell )})\text{”},$$

$$\begin{aligned} &\big{[}f_{2}(u_{1}(1^{(\ell)}),e_{1}(1^{(\ell)}))=(1^{(n_{2})},C_{n_{2}}^{2})\wedge|C^{2}_{n_{2}}|\leq n_{2}^{k}\wedge(|x_{2}|=n_{2}\rightarrow C^{2}_{n_{2}}(x_{2})=g_{k^{\prime}}(x_{2}))\big{]}\\ \vee&\ldots\\ \vee{}&\left[\begin{split}f_{r}(u_{1}(1^{(\ell)}),e_{1}(1^{(\ell)}),&x_{2},\ldots,x_{r-1})=(1^{(n_{r})},C_{n_{r}}^{r})\wedge|C^{r}_{n_{r}}|\leq n_{r}^{k}\\ &\wedge{}(|x_{r}|=n_{r}\rightarrow C^{r}_{n_{r}}(x_{r})=g_{k^{\prime}}(x_{r}))\end{split}\right],\end{aligned}$$

$${\phi }_{\mathsf{P}=\mathsf{NP}}(f)\stackrel{\mathrm{def}}{=}\forall x\forall y[{\psi }_{\mathsf{SAT}}(x,y)\to {\psi }_{\mathsf{SAT}}(x,f(x))]$$

$${\mathsf{LB}}_k^{\text{a.e.}}(h)\stackrel{\mathrm{def}}{=}\neg {\mathsf{UB}}_k^{i.o.}(h),$$

Full text

Can we show that a large set of techniques cannot prove that $\mathsf{NP}$ is easy infinitely often?

Motivated by this and related questions about the interaction between mathematical proofs and computations, we investigate circuit complexity from the perspective of logic.

Among other results, we prove that for any parameter $k\geq 1$ it is consistent with theory $T$ that computational class ${\mathcal{C}}\not\subseteq\textit{i.o.}\mbox{SIZE}(n^{k})$, where $(T,\mathcal{C})$ is one of the pairs:

$T=\mathsf{T}^{1}_{2}$ and ${\mathcal{C}}=\mathsf{P}^{\mathsf{NP}}$, $\quad T=\mathsf{S}^{1}_{2}$ and ${\mathcal{C}}=\mathsf{NP}$, $\quad T=\mathsf{PV}$ and ${\mathcal{C}}=\mathsf{P}$.

In other words, these theories cannot establish infinitely often circuit upper bounds for the corresponding problems. This is of interest because the weaker theory $\mathsf{PV}$ already formalizes sophisticated arguments, such as a proof of the PCP Theorem [47]. These consistency statements are unconditional and improve on earlier theorems of [31] and [7] on the consistency of lower bounds with $\mathsf{PV}$.

1. Introduction

Understanding the computational power of polynomial size boolean circuits is one of the most mysterious questions in computer science. Despite major efforts to address this problem and significant progress in several restricted settings (e.g. [41, 50, 42]), it is consistent with current knowledge that every problem in $\mathsf{NP}$ can be computed by circuits containing no more than $4n$ gates [19]. This bound is much weaker than the lower bound results conjectured by most (but not all) researchers in the field. For instance, it is reasonable to expect that computing $k$-clique on $n$-vertex graphs requires circuits of size $n^{\Omega(k)}$, but we appear to be very far from establishing a result of this form for unrestricted boolean circuits.

Fixed-polynomial size circuit lower bounds.

Given the difficulty of proving stronger lower bounds for problems in $\mathsf{NP}$, a natural research direction is to investigate super-linear and fixed-polynomial circuit size lower bounds for problems in larger complexity classes. This line of work was started by Kannan [30], who showed that for each $k\geq 1$ there is a problem in $\Sigma^{p}_{2}\cap\Pi^{p}_{2}$ that cannot be computed by circuits of size $n^{k}$. The result was subsequently improved by Köbler and Watanabe [36], who obtained the same lower bound for the class $\mathsf{ZPP}^{\mathsf{NP}}\subseteq\Sigma^{p}_{2}\cap\Pi^{p}_{2}$, and by Cai [10], who showed it for $\mathsf{S}_{2}^{p}\subseteq\mathsf{ZPP}^{\mathsf{NP}}$. Two incomparable results were then obtained by Vinodchandran [53] and Santhanam [51], who proved that $\mathsf{PP}\nsubseteq\mathsf{SIZE}[n^{k}]$ and $\mathsf{MA}/1\nsubseteq\mathsf{SIZE}[n^{k}]$, respectively.111We use $\mathsf{SIZE}[s]$ to denote the set of languages computable by circuits of size at most $s(n)$ on every large enough input length. We say that a language $L$ is in $\textit{i.o.}\mathsf{SIZE}[s]$ if there is a language $L^{\prime}\in\mathsf{SIZE}[s]$ such that $L$ and $L^{\prime}$ agree on infinitely many input lengths.

Modulo the use of a single bit of advice on each input length, Santhanam’s lower bound is known to imply all aforementioned results. Unfortunately, there exist barriers to adapting his techniques to prove super-linear lower bounds for smaller classes such as $\mathsf{NP}$, as explained by Aaronson and Wigderson [2]. Establishing such lower bounds is also open for $\mathsf{P^{\mathsf{NP}}}$, and constitutes an important frontier in the area of fixed-polynomial size lower bounds.222Indeed, a proof that $\mathsf{E}^{\mathsf{NP}}\nsubseteq\mathsf{SIZE}[n^{1.01}]$ would be considered a breakthrough by some researchers in the field. Interestingly, it is known that proving that $\mathsf{P}^{\mathsf{NP}}\nsubseteq\mathsf{SIZE}[n^{k}]$ for all $k$ is equivalent to showing a stronger Karp-Lipton collapse under the assumption that $\mathsf{NP}\subseteq\mathsf{SIZE}[\mathsf{poly}]$ [13].333Some of our consistency results can be interpreted from this perspective: it is possible to establish stronger “logical” Karp-Lipton collapses if $\mathsf{NP}\subseteq\mathsf{SIZE}[\mathsf{poly}]$ and this inclusion is provable in certain theories [12]. We refer to [11, 22] for more information about uniform complexity classes around $\mathsf{P}^{\mathsf{NP}}$.

While existing circuit lower bounds might not be entirely satisfactory from the perspective of the uniform complexity of the problems, there is another important issue with these results: they only establish hardness on infinitely many input lengths. Could it be the case that some natural problems are easy on some input lengths and hard on others? Perhaps the existence of exceptional mathematical structures444In the sense of https://en.wikipedia.org/wiki/Exceptional_object of certain sizes might affect (non-uniform) complexity theory around some input lengths? This possibility seems unlikely, but we are far from understanding the situation. For instance, a basic question in complexity that remains open is whether the nondeterministic time-hierarchy theorem can be extended to an almost-everywhere result (see [3]). On the algorithmic side, an intriguing example is that the natural problem of generating canonical prime numbers admits a faster algorithm on infinitely many input lengths [44], but showing that the algorithm succeeds on all input lengths is open. More recent works such as [20] and [42] show that quite often some control can be obtained over the set of hard input lengths. Still, proving an almost-everywhere circuit size lower bound beyond $4n$ gates remains open even for problems in $\mathsf{MATIME}[2^{n}]$ (see [4] for a related lower bound).

Addressing these questions without further assumptions (i.e. unconditionally) appears to be extremely challenging. In this work, we attempt to provide formal evidence that some problems in lower uniform complexity classes are hard on every large enough input length. This can be done via the investigation of circuit complexity from the perspective of mathematical logic. More precisely, we are interested in unconditional results showing that lower bounds such as $\mathsf{NP}\nsubseteq\textit{i.o.}\mathsf{SIZE}[n^{3}]$ are consistent with certain logical theories.555Note also that establishing a consistency statement is a necessary step before the corresponding circuit lower bound can be unconditionally established, since a true statement is always consistent with a sound theory. To obtain interesting results, we consider theories that can formalize a variety of techniques from algorithms, complexity, and related areas. We focus on first-order theories in the standard sense of mathematical logic, which offers a principled way of investigating consistency statements of the form above. We describe next the theories relevant to our work.

Bounded Arithmetic.

Bounded arithmetic theories are fragments of Peano Arithmetic with close connections to computational complexity and proof complexity. Such theories have been widely investigated by logicians and complexity theorists since the 1970’s. Among the most influential theories we have Cook’s equational theory $\mathsf{PV}$ [16] and its corresponding first-order formalization [32] (see also [26]),666In this paper we use $\mathsf{PV}$ to refer to its first-order formulation (cf. [34, Section 5.3]). Buss’s theories $\mathsf{S}^{1}_{2}$ and $\mathsf{T}^{1}_{2}$ [8], and extensions of these theories by variants of the pigeonhole principle developed primarily by Jeřábek [24, 25, 27, 28] (such as theory $\mathsf{APC}_{1}$ extending $\mathsf{PV}$). The objects of study in these theories are natural numbers (representing finite binary strings), and the basic functions and relations are given by polynomial-time ($p$-time) algorithms in some programming scheme. For instance, Cook [16] relied on Cobham’s theorem [15] that all $p$-time functions can be generated from few initial ones by composition and bounded recursion on notation. For convenience, the language ${L({\mathsf{PV}})}$ we adopt here is the language of $\mathsf{PV}$, having a function symbol for each $p$-time algorithm.777This does not necessarily imply that $\mathsf{PV}$ can prove the relevant properties of its function symbols. For instance, the $\mathsf{AKS}$ algorithm [1] for testing primality appears as some symbol $f_{\mathsf{AKS}}\in L(\mathsf{PV})$, but $\mathsf{PV}$ might not be able to prove that $x$ is prime if and only if $f_{\mathsf{AKS}}(x)=1$. There are relation symbols $=$ and $\leq$ with their usual meaning, and all other relations we want to include are represented by their characteristic functions. The specific axiomatization of $\mathsf{PV}$ is not important here: everything will also work for the theory of all true universal ${L({\mathsf{PV}})}$-sentences (to be denoted by $\mathsf{True}_{0}$), and $\mathsf{PV}\subseteq\mathsf{True}_{0}$. We only note that $\mathsf{PV}$ proves induction for all $p$-time predicates by formalizing binary search, cf. [32, 34].

The original language of theories $S^{1}_{2}$ and $T^{1}_{2}$ as defined in [8] is a finite subset of ${L({\mathsf{PV}})}$, but we consider theories $S^{1}_{2}(\mathsf{PV})$ and $T^{1}_{2}(\mathsf{PV})$ in the richer language ${L({\mathsf{PV}})}$. (We will add to these theories even more axioms, which makes any consistency statement stronger.) The principal axioms of the two theories are length-induction (LIND) and induction (IND), respectively, accepted for $\Sigma^{b}_{1}(\mathsf{PV})$-formulas.888We review later in the text some definitions necessary in this work. For more information about standard concepts in bounded arithmetic, we refer to a reference such as [34]. Theory $S^{1}_{2}(\mathsf{PV})$ is close to $\mathsf{PV}$ (it is $\forall\Sigma^{b}_{1}(\mathsf{PV})$-conservative over it), but $T^{1}_{2}(\mathsf{PV})$ appears to be significantly stronger (cf. [34]). Theories $\mathsf{PV}$, $\mathsf{S}^{1}_{2}(\mathsf{PV})$ and $\mathsf{T}^{1}_{2}(\mathsf{PV})$ and their extensions by a form of the pigeonhole principle (often referred to as $\mathsf{dWPHP}$ or $\mathsf{sWPHP}$) are actually quite strong for the purposes of complexity theory. They are now known to formalize many key theorems in algorithms, combinatorics, complexity, and related fields (cf. [54, 8, 34, 49, 25, 24, 27, 28, 14, 45, 46, 47, 6, 37, 43, 38, 40] and references therein).

Recall that the class of $\Sigma^{b}_{1}(\mathsf{PV})$-formulas consists of formulas of the form

[TABLE]

where the $t_{i}$ are ${L({\mathsf{PV}})}$-terms not involving $y_{i}$, and $A$ is quantifier free. The definition of this class in the original language of $S^{1}_{2}$ is a bit more complicated (distinguishing two kinds of bounded quantifiers), but in our language ${L({\mathsf{PV}})}$ it is equivalent to this simpler definition. The class of $\Sigma^{b}_{2}(\mathsf{PV})$-formulas is defined similarly, but the formula $A$ can also be the negation of a $\Sigma^{b}_{1}(\mathsf{PV})$-formula (these negations are $\Pi^{b}_{1}(\mathsf{PV})$-formulas). The predicates definable over the natural numbers by $\Sigma^{b}_{1}(\mathsf{PV})$-formulas and by $\Sigma^{b}_{2}(\mathsf{PV})$-formulas are exactly the predicates from $\Sigma^{p}_{1}=\mbox{NP}$ and from $\Sigma^{p}_{2}$, respectively. We shall denote the theory of all true $\forall\Sigma^{b}_{1}(\mathsf{PV})$-sentences by $\mathsf{True}_{1}$.

Our results.

For an ${L({\mathsf{PV}})}$-formula $\varphi(x)$ and an integer $k\geq 1$, the ${L({\mathsf{PV}})}$-sentence ${\mathsf{UB}^{i.o.}_{k}}(\varphi)$ is defined as follows:

[TABLE]

The sentence ${\mathsf{UB}^{i.o.}_{k}}(\varphi)$ formalizes that the $m$-bit boolean functions defined by $\varphi$ (over different input lengths) are computed infinitely often (i.o.) by circuits of size $m^{k}$.999The notation $1^{(n)}$ means that $n$ is the length of another variable. We abuse notation and use $|C_{m}|$ to denote the number of gates in $C_{m}$. We refer to [46] for a detailed discussion of the formalization of circuit complexity in bounded arithmetic.

We unconditionally establish that almost-everywhere circuit lower bounds for complexity classes contained in $\mathsf{P}^{\mathsf{NP}}$ are consistent with bounded arithmetic theories.

Theorem 1** (Consistency of almost-everywhere circuit lower bounds with bounded theories).**

Let $k\geq 1$ be any positive integer. For any of the following pairs of an ${L({\mathsf{PV}})}$-theory $T$ and a uniform complexity class ${\mathcal{C}}$:

1. (a)

$T=\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$* and ${\mathcal{C}}=\mathsf{P}^{\mathsf{NP}}$,* 2. (b)

$T=\mathsf{S}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{0}$* and ${\mathcal{C}}=\mathsf{NP}$,* 3. (c)

$T=\mathsf{PV}\cup\mathsf{True}_{0}$* and ${\mathcal{C}}=\mathsf{P}$,*

there is an ${L({\mathsf{PV}})}$-formula $\varphi(x)$ defining a language $L\in\mathcal{C}$ such that $T$ does not prove the sentence ${\mathsf{UB}^{i.o.}_{k}}(\varphi)$.

Our arguments are somewhat non-constructive and do not provide a single explicit formula $\varphi(x)$ in each case of the result. Informally, Theorem 1 shows (in particular) the following consistency statements:

[TABLE]

In other words, there are models of these theories (satisfying a large fraction of modern complexity theory) that contain explicit problems that require circuits of size $n^{k}$ on every large enough input length.101010A bit more precisely, the lower bound holds for every input length $n\geq n_{0}$, where $n_{0}$ is an element of the model. Note that $n_{0}$ might be a nonstandard element of this model. Another interpretation is that one can develop theories of computational complexity that postulate the existence of hard problems (as new axioms) without ever proving a contradictory statement.111111One can even contemplate the possibility that more advanced consistency results might allow the development of “logic-based” cryptography: protocols that are unconditionally secure against all efficient algorithms that can be proved correct in a given theory. As alluded to above, given the expressive power of these theories, we view the consistency results as evidence that such lower bounds hold in the standard mathematical universe. Nevertheless, if one strongly believes in an inclusion such as $\mathsf{NP}\subseteq\mathsf{SIZE}[n^{k}]$ for a large enough $k$, then Theorem 1 shows that even to prove this inclusion on infinitely many input lengths it will be necessary to use mathematical arguments that are beyond the reasoning capabilities of the corresponding theories.

We stress that $\mathsf{True}_{0}$ and $\mathsf{True}_{1}$ contain several statements of interest about algorithms, boolean circuits, extremal combinatorial objects, etc. Theorem 1 shows that even assuming such statements as axioms the corresponding theories cannot prove fixed-polynomial size circuit upper bounds.121212For instance, $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$ proves the correctness of the AKS primality testing algorithm (see Footnote 7), i.e., it shows that $\forall x\,(\exists y\,(1<y<x\wedge y\,|\,x)\leftrightarrow f_{\mathsf{AKS}}(x)=0)$ since this sentence is in $\mathsf{True}_{1}$. This implies that this theory proves that primality testing can be done by circuits of size $n^{c}$ for a fixed $c$ on every large enough input length $n$.

We note that the particular syntactic form of $\varphi$ defining the hard language in Theorem 1 items (a) and (c) is irrelevant as long as $p$-time functions and predicates are defined by open formulas of the language of $\mathsf{PV}$ and the SAT predicate used in the argument is defined by a $\Sigma^{b}_{1}$-formula. Indeed, if two open $L(\mathsf{PV})$-formulas define the same predicate then this universal statement is included in theory $\mathsf{True}_{0}$ and hence (c) holds identically for all open formulas defining the same language. An analogous observation applies to (a): languages in $\mathsf{P}^{\mathsf{NP}}$ are definable by $\Delta^{b}_{2}$-formulas w.r.t. the theory131313In other words, the languages have both $\Sigma^{b}_{2}$ and $\Pi^{b}_{2}$ definitions that are provably equivalent in the theory. and the universal statement stating their equivalence is thus in $\mathsf{True}_{1}$.

Related work and techniques.

Some works have investigated the unprovability of circuit lower bounds, or equivalently, the consistency of upper bounds. We refer to the introduction of [40] for more information about this line of work, and to Appendix A for some related remarks that might be of independent interest. Theorem 1 and our techniques are more directly connected to [12], [31], and [7]. We review the relevant results next.

Cook and Krajíček [12] (see also [35]) were the first to systematically investigate the consistency of circuit lower bounds. They established several results showing that $\mathsf{NP}\nsubseteq\mathsf{SIZE}[\mathsf{poly}]$ is consistent with $\mathsf{PV}$, $\mathsf{S}^{1}_{2}$, and $\mathsf{T}^{1}_{2}$ under appropriate assumptions regarding the collapse of $\mathsf{PH}$. For instance, it was shown (in particular) that $\mathsf{T}^{1}_{2}\nvdash\mathsf{NP}\subseteq\mathsf{SIZE}[\mathsf{poly}]$ if $\mathsf{PH}\nsubseteq\mathsf{P}^{\mathsf{NP}}$. While their results are conditional, [12] considered consistency statements for a fixed language in $\mathsf{NP}$ with respect to all polynomial bounds. In [31], two of the authors established an unconditional result showing that $\mathsf{PV}\nvdash\mathsf{P}\subseteq\mathsf{SIZE}[n^{k}]$, where $k$ is any fixed integer. This consistency statement was subsequently improved by [7], who considered a more natural formalization of the statement that a language has circuits of size $O(n^{k})$ and adapted the argument [31] using polynomial-time ultrapowers.141414The formalizations in [31] and [7] differ on how the $O(\cdot)$ notation is handled, and we refer to the corresponding papers for details. Here the sentences ${\mathsf{UB}^{i.o.}_{k}}(\varphi)$ refer to infinitely often upper bounds, and this issue is not relevant. All previous results refer to the consistency of lower bounds on infinitely many input lengths, and Theorem 1 part (c) strictly improves upon [31] and [7].151515In model-theoretic terms, [31] and [7] provide models where the circuit lower bound holds on some large enough input length. A slight modification of the proof in [7] gives a fixed model with arbitrarily large hard input lengths (Moritz Müller, private communication). On the other hand, our results provide a model where the lower bound holds on every large enough input length.

In terms of techniques, the proof of Theorem 1 explores methods from complexity theory and mathematical logic to establish the unprovability of infinitely often upper bounds. We combine ideas from the conditional results of [12] with the unconditional approach of [31]. The general theme is to obtain computational information from proofs in the corresponding bounded theories. For instance, under the assumption that there is a $\mathsf{PV}$-proof $\pi$ that a problem in $\mathsf{P}$ admits non-uniform circuits of size $n^{k}$, we attempt to extract from $\pi$ a more “uniform” construction of such circuits. The ideal plan is to contradict existing lower bounds against uniform circuits, such as those investigated in [52] and other works. However, as explained in [31], implementing this plan is not straightforward, since the “uniformity” one obtains from $\pi$ does not match existing results in the area of uniform circuit lower bounds. Moreover, the proof of Theorem 1 creates additional difficulties because the uniform circuit lower bounds, already insufficient, only hold on infinitely many input lengths. In order to overcome this difficulty, we make use of further insights on the logical side of the argument. In turn, this requires appropriate extensions of the complexity-theoretic arguments.

Extensions and open problems.

One can adapt the methods used in the proof of Theorem 1 to show that $\mathsf{APC}^{1}$ and indeed theory

[TABLE]

for some $L(\mathsf{PV})$-formula $\varphi(x)$ defining a language in $\mathsf{ZPP}^{\mathsf{NP}[O(\log n)]}$.161616This is obtained as in Theorem 1 parts (a) and (b) by proving the following “logical” Karp-Lipton collapse: If $\mathsf{S}^{1}_{2}(\mathsf{PV})\cup\mathsf{sWPHP}(\mathsf{PV})\vdash\mathsf{NP}\subseteq\mathsf{SIZE}[\mathsf{poly}]$ then $\mathsf{PH}$ collapses to $\mathsf{ZPP}^{\mathsf{NP}[O(\log n)]}$. The proof of the latter adapts the argument in [12, Theorem 5.1 (ii)], using randomization to obtain witnesses for the required $\mathsf{dWPHP}$ axioms and an $\mathsf{NP}$ oracle to check that they are correct. (A bit more formally, the idea is to first Skolemize the theory, reducing the argument to the case of $\mathsf{S}^{1}_{2}(\mathsf{PV})$, then to handle the newly introduced function symbols by witnessing them in the standard model through a probabilistic computation with an $\mathsf{NP}$ oracle.) In contrast, existing (infinitely often) lower bounds for $\mathsf{ZPP}^{\mathsf{NP}}$ seem to hold only when the $\mathsf{NP}$ oracle is adaptively queried polynomially many times [36, 10], or with respect to non-adaptive queries but for a promise version of this class (see the discussion in [51, Section 3.2]). There is strong evidence that asking more queries increases computational power (see [11, 17] and references therein), and it is known that polynomially many non-adaptive queries to an $\mathsf{NP}$ oracle are equivalent in power to logarithmic many adaptive queries [23, 5]. The problem of proving super-linear circuit lower bounds for $\mathsf{ZPP}^{\mathsf{NP}}_{\mathsf{tt}}$ (i.e. $\mathsf{ZPP}^{\mathsf{NP}}$ with non-adaptive queries) was investigated recently by [18], and in a sense the consistency statement in (2) addresses this question with respect to $\mathsf{APC}^{1}$.

On the one hand, this consistency statement feels less appealing than the results in Theorem 1 due to its proximity to existing lower bounds in complexity theory. But on the other hand, it highlights the importance of $\mathsf{APC}^{1}$ in connection to frontier questions in complexity theory and lower bounds. As one of our main open problems, we ask for the proof of stronger consistency results for the theory $\mathsf{APC}^{1}$. For instance, can one show that $\mathsf{APC}^{1}\nvdash\mathsf{MA}\subseteq\mathsf{SIZE}[n^{k}]$, partially addressing the use of non-uniform advice in [51]? In connection to this and related problems, it might be fruitful to investigate a potential extension of the equivalence in [13] to a result that relates consistency statements, witnessing theorems, and logical Karp-Lipton theorems.

It would also be interesting to improve our consistency results for $\mathsf{S}^{1}_{2}$ and $\mathsf{T}^{1}_{2}$ with respect to the uniformity of the hard problems, and to establish a non-trivial statement about the consistency of circuit lower bounds with $\mathsf{T}^{2}_{2}$ (Theorem 1 part (a) extends to $\mathsf{S}^{2}_{2}$ using a similar argument and appropriate results from [12]).

We include in Appendix A a discussion on the consistency of $\mathsf{P}\neq\mathsf{NP}$ and its connection to the unprovability of circuit lower bounds.

2. Background and notation

In order to emphasize the main ideas, we assume some familiarity with logic, bounded arithmetic, and complexity theory. Everything needed can be found in [34]. The interested reader can consult [14] for a more recent reference in bounded arithmetic, [9] for a concise introduction, and [48] for an accessible exposition. For more background in circuit complexity, we refer to [29]. For a discussion of the formalization of complexity theory and circuit complexity in bounded arithmetic, see [40] and references therein.

Our proofs will rely on some results and arguments from [12] and [31], and we refer to the detailed presentation in these papers instead of repeating the proofs here. In more detail, what is needed from [12] is that some or their theorems can be modified to include $\mathsf{True}_{0}$ or $\mathsf{True}_{1}$. On the other hand, the proof of Theorem 1 (c) can only be followed if the reader is familiar with the simpler argument from [31].

We use $\mathsf{P}^{\mathsf{NP}[\ell(n)]}$ to denote the set of languages decided by a deterministic polynomial time machine that makes at most $\ell(n)$ queries to an $\mathsf{NP}$ oracle. We will assume without loss of generality that the oracle is some fixed $\mathsf{NP}$-complete language such as formula satisfiability.

3. Consistency of lower bounds with bounded arithmetic

This section proves Theorem 1. Let $k$ be a positive integer. We argue in each item as follows.

(a) We consider two cases. If the polynomial hierarchy $\mathsf{PH}$ collapses to $\mathsf{P}^{\mathsf{NP}}$, then we can define a language $L\in\mathsf{P}^{\mathsf{NP}}$ such that $L\notin\textit{i.o.}\mathsf{SIZE}[n^{k}]$. More precisely, $L$ computes on input length $n$ as the lexicographic first truth-table corresponding to a function $h\colon\{0,1\}^{n}\to\{0,1\}$ that cannot be computed by circuits of size $n^{k}$. This language can be easily specified using a constant number of quantifiers over strings of length $\mathsf{poly}(n)$ (cf. [30]). By the equivalence between languages in $\Sigma^{p}_{i}$ and predicates definable by $\Sigma^{b}_{i}(\mathsf{PV})$ formulas (see e.g. [34, Theorem 3.2.12]), there is an $L(\mathsf{PV})$-formula $\varphi_{L}(x)$ that defines $L$ (using the correspondence between $\{0,1\}^{*}$ and $\mathbb{N}$). Since $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$ is sound and $L$ is hard on every large enough input length, this theory cannot prove the sentence ${\mathsf{UB}^{i.o.}_{k}}(\varphi_{L})$.

Assume now that $\mathsf{PH}$ does not collapse to $\mathsf{P}^{\mathsf{NP}}$. Let $\varphi_{\mathsf{SAT}}(x)$ be a $\Sigma^{b}_{1}(\mathsf{PV})$-formula that defines the formula satisfiability problem (SAT). We take a particular formulation of $\varphi_{\mathsf{SAT}}(x)$ for which the input encoding is paddable, meaning that inputs of the satisfiability problem of length $\ell<m$ can be easily converted into equivalent inputs of length $m$. If $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$ does not prove ${\mathsf{UB}^{i.o.}_{k}}(\varphi_{\mathsf{SAT}})$, we are done, given that this formula defines a language in $\mathsf{NP}\subseteq\mathsf{P}^{\mathsf{NP}}$. Suppose $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}\vdash{\mathsf{UB}^{i.o.}_{k}}(\varphi_{\mathsf{SAT}})$. This formula has unbounded existential quantifiers, but since $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$ is axiomatized by bounded formulas, Parikh’s theorem (cf. [34, Section 5.1]) implies that there is an ${L({\mathsf{PV}})}$-term $t(x)$ such that ${\mathsf{UB}^{i.o.}_{k}}(\varphi_{\mathsf{SAT}})$ is provable in the theory even if the existential quantifiers are bounded by $t({1^{(n)}})$. In particular, $m$ and $|C_{m}|$ in Equation (1) can be bounded as

[TABLE]

By our assumption on paddability, a circuit $C_{m}$ deciding satisfiability on formulas encoded using $m$ bits also works for all formulas of length $n\leq m$. But by (3), $|C_{m}|\leq n^{O(1)}$ and hence $C_{m}$ can serve as a polynomial size circuit solving SAT on formulas of size $n$. Consequently, if $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$ proves that SAT is infinitely often in $\mathsf{SIZE}[n^{k}]$ it also proves that SAT is in $\mathsf{SIZE}[\mathsf{poly}(n)]$. We now invoke the argument of [12, Theorem 5.1 (iii)] who showed (in particular) that if $\mathsf{T}^{1}_{2}$ proves that SAT $\in\mathsf{SIZE}[\mathsf{poly}]$ then $\mathsf{PH}$ collapses to $\mathsf{P}^{\mathsf{NP}}$. Their proof can be adapted to $\mathsf{T}^{1}_{2}(\mathsf{PV})\cup\mathsf{True}_{1}$, since all sentences in $\mathsf{True}_{1}$ are witnessed by $\mathsf{FP}^{\mathsf{NP}}$ functions and adding these sentences as new axioms does not affect the required witnessing theorem.171717In more detail, adding a function symbol for these witnessing functions turns sentences from $\mathsf{True}_{1}$ into universal sentences, and universal sentences do not influence witnessing theorems. For example, if $\forall x\exists y\;(y\leq s(x)\wedge A(x,y))$ is in $\mathsf{True}_{1}$ and $f$ is the symbol for the associated witnessing function, the universal sentence will be $\forall x\;(f(x)\leq s(x)\wedge A(x,f(x)))$. This collapse of $\mathsf{PH}$ is in contradiction to our assumption in this case of the proof, which completes the argument.

(b) Consider the formula $\varphi_{\mathsf{SAT}}(x)$ defined in item (a) above. If $\mathsf{S}^{1}_{2}\cup\mathsf{True}_{0}\nvdash{\mathsf{UB}^{i.o.}_{k}}(\varphi_{\mathsf{SAT}})$ there is nothing else to prove. Otherwise, by the same argument via Parikh’s Theorem it follows that $\mathsf{S}^{1}_{2}\cup\mathsf{True}_{0}$ proves that SAT admits polynomial size circuits on every input length. Now the argument in [12, Theorem 5.1 (ii)] (easily modifiable to handle $\mathsf{True}_{0}$ because axioms in it are universal sentences) implies that every language $L\in\mathsf{PH}$ is also in $\mathsf{P}^{\mathsf{NP}[c\cdot\log n]}$ for some $c\in\mathbb{N}$. In particular, every such language is in $\mathsf{P}^{\mathsf{NP}[n]}$. Consequently, by Kannan’s construction [30] there is a language $L_{\mathsf{hard}}\in\mathsf{P}^{\mathsf{NP}[n]}$ such that $L_{\mathsf{hard}}\notin\textit{i.o.}\mathsf{SIZE}[n^{k+2}]$. We will need the following lemma.181818The proof of the lemma uses ideas from the proof of [33, Proposition 1.3] showing that $\mathsf{S}^{1}_{2}$ can define all $\mathsf{FP}^{\mathsf{NP}[wit,O(\log n)]}$ functions, extending a proof from [8] that $\mathsf{T}^{1}_{2}$ can define all $\mathsf{FP}^{\mathsf{NP}}$ functions. A similar argument was employed in the proof of [21, Theorem 10] (without the infinitely often condition).

Lemma 2**.**

If $\mathsf{NP}\subseteq\textit{i.o.}\mathsf{SIZE}[n^{k}]$ then $\mathsf{P}^{\mathsf{NP}[n]}\subseteq\textit{i.o.}\mathsf{SIZE}[n^{k+2}]$.

Proof 3.1**.**

Let $L$ be a language in $\mathsf{P}^{\mathsf{NP}[n]}$ decided by a deterministic polynomial-time oracle machine $M$ running in time at most $q(n)$. For convenience, we assume without loss of generality that $M$ makes exactly $n$ queries before accepting or rejecting an input string, regardless of the answers provided by its $\mathsf{NP}$ oracle $O$.

We consider the language $L_{\mathsf{aux}}$ containing all tuples $(a,j,b_{1},\ldots,b_{n},1^{(t)},c)$, where $|a|=n$, $1\leq j\leq n$, each $b_{i}\in\{0,1\}$, $t\in\mathbb{N}$ is a padding parameter, and $c\in\{0,1\}$ is a control bit, which satisfy the following conditions:

• •

If $c=0$, then when $M$ computes on $a$ and its first $j$ queries are answered according to $b_{1},\ldots,b_{j}$, for each $i\leq j$ if $y_{i}\in\{0,1\}^{\star}$ is the $i$-th query and $b_{i}=1$ we have $y_{i}\in O$.

• •

If $c=1$, the machine $M$ accepts $a$ within $q(n)$ steps under oracle answers $b_{i}$ for $1\leq i\leq n$.

Since $O\in\mathsf{NP}$ and $M$ is a deterministic polynomial time machine, $L_{\mathsf{aux}}\in\mathsf{NP}$. Using the hypothesis of the lemma, for infinitely many values of $n$ there exists $t\leq 10n$ and a circuit $D_{n}$ for $L_{\mathsf{aux}}$ of size at most $C(n+\log n+n+t+1)^{k}\leq n^{k+1}$ (for large enough $n$) that decides $L_{\mathsf{aux}}$ with respect to our parameter $n$ (the input length for an instance of $L$). Note that the parameter $t$ allows us to hit the “good” input lengths without technical considerations about the input encoding employed in the definition of $L_{\mathsf{aux}}$.

We will use $D_{n}$ (with the correct value $t$ non-uniformly hardcoded in the input) as a sub-routine in order to solve $L$ on inputs of length $n$, as described next. First, we recover the correct oracle answers $d_{1},\ldots,d_{n}$ for a given input string $a$. This is done in $n$ steps, where the $i$-th step recovers $d_{i}$. To recover $d_{1}$, we use $D_{n}$ to compute

[TABLE]

where each $\star$ can be replaced by an arbitrary bit. If the output is $1$, the first query made by $M$ on $a$ has a positive answer with respect to $O$ (since positive queries must be strings in $O$ by the definition of tuples in $L_{\mathsf{aux}}$ when $c=0$). Otherwise, we must have $d_{1}=0$. Next, we invoke

[TABLE]

knowing that the answer to the first query is correct. By the same argument, we are able to recover $d_{2}$, and proceeding similarly, we can recover all correct answers $d_{1},\ldots,d_{n}$. Finally, by invoking $D_{n}(a,n,d_{1},\ldots,d_{n},1^{(t)},1)$ with $c=1$ and using the correct oracle answers, we can decide if $a\in L$. Clearly, this entire computation can be performed by a circuit of size at most $O(n\cdot|D_{n}|)=O(n^{k+2})$, which completes the proof.

It follows from Lemma 2 and the properties of $L_{\mathsf{hard}}$ that there is a language $L\in\mathsf{NP}$ such that $L\notin\textit{i.o.}\mathsf{SIZE}[n^{k}]$. Consequently, if $\varphi_{L}(x)$ is a formula that defines $L$ then $\mathsf{S}^{1}_{2}\cup\mathsf{True}_{0}\nvdash{\mathsf{UB}^{i.o.}_{k}}(\varphi_{L})$. This completes the proof of item (b).

(c) We follow the overall strategy of the proof of [31, Theorem 2.1] (which combines the proof of [52, Theorem 1.1] with other ideas), but the infinitely often statement considered here introduces certain difficulties. In particular, it is not clear how to adapt the proof in [52] to show that $\mathsf{P}$ is not contained infinitely often in $\mathsf{P}$-uniform $\mathsf{SIZE}[n^{k}]$. In general, combining different computations that succeed infinitely often might not produce a computation that succeeds infinitely often. We explain below how the argument from [31] can be modified to establish the stronger statement in part (c). (For simplicity of notation, we restrict our discussion to $\mathsf{PV}$, but the argument works for $\mathsf{PV}\cup\mathsf{True}_{0}$ as well.)

Let $g_{k^{\prime}}$ for $k^{\prime}=3k$ be the $\mathsf{PV}$ function symbol provided by [31, Lemma 3.1]. Recall that $\mathsf{PV}$ proves that any uniform algorithm $h$ running in time at most $n^{k^{\prime}-1}$ will fail to compute $g_{k^{\prime}}$, even if $h$ is given a certain amount of advice that can depend on the input length. If $\mathsf{PV}\nvdash{\mathsf{UB}^{i.o.}_{k}}(g_{k^{\prime}})$ we are done. Otherwise, applying the KPT Theorem (see e.g. [31, Theorem 4.1]) to sentence ${\mathsf{UB}^{i.o.}_{k}}(g_{k^{\prime}})$ (note crucially that ${\mathsf{UB}^{i.o.}_{k}}(g_{k^{\prime}})$ has the right quantifier complexity), we obtain a fixed $r\in\mathbb{N}$ (independent of $n$) and $\mathsf{PV}$ function symbols $f_{1},\ldots,f_{r}$ such that on input $1^{(n)}$ each function $f_{i}$ outputs $n\leq n_{i}\leq n^{a_{i}}$ (represented as $1^{(n_{i})}$) and a circuit $C^{i}_{n_{i}}$ of size at most $n_{i}^{k}$ that is a candidate circuit for $g_{k^{\prime}}$ on inputs of length $n_{i}$ (the upper bound $n^{a_{i}}$ is provable in $\mathsf{PV}$). As usual in applications of the KPT Theorem, each function $f_{i}$ in addition to $1^{(n)}$ might also depend on potential counter-examples to the correctness of the pairs $(n_{j},C^{j}_{n_{j}})$ for $j<i$. In other words, from the provability of ${\mathsf{UB}^{i.o.}_{k}}(g_{k^{\prime}})$ theory $\mathsf{PV}$ proves the universal closure of the following disjunction:191919For simplicity of notation, we left out in each row of (4) the condition $n_{i}\geq n$, for $i=1,2,\ldots,r$.

[TABLE]

Modifying the strategy of [31], we argue that either $\mathsf{PV}\nvdash{\mathsf{UB}^{i.o.}_{k}}(\widetilde{f_{1}})$ for a certain $\mathsf{PV}$ function symbol $\widetilde{f_{1}}$ that depends on $f_{1}$ (we are done in this case), or $\mathsf{PV}$ proves that the circuit $C^{1}_{n_{1}}$ output by $f_{1}(1^{(n)})$ does not succeed in computing $g_{k^{\prime}}$ on inputs of length $n_{1}=n_{1}(1^{(n)})$ for infinitely many values of $n$. It will be important that such values of $n$ are polynomially gapped, and that an infinite set $S_{1}$ of strings of the form $1^{(n)}$ corresponding to them can be enumerated by a $\mathsf{PV}$ function symbol $u_{1}(1^{(\ell)})$. This allows us to eliminate one disjunct in the sentence obtained from the KPT Theorem if we quantify not over $1^{(n)}$ for all $n$ but just over strings $1^{(n)}$ in the image of $u_{1}(1^{(\ell)})$,202020As opposed to [31], which focuses on larger input lengths after each iteration of the argument. since on these specific $1^{(n)}$ the function $f_{1}$ never succeeds in generating a circuit that correctly computes $g_{k^{\prime}}$ on input length $n_{1}=n_{1}(1^{(n)})$, and in addition (as we explain below) there is a $\mathsf{PV}$ function symbol that provably produces counter-examples. The proof of our result can be completed by iterating the argument $r$ times while focusing on the relevant input lengths. The idea is similar in spirit to [31], but the argument is more involved because intuitively we need to consider a chain $S_{r}\subseteq\ldots\subseteq S_{1}$ of infinite sets of input parameters: If $j\leq i$ then $\mathsf{PV}$ proves that function $f_{j}$ from the KPT disjunction (with appropriate counter-examples) does not succeed on $1^{(n)}\in S_{i}$ (assuming the provability of certain auxiliary sentences ${\mathsf{UB}^{i.o.}_{k}}(\widetilde{f_{j}})$). We provide the details next.

Recall that in the terminology of [31] the function symbol $\widetilde{f}$ decides $L_{\mathsf{succ}}$, a padded version of the language $L_{\mathsf{dc}}$ encoding the direct connection language of the circuits generated by $f$. Our definition of $\widetilde{f_{1}}$ is analogous to the construction in [31], but we need to change the amount of padding in order to accommodate the new setting. Here $f_{1}(1^{(n)})$ might generate candidate circuits for $g_{k^{\prime}}$ on larger input lengths. Moreover, the circuits for $\widetilde{f_{1}}$ obtained from the provability of ${\mathsf{UB}^{i.o.}_{k}}(\widetilde{f_{1}})$ are only guaranteed to work infinitely often. Handling these complications in the case of $f_{1}$ (and in subsequent cases) will be possible because $g_{k^{\prime}}$ is hard on every large enough input length and the relevant input lengths ($n_{1}=n_{1}(1^{(n)})\leq n^{a_{1}}$ in the case of $f_{1}$) are provably computable in polynomial time.

In more detail, let $L^{1}_{\mathsf{dc}}$ encode the direct connection language of the sequence of circuits $C^{1}_{n_{1}}$ on $n_{1}\leq n^{a_{1}}$ input bits produced by $f_{1}(1^{(n)})$. Similarly to [31], our language $L^{1}_{\mathsf{succ}}$ will be a succinct version of $L^{1}_{\mathsf{dc}}$. This time we compress the tuples encoding $C^{1}_{n_{1}}$ to:

[TABLE]

where crucially $t$ is arbitrary. (The parameter $t$ is needed in connection to an infinitely often circuit upper bound for $L^{1}_{\mathsf{succ}}$, since it makes this language paddable. The use of $t$ here is different than in [31], where it appears only for convenience and as a function of other input parameters.) Under our assumptions, a $p$-time algorithm $\widetilde{f_{1}}$ deciding $L^{1}_{\mathsf{succ}}$ can be defined in $\mathsf{PV}$. Suppose that $\mathsf{PV}\vdash{\mathsf{UB}^{i.o.}_{k}}(\widetilde{f_{1}})$. Recall that, assuming $C^{1}_{n_{1}}$ is a correct circuit for $g_{k^{\prime}}$, a small circuit for $\widetilde{f_{1}}$ allows one to obtain a short advice string representing a circuit that decides the tuples of $C^{1}_{n_{1}}$, which in turn allows us to compute $g_{k^{\prime}}$ in time $\ll n_{1}^{k^{\prime}-1}$. Arguing in $\mathsf{PV}$ and adapting the proof of [31, Lemma 3.2] in the natural way (i.e. by padding $t$ appropriately and using the almost-everywhere hardness of $g_{k^{\prime}}$), it follows that for infinitely many choices of $1^{(n)}$, $C^{1}_{n_{1}}$ does not compute $g_{k^{\prime}}$ on inputs of length $n_{1}=n_{1}(1^{{(n)}})$. Equivalently,

[TABLE]

Using Herbrand’s Theorem and in analogy to [31, Lemma 3.2], there are $\mathsf{PV}$ function symbols $u_{1}$ and $e_{1}$ witnessing these existential quantifiers. Furthermore, provably in $\mathsf{PV}$ we have $|u_{1}(1^{(\ell)})|\leq\ell^{c_{1}}$ for some constant $c_{1}$. Therefore, we can take $S_{1}$ as the infinite set of strings $1^{(n)}$ obtained from $u_{1}(1^{(\ell)})$ over all choices of $\ell$, and $e_{1}(1^{(\ell)})$ witnesses that the corresponding circuits $C^{1}_{n_{1}}$ are incorrect over the associated input lengths $n_{1}=n_{1}(1^{(n)})$.

The formula obtained from our initial application of the KPT Theorem to ${\mathsf{UB}^{i.o.}_{k}}(g_{k^{\prime}})$ can now be simplified in $\mathsf{PV}$ to a formula equivalent to:

[TABLE]

where the quantifier $\forall 1^{(n)}\in S_{1}$ is expressed in $\mathsf{PV}$ by “$\forall 1^{(\ell)}\,\forall 1^{(n)}$ such that $1^{(n)}=u_{1}(1^{(\ell)})$”. A bit more precisely, the second and later disjuncts in the KPT expression (4) contain functions $f_{i}$ for $i>1$ depending on $1^{(n)}$ and on each $x_{j}$ for which $j<i$, where the $x_{j}$ are the variables for counter-examples to the correctness of circuits $C^{j}_{|x_{j}|}$. Now substitute everywhere $1^{(n)}=u_{1}(1^{(\ell)})$ and $x_{1}=e_{1}(1^{(\ell)})$. By the choice of $u_{1}$ and $e_{1}$, this substitution provably falsifies the first disjunct and also $n_{1}(1^{(n)})\geq n\geq\ell$. Hence (4) is turned into a KPT expression with $r-1$ disjuncts, i.e.:

[TABLE]

where for convenience of notation we have omitted the conditions $n_{i}\geq\ell$, for $i=2,\ldots,r$. One can also replace $f_{2}(u_{1}(1^{(\ell)}),e_{1}(1^{(\ell)}))$ by an equivalent term in the language of $\mathsf{PV}$, say, $f^{\prime}_{1}(1^{(\ell)})$, and similarly for each $f_{i}$ appearing in the expression above. We have therefore eliminated one disjunct from the formula appearing in Equation (4).

The result is proved as in [31] by iterating this argument in the natural way until some derived sentence ${\mathsf{UB}^{i.o.}_{k}}(\widetilde{f_{i}})$ is unprovable or one eliminates all disjuncts. The latter case leads to a contradiction. (Intuitively, the sets $S_{i}$ contain infinitely many elements and on every string $1^{(n)}$ one of the functions obtained from the initial KPT disjunction must succeed when given appropriate counter-examples. Eliminating all disjuncts contradicts the formula obtained from KPT witnessing, or more precisely, one of the subsequent formulas derived from it in the argument presented above.)

For instance, in the case we get $r=2$ after the application of the KPT Theorem, assuming that $\mathsf{PV}$ also proves ${\mathsf{UB}^{i.o.}_{k}}(\widetilde{f^{\prime}_{1}})$, and arguing identically as before, we now get functions $u^{\prime}_{1}$ and $e^{\prime}_{1}$ computing witnesses (lengths and inputs) that circuits provided by $f^{\prime}_{1}$ fail infinitely often to compute $g_{k^{\prime}}$.212121Complementing our initial informal discussion, while the set $S_{1}$ is the range of $u_{1}$, the set $S_{2}\subseteq S_{1}$ is the range of the composed map $u_{1}\circ u^{\prime}_{1}$. This is contradictory, because this time the formula from Equation (5) claims that $f^{\prime}_{1}$ must succeed (recall that $f^{\prime}_{1}(1^{(\ell)})=f_{2}(u_{1}(1^{(\ell)}),e_{1}(1^{(\ell)}))$) as there are no more disjuncts if $r=2$.

This completes the proof of Theorem 1 item (c).

Remark 3**.**

We note that in Theorem 1 it is possible to syntactically enforce the language $L$ to be in the class $\mathcal{C}$ from the formula $\varphi(x)$ and theory $T$. In general, this follows from the definability of these languages in the corresponding theories by formulas of appropriate complexity (see e.g. [9, Section 2.6]). In more detail, for part (a), as we observed in the concluding remarks of Section 1, the consistency result extends to theory $\mathsf{S}^{2}_{2}(\mathsf{PV})$. In this case, a language in $\mathsf{P}^{\mathsf{NP}}$ is definable in the theory via two provably equivalent $\Sigma^{b}_{2}$ and $\Pi^{b}_{2}$ formulas. (The provability of the equivalence needs to be done in $\mathsf{S}^{2}_{2}(\mathsf{PV})$.) For part (b), the corresponding language $L$ is definable in $\mathsf{S}^{1}_{2}(\mathsf{PV})$ by a $\Sigma^{b}_{1}(\mathsf{PV})$ formula. Lastly, for part (c) the proof presented above already implies the claim, since the language is given by a $\mathsf{PV}$ function symbol. Note that in parts (b) and (c) provability in the theory is not necessary: the syntactic form of the formula (i.e. $\Sigma^{b}_{1}(\mathsf{PV})$ and atomic $\mathsf{PV}$ formula, respectively) imply that the language is in the corresponding class.

Acknowledgements

We would like to thank Ján Pich, Rahul Santhanam, and Moritz Müller for several related discussions. We are also grateful to the reviewers for comments that improved our presentation.

This work was supported in part by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2014)/ERC Grant Agreement no. 615075 and by a Royal Society University Research Fellowship. Jan Bydžovský is currently partially supported by the Austrian Science Fund (FWF) under Project P31955.

Appendix A Consistency of $\mathsf{P}\neq\mathsf{NP}$ from unprovability of lower bounds

Imagine that against most expectations $\mathsf{P}$ is actually equal to $\mathsf{NP}$ and there is a polynomial time algorithm $f$ (i.e. a $\mathsf{PV}$ function symbol) that finds a satisfying assignment for all satisfiable formulas. In other words, if $\psi_{\mathsf{SAT}}(x,y)$ denotes an $L(\mathsf{PV})$-formula that checks if $y$ satisfies the formula encoded by $x$, then the sentence

[TABLE]

is true in the standard model. Now suppose that in order to prove the universal statement $\varphi_{\mathsf{P}=\mathsf{NP}}(f)$ in Equation (6) you have to use concepts (definitions, predicates, etc.) that cannot be defined as polynomial-time algorithms. To be more specific, assume that (6) is provable using induction for non-deterministic polynomial-time algorithms (corresponding to theory $\mathsf{T}^{1}_{2}(\mathsf{PV})$), but not using induction for polynomial-time algorithms only (corresponding to theory $\mathsf{PV}$). Could we still maintain that the mere existence of $f$ implies that the satisfiability problem is “feasible”?

This question is more philosophical than mathematical, and we are not going to offer an answer. Instead, we suggest to consider a strictly mathematical question.

Conjecture 4**.**

For no polynomial-time algorithm $f$ theory $\mathsf{PV}$ proves the sentence $\varphi_{\mathsf{P}=\mathsf{NP}}(f)$.

Informally, Conjecture 4 states that $\mathsf{PV}$ and by standard conservation results $\mathsf{S}^{1}_{2}$ are both consistent with $\mathsf{P}\neq\mathsf{NP}$. That is, either $\mathsf{P}\neq\mathsf{NP}$ as often assumed, and hence the conjecture is trivially true, or $\mathsf{P}=\mathsf{NP}$ but you cannot prove it using only polynomial-time concepts and reasoning. For this reason, Conjecture 4 is a formal weakening of the conjecture that $\mathsf{P}\neq\mathsf{NP}$.

We do not claim any originality for the conjecture; not only it follows from $\mathsf{P}\neq\mathsf{NP}$ but the statement is also known to follow from the conjectures that bounded arithmetic does not collapse to $\mathsf{PV}$ or that the Extended Frege propositional proof system is not polynomially bounded. The conjecture must have been also one of the ideas leading Stephen Cook to his seminal paper [16]. We think it is a weakening of the $\mathsf{P}$ vs. $\mathsf{NP}$ conjecture that has an intrinsic relevance to it, and that it ought to be studied more (cf. [12] for more discussion).

In this appendix, we observe that Conjecture 4 is related to the unprovability of circuit lower bounds. For a $\mathsf{PV}$ function symbol $h$ and a circuit size parameter $k\in\mathbb{N}$, consider the sentence

[TABLE]

where ${\mathsf{UB}^{i.o.}_{k}}(h)$ is the sentence from Equation (1). Intuitively, $\mathsf{LB}_{k}^{\textit{a.e.}}(h)$ states that the language defined by $h$ is hard on input length $m$ for circuits of size $m^{k}$ whenever $m\geq n$, for a fixed value $n$.

Theorem 5** (Consistency of lower bounds with $\mathsf{PV}$ from the unprovability of lower bounds).**

If there exists $k\in\mathbb{N}$ such that for no function symbol $h$ theory $\mathsf{PV}$ proves the sentence $\mathsf{LB}_{k}^{\textit{a.e.}}(h)$, then Conjecture 4 holds.

Note that the hypothesis of Theorem 5 is weaker than the assumption that $\mathsf{PV}$ does not prove that $\mathsf{NP}\nsubseteq\mathsf{SIZE}[n^{k}]$ for some $k$. Roughly speaking, Theorem 5 shows that if $\mathsf{PV}$ does not prove circuit lower bounds then $\mathsf{P}\neq\mathsf{NP}$ is consistent with $\mathsf{PV}$.

Proof A.1** (Sketch of the proof of Theorem 5).**

The argument proceeds in the contrapositive. We formalize in $\mathsf{PV}$ the result that if $\mathsf{P}=\mathsf{NP}$ then for each parameter $k$, $\mathsf{P}\nsubseteq\textit{i.o.}\mathsf{SIZE}[n^{k}]$ (see e.g. [39, Theorem 3]). Recall that this is obtained by combining the collapse of $\mathsf{PH}$ to $\mathsf{P}$ together with Kannan’s argument [30] showing that $\mathsf{PH}$ can define languages that are almost-everywhere hard against circuits of fixed-polynomial size. The usual proof of this claim shows via a counting argument the existence of a truth-table of size $2^{n}$ that is hard against circuit size $n^{k}$. A potential issue is that this result might not be available in $\mathsf{PV}$.

We overcome this difficulty as follows. From the provability in $\mathsf{PV}$ that $\mathsf{P}=\mathsf{NP}$, it follows that the hierarchy $\mathsf{T_{2}}(\mathsf{PV})$ of bounded arithmetic theories $\mathsf{T}^{i}_{2}(\mathsf{PV})$ collapses to $\mathsf{PV}$ [32]. Recall that the surjective weak pigeonhole principle $\mathsf{sWPHP}$ for $\mathsf{PV}$ function symbols is provable in $\mathsf{T}^{2}_{2}(\mathsf{PV})$ (see e.g. [34]). Define a $\mathsf{PV}$ function symbol $g$ that takes as input a circuit $C$ of size $n^{k}$ and outputs the first $n^{k+1}$ bits of the truth-table computed by $C$. From $\mathsf{sWPHP}(g)$ we now derive in $\mathsf{PV}$ that the prefix of some truth-table is not computable by circuits of size $n^{k}$, if $n$ is sufficiently large. We can (implicitly) extend the lexicographic first truth-table prefix satisfying this property with zeroes, and use the resulting truth-table to define a $\mathsf{PV}$-formula $\varphi(x)$ with a constant number of bounded quantifiers that defines a language $L$ that is hard against circuits of size $n^{k}$, where the hardness is provable in $\mathsf{PV}$. Since the provability in $\mathsf{PV}$ that $\mathsf{P}=\mathsf{NP}$ implies the provability in $\mathsf{PV}$ that $\mathsf{PH}$ collapses to $\mathsf{P}$, it follows that $\varphi(x)$ is equivalent in $\mathsf{PV}$ to the language defined by some $\mathsf{PV}$ function symbol $h$. In other words, $\mathsf{PV}\vdash\mathsf{LB}_{k}^{\textit{a.e.}}(h)$, which completes the proof of Theorem 5.