[FOM] When is it appropriate to treat isomorphism as identity?
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