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

[Vaughan Pratt]

On 5/21/2009 2:31 AM, karim zahidi wrote:
 > On Wed, 20 May 2009, Andrej Bauer <andrej.bauer at andrej.com> 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.

Consider (x+c)^2 where c is 1/n in case a given Turing machine halts 
within n > 0 steps, or zero if it never halts.  c is a computable real 
number (it can be computed to within any desired precision), but if you 
could decide whether (x+c)^2 had zero or one real root you would have 
decided whether the given Turing machine halts.

Vaughan Pratt