Dedekind versus Cauchy reals

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Paul has asked why most constructivists have a preference for Cauchy numerals.
Well, most constructivists haven't since under the widely accepted AC_N they
coincide. This, of course, doesn't deny the fact that in many sheaf toposes
AC_n fails. But from point of view of the BHK interpretation AC_N is most
natural.

But I think the reason for prefering Cauchy over Dedekind has a quite
pragmatic reason. What you are interested in is a Cauchy sequence of reals
with a fixed rate of convergence (ensuring e.g. that the n-th item has distance
< 2^{-n} to the limit). AC_N of course allows you to magically find a modulus
of convergence for every Cauchy sequence. But like Church's Thesis or Brouwer's
Theorem this is sort of a Deus ex machina (actually those are 2 contradictory
dei ex machina!) and thus of moderate help for exact computation on the reals.

If you base your reals on Dedekind's idea you may certainly compute with them
but the result isn't very telling because a computable Dedkind real is a
semidecision procedure telling you whether a given rational interval contains
the (ideal) real under consideration. This doesn't help you at all to compute
the real up to a given precision because you have to first guess the right
interval. Of course, you may consider a partition of some area of guesses
and apply the semidecision procedure to all those intervals in parallel. But
that's very inefficient and can't be implemented within usual sequential
programming languages.

Thomas