 Since HA proves the law of the excluded middle for every primitive recursive predicate, it follows that for such \(A\) the derivability of \(\neg\neg \exists x A(x)\) in HA implies the derivability of \(\exists x A(x)\) as well. From this it follows that PA is \(\Pi^0_2\)-conservative over HA. That is, for primitive recursive \(A\):  \[  {\bf PA} \vdash \forall x \exists y A(x,y)   \Rightarrow   {\bf HA} \vdash \forall x \exists y A(x,y). \]   Thus the class of provably recursive functions of HA coincides with the class of provably recursive functions of PA, a property that, on the basis of the ideas underlying constructivism and intuitionism, may not come as a surprise. 