A Theory for Probabilistic Polynomial-Time Reasoning
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908825214255104 |
|---|---|
| author | Chen, Lijie Li, Jiatu Oliveira, Igor C. Williams, Ryan |
| author_facet | Chen, Lijie Li, Jiatu Oliveira, Igor C. Williams, Ryan |
| contents | 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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_09302 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Theory for Probabilistic Polynomial-Time Reasoning Chen, Lijie Li, Jiatu Oliveira, Igor C. Williams, Ryan Computational Complexity Logic in Computer Science Logic 03F20 F.4.1; F.0 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). |
| title | A Theory for Probabilistic Polynomial-Time Reasoning |
| topic | Computational Complexity Logic in Computer Science Logic 03F20 F.4.1; F.0 |
| url | https://arxiv.org/abs/2602.09302 |