What can be proven in Peano arithmetic but not Heyting arithmetic? - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-20T10:13:47Z http://mathoverflow.net/feeds/question/88252 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/88252/what-can-be-proven-in-peano-arithmetic-but-not-heyting-arithmetic What can be proven in Peano arithmetic but not Heyting arithmetic? Brad Rodgers 2012-02-12T01:34:30Z 2013-05-30T16:06:34Z <p>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.)</p> <p>The question is: <em>Are there any "natural" statements which can be proven in <a href="http://en.wikipedia.org/wiki/Peano_axioms" rel="nofollow">Peano Arithmetic</a>, but not in <a href="http://en.wikipedia.org/wiki/Heyting_arithmetic" rel="nofollow">Heyting Arithmetic</a> (Peano Arithmetic but with a logic that does not admit the law of the excluded middle)?</em> </p> <p>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.</p> http://mathoverflow.net/questions/88252/what-can-be-proven-in-peano-arithmetic-but-not-heyting-arithmetic/88253#88253 Answer by Andreas Blass for What can be proven in Peano arithmetic but not Heyting arithmetic? Andreas Blass 2012-02-12T02:40:18Z 2012-02-12T02:40:18Z <p>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.)</p> http://mathoverflow.net/questions/88252/what-can-be-proven-in-peano-arithmetic-but-not-heyting-arithmetic/88256#88256 Answer by François G. Dorais for What can be proven in Peano arithmetic but not Heyting arithmetic? François G. Dorais 2012-02-12T03:16:11Z 2012-02-12T03:16:11Z <p>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 <a href="http://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation" rel="nofollow">negative translation</a> 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.</p> <p>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 <a href="http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem" rel="nofollow">Hilbert's Tenth Problem</a>, 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.</p> http://mathoverflow.net/questions/88252/what-can-be-proven-in-peano-arithmetic-but-not-heyting-arithmetic/128995#128995 Answer by Danko Ilik for What can be proven in Peano arithmetic but not Heyting arithmetic? Danko Ilik 2013-04-28T11:58:37Z 2013-05-30T16:06:34Z <p>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). </p> <p>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 <em>closed</em> statements, while statements like the one above have a prefixing $\forall m \forall x \cdots$.</p> <p>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. <em>Now</em>, as the result is a closed statement one can apply EP to extract a recursive function solving an unsolvable problem.</p> <p>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.</p> <p>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).</p> <p>On the other hand, a <em>natural</em> statement was demanded in the original question, and I am not sure $\neg$CT$_0$ is so natural.</p>