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).

翻译：本文提出了一种新的有界算术理论，记作$APX_1$，旨在形式化理论计算机科学中常用的一类广泛的概率论证。在合理的假设下，$APX_1$严格弱于先前提出的框架，例如Jerabek（2007）开创性工作中引入的理论$APC_1$。从计算的角度来看，$APX_1$与近似计数以及去随机化中的核心问题——prBPP与prP问题——紧密相关，而$APC_1$则与对偶弱鸽巢原理以及具有指数级电路复杂度的布尔函数的存在性相关联。引入$APX_1$的一个关键动机在于其较弱的公理揭示了更精细的证明论结构，使其成为多个研究方向的自然框架，包括复杂性猜想的不可证性以及随机化下界的逆数学。特别地，我们为$APX_1$开发的框架使得能够精确地提出关于prBPP=prP在确定性可行数学中的可证性问题。由于P与NP问题在有界算术中的（不）可证性长期以来一直是该领域的核心主题，我们预计这一研究方向将具有特别的意义。我们的技术贡献包括：基于较弱公理为概率推理建立全面基础，在$APX_1$中形式化理论计算机科学中的非平凡结果，以及为其可证全的TFNP问题建立一个量身定制的见证定理。作为分析形式化理论计算机科学中陈述所需最小证明论强度的一个副产品，我们解决了一个关于$AC^0$下界在$PV_1$中可证性的开放问题，该问题在Razborov（1995）、Krajicek（1995）以及Muller和Pich（2020）的早期工作中曾被探讨。