<p>Cook's theory <span class="math-container">$\mathsf{V}^0$</span> and the relativized Buss hierarchy <span class="math-container">$\mathsf{T}_2(\alpha)$</span> both have propositional translations to <span class="math-container">$\mathsf{AC}^0$</span>-Frege. As well, both prove (different) formulations of the reflection principle for <span class="math-container">$\mathsf{AC}^0$</span>-Frege. My question is, given a proof in <span class="math-container">$\mathsf{T}_2(\alpha)$</span> of some <span class="math-container">$\forall\Sigma^b_i(\alpha)$</span>-sentence, how would one give a corresponding proof in <span class="math-container">$\mathsf{V}^0$</span>?</p>
<p>To make this more formal, let me instantiate this with the weak pigeonhole principle <span class="math-container">$\mathsf{WPHP}^{2n}_n(\alpha)$</span>, where <span class="math-container">$\alpha$</span> specifies the pigeon oracle. From Maciel-Pitassi-Woods, we know <span class="math-container">$\mathsf{T}^2_2(\alpha)\vdash \mathsf{WPHP}^{2n}_n(\alpha)$</span>. What formulation of the weak pigeonhole principle is <span class="math-container">$\mathsf{V}^0$</span> able to prove? In particular, can <span class="math-container">$\mathsf{V}^0 \vdash \mathsf{WPHP}^{2n}_n(f)$</span> for any <span class="math-container">$f\in\mathsf{FAC}^0$</span>? If so, what does the proof look like in comparison to the <span class="math-container">$\mathsf{T}^2_2(\alpha)$</span> proof? I guess my confusion is in going from <span class="math-container">$\Sigma^b_i(\alpha)$</span>-induction for <em>arbitrary</em> <span class="math-container">$i$</span> in the relativized Buss Hierarchy to just the use of <span class="math-container">$\Sigma^B_0$</span>-comprehension in <span class="math-container">$\mathsf{V}^0$</span>.</p>

CC BY-SA 4.0
2024-12-18T07:51:49.333Z
This won’t work. You’re forgetting that $\mathsf{V^0}$ translates to *polynomial* $\mathsf{AC}^0$-Frege proofs, whereas $\mathsf{T_2}(\alpha)$ to *quasipolynomial* $\mathsf{AC}^0$-Frege proofs. Indeed, you get $\mathsf{V^0}$ proofs from $\mathsf{I\Delta_0}(\alpha)$ proofs, while $\mathsf{T_2}(\alpha)$ only yields proofs in a quasipolynomial version of $\mathsf{V^0}$. Otherwise, this correspondence is pretty trivial: an $\mathsf{I\Delta_0}(\alpha)$ proof essentially *already is* a $\mathsf{V^0}$ proof, where you treat the numbers of $\mathsf{I\Delta_0}(\alpha)$ as referring to the ...
Emil Jeřábek
CC BY-SA 4.0
2024-12-18T07:53:30.723Z
... unary number sort of $\mathsf{V^0}$, and you treat $\alpha$ as a free variable of the string sort. Actually, it appears you want $\alpha$ to be a function rather than a predicate; so translate it to a predicate first.
Emil Jeřábek
CC BY-SA 4.0
2024-12-18T07:59:21.467Z
Note that it is an *open problem* whether $\mathsf{V^0}$ can prove WPHP, and whether there are polynomial-size $\mathsf{AC^0}$-Frege proofs of WPHP.
Emil Jeřábek
CC BY-SA 4.0
2024-12-18T14:27:03.280Z
I see. Is there cryptographic evidence that $\mathsf{V}^0$ does not prove WPHP?
Stefan G.
<proof-complexity><first-order-logic><ac0>
Translating between proofs in bounded arithmetic theories $\mathsf{V}^0$ and $\mathsf{T}_2(\alpha)$
Stefan G.
# Translating between proofs in bounded arithmetic theories $\mathsf{V}^0$ and $\mathsf{T}_2(\alpha)$

(Asked by: username_0 on 2024-12-18)

Cook's theory $\mathsf{V}^0$ and the relativized Buss hierarchy $\mathsf{T}\_2(\alpha)$ both have propositional translations to $\mathsf{AC}^0$-Frege. As well, both prove (different) formulations of the reflection principle for $\mathsf{AC}^0$-Frege. My question is, given a proof in $\mathsf{T}\_2(\alpha)$ of some $\forall\Sigma^b\_i(\alpha)$-sentence, how would one give a corresponding proof in $\mathsf{V}^0$?

To make this more formal, let me instantiate this with the weak pigeonhole principle $\mathsf{WPHP}^{2n}\_n(\alpha)$, where $\alpha$ specifies the pigeon oracle. From Maciel-Pitassi-Woods, we know $\mathsf{T}^2\_2(\alpha)\vdash \mathsf{WPHP}^{2n}\_n(\alpha)$. What formulation of the weak pigeonhole principle is $\mathsf{V}^0$ able to prove? In particular, can $\mathsf{V}^0 \vdash \mathsf{WPHP}^{2n}\_n(f)$ for any $f\in\mathsf{FAC}^0$? If so, what does the proof look like in comparison to the $\mathsf{T}^2\_2(\alpha)$ proof? I guess my confusion is in going from $\Sigma^b\_i(\alpha)$-induction for *arbitrary* $i$ in the relativized Buss Hierarchy to just the use of $\Sigma^B\_0$-comprehension in $\mathsf{V}^0$.

**Tags:** proof-complexity, first-order-logic, ac0

> **Comments:**
> **username_1**: This won’t work. You’re forgetting that $\mathsf{V^0}$ translates to *polynomial* $\mathsf{AC}^0$-Frege proofs, whereas $\mathsf{T_2}(\alpha)$ to *quasipolynomial* $\mathsf{AC}^0$-Frege proofs. Indeed, you get $\mathsf{V^0}$ proofs from $\mathsf{I\Delta_0}(\alpha)$ proofs, while $\mathsf{T_2}(\alpha)$ only yields proofs in a quasipolynomial version of $\mathsf{V^0}$. Otherwise, this correspondence is pretty trivial: an $\mathsf{I\Delta_0}(\alpha)$ proof essentially *already is* a $\mathsf{V^0}$ proof, where you treat the numbers of $\mathsf{I\Delta_0}(\alpha)$ as referring to the ...  
> **username_1**: ... unary number sort of $\mathsf{V^0}$, and you treat $\alpha$ as a free variable of the string sort. Actually, it appears you want $\alpha$ to be a function rather than a predicate; so translate it to a predicate first.  
> **username_1**: Note that it is an *open problem* whether $\mathsf{V^0}$ can prove WPHP, and whether there are polynomial-size $\mathsf{AC^0}$-Frege proofs of WPHP.  
> **username_0**: I see. Is there cryptographic evidence that $\mathsf{V}^0$ does not prove WPHP?  

---

## 0 answers

