概率多项式时间推理的一种理论
A Theory for Probabilistic Polynomial-Time Reasoning
AI总结：
本文提出一种新的有界算术理论$APX_1$，用于形式化概率性论证，并解决了$AC^0$下界在$PV_1$中的可证性问题。
摘要：
在本工作中，我们提出了一种新的有界算术理论，记为$APX_1$，旨在形式化理论计算机科学中广泛使用的各类概率性论证。在合理的假设下，$APX_1$严格弱于之前提出的框架，例如Jerabek（2007） seminal work中引入的理论$APC_1$。从计算角度来看，$APX_1$与近似计数以及去随机化中的核心问题，即prBPP与prP问题密切相关，而$APC_1$则与弱鸽巢原理以及存在具有指数电路复杂度的布尔函数相关。引入$APX_1$的主要动机是其较弱的公理揭示了更精细的证明论结构，使其成为几个研究方向的自然环境，包括复杂性猜想的不可证性以及随机下界的反向数学。特别是，我们为$APX_1$开发的框架使能够提出关于prBPP=prP在确定性可行数学中可证性的精确问题。由于P versus NP在有界算术中的（不可）证性长期以来一直是该领域的核心主题，我们预计这一研究方向将特别有趣。我们的技术贡献包括发展从较弱公理出发的概率推理的全面基础，将理论计算机科学中的非平凡结果形式化为$APX_1$，并建立其可证总TFNP问题的定制见证定理。作为我们分析形式化理论计算机科学中出现的陈述所需的最小证明论强度的副产品，我们解决了关于$AC^0$下界在$PV_1$中可证性的开放问题，该问题在Razborov（1995）、Krajicek（1995）以及Müller和Pich（2020）的先前工作中被考虑过。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
