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

Vaughan Pratt pratt at cs.stanford.edu
Thu May 21 21:15:42 EDT 2009

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 

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.


More information about the FOM mailing list