Welcome to MathOverflow

Question

11

2

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.

edited Feb 16 2012 at 0:24

asked Feb 12 2012 at 1:34

Brad Rodgers
970●6●13

6

It is worth noting that every Π<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 2012 at 21:59

3

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 at 15:55

Andreas Blass · Accepted Answer · 2012-02-12 02:40:18Z UTC

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

François G. Dorais · Answer 2 · 2012-02-12 03:16:11Z UTC

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.

Danko Ilik · Answer 3 · 2013-04-28 11:58:37Z UTC

1

I am not sure that the examples given by Andreas and François are correct as stated. Extracting a recursive realizer involves adding (the arithmetical version of) Church's Thesis (CT) to HA. So, the examples given are those of statements provable in PA (which refutes CT) but not not provable in HA+CT -- not only HA.

answered Apr 28 at 11:58

Danko Ilik
11●1

I'm confused: to what are you referring when you say "(which refutes CT)"? – András Salamon Apr 28 at 12:13

2

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 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 at 13:16

1

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 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 at 18:04

show 2 more comments

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

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

3 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.