FOM: Intuitionistic reals

[Alex Simpson]

In intuitionistic set theory (the exact variant doesn't much  
matter), many classically equivalent descriptions of the set 
of real numbers give rise to different notions of intuitionistic 
reals.  For example, there are different definitions of "Cauchy reals",
obtained by varying the notion of Cauchy sequence (of rationals)
and perhaps also the notion of equivalence between Cauchy sequences.
Nevertheless, there is a widely accepted `correct' intuitionistic 
definition, according to which the rate of convergence of a Cauchy 
sequence must be given by a function (from natural numbers to 
rationals), in which case the definition of the equivalence of
Cauchy sequences is uncontroversial (the two most natural alternatives 
agree). In fact, an equivalent and often more convenient approach
is to assume a fixed rate of convergence (e.g. 1/2^i). Thus one can 
define the set of Cauchy reals to be the  set of equivalence classes 
of such fixed-rate-convergent Cauchy sequences of rationals.

I have some questions concerning such Cauchy reals, and other
related notions of real number.


1.  In Troelstra and van Dalen's "Constructivism in Mathematics",
the "Cauchy completeness" of the Cauchy reals is proved by defining
a "Cauchy sequence of reals" to be given by a sequence of representative
Cauchy sequences of rationals. However, a more natural definition of
Cauchy sequence of reals is to take instead sequences of reals themselves
(i.e. sequences of equivalence classes of Cauchy sequences of rationals).
Without number-number choice (by which I mean the, classically provable,
Axiom of Choice for forall-exists prefixes that quantify over natural
numbers - often called AC_{00}) the more natural notion of sequence 
is apparently more general than version using representatives. In fact, 
if the more natural definition is used, it does not seem to be possible 
to prove that the Cauchy reals are Cauchy complete. My first
question is: does anybody know a model for some reasonable intuitionistic 
set theory (e.g. a topos) in which the Cauchy reals are *not* Cauchy 
complete in this sense?


2. In an impredicative set theory, one can also define a natural
notion of Dedekind real (again there is one `correct' definition -
namely R_d in Troelstra and van Dalen). The set of Dedekind reals
*is* Cauchy complete. Thus one can also define the "Cauchy-completed 
reals" R_cc as the intersection of all Cauchy-complete subsets of
R_d containing the rationals Q. Easily, the Cauchy reals, R_c, embed
in R_cc. Thus one has injections:

     R_c  -->  R_cc  -->  R_d

Given number-number choice, both inclusions are isomorphisms. I know
models (e.g. sheaves on R) in which the inclusion R_cc --> R_d is
proper (i.e. it is not an isomorphism). A reformulation of Question 1 is 
whether there exists a model in which the other inclusion, R_c --> R_cc,
is proper. Question 2 is: has anyone seen the Cauchy-completed reals 
(or something equivalent to them) defined before? Any references would 
be very welcome.


3. There is an alternative take on the inclusions in 2. One can define
R_d as: convergent round filters of proper rational intervals (a proper
interval is a pair (q1,q2) with q1<q2; a round filter is a filter
w.r.t. strict (i.e. proper) inclusion of intervals; convergent simply
means that for any epsilon there is an interval of width < epsilon in the
filter). One can also exhibit R_c explicitly as a subset of R_d as
the set of all "countably-based" such filters (where countably-based means
that there exists a function N --> the filter giving a filter base). 
Question 3 is: does there exist similar explicit description of R_cc as 
those filters in R_d satisfying some good property?


4. The above questions are motivated by a geometrically-based approach
to axiomatizing the real numbers that Martin Escardo and I have been
working on. When interpreted in intuitionistic set theory, our
axioms yield the Cauchy-completed reals. The above roundabout 
construction of the Cauchy-completed reals via Dedekind reals makes
crucial use of impredicative notions such as powerset and
intersection of all subsets. Is this essential? More generally, in
predicative intuitionistic set theories, like Aczel's CZF, is it possible
to define *any* reasonable Cauchy-complete notion of real number *without*
first assuming number-number choice?

-- 
Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
Email: Alex.Simpson at dcs.ed.ac.uk             Tel: +44 (0)131 650 5113
FTP: ftp.dcs.ed.ac.uk/pub/als                Fax: +44 (0)131 667 7209  
URL: http://www.dcs.ed.ac.uk/home/als