Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
1Igor Oliveira (University of Warwick)
https://simons.berkeley.edu/talks/igor-oliveira-university-warwick-2023-03-21-0
Proof Complexity and Meta-Mathematics
While there has been progress in establishing the unprovability of complexity statements in lower fragments of bounded arithmetic, understanding the limits of Jeřábek's theory APC_1 (2007) and of higher levels of Buss's hierarchy S^i_2 (1986) has been a more elusive task. Even in the more restricted setting of Cook's theory PV_1 (1975), known results often rely on a less natural formalization that encodes a complexity statement using a collection of sentences instead of a single sentence. This is done to reduce the quantifier complexity of the resulting sentences so that standard witnessing results can be invoked.
In this work, we establish unprovability results for stronger theories and for sentences of higher quantifier complexity. In particular, we unconditionally show that APC_1 cannot prove strong complexity lower bounds separating the third level of the polynomial hierarchy. In more detail, the lower bound sentence refers to the non-uniform setting (∃∀∃ Circuits vs. ∀∃∀ Circuits) and to a mild average-case lower bound for polynomial size circuits against sub-exponential size circuits.
Our argument employs a convenient game-theoretic witnessing result that can be applied to sentences of arbitrary quantifier complexity. We combine it with extensions of a technique introduced by Krajíček (2011) that was recently employed by Pich and Santhanam (2021) to establish the unprovability of lower bounds in PV_1 and in a fragment of APC_1.
Based on joint work with Jiatu Li (Tsinghua University)