Intuitionistically unprovable statements about the natural numbers

Question

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.)

Answer 1

Here is one possible such statement: every function $f : \mathbb{N} \to \mathbb{N}$ is either injective or "constructively non-injective", i.e. $$\forall f : \mathbb{N} \to \mathbb{N}, (\forall m, n \in \mathbb{N}, f(m) = f(n) \rightarrow m = n) \lor (\exists m, n \in \mathbb{N}, m \ne n \wedge f(m) = f(n)).$$

To give an informal argument why this is not provable in intuitionistic logic, consider an instance of the halting problem, a Turing machine along with an initial tape state. Then we can construct a function $f : \mathbb{N} \to \mathbb{N}$ where $f(n)$ gives an integer encoding of the execution state after executing the Turing machine for $n$ steps, including the current state number, the contents of the tape, and the position of the "read/write head". Then, using a combination of ${\vee}E$, and ${\exists}E$ along with analyzing the involved cycle in the second case to see whether it represents an infinite loop or whether it represents "holding at the terminating state", from a constructive proof of the statement above we would be able to derive an algorithm for solving the halting problem, giving a contradiction.

Answer 2

There is a bunch of examples. Let me give more examples, although Daniel Schepler's example is nice.

The obvious example is the law of the excluded middle. Wait, you may not count excluded middle as a statement that is not related to natural numbers. I think it may depend on how to instantiate the excluded middle. For example, the statement $\forall x(x\in\mathbb{N}\lor x\notin\mathbb{N})$ is an unprovable example of the excluded middle.

Note that, however, the law of excluded middle for bounded statements on the natural number is provable (from Heyting arithmetic and its weakening, or whatever.) Here the bounded statement means every bounded variable of a quantifier has a bounded size. e.g., $\forall x<5\exists y<z (x+y<z)$ is a bounded formula.

Its formal proof uses induction on formulas, but the following description would be helpful for why the excluded middle for bounded formulas holds: evaluating every instance of a bounded formula just takes a finite time, hence we can decide its validity.

The consequences of the excluded middle would be interesting. For example, the omniscience principles are constructively unprovable statements on natural numbers:

(The limited omniscience principle $\mathsf{LPO}$) Let $\phi(x)$ be a decidable statement on natural numbers. (i.e., $\phi(n)\lor\lnot\phi(n)$ for all $n\in\mathbb{N}$. Then $$(\exists n\in\mathbb{N} \phi(n))\lor (\forall n\in\mathbb{N} \lnot\phi(n)).$$

There are various weakening of $\mathsf{LPO}$, and interestingly, they intertwine with various statements of (constructive) analysis. For example, $\mathsf{LPO}$ holds if and only if the trichotomy of real numbers holds (under the presence of the countable choice.)

Another example is the Markov's principle $\mathsf{MP}$:

(Markov's principle) If $\phi$ is decidable, then $$\lnot\lnot\exists n\in\mathbb{N} \phi(n)\to\exists n\in\mathbb{N}\phi(n).$$

Markov's principle is equivalent to the following fact on real numbers: if $a\ge 0$ and $a\neq 0$, then $a>0$.

The variations of $\mathsf{LPO}$ and the Markov's principle are classical statements that are not provable constructively. Constructive reverse mathematics studies how to reduce ordinary statements of constructive mathematics to the known classical principles, like $\mathsf{LPO}$ and $\mathsf{MP}$. This field is pioneered by Ishihara Hajime, and you may refer to Hans Diener's Habilitation thesis for details.

---

Let me finish my answer with a slight digression. We know that not every function on natural numbers is computable classically. In constructive mathematics, every function can be computable. This is known as Church's thesis. The negation of the Church's thesis also fits into your question.

Answer 3

> "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 disagree with the implicit assumption that Goodstein's theorem is much different from Godel's statement in terms of being 'purely a statement about numbers'. In the first place, merely stating Goodstein's theorem requires encoding of arbitrary-length finite sequences of naturals and worse still the procedure of decomposing a given natural number into 'hereditary base-$n$' notation takes non-trivial computational work, and you would have no choice but to resort to expressing it as a computation if you want to state it in the language of arithmetic. That would make the resulting arithmetical sentence just as complicated as Godel sentences in that you have to interpret it as a statement about some encoded computation.

> "I'm hoping for something along the lines of Goodstein's theorem [...]"

There is a trivial sentence that satisfies your criteria: $G∨¬G$ where $G$ is Goodstein's theorem.

HA (Heyting Arithmetic) satisfies the disjunction property, and hence if it proves $G∨¬G$ then it would either prove $G$ or prove $¬G$. But we believe that PA is consistent, and so HA (being weaker than PA) does not prove $G$. And we also believe that $G$ is true and HA is arithmetically sound, and so HA cannot prove $¬G$.