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

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

2012-02-12T01:34:30Z

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.

Answer by Andreas Blass for What can be proven in Peano arithmetic but not Heyting arithmetic?

2012-02-12T02:40:18Z

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

Answer by François G. Dorais for What can be proven in Peano arithmetic but not Heyting arithmetic?

2012-02-12T03:16:11Z

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.

Answer by Danko Ilik for What can be proven in Peano arithmetic but not Heyting arithmetic?

2013-04-28T11:58:37Z

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.