A Theory for Probabilistic Polynomial-Time Reasoning

TL;DR

This work introduces APX_1, a minimal bounded-arithmetic theory that formalizes probabilistic polynomial-time reasoning via a dedicated approximate-counting oracle $\P$. By constraining counting with local, boundary, and precision axioms, APX_1 enables a self-contained probabilistic calculus, including expectation, independence, and concentration inequalities, while remaining strictly weaker than Jeřábek’s APC_1 under plausible assumptions. The authors demonstrate formalizations of classical TCS results (Yao’s D2P, Schwartz–Zippel, BLR, and AC^0 parity lower bounds) within APX_1 and showcase a tailored witnessing theorem that reduces $\forall\Sigma^b_1(PV)$-consequences to the total-search problem $\mathsf{Refuter}(\mathsf{Yao})$, with connections to derandomization via $\mathsf{LossyCode}$ and reverse mathematics of randomized lower bounds. The framework clarifies which probabilistic reasoning can be carried with weaker axioms and opens pathways to unprovability and reverse-m mathematics of randomized lower bounds, while providing a baseline for feasible derandomization questions such as whether $\mathsf{pr}\BPP=\mathsf{prP}$ admits a feasible proof. Overall, APX_1 offers a solid, minimal foundation for probabilistic reasoning in feasible mathematics and a bridge between proof complexity and algorithmic derandomization.

Abstract

In this work, we propose a new bounded arithmetic theory, denoted $APX_1$, designed to formalize a broad class of probabilistic arguments commonly used in theoretical computer science. Under plausible assumptions, $APX_1$ is strictly weaker than previously proposed frameworks, such as the theory $APC_1$ introduced in the seminal work of Jerabek (2007). From a computational standpoint, $APX_1$ is closely tied to approximate counting and to the central question in derandomization, the prBPP versus prP problem, whereas $APC_1$ is linked to the dual weak pigeonhole principle and to the existence of Boolean functions with exponential circuit complexity. A key motivation for introducing $APX_1$ 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 $APX_1$ 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 $APX_1$, 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 $PV_1$, which was considered in earlier works by Razborov (1995), Krajicek (1995), and Muller and Pich (2020).

Theorems & Definitions (183)

• Remark 1.1: Computational Aspects of $\mathsf{dWPHP}$
• Remark 1.2: Minimal Assumption for Derandomization
• Remark 1.3: $\mathsf{PV}$ and $\mathsf{PV}_1$
• Remark 1.4: Example: Union Bound in $\APX_1$; see \ref{['thm: union bound']}
• Remark 1.5: Example: One-Sided Error Reduction in $\APX_1$; see \ref{['thm:one-sided']}
• Theorem 1.6: Average-Case $\AC^0$ Lower Bound for $\oplus_n$ in $\APX_1$
• Theorem 1.7: Worst-Case $\AC^0$ Lower Bound for $\oplus_n$ in $\PV_1$
• Remark 1.8: $\mathsf{Refuter}(\mathsf{Yao})$ and Derandomization
• Theorem 1.9: Witnessing for $\APX_1$
• Theorem 1.10: Main Equivalence Result (Informal); see \ref{['thm:rev_equivalences']}