When does classical logic speed up arithmetic? Let $HA$ denote the theory of Heyting Arithmetic, referring to the intuitionistic fragment of $PA$. Is there some infinite set of formulas $\Gamma$ such that both $HA \vdash \Gamma$ and $PA \vdash \Gamma$, yet the length of the shortest cut-free $HA$-proof of some formula $\phi \in \Gamma$ grows asymptotically faster than its shortest cut-free proof in $PA$?
In particular, are there sets of only $\Sigma_0$- or $\Sigma_1$-formulas such that this condition holds? Quantifier-free formulas can be ruled out, I think, since $HA$ decides equality on naturals and thus is equivalent to $PA$ on these formulas with only a multiplicative slowdown.
 A: I'm not sure if this is exactly what you want, but there's a fairly short argument along those lines. Given a natural number $n$, you can produce by Gödel style diagonalisation a sentence $\varphi$ that says "$\varphi$ is not provable by a derivation of length less than $n$". I believe this ends up being $\Delta_0$. By the usual diagonal tricks $\varphi$ is provable in $\mathbf{HA}$, but it is also true, and so has no derivation shorter than $n$. Then $\varphi \vee \neg \varphi$ is also provable in $\mathbf{HA}$ by first proving $\varphi$ and then applying $\vee$-introduction. Moreover, in cut free intuitionistic sequent calculus that is the only possible way to derive $\varphi \vee \neg \varphi$. On the other hand, in $\mathbf{PA}$ $\varphi \vee \neg \varphi$ is simply an instance of excluded middle and so has a trivial proof. For example, in the formulation of classical sequent calculus $\mathbf{LK}$ on the wikipedia page this can be done in 4 steps using $(I)$, $(\vee R_1)$, $(\vee R_2)$, and finally the right hand contraction rule, $(CR)$.
You might worried about the length of the formula $\varphi$, since it increases at least linearly with $n$. In that case you can instead consider $\varphi$ stating "$\varphi$ is not provable by a derivation of length less than $F(n)$" where $F$ is any primitive recursive function. That can ensure the shortest possible proof grows faster than the length of $\varphi$. I think this would make $\varphi$ a $\Sigma_1$ sentence.
