[FOM] When is it appropriate to treat isomorphism as identity?
Vaughan Pratt
pratt at cs.stanford.edu
Sat May 23 22:53:59 EDT 2009
Andrej Bauer wrote:
> On Fri, May 22, 2009 at 3:15 AM, Vaughan Pratt <pratt at cs.stanford.edu> wrote:
>> 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.
>
> I was not going to trifle over your construction, but since you would
> like to compare notes, I should say that your construction does not
> work :-), at least not if you want rational numbers to be represented
> in the usual way by their numerators and denominators.
Sorry, I should have been clearer that I was addressing only the case of
computable coefficients, not rational coefficients per se. (Recall that
Karim asked about both cases.) As it happened my example of a
computable coefficient was provably rational (at least when argued
classically), but this aspect wasn't essential to the example.
> [...] Reductions of the Halting problem to various properties of numbers
> typically use a limiting process, i.e., a number is defined as an
> (effective) limit of an (effective) Cauchy sequence with known speed
> of convergence.
Yes, that was what I was assuming for my example.
>> 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.
>
> No, this is not the case. Constructive analysis _can_ speak about
> rational and real numbers _without_ mentioning their representations.
> Instead we can use the universal properties: the rationals are the
> initial field, the reals are the Cauchy-complete archimedean ordered
> field (you have to write down the trichotomy law for < in a
> constructively acceptable way), the complex numbers are the algebraic
> closure of the reals, etc. (Incidentally, I think the last word on a
> universal characterization of the reals has not been said.)
First, as a picky point, the rationals are not the initial field (there
are no ring homomorphisms from Q to GF(4) for example). Q *is* the
initial ordered field however, but now you need to bring in order earlier.
Second, I don't understand in what sense the elements of an initial
algebra aren't thereby being represented. For example the natural
numbers can be understood as either the initial algebra with one
constant 0, one unary operation s, and no laws, or the free monoid on
one generator. In the former case 3 is represented as s(s(s(0))), in
the latter as III (writing I for the generator). These are not the same
representation, in fact they don't even belong to equivalent categories.
The best one can say is that they are inequivalent variants of tally
notation.
> Concerete representations can be recovered when constructive
> mathematics is interpreted in a realizability model, see e.g.,
>
> http://math.andrej.com/2007/01/21/rz-a-tool-for-bringing-constructive-and-computable-mathematics-closer-to-programming-practice/
Granted logicians seem to have a predilection for the term "s(s(s(0)))"
as representing 3 more canonically than say "III" or "3". (Personally I
prefer III because it greatly shortens Russell and Whitehead's proof
that I+I = II.) But how do you get from there to the stronger claim
that this representation is so canonical that it is not a
representation? Putting a mortal on a pedestal doesn't make them
immortal without special dispensation.
Vaughan
More information about the FOM
mailing list