Intuitionistic first-order logic is first-order logic without the law of the excluded middle. A statement $P$ can be proven in classical first-order logic precisely when its double negation translation can be proven intuitionistically. (The double negation translation of $P$ is closely related to $\neg \neg P$.)
I'm curious about examples of statements that can be proven classically but not intuitionistically, in the context of arithmetic. Are there any known, simple, easily-understood statements about the natural numbers (i.e. statements of Peano arithmetic) for which this is the case?
Of course, "Simple" and "easily understood" are subjective properties, but basically I'm asking for statements about prime numbers and so on, rather than for complicated constructions based on Gödel numbering and the like. (Though in the absence of any simple or easily understood examples, any example at all would be helpful.)
As an illustrative example, Goodstein's theorem is known to be unprovable in PA but provable in a stronger theory, and it can be understood purely as a statement about numbers. (This is in contrast to Gödel statements, which, while they technically are statements about numbers, can't readily be understood without interpreting them as statements about something else.) I'm hoping for something along the lines of Goodstein's theorem, but where the statement is provable in PA, if and only if you assume the law of the excluded middle.
Edited to emphasise: I'm asking for statements of Peano arithmetic, rather than statements of ZFC or another set theory. That means in particular that every term has to be a natural number, not a function or a set. (I mention this because, although they are both good answers, both answers so far concern set theoretic statements, not statements of PA.)