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

[Vaughan Pratt]

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