Reverse Mathematics of Complexity Lower Bounds

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are necessary to prove a given theorem. In this work, we systematically explore the reverse mathematics of complexity lower bounds. We explore reversals in the setting of bounded arithmetic, with Cook's theory PV1 as the base theory, and show that several natural lower bound statements about communication complexity, error correcting codes, and Turing machines are equivalent to widely investigated combinatorial principles such as the weak pigeonhole principle for polynomial-time functions and its variants. As a consequence, complexity lower bounds can be formally seen as fundamental mathematical axioms with far-reaching implications. The proof-theoretic equivalence between complexity lower bound statements and combinatorial principles yields several new implications for the (un)provability of lower bounds. Among other results, we derive the following consequences: • Under a plausible cryptographic assumption, the classical single-tape Turing machine (n2)-time lower bound for Palindrome is unprovable in Jerabek's theory APC1. The conditional unprovability of this simple lower bound goes against the intuition shared by some researchers that most complexity lower bounds could be established in APC1. • While APC1 proves one-way communication lower bounds for Set Disjointness, it does not prove one-way communication lower bounds for Equality, under a plausible cryptographic assumption. • An amplification phenomenon connected to the (un)provability of some lower bounds, under which a quantitatively weak lower bound is provable if and only if a stronger (and often tight) n^c lower bound is provable. • Feasibly definable randomized algorithms can be feasibly defined deterministically (APC1 is over PV1) if and only if one-way communication complexity lower bound for Set Disjointness are provable in PV1.