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.

  • 10
    $\begingroup$ 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. $\endgroup$ Feb 13, 2012 at 21:59
  • 7
    $\begingroup$ 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. $\endgroup$ Apr 28, 2013 at 15:55
  • $\begingroup$ As regards the tag theories-of-arithmetic, see the Meta question Creating theories-of-arithmetic logic tag. $\endgroup$
    – YCor
    Oct 14, 2020 at 9:19

4 Answers 4


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

  • $\begingroup$ 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. $\endgroup$ May 30, 2013 at 17:06
  • 1
    $\begingroup$ @François: the proof seems OK to me; realizability works for all sentences; every provably total function of HA is computable. $\endgroup$ May 30, 2013 at 20:44
  • $\begingroup$ 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). $\endgroup$ May 30, 2013 at 23:41
  • 1
    $\begingroup$ 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. $\endgroup$ May 31, 2013 at 12:32
  • $\begingroup$ 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. $\endgroup$ May 31, 2013 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.

  • 6
    $\begingroup$ (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.) $\endgroup$ Feb 12, 2012 at 3:18
  • 1
    $\begingroup$ Thanks! I put the 'check mark' by Andreas's answer just because he posted it first, but this was helpful as well. $\endgroup$ Feb 13, 2012 at 4:23

According to Harvey Friedman, the following theorem is provable in PA but not HA:

Every polynomial $P:\mathbb{Z}^n \to \mathbb{Z}^m$ with integer coefficients assumes a value closest to the origin.

That is, there is a value which is at least as close to the origin, in the Euclidean distance, than any other value. This is unprovable in HA even when $m=1$.

  • $\begingroup$ That's very interesting, and surprising on the surface of it -- thanks for adding this answer! It's been a while since I've thought about this, but I would be interested in further references if you or anyone knows of them. A little naively, I wonder if the provability in HA changes if the coefficients of the polynomials have restricted to be generated according some 'constructive procedure'. $\endgroup$ Dec 2, 2018 at 21:27
  • 2
    $\begingroup$ The theorem says that there exists some attained value $x$ with the property that no value smaller than $x$ is attained. The sticking point is that, by the negative results on Hilbert's tenth problem, we have no algorithmic method of verifying that no smaller value is attained. To "fix" this we have to restrict to some family of polynomials for which we have effective algorithms for determining that a given value is not attained. Constructivity of the coefficients is sort of irrelevant. $\endgroup$ Dec 2, 2018 at 21:56

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.

  • $\begingroup$ I'm confused: to what are you referring when you say "(which refutes CT)"? $\endgroup$ Apr 28, 2013 at 12:13
  • 2
    $\begingroup$ 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? $\endgroup$ Apr 28, 2013 at 12:56
  • $\begingroup$ In particular, you say "not not provable in HA+CT", with double negation; is this really what you mean? $\endgroup$ Apr 28, 2013 at 13:16
  • 2
    $\begingroup$ 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. $\endgroup$ Apr 28, 2013 at 15:49
  • 2
    $\begingroup$ 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.) $\endgroup$ Apr 28, 2013 at 18:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.