TR24-083 Authors: Lijie Chen, Jiatu Li, Igor Carboni Oliveira

Publication: 21st April 2024 19:11

Downloads: 131

Keywords:

We show that there is a constant $k$ such that Buss's intuitionistic theory $\mathbf{IS}^1_2$ does not prove that SAT requires co-nondeterministic circuits of size at least $n^k$. To our knowledge, this is the first unconditional unprovability result in bounded arithmetic in the context of worst-case fixed-polynomial size circuit lower bounds. We complement this result by showing that the upper bound $\mathbf{NP} \subseteq \mathbf{coNSIZE}[n^k]$ is unprovable in $\mathbf{IS}^1_2$.