A Theory for Probabilistic Polynomial-Time Reasoning

In this work, we propose a new bounded arithmetic theory, denoted APX1, designed to formalize a broad class of probabilistic arguments commonly used in theoretical computer science. Under plausible assumptions, APX1 is strictly weaker than previously proposed frameworks, such as the theory APC1 introduced in the seminal work of Jeřábek (2007). From a computational standpoint, APX1 is closely tied to approximate counting and to the central question in derandomization, the prBPP versus prP problem, whereas APC1 is linked to the dual weak pigeonhole principle and to the existence of Boolean functions with exponential circuit complexity.

A key motivation for introducing APX1 is that its weaker axioms expose finer proof-theoretic structure, making it a natural setting for several lines of research, including unprovability of complexity conjectures and reverse mathematics of randomized lower bounds. In particular, the framework we develop for APX1 enables the formulation of precise questions concerning the provability of prBPP = prP in deterministic feasible mathematics. Since the (un)provability of P versus NP in bounded arithmetic has long served as a central theme in the field, we expect this line of investigation to be of particular interest.

Our technical contributions include developing a comprehensive foundation for probabilistic reasoning from weaker axioms, formalizing non-trivial results from theoretical computer science in APX1, and establishing a tailored witnessing theorem for its provably total TFNP problems. As a byproduct of our analysis of the minimal proof-theoretic strength required to formalize statements arising in theoretical computer science, we resolve an open problem regarding the provability of AC 0 lower bounds in PV1, which was considered in earlier works by Razborov (1995), Krajíček (1995), and Müller and Pich (2020).