PA is conservative over HA for $\Pi^{0}_{2}$ sentences. If $\phi$ is $\Delta^{0}_{1}$, then $\forall x [\phi (x) \vee \neg \phi (x)]$ is equivalent to a $\Pi^{0}_{2}$ sentence. Since PA trivially proves that sentence in the language of arithmetic, oughtn't HA to too? What am I missing?
(The usual counterexample offered for $\Pi^{0}_{3}$ sentneces is an instance of the same applied to $\phi$ of $\Sigma^{0}_{2}$ complexity, which made me think...)
If $\phi(x,y)$ and $\psi(x,y)$ are quantifier free formulas of PA such that $$ \text{HA} \vdash (\forall x)[(\exists z)\phi(x,z) \leftrightarrow \lnot (\exists y)\psi(x,y)] \qquad (*) $$ then in HA we can prove the following sequence of formulas are all pairwise equivalent: $$ \begin{split} &(\forall x)[(\exists y)\psi(x,y) \lor \lnot (\exists y)\psi(x,y)] \\ &(\forall x)[(\exists y)\psi(x,y) \lor (\exists z)\phi(x,z)] \qquad\qquad(\dagger)\\ &(\forall x)(\exists y)(\exists z)[\psi(x,y)\lor \phi(x,z)] \end{split} $$ The equivalence of the first two is by assumption. The equivalence of the second and third can be checked (among other ways) by verifying that the equivalence holds in every Kripke model.
Using the standard number theoretic method to combine existential number quantifiers, which can be formalized in HA, the last formula in the list above is equivalent over HA (and thus also over PA) to a formula of the form $$ (\forall x)(\exists x)\theta(x,w) $$ where $\theta$ is $\Delta^0_0$, that is, $\theta$ has only bounded quantifiers.
Therefore, by the result that PA is conservative over HA for $\Pi^0_2$ sentences of PA, we have that $$ \text{PA} \vdash (\forall x)[(\exists y)\psi(x,y) \lor \lnot (\exists z)\psi(x,z)] $$ if and only if $$ \text{HA} \vdash (\forall x)[(\exists y)\psi(x,y) \lor \lnot (\exists z)\psi(x,z)] $$ as long as (*) above holds for $\psi$.
The limitation in this result is that we assumed (*) above at the beginning, and in particular that $\phi$ and $\psi$ are quantifier-free (we could take them to be $\Delta^0_0$ as well).