Re: "Kantor dust"

[gcuri@math.unipd.it]

Quoting "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>:

> > If the latter then that's no
> > surprise---carrying out constructions with open order filters is less
> > constructive than with the Cauchy sequence concept.  Lubarsky and
> > Rathien in Logic and Analysis 1:2 131-152 have recently made the point
> > that whereas Cauchy reals can be understood constructively as a set, any
> > attempt to make Dedekind's reals constructive turns them into a proper
> > class.
> >
> > Between Dedekind cuts and Cauchy sequences, the more appropriate notion
> > of reals for constructive analysis would surely be the Cauchy reals.
>
> I could take issue with you on this. If you insist that "constructive"
> entails "predicative", then you are  of course right; but in a topos-
> theoretic context, where you don't have countable choice automatically
> available, it's very much the other way round.


Even if one insists that constructive entails predicative the appropriateness of
Cauchy reals is questionable: Lubarsky and Rathjen prove in fact that in a 
subsystem of CZF (Aczel' constructive set theory), i.e., in CZF with
Subset Collection replaced by exponentiation, the Dedekind reals  form a proper
class.
In ordinary CZF (that has no choice principle and no powersets),
the Dedekind reals *do* form a set (Aczel & Rathjen), as do more generally the
points of any weakly set-presented T^*_1 locale (Aczel & Curi),
in particular of any locally compact regular one.

It is also useful to recall that (in "On the Cauchy Completeness of the
Constructive Cauchy Reals", MLQ, 53, No. 4-5 (2007), pp. 396-414)
Lubarsky has  proved that the Cauchy Reals are not complete in intuitionistic
set theory without choice.

There's then the point of view that, constructively, the reals should be
considered as a `space', rather than a set, and that in this perspective they
are more properly regarded e.g. as a locale/formal space (rather than as a
set/class of points with a topology)...

Regards,

   Giovanni Curi

-----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it