[FOM] When is it appropriate to treat isomorphism as identity?

[Andrej Bauer]

On Thu, May 21, 2009 at 11:31 AM, karim zahidi
<zahidi at logique.jussieu.fr> wrote:
>> Here is an example: a well educated computer scientist typically knows
>> that a polynomial (with real coefficients) has finitely many roots. He
>> therefore naturally expects that there is a thing called "the number of
>> distinct roots of a polynomial". Surely, such a simple number can be
>> computed, yes? No.
>
> I'm a bit confused by this remark. Surely if the coefficients themselves
> are rational numbers (or even computable real numbers) then this number is
> computable. I guess it comes out of the elimination theory for the reals.

If the coefficients are rational, then the roots are algebraic, and
the field of algebraic numbers has decidable equality (there is an
algorithm which tells whether two algebraic numbers are equal), so we
can count the number of distinct roots.

If the coeffficients are real, then we cannot count the number of
distinct roots because that would give us the Halting Oracle. Here is
how: suppose f is a computable function which accepts a real
polynomial and returns the number of distinct real roots. Consider and
Turing machine T and define the sequence a_0, a_1, a_2, ...

a_n = 0 if T has not stopped in the first n steps of execution
a_n = 1 if T has terminated in n steps or fewer

Define the real number b = sum_n a_n * 2^(-n), and consider the
polynomial p(x) = x^2 - b.
Then we have f(p) = 1 if T does not halt and f(p) = 2 if T halts. So
we can solve the Halting problem.

The elimination theory of the reals does not help because in the
first-order language of the reals-closed fields only the algebraic
numbers are definable. For example the number b above cannot be
expressed in that language. So the elimination theory shows that
equality on the algebraic numbers is decidable, not on all reals.

With kind regards,

Andrej