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

[Andrej Bauer]

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.

For every (description of) Turing machine T define a rational number
q_T as you do:

q_T = 1/n if T stops in the n-th step
q_T = 0    otherwise

If there were an algorithm for computing q_T from T, then we could
solve the Halting oracle by checking whether q_T equals zero (which
can be done because we just look at the numerator of q_T).

Your number q_T can be defined as a real number. It is

q_T = lim_k q_{k,T}

where

q_{k,T} = 1/k if T does not stop in the first k steps
q_{k,T} = 1/n if T stops in the n-th step and n <= k

There is an algorithm that computes q_T, i.e., produces a sequence of
rationals that converge to q_T, together with an explicit rate of
convergence.

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.

> 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.)

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/

With kind regards,

Andrej