Re: Cauchy completeness of Cauchy reals

Re: Cauchy completeness of Cauchy reals

[Andrej Bauer]

Alex Simpson <als@inf.ed.ac.uk> writes:
>
> > The map e : 2^N --> [0,1] defined by
> >
> >   e x = x_0/2 + x_1/4 + x_2/8 + ...
> >
> > is epi in the effective topos, but it is not regular epi.
>
> This is clearly wrong. Every epi is regular, in a topos.
>
> My original statement was correct. In the effective topos,
> the map from binary representations to Cauchy (= Dedekind)
> reals is not epi.

I stand corrected. I am confusing the effective topos with assemblies
(or modest sets) over the first Kleene algebra.

Andrej

Re: Cauchy completeness of Cauchy reals

[Toby Bartels]

Dusko Pavlovic wrote:

>Alex Simpson wrote:

>>Somebody wrote:

>>>that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k
>>>s.t. 1/2^k < e. this is *equivalent* to markov's principle.

>>The property quoted is in fact a trivial consequence of intuitionistic
>>arithmetic alone. It has nothing to do with Markov's principle.

>for a real number e, i am pretty sure that the above is equivalent with
>markov's principle. it must be in books, but i think you can't miss the
>proof if you try.

I don't remember the original context, so I don't know who's right,
but the answer depends on what sort of real number e could be.
It can't be 0, for example, so what can it be?

* If e > 0, then work with 1/e and use the Archimedean property;
  Bishop would recognise and accept this proof.
* But if you only know that e <= 0 is false,
  then you need Markov's principle to deduce e > 0.


-- Toby

Re: Cauchy completeness of Cauchy reals

[Prof. Peter Johnstone]

On Mon, 3 Feb 2003, Vaughan Pratt wrote:
>
> While I'm comfortable with coalgebraic presentations of the continuum, as
> well as such algebraic presentations as the field P/I (P being a ring of
> certain polynomials, I the ideal of P generated by 1-2x) that I mentioned
> a week or so ago, I'm afraid I'm no judge of constructive approaches to
> formulating Dedekind cuts.  Would a toposopher (or a constructivist of
> any other stripe) view the following variants as all more or less equally
> constructive, for example?
>
> 1.  Define a (closed) interval in the reals as a disjoint pair (L,R)
> consisting of an order ideal L and an order filter R, both in the rationals
> standardly ordered, both lacking endpoints.  Order intervals by pairwise
> inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'.
> Define the reals to be the maximal elements in this order.  Define an
> irrational to be a real for which (L,R) partitions Q.
>
> 2.  Ditto but with the reals defined instead to be intervals for which
> Q - (L U R) is a finite set.  ("Finite set" rather than just "finite" to
> avoid the other meaning of "finite interval."  The order plays no role
> in this definition, maximality of reals in the order being instead a
> theorem.)
>
> 3.  As for 2 but with "finite" replaced by "cardinality at most 1".
> The predicate "rational" is identified with the cardinality of Q - (L U R).
>
No constructivist (of whatever stripe) would be happy talking about
Q - (L U R), as in your second and third definitions, since he wouldn't
want to assume that L and R were complemented as subsets of Q.
Your first definition, if I understand it correctly, is equivalent to
what most toposophers would call the MacNeille reals -- that is, the
(Dedekind-MacNeille) order-completion of Q. If you "positivize" the
second and third (which would appear to be equivalent, for any sensible
notion of finiteness) by saying "Whenever p and q are rationals with
p < q, then either p \in L or q \in R", you get the Dedekind reals,
which are a proper subset of the MacNeille reals (though they
coincide iff De Morgan's law holds) but have rather better algebraic
properties.

Peter Johnstone

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

(not sure whether i shouldn't let this thread die, since i didn't read
mail for a week, and we all have things to do. but it's not like this
list is filling anyone's mailbox with megabytes of usolicited research
problems, and it seems a couple more dekabytes on cauchy reals might be
useful.)

Alex Simpson wrote:

>>      |cb(x)i - cb(y)i| <= [... calculation omitted ...]
>>                       <=   1/2^i
>>
>>means that cb(x)i and cb(y)i have the first i digits equal.
>>
>I don't see that cb(x)i and cb(y)i have the first i digits equal.
>
i stand corrected (as they say).

>>now, as everyone has been pointing out, the dyadic representation
>>depends on markov's principle.
>>
>
>This is *not* what has been pointed out (whatever you mean
>by dyadic representation).
>
>What I previously pointed out was that the existence of
>ordinary binary representations may fail even in the presence
>of Markov's principle.
>
dyadic numbers are rationals in the form p/2^n. (google helps with such
things.)

the intuition that dyadic approximation has to do with markov's
principle is supported by the fact that markov's principle is equivalent
with the statement

>>that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k
>>s.t. 1/2^k < e. this is *equivalent* to markov's principle.
>>
>
>The property quoted is in fact a trivial consequence of intuitionistic
>arithmetic alone. It has nothing to do with Markov's principle.
>
for a real number e, i am pretty sure that the above is equivalent with
markov's principle. it must be in books, but i think you can't miss the
proof if you try.

*however* you are right that in my "construction", it is used in a wrong
place, for a rational number, and k exists trivially.

>Such an f is tantamount to giving a splitting to the epi
>
>  r: {x: Q^N | x a Cauchy sequence} --> I_C
>
>where I_C is the Cauchy interval. There are many toposes
>in which Q^N is basically Baire space and I_C is basically
>the closed unit interval in Euclidean space
>Furthermore,
>in many such toposes (e.g. Johnstone's), countable
>choice and Markov's principle both hold.
>
splitting r is only the strongest sense of finding the canonical
representatives, not the only one. r may not split by a topos morphism,
but the canonical representatives can be found externally, and suffice
for a completeness proof.

after all, if i remember correctly, such is the situation with markov's
principle itself: for a decidable P,

* heyting arithmetic does not validate |- ~forall x. P(x) -> exists x.~ P(x)
* but if |-~foral x. P(x) can be derived, then |- exists x.~P(x) can be
derived.

in particular, if i can prove that not all numbers in a binary stream
are 0, then i can extract the first 1 from that proof, although that
proof transformation cannot be internalized as a recursive function, to
realize the implication.

all this is, of course, just more intuitive support for the idea that i
have been trying out, that *dyadic approximations might yield
representatives of cauchy sequences, and since they are a coalgebra,
help with their completeness*. i know that it is probably a wrong idea,
but it also feels wrong to me to settle with incomplete cauchy reals.
i'd like to understand why in the world would toposes deviate from
cantor's idea of continuum, so pervasive in everyday math?

-- dusko

Re: Cauchy completeness of Cauchy reals

[Vaughan Pratt]

While I'm comfortable with coalgebraic presentations of the continuum, as
well as such algebraic presentations as the field P/I (P being a ring of
certain polynomials, I the ideal of P generated by 1-2x) that I mentioned
a week or so ago, I'm afraid I'm no judge of constructive approaches to
formulating Dedekind cuts.  Would a toposopher (or a constructivist of
any other stripe) view the following variants as all more or less equally
constructive, for example?

1.  Define a (closed) interval in the reals as a disjoint pair (L,R)
consisting of an order ideal L and an order filter R, both in the rationals
standardly ordered, both lacking endpoints.  Order intervals by pairwise
inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'.
Define the reals to be the maximal elements in this order.  Define an
irrational to be a real for which (L,R) partitions Q.

2.  Ditto but with the reals defined instead to be intervals for which
Q - (L U R) is a finite set.  ("Finite set" rather than just "finite" to
avoid the other meaning of "finite interval."  The order plays no role
in this definition, maximality of reals in the order being instead a
theorem.)

3.  As for 2 but with "finite" replaced by "cardinality at most 1".
The predicate "rational" is identified with the cardinality of Q - (L U R).

Vaughan

Re: Cauchy completeness of Cauchy reals

[Alex Simpson]

Dear Dusko,

> is there still an error? please ignore the trivial ones this time, and
> i'll try to learn from errors.

Yes, I think there's an error.

> here is a slight modification of sequences from my previous post. let
> Q be the set of rationals between 0 and 1, D <= Q dyadic rationals and
> N natural numbers. a cauchy real A is now a subobject of Q^N such that
>
> [... construction omitted ...]
>
> the proofs proceed like for the corresponding sequences in my previous
> post. in particular, for every x,y : A holds
>
>      |cb(x)i - cb(y)i| <= [... calculation omitted ...]
>                        <=   1/2^i
>
> means that cb(x)i and cb(y)i have the first i digits equal. hence
> dcb(x)i =dcb(y)i. since this holds for all i, dcb(x) = dcb(y).

I don't see that cb(x)i and cb(y)i have the first i digits equal.
It seems possible to have e.g. cb(x)i = .0111 and cb(y)i = .1000.
Indeed, .0111, although it is sufficiently close to b(x)i to
be the value of cb(x)i, may nonetheless be too far from b(y)i
to qualify as a "simpler" candidate for cb(y)i than .1000.

This problem is not easily repaired. In fact, there is a
fundamental obstacle to this approach. Your argument attempts
to construct a function f: Q^N --> Q^N (in your proof given
by f=dcb) satisfying:

  1. f maps any Cauchy sequence to a Cauchy sequence representing
    the same real number.

  2. All sequences that represent the same real number get mapped to
    a single unique Cauchy sequence representative.

Such an f is tantamount to giving a splitting to the epi

  r: {x: Q^N | x a Cauchy sequence} --> I_C

where I_C is the Cauchy interval. There are many toposes
in which Q^N is basically Baire space and I_C is basically
the closed unit interval in Euclidean space
(e.g. Johnstone's "topological topos", many "Gros toposes").
In such toposes, a splitting of r would
correspond to a non-constant continuous function from the
Euclidean interval to Baire space. This is clearly impossible,
as Baire space is totally disconnected. Furthermore,
in many such toposes (e.g. Johnstone's), countable
choice and Markov's principle both hold.

In conclusion, it is impossible to prove the existence of
an f satisfying 1 and 2 above using intuitionistic logic,
even if one further assumes countable choice and Markov's
principle.


Regarding Markov's principle:

> now, as everyone has been pointing out, the dyadic representation
> depends on markov's principle.

This is *not* what has been pointed out (whatever you mean
by dyadic representation).

It is well-known that, in general, very many different
versions of Cauchy sequence coincide, including: Cauchy
sequences of rationals, indeed many variants depending on
properties of the modulus; ditto for sequences of dyadic
rationals; nested sequences of closeed proper intervals;
"signed" binary representation, etc, etc.

What I previously pointed out was that the existence of
ordinary binary representations may fail even in the presence
of Markov's principle.

> in order to prove that the map c is
> total, we need the fact that for every e>0 in Q there is some k such
> that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k
> s.t. 1/2^k < e. this is *equivalent* to markov's principle.

The property quoted is in fact a trivial consequence of intuitionistic
arithmetic alone. It has nothing to do with Markov's principle.
Indeed your function c is total in any elementary topos.

> how bad is markov's principle? well, i think that markov proposed it
> as a valid *intuitionistic* principle:
>
> ** given an algorithm, if i can prove that it terminates, then i
> ** should be able to construct its output.

This is a curious paraphrasing. It should rather be:

  "if the algorithm cannot fail to terminate then ..."

> it would be nice to know that this is all we need in order to have
> cauchy complete cauchy reals.

It would be nice and may be true. At present we don't have a
single example topos in which the Cauchy reals are not complete
(w.r.t. sequences).

However, there is, as yet, no convincing reason to link Markov's
principle to this question.

Best wishes,

Alex

Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209

Re: Cauchy completeness of Cauchy reals

[Toby Bartels]

Dusko Pavlovic wrote in part:

>(i think this does deserve some general interest because we often say
>that categories capture real mathematical practices --- but as it
>happens, cauchy reals are not complete, and the mean value theorem
>fails, and so on. i was hoping to understand where does the usual
>intuition of continuum fail, and what categorical property do we need
>to do basic calculus.

It depends on what you mean by "basic calculus".
Bishop would argue that he can do basic calculus just fine
using a constructive version of the mean value theorem.

This is not to say that you don't have an interesting question;
from the POV of the mathematician on the street (not very theoretical),
classical theorems often follow from constructivist (a la Bishop) one
if you assume that sequentially compact metric spaces are compact
(which means complete and totally bounded to Brouwer and Bishop),
so that might be one place to look.


-- Toby

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

[this is a copy of my post of monday morning, which bounced between
bob and me a couple of times, courtesy of our mailers. -- dusko]


thanks for the replies. sorry to clog people's mailboxes, but i'll
permit myself one more post on cauchy.

(i think this does deserve some general interest because we often say
that categories capture real mathematical practices --- but as it
happens, cauchy reals are not complete, and the mean value theorem
fails, and so on. i was hoping to understand where does the usual
intuition of continuum fail, and what categorical property do we need
to do basic calculus. i came to think that coalgebras help with this,
since they capture the various notions of completeness, and wondered
why they don't capture the standard cauchy completeness argument in
this context. hence my post that invoked the reactions.)

On Sat, 25 Jan 2003 Prof. Peter Johnstone wrote:

>>>> > >If so, what
>>>> > >would "Cauchy reals" mean precisely in this general context?
>>>> > >
>>>
>>>
>>> > it means fundamental sequence, with the equivalence relation in the
>>> > "lazy" mode, a la bishop, as described in andrej bauer's message.
>>> >
>>
>>
>> I'm sorry, but this won't do. In a topos, equality is equality; you can't
>> treat it "lazily". So a Cauchy real has to be an equivalence class of
>> Cauchy sequences, and there is in general no way of choosing a
>> canonical representative for it.
>
>

one would hope that equality in a topos is widely understood, even by
me. treating fundamental sequences up to an equivalence relation in a
lazy mode just means not taking their quotient, but carrying the
explicit equivalence relation. such structures are commonly considered
in toposes. on the other hand, many constructivists (martin-lof,
bishop) say that this is the way to do constructivist
mathematics. (although i am not sure whether i came to think of cauchy
reals in this way because constructivist education left some trace, or
because undergraduate analysis didn't.)

sorry i didn't make all this clear. martin escardo's remark to which i
responded was rather cursory, he just attributed two things, so i kept
mine short. moreover, toposes were not mentioned, and as far as i
remember, the validity in toposes was not discussed either by freyd,
or by vaughan and me. we all talked about streams of digits and it
seemed to me that we were talking about cauchy reals (the
constructivist ones), until peter johnstone observed that freyd =
dedekind++.

On Sat, 25 Jan 2003 Alex Simpson wrote:

>> The question is: does every Cauchy sequence (x_i) in R_C have a
>> limit in R_C
>>
>> Here we are not starting off with a Cauchy sequence of rationals;
>> not even a Cauchy sequence of Cauchy sequences.
>
>

i realized that i typed "let a = (a_i) be a sequence of rationals"
instead of "a sequence of cauchy reals" as soon as i woke up, the
morning after i typed it, and sent a correction a couple of hours
after the post --- but our watchful moderator for some reason didn't
forward it to the list.

in any case, i said i thought that the construction went through for
cauchy sequences of constructivist cauchy reals, as described in
andrej bauer's message:


>> (2) we say that a real _is_ a fundamental sequence, where two reals
>> are claimed "equal" if they coincide (the approach taken by Bishop).
>
>

now it turns out that such cauchy reals don't count, that cauchy reals
must be


>> (1) we say that a real is an equivalence class of fundamental
>> sequences under the relation ~,
>
>

well, call me irresponsible, but i think that the same idea still
applies: the irredundant coalgebraic reals give canonical
representatives for equivalence classes too. with them, one can prove
completeness as usually.

here is a slight modification of sequences from my previous post. let
Q be the set of rationals between 0 and 1, D <= Q dyadic rationals and
N natural numbers. a cauchy real A is now a subobject of Q^N such that

     exists x in A
     forall x in A holds: |xm - xn| < 1/m+1/n
     forall x in A and all y in Q^N holds: |xm - yn| < 2/m+2/n iff y in A.

consider maps b: Q^N --> Q^N, c: Q^N --> D^N and d : D^N --> Q^N,
defined

     b(x)i = x(2^(i+3))
     c(x)i = p/2^n, such that |xi - p/2^n| < 1/2^(i+2)
                         and  |xi - q/2^m| < 1/2^(i+2) implies m>=n of q>=p
     d(x)i = x truncated after i'th digit

** i claim that the image dcb(A) of A along is a representative of A, ie
**
** 1. it is a singleton, and
** 2. an element of A.

this means that the function dcb : Q^N-->Q^N induces a choice function
from Q^N/~ to Q^N, assigning to each cauchy real a cauchy sequence of
ratioanls representing it.

the proofs proceed like for the corresponding sequences in my previous
post. in particular, for every x,y : A holds

     |cb(x)i - cb(y)i| <= |cb(x)i - b(x)i| + |b(x)i-b(y)i| + |b(y)i-cb(y)i| <
                       <  1/2^(i+2)    + 2/2^(i+3)+2/2^(i+3) +    1/2^(i+2) =
                       =  1/2^i

means that cb(x)i and cb(y)i have the first i digits equal. hence
dcb(x)i =dcb(y)i. since this holds for all i, dcb(x) = dcb(y).

now, as everyone has been pointing out, the dyadic representation
depends on markov's principle. in order to prove that the map c is
total, we need the fact that for every e>0 in Q there is some k such
that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k
s.t. 1/2^k < e. this is *equivalent* to markov's principle.

how bad is markov's principle? well, i think that markov proposed it
as a valid *intuitionistic* principle:

** given an algorithm, if i can prove that it terminates, then i
** should be able to construct its output.

it would be nice to know that this is all we need in order to have
cauchy complete cauchy reals.

also, if this is the case, the challenge topos, where cauchy reals are
not complete, would be the realizability topos invalidating markov:
the cauchy sequence without a cauchy limit would have to be the one
that can be proven different from 0, but cannot be proven apart from
0.

is there still an error? please ignore the trivial ones this time, and
i'll try to learn from errors.

all the best,
-- dusko

Re: Cauchy completeness of Cauchy reals

[Alex Simpson]

Andrej Bauer writes:

> The map e : 2^N --> [0,1] defined by
>
>   e x = x_0/2 + x_1/4 + x_2/8 + ...
>
> is epi in the effective topos, but it is not regular epi.

This is clearly wrong. Every epi is regular, in a topos.

My original statement was correct. In the effective topos,
the map from binary representations to Cauchy (= Dedekind)
reals is not epi.

Alex Simpson

Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209

Re: Cauchy completeness of Cauchy reals

[Andrej Bauer]

Alex Simpson <als@inf.ed.ac.uk> writes:
> In fact not. Markov's principle holds in the effective topos, and
> there, unless I'm much mistaken, it is not even true that the map from
> binary representations to Cauchy (= Dedekind) reals in [0,1] is epi,
> let alone split epi.

The map e : 2^N --> [0,1] defined by

  e x = x_0/2 + x_1/4 + x_2/8 + ...

is epi in the effective topos, but it is not regular epi. In terms of
logic, this means that

  forall a : [0,1]. (not not (exists x : 2^n. (e x = a)))

is valid in the effective topos, but

  forall a : [0,1]. (exists x : 2^n. (e x = a))

is not valid.

Andrej

Re: Cauchy completeness of Cauchy reals

[Alex Simpson]

Peter Johnstone writes:

> I'm sorry, but this won't do. In a topos, equality is equality; you
> can't
> treat it "lazily". So a Cauchy real has to be an equivalence class of
> Cauchy sequences, and there is in general no way of choosing a
> canonical representative for it. Markov's principle would, I think
> (I haven't checked the details), suffice to give a canonical
> representation as a binary expansion with no infinite sequence of
> 1's,

In fact not. Markov's principle holds in the effective topos, and
there, unless I'm much mistaken, it is not even true that the map from
binary representations to Cauchy (= Dedekind) reals in [0,1] is epi,
let alone split epi.

Alex Simpson

Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209

Re: Cauchy completeness of Cauchy reals

[Prof. Peter Johnstone]

On Fri, 24 Jan 2003, Dusko Pavlovic wrote:

> >
> >
> >Set. Do you think your construction works in any topos?
> >
> the coalgebraic structures are defined using just arithmetic. in the
> first one, there is the "no infinite sequences of 1s" condition, which i
> am reminded depends on markov's principle; but that is just used in the
> explanation. i don't think there are other constraints.
>
> >If so, what
> >would "Cauchy reals" mean precisely in this general context?
> >
> it means fundamental sequence, with the equivalence relation in the
> "lazy" mode, a la bishop, as described in andrej bauer's message.
>
I'm sorry, but this won't do. In a topos, equality is equality; you can't
treat it "lazily". So a Cauchy real has to be an equivalence class of
Cauchy sequences, and there is in general no way of choosing a
canonical representative for it. Markov's principle would, I think
(I haven't checked the details), suffice to give a canonical
representation as a binary expansion with no infinite sequence of
1's, and then Dusko's argument would suffice to show that the Cauchy
reals are Cauchy complete. But there are many toposes where Markov's
principle fails.

I doubt very much whether the Cauchy reals occur
as a final coalgebra for anything, in any topos where they fail to
coincide with the Dedekind reals, simply because the Dedekind reals
are likely to be a coalgebra for the same endofunctor (and they're
more "final" than the Cauchy reals). Incidentally, Peter Freyd and
I worked out how to do his coalgebra construction constructively,
and I showed that its final coalgebra is the Dedekind interval in any
topos -- the proof is in the Elephant, at the end of section D4.7.

Peter Johnstone

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

>
>
>Set. Do you think your construction works in any topos?
>
the coalgebraic structures are defined using just arithmetic. in the
first one, there is the "no infinite sequences of 1s" condition, which i
am reminded depends on markov's principle; but that is just used in the
explanation. i don't think there are other constraints.

>If so, what
>would "Cauchy reals" mean precisely in this general context?
>
it means fundamental sequence, with the equivalence relation in the
"lazy" mode, a la bishop, as described in andrej bauer's message.

if my last night's posting makes sense, then these constructivist cauchy
reals make a whole lot of difference, because they really let you avoid
the choice and get limits.

-- dusko

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

heh, i typed this late, and managed to confuse the basic assumption.
instead of

> let a = (a_i) be a cauchy sequence of rationals between 0 and 1.

let a = (a_i) be a cauchy sequence of *cauchy reals*, i.e. each a_i is a
cauchy sequence of rationals between 0 and 1.

i think the rest goes unchanged: you take a fast converging subsequence
b of a, and then approximate b by irredundant rational prefixes. the
irredundant representation is thus used instead of choice. the
completeness of such representation is the finality of its coalgebraic
structure.

-- dusko

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

Andrej Bauer wrote:

>There seems to be an open question in regard to this, advertised by
>Alex Simpson and Martin Escardo: find a topos in which Cauchy reals
>are not Cauchy complete (i.e., not every Cauchy sequence of reals has
>a limit). For extra credit, make it so that the Cauchy completion of
>Cauchy reals is strictly smaller than the Dedekind reals.
>
this will give me negative credits one way or another, but here it goes:

let a = (a_i) be a cauchy sequence of rationals between 0 and 1. (cauchy
means |a_m - a_n| < 1/m + 1/n, as in andrej's message.)

let b = (b_i) be the subsequence b_i = a_{2^i+3}. b and a are equivalent
in the sense from the message, because

     |a_m - b_n| < 1/m + 1/(2^n+3) < 2/m + 2/n

note that

     |b_i - b_{i+k}| < 1/(2^i+3) + 1/(2^(i+k)+3) < 1/(2^i+2)

now define x_i to be the simplest dyadic that falls in the interval
between b_i - 1/2^(i+2) and b_i + 1/2^(i+2). in other words, to get x_i,
begin adding 1/2 + 1/4 + 1/8... until you overshoot b_i - 1/2^(1+2). if
you also overshoot b_i + 1/2^(1+2), and the last summand was 1/2^k, skip
it, and try adding 1/2^(k+1), etc. one of them must fall in between. a
less childish way to say this is that x_i is the shortest irredundant
binary (no infinite sequences of 1) such that

     |b_i - x_i| < 1/2^(i+2)

so x =  (x_i) is a cauchy sequence equivalent to b, with

     |x_i - x_{i+k}| <= |x_i-b_i| + | b_i - b_{i+k}| + |b_{i+k} - x_{i+k}| <
                     <  1/2^(i+2) + 1/2^(i+2)        + 1/2^(i+k+2) <
                     <  1/2^i

this means that the first i digits of x_i and x_{i+k} coincide.

now let X be the binary number such that its first i digits are the same
as in x_i, for every i. (if it ends on an infinte sequence of 1s,
replace it by the corresponding irredundant representative.) this is
clearly a constant cauchy sequence equivalent to x, so it is its limit.
since x is equivalent to b

    |b_m - x_n| <= |b_m - b_n| + |b_n - x_n| < 1/2^(m+3) + 1/2^(n+3) +
1/2^(n+2) < 2/m + 2/n

and b is equivalent to a, X is also the limit of a.

is there an error in the above reasoning? i can't find it. on the other
hand, i printed out the paper by alex and martin, and the conjecture is
stated rather strongly, so i guess i must be missing something.

-- dusko

Re: Cauchy completeness of Cauchy reals

[Martin Escardo]

Dusko Pavlovic writes:
 > >NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
 > >Simpson and I characterized "the Cauchy completion of the rationals
 > >within the Dedekind reals" as a free algebra
 > >
 > and vaughan pratt and i characterized the cauchy reals as a final
 > coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280.

I forgot to mention this --- I apologize. In your paper, you work in
Set. Do you think your construction works in any topos? If so, what
would "Cauchy reals" mean precisely in this general context? Thanks.

ME

Re: Cauchy completeness of Cauchy reals

[Ross Street]

With all this talk about real numbers, perhaps readers would be
interested in my little paper (reporting an idea of Steve Schanuel):

	An efficient construction of the real numbers,
	Gazette Australian Math. Soc. 12 (1985) 57-58.

which may be hard to find. However, a recent report of an
undergraduate vacation project can be obtained at

	http://www.maths.mq.edu.au/~street/efficient.pdf

This project convinced me that this construction is a good one for
teaching undergraduates.

Others have had this idea too.  In particular, the following was
recently posted on the math arXiv:

	Norbert A'Campo, A natural construction of the real numbers,
		arXiv:math.GN/0301015 v1  3 Jan 2003.

With regards,
	Ross

Re: Cauchy completeness of Cauchy reals

[Mamuka Jibladze]

> NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
> Simpson and I characterized "the Cauchy completion of the rationals
> within the Dedekind reals" as a free algebra (to be precise, we
> started from the algebras as a primitive notion and later found this
> construction of the free one). But this has already been discussed in
> postings in the past few years.
>
> Martin Escardo

Does one get any known versions of reals by performing the Cauchy or
Dedekind construction starting with initial algebras I for non-decidable
lifts L
instead of the NNO? It would be then also natural to interpret Cauchy
sequences and completeness using appropriate I-indexed families, of course.

Even for "integers" Z one has at least three different options:
taking I^op+1+I, taking the colimit of I->LI->LLI->..., each map being
the unit, or taking the colimit of the corresponding I-indexed diagram.
It would be strange if these turn out to be isomorphic. Is any of them an
initial
algebra for some simple functor?

Similarly there are various possibilities for rationals - taking fractions,
i.e. a quotient
of ZxZ, or colimit of all multiplication maps Z->Z, or of the corresponding
Z-indexed
diagram.

Actually I have not followed the ongoing research for a while, so maybe my
questions
are outdated. I would be grateful for any references to related work.

Mamuka Jibladze

Re: Cauchy completeness of Cauchy reals

[Vaughan Pratt]

Dear toposophers,

With constructivity of real arithmetic back on the front burner for the
moment, let P be the ring of bounded power series a0 + a1.x + a2.x^2 + ...
with integer coefficients a_i, where the bound is, for each such series,
an integer c such that |a_i| < c (3/2)^i / i^(3/2).

Let 1-2x generate the ideal I of P.  Then the quotient ring P/I turns out
to be the field of reals [AMM 105(1998), p.769].

This is more constructive than it might appear, being just an obscure
(or clear depending on your upbringing) way of representing reals in a
redundant binary notation.  The ring P permits fast arithmetic essentially
by deferring carries.  Carries are "propagated" when needed by quotienting
by I, which works by collapsing every formal power series to one all of
whose coefficients other than a0 are either 0 or 1 and which has infinitely
many 0s (equivalently, no infinite run of 1's).

In this view of things, a real is understoood as an integer (a0) plus a
binary fraction in [0,1) (the rest of some "binary" formal power series,
meaning one with a_i = 0 or 1 for i > 0 and infinitely many 0s).  A general
formal power series without this restriction to 0 and 1 then constitutes
a redundant representation of a real, which can be made irredundant when
needed (e.g. when comparing with <) by quotienting by I.

An intuitively clear but less constructive view is to evaluate each series at
x = 1/2, the root of 1-2x, noting that any series bounded as above converges
absolutely there.  Series identified by I are those that evaluate to the
same real at x = 1/2.

What is nonconstructive about this is that direct evaluation of an infinite
series at a point requires infinite time, no matter how large and parallel
the infinite circuit computing it may be.

In contrast, P and P/I are more constructive in the following sense.
Addition and subtraction in P require circuit depth O(1) using an infinite
circuit whose gates perform integer addition and subtraction (just do it
coordinatewise).  Reduction mod I takes longer, but there is a variant of
the above in which it is fast enough.  Instead of the field R we settle
for just the group R, and instead of |a_i| < c (3/2)^i / i^(3/2) we settle
for simply |a_i| < c.  In this case any given series can be reduced (same
generator 1-2x) to the above normal form in circuit depth log_2(c) (nice
exercise), a finite quantity despite the series itself being of infinite
length and fluctuating arbitrarily within ±c.

Multiplication is problematic for two reasons.  First it obliges the weaker
bound, complicating reduction.  Secondly it is a convolution, complicating
arithmetic even when carry propagation is deferred.  I don't see obvious
solutions to either of these problems.  On the other hand I have no a priori
reason to suppose that these circuit-theoretic complications of passing
from R as a group to R as a ring or field would be reflected in suitably
constructive topos-theoretic developments of these notions.

Vaughan Pratt

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

Martin Escardo wrote:

>NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
>Simpson and I characterized "the Cauchy completion of the rationals
>within the Dedekind reals" as a free algebra
>
and vaughan pratt and i characterized the cauchy reals as a final
coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. in
fact, freyd came up with his characterization of the closed interval
while commenting on our first paper, where vaughan and i worked with the
semiopen interval.

but it is fair to say that the algebraic approach allows easier
algebraic operations on reals. (i only managed to multiply them in one
of our coalgebras, and in a very inefficient way.)

-- dusko

BTW have you seen the book:

    Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and
Fabrication of Life
    by Robert Rosen (Columbia University Press 1991)

it was referenced in a biology paper, i found it in the biology library,
and it's full of categories. (yes, i kno, people often do that to sound
complicated, but this seems like honest work, perhaps even inspiring,
although it does not go very deep.)

Cauchy completeness of Cauchy reals

[Martin Escardo]

Andrej Bauer writes:
 > find a topos in which Cauchy reals
 > are not Cauchy complete (i.e., not every Cauchy sequence of reals has
 > a limit). For extra credit, make it so that the Cauchy completion of
 > Cauchy reals is strictly smaller than the Dedekind reals.

One small clarification: Regarding the extra credit, there doesn't
seem to be a reasonable "absolute" way of defining the completion in
question. E.g.  the various, constructively different, notions of
metric completion already assume the existence of some given complete
reals. However, one can always embed the Cauchy reals into the
Dedekind reals, which are always Cauchy complete, and then look at the
smallest "subset" containing this which is closed under limits of
Cauchy sequences (where Cauchy sequences are defined as in Andrej's
message). We sometimes call this, somewhat verbosely, "the Cauchy
completion of the Cauchy reals within the Dedekind reals".  But notice
that this is the same as what one gets starting from the rationals
within the Dedekind reals and then closing under limits and hence
could be called the "Cauchy completion of the rationals within the
Dedekind reals".

NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
Simpson and I characterized "the Cauchy completion of the rationals
within the Dedekind reals" as a free algebra (to be precise, we
started from the algebras as a primitive notion and later found this
construction of the free one). But this has already been discussed in
postings in the past few years.

Martin Escardo