[FOM] Classical/Constructive Arithmetic

[Harvey Friedman]

I would like to start two threads, one on classical and constructive
arithmetic and discrete math, the other on classical and constructive real
analysis.

The aim is to concentrate on the following questions.

1. Examples where the known proofs are nonconstructive, and nobody knows if
there are constructive proofs.

2. Examples where the known proofs are nonconstructive, and we know that all
proofs are nonconstructive.

3. Examples where the known proof is nonconstructive, and where one can give
a constructive proof, but all known constructive proofs are grotesque (e.g.,
extremely long, or extremely unpleasant, etc.).

4. Examples where the known proof is nonconstructive, and where one can give
a constructive proof, but it is known that all constructive proofs are
grotesque (e.g., extremely long, or extremely unpleasant, etc.).

5. Conservative extension and non conservative extension results between PA
and HA (Heyting arithmetic = Peano Arithemtic with intuitionistic logic),
and variants thereof.

Here are some things I know.

In

http://www.cs.nyu.edu/pipermail/fom/2006-January/009603.html
http://www.cs.nyu.edu/pipermail/fom/2006-January/009607.html

I stated this:

THEOREM A. Every polynomial P:Z^n into Z^m assumes a value closest to the
origin.

THEOREM A'. Every polynomial P:Z^n into Z^m with integral coefficients
assumes a value closest to the origin.

I.e., there is a value which is at least as close to the origin, in the
Euclidean distance, than any other value.

The above are provable in PA, but not in HA, even for m = 1. In fact, it is
provably equivalent to single quantifier PA over intuitionistic EFA (even if
we fix m = 1). (We can use any reasonable norm, such as Euclidean or sup
norm).

Note that version A is a bit stronger in that it does cover some polynomials
whose coefficients are not all integers - e.g., n(n+1)/2.

Apparently there are quite a number of famous AEA theorems of mathematics
which people would like to prove constructively, but can't. Nobody knows if
they can be proved constructively. Here there is a real criterion:

*if (forall x)(therexists y)(forall z)(R(x,y,z)) can be proved
constructively (i.e., in, e.g., HA), then there is a recursive function f
such that (forall x)(forall z)(R(x,fx,z)) is true*.

So the mathematicians don't have to know hardly anything about HA or
constructivity in general, or even buy into any related philosophy, in order
to get interested and clearly formulate the problem: find a recursive
function f. And also for that, they don't even have to know what recursive
means! They only need to recognize that something is recursive if it is.

Of course, mathematicians are looking for something weaker and stronger
than merely a recursive f such that (forall x)(forall z)(R(x,fx,z)). They
want a "reasonable" function f such that

(forall x)(therexists y < fx)(forall z)(R(x,fx,z)).

This is likely to, but *might* not be enough to give a constructive proof of
(forall x)(therexists y)(forall z)(R(x,y,z)).

Let us summarize this situation by formal results.

THEOREM 1. Let P be an AEA sentence, (forall x)(therexists y)(forall
z)(R(x,y,z,)). Then P has a proof in HA if and only if there is a
presentation of a partial recursive function f such that PA proves (forall
x)(forall z)(R(x,fx,z)).

THEOREM 2. There exists a sentence "(forall x)(R(x)) or (forall x)(S(x))"
which is provable in PA but not in HA.

The above theorem presumably applies to various fragments of PA/HA. In
particular, it applies to EFA = exponential function arithmetic.

Let me remind readers of the following, originally due to Godel.

THEOREM 3. Every AE sentence provable in PA is provable in HA. There is no
significant blowup involved.

Theorem 1 can be extended in the obvious way to prenex sentences.

PROGRAM: Give an appropriate necessary and sufficient criteria for a
sentence to be provable in HA in terms of provability in PA. For striking
progress, one should be doing this for various special syntactic classes, as
I have done here with the known Theorems 1 and 3.

This program should be gone through systematically. Note that syntactic
classes here should not be merely prenex classes. That would be already
clear from Theorem 1 and its obvious extension to prenex sentences.

Also, worthy of discussion, are the status of:

there exists a positive integer n such that e^(e+n) is irrational.

there exists a positive integer n such that e^(pi + n) is irrational.

for all irrationals x there exists a positive integer n such that x^(x+n) is
irrational.

For all irrationals x,y there exists a positive integer n such that x^(y+n)
is irrational.

Some people should push this discussion forward, and then I will return to
it.

Harvey Friedman