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