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

[Vaughan Pratt]

On 5/21/2009 2:06 PM, Andrej Bauer wrote:
> On Thu, May 21, 2009 at 11:31 AM, karim zahidi 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.

Andrej, since your answer isn't entirely consistent with mine, maybe we 
should compare notes.  In my example of the polynomial x^2 + c where c 
is 1/n if a certain Turing machine halts at the n-th step and 0 
otherwise, c meets the criterion for being a computable number.  However 
c is also clearly rational, we just don't find out which rational until 
T halts, and may never find out, in which case c = 0, which is still 
rational.

To sort this out you might want to further specify that the rational 
coefficients are presented in some pre-agreed normal form for which 
equality is decidable.

The concept of a rational number divorced from its representation is 
intrinsically nonconstructive.  Constructive analysts probably shouldn't 
talk about rational numbers at all, or integers for that matter, other 
than perhaps as a way of speaking about some pre-agreed representation 
of them for which equality is decidable, and then only in situations 
where there is no danger of this sort of confusion.

Vaughan