Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
Jiatu Li, Igor Carboni Oliveira · 2023
While there has been progress in establishing the unprovability of complexity statements in lower fragments of bounded arithmetic, understanding the limits of Jerabek’s theory APC1 (2007) and of higher levels of Buss’s hierarchy S2i (1986) has been a more elusive task. Even in the more restricted setting of Cook’s theory PV (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.