[FOM] Role of Polemics/Clarification

[Harvey Friedman]

This is a clarification of a point in
http://www.cs.nyu.edu/pipermail/fom/2006-January/009598.html

There I wrote

THEOREM A. Every polynomial of several variables, with integer coefficients,
assumes a value closest to the origin.

And that this is provable in PA but not in HA. In fact, provably equivalent
to single quantifier PA over intuitionistic EFA.

I didn't make it clear that I was considering only integral arguments. Of
course, many FOM readers would automatically assume that that is what I was
talking about. 

For real arguments, the statement is provable in, say, intuitionistic RCA0.
For rational arguments, the statement is refutable with, e.g., P(x) = x^2
-2. 

I should have written

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

The above is 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).

It does cover some polynomials whose coefficients are not all integers -
e.g., n(n+1)/2. The same results hold for

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

Harvey Friedman