What can be proven in Peano arithmetic but not Heyting arithmetic?

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.

-
It is worth noting that every &Pi;<sub>2</sub> formula that is provable in PA is also provable in HA, so any example must be more complex than that. –  Russell O'Connor Feb 13 '12 at 21:59
It's also worth noting that complexity over HA and complexity over PA are rather different. The examples below are of the form $\Pi_1 \lor \Sigma_1$, which is equivalent to a $\Pi_2$ statement in PA but not in HA. –  François G. Dorais Apr 28 '13 at 15:55

The first example that occurs to me is (a formalization in the language of arithmetic, via coding, of) "For every Turing machine M and every input x, the computation of M on input x either terminates or doesn't terminate." With classical logic, this is trivially provable, as an instance of the law of the excluded middle. But it's not intuitionistically provable because the halting problem is undecidable. (In a bit more detail, if it were provable, then it would be recursively realizable, and the realizer would be an index for an algorithm that solves the halting problem.)

-
Andreas, I think Danko Ilik is right that there is a subtle issue with the parenthetical remark if the universal quantification on $M$ and $x$ inside the statement. However, the easy fix is to let $M$ and $x$ be closed terms and only conclude that there are such closed terms such that "the computation of M on input x either terminates or doesn't terminate" is not provable in HA. –  François G. Dorais May 30 '13 at 17:06
@François: the proof seems OK to me; realizability works for all sentences; every provably total function of HA is computable. –  Carl Mummert May 30 '13 at 20:44
Yes, but that realizability is not necessarily provable in HA. In reality, that doesn't matter much at all, except that Andreas's statement is not accurate if interpreted exactly the wrong way (as Danko apparently did). –  François G. Dorais May 30 '13 at 23:41
Maybe I should repeat here what I wrote in a comment on Danko's answer. I claim only that, if HA proved the statement "for all M and x the computation terminates or doesn't terminate", then that statement is realizable. I don't claim that this realizability is provable in HA. If one really wants to be formal, I suppose I'm claiming that the realizability is provable in ZFC (obviously overkill). Any realizer for that statement would be an index of a recursive function assigning to each M and x certain information that includes a decision whether M terminates on input x. –  Andreas Blass May 31 '13 at 12:32
Actually, Carl is completely right. My arrows were pointing the wrong way: every provable sentence in HA is provably realizable in HA but the converse is not true. Apologies for the confusion. –  François G. Dorais May 31 '13 at 13:38

First, since Peano Arithmetic (PA) is simply Heyting Arithmetic (HA) with the Law of Excluded Middle, everything provable in HA is provable in PA. The negative translation can be used to transform every statement $\phi$ into a statement $\phi^N$ such that (1) PA proves that $\phi$ and $\phi^N$ are logically equivalent, and (2) PA proves $\phi$ if and only if HA proves $\phi^N$. So PA and HA are relatively close to each other.

For a statement provable in PA but not in HA, consider the classically valid statement $\forall \bar{x}(p(\bar{x}) \neq 0) \lor \exists \bar{x}(p(\bar{x}) = 0)$, where $p(\bar{x})$ is a polynomial in the variables $\bar{x} = x_1,\dots,x_n$. In order for this to be provable in HA, we must have either a proof of $\forall \bar{x}(p(\bar{x}) \neq 0)$ or a proof of $\exists \bar{x}(p(\bar{x}) = 0)$. A proof of the former would show that the problem $p(\bar{x}) = 0$ has no solution, and a proof of the latter would show that the problem $p(\bar{x}) = 0$ has a solution. Since proofs are finite, this gives an effective procedure to decide whether the Diophantine equation $p(\bar{x}) = 0$ has a solution. Because of the negative solution to Hilbert's Tenth Problem, we know that there is some polynomial $p(\bar{x})$ such that $\forall \bar{x}(p(\bar{x}) \neq 0) \lor \exists \bar{x}(p(\bar{x}) = 0)$ is not provable in HA.

-
(My example is actually pretty much the same as Andreas's but I think using Diophantine equations makes things a bit more concrete than Turing machines, so I decided to post it anyway.) –  François G. Dorais Feb 12 '12 at 3:18
Thanks! I put the 'check mark' by Andreas's answer just because he posted it first, but this was helpful as well. –  Brad Rodgers Feb 13 '12 at 4:23

A proof in HA of statements like $\forall m\forall x (\exists y T(m,x,y) \vee \neg\exists y T(m,x,y))$ is, in itself, not enough to extract recursive functions solving unsolvable problems (which would show that such statements are not provable in HA).

It has been suggested that this somehow follows from the disjunction and existence properties (DP, EP) of HA (see François' comment), however one can only apply DP and EP on closed statements, while statements like the one above have a prefixing $\forall m \forall x \cdots$.

That is why in recursive realizability (Kleene number realizabilty), that extracts recursive functions from intuitionistic arithmetic proofs, one must assume a version of the formal arithmetical Church's Thesis like CT$_0$: $\forall x\exists y A(x,y) \to \exists e\forall x\exists u (T(e,x,u)\wedge A(x,U(u))$, that allows to transform the $\forall\exists$-quantifier-alternation from $\forall m\forall x\exists z ((z=0\to\exists y T(m,x,y)) \wedge (z\neq 0 \to \neg\exists y T(m,x,y)))$ into a $\exists\forall$-one. Now, as the result is a closed statement one can apply EP to extract a recursive function solving an unsolvable problem.

However, the last argument would just show that the original statement is not provable in HA+CT$_0$ while being provable in PA -- ignoring the fact that $\neg$CT$_0$ is provable in PA.

Indeed, the statement $\neg$CT$_0$ is an example of a statement provable in PA, but not provable in HA. The latter follows from existence of models of HA refuting CT$_0$ (for ex. PA itself).

On the other hand, a natural statement was demanded in the original question, and I am not sure $\neg$CT$_0$ is so natural.

-
I'm confused: to what are you referring when you say "(which refutes CT)"? –  András Salamon Apr 28 '13 at 12:13
Have you said what you meant to say? If a statement isn't provable in HA+something, then how could it be provable in HA? –  Joel David Hamkins Apr 28 '13 at 12:56
In particular, you say "not not provable in HA+CT", with double negation; is this really what you mean? –  Joel David Hamkins Apr 28 '13 at 13:16
I think Danko is thinking about the fact that HA proves $\phi$ is realizable (in the sense of Kleene) if and only if HA + CT (or HA + ECT?) proves $\phi$. The answers don't rely on this deep characterization result, they only rely on the fact that HA is recursively axiomatizable and has the disjunction property. –  François G. Dorais Apr 28 '13 at 15:49
To clarify, when I wrote "if it were provable, then it would be recursively realizable", I meant to assert just that, not that it is itself provable in this or that formal system (except possibly the system ZFC, which I normally rely on). (Incidentally, it seems that Danko's answer, by bumping the question to the front page, has gotten my answer four new upvotes.) –  Andreas Blass Apr 28 '13 at 18:04