On the consistency of stronger lower bounds for NEXP

TL;DR

The paper investigates the consistency of stronger NEXP lower bounds within bounded-arithmetic frameworks. It extends the Atserias–Buss–Müller approach by using a two-sorted theory $V^0_2$ augmented with $\forall \tilde{\Sigma}^{1,b}_1(\mathbb{N})$ to capture universal number-sort sentences and to formalize $\mathsf{NEXP}$ predicates as $\tilde{\Sigma}^{1,b}_1$ formulas. The main results show that $\mathsf{NEXP} \notin \mathsf{EXP}/\mathsf{poly}$ is not provable in $V^0_2 + \mathrm{Exp}$ and remains unprovable even in the stronger theory, with a parallel result for $\mathsf{NEXP} \notin \mathsf{coNEXP}$ under a particular coNEXP formalization without parameters. These findings illustrate the limits of current bounded-arithmetic approaches in settling the strongest exponential-time separations and highlight the role of pigeonhole-principle lower bounds and Parikh translations in linking complexity statements to propositional-proof systems.

Abstract

It was recently shown by Atserias, Buss and Mueller that the standard complexity-theoretic conjecture NEXP not in P / poly is consistent with the relatively strong bounded arithmetic theory V^0_2, which can prove a substantial part of complexity theory. We observe that their approach can be extended to show that the stronger conjectures NEXP not in EXP / poly and NEXP not in coNEXP are consistent with a stronger theory, which includes every true universal number-sort sentence.

Theorems & Definitions (10)

• Theorem 1.1: atserias2024consistency
• Theorem 1.2
• Theorem 1.3
• Definition 1.4
• Proposition 2.1
• Lemma 2.2
• proof
• proof : Proof of Proposition \ref{['pro:exp_poly_simple']}
• proof : Proof of Theorem \ref{['the:exp_poly']}
• proof : Proof of Theorem \ref{['the:conexp']}