[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^2 + c where c is 1/n in case a given Turing machine halts at 
step n (counting from n = 1), 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^2 + c had zero or one real 
root you would have decided whether the given Turing machine halts.

Vaughan Pratt