Hi. I'll confess from the start to not being a logician. In fact this question came up not from research but during a discussion with a friend about whether the classical proof that $\sqrt{2}$ is irrational can be made acceptable to an intuitionist. (It can be.)

The question is: Are there any "natural" statements which can be proven in Peano Arithmetic, but not in Heyting Arithmetic (Peano Arithmetic but with a logic that does not admit the law of the excluded middle)?

In fact, any statements -- even pathological ones -- that can be proven in one but not the other would be interesting to me, since I wasn't able to come up with any. (Even after doing a few web searches!) But of course, the closer to the surface the better.