This seminar by Cale took place on Fri Nov 23 2007, in #mathematics channel of

The timestamps displayed in the IRC text are at an unknown offset.
Any explanation or errors regarding this seminar should be recorded in the discussion page.

Topic Edit

Construction of the Reals from Cauchy Sequences

Seminar Edit

<thermoplyae> says it's ready when you are
<Cale> :)
<Cale> Who is here?
* arcatan 
<Cale> I'd prefer a little bit of interactivity to just typing out lots of stuff on my own,
       so everyone should feel free to stop me and ask questions at any point.
<TRWBW> i think it's like that gary larson cartoon where wolf takes off the sheepskin, looks
        at the rest of the flock that has suspicious paws and snouts, and asks "hey, is there
        anyone here who isn't a wolf?"
<Cale> hehe :)
<Cale> Who here hasn't seen a construction of the real numbers before?
<thermoplyae> it'll get thrown up on freenode-math. whatever, so it won't all be in vain
<sorear> Am I suppposed to construct the reals now?
<Cale> sorear: hm? 
<Cale> I am :)
<TRWBW> could have a weirdest construction contest. or could not, and say we did.
<Cale> However, I'd like to know if there's any real point in it, or what? :)
<Cale> It would be good to have at least one person who hasn't seen the construction of the
       reals before. If there isn't, we can blame Faisceaux -- I think that's who asked me to
       use this topic. :)
<TRWBW> Cale: think it's bad scheduling. friday after thanksgiving, combination of friday
        night deadness with the college kids being on vacation
<Mulder> it could be good revision for some of us
<sorear> Let's see.  There is the Cauchy equqivalence class construction; Dedekind's
         complete cut construction; Conway's omega-iterated separated set construction;
         place value construction; any other fun ones?
<TRWBW> sorear: i like decimal expansion construction
<Kasadkad> There's one with almost-homomorphisms which I've never looked at in detail,
           dunno if that's the same as Conway's
<sorear> that's what I meant by place value...
<TRWBW> sorear: oh and for cauchy i like the specific variant that shows that cauchy
        sequences form a ring and ones that go to 0 form a prime ideal
<sorear> TRWBW: ooh, pretty
<Cale> Yeah, the (almost) purely algebraic variant of Cauchy sequences is nice :)
<arcatan> I've seen only decimal expansion construction so seeing some other way might be
<Cale> I was just going to do Dedekind cuts :)
<Cale> arcatan: okay, great :) 
<ihope_> Is there a term for calling the real numbers a subset of the surreal numbers? :-)
<sorear> The surreals are a field extension of the reals
<sorear> (Asssuming they are a field - don't recall if this is true)
<Cale> Sort of :)
<Cale> The surreals are a proper class.
<jahlin> i have never seen a construction of real
<Cale> okay
<ihope_> sorear: the surreal numbers satisfy all the field axioms, but they're not a set,
         making them not a field.
<Cale> So, I take it that people who haven't seen a construction of the reals all know
       what rational numbers are?
<TRWBW> Cale: before you jump in, maybe check if he has the prerequisits, basically Q
        is an ordered archimedian field
<jahlin> a rational number can be written in the form p/q where p and q both are integers
         q!=0 right?
<Mulder> a lecture on why R is the unique ordered field up to isomorphism with the archimedian
         proprety might be interesting too
<Cale> jahlin: right. 
<sorear> jahlin: that's a valid definition, but a bit circular - we're about to construct the reals
<TRWBW> Mulder: cauhcy-complete. or you can lump archimedean and complete into dedekind complete
<Cale> Perhaps just for the sake of being thorough, I'll start off with the natural numbers, and do
       the integers and rationals from there :)
<Cale> jahlin, arcatan: do you know what an equivalence relation is?
<TRWBW> Cale: not a bad idea, gives a warmup on the idea of "construction"
<arcatan> yeah
<jahlin> i dont.
<Cale> Okay
<Cale> If S is a set, then a relation ~ on S is a set of pairs (x,y), with x in S and y in S.
<Cale> When (x,y) is in that set, we write x ~ y.
<Cale> An equivalence relation is a relation which behaves in a few ways that we'd expect
       equality to behave in:
<Cale> The relation ~ is an equivalence relation if and only if the following three things
       are true:
<Cale> 1) For any x in S, it's the case that x ~ x.
<Cale> 2) For any x and y in S, then whenever x ~ y, we have that y ~ x as well.
<Cale> 3) For any x, y, z in S, if x ~ y, and y ~ z, then x ~ z.
<Cale> 1 is called reflexivity, 2 is symmetry, and 3 is transitivity
<Cale> So for example, if we have a set of people, say, we can define an equivalence relation
       on them by saying that x ~ y if and only if x and y have the same colour eyes.
<ihope_> You know, if you have symmetry, it seems you might as well make it an unordered pair.
         The construction of that is slightly simpler than that of an ordered pair: {x,y} rather
         than something like {{x},{x,y}}.
<Cale> This is an equivalence relation because 1) a person has the same colour eyes as themselves,
       2) if x has the same colour eyes as y, then y has the same colour eyes as x
<Cale> and 3) if x has the same colour eyes as y and y has the same colour eyes as z, then x has
       the same colour eyes as z
<jahlin> is it also known as inclusive relation?
<Cale> Hmm, I've never heard it called that
<Cale> An example of a relation on people which is not an equivalence relation is
       "has shaken hands with"
<TRWBW> jahlin: you've been working with equivalence relations all your life, you just
        may not have known the name for it
<Cale> Because it's not necessarily the case that if x has shaken hands with y and y has
       shaken hands with z, that x has shaken hands with z as well.
<Cale> So does that idea roughly make sense?
<jahlin> yes.
<Cale> We'll see a few examples of it
<ihope_> Not to mention that not everybody has shaken hands with themself.
<Cale> ihope_: right :)
<Cale> So we start off with the natural numbers: 0 is a natural number, and if n is a natural
       number, then so is n+1, and every natural number can be obtained from those two rules.
       I don't really want to get too in depth into that :)
<Cale> N = {0,1,2,...}
<TRWBW> Cale: hehe, i predicted you'd you be starting with peano axioms
<arcatan> i'm bit confused with the status of 0. some mention it as a natural number and some don't
<Cale> Yeah, that's true. Here we'll accept 0 as a natural number. Some people (mostly number
       theorists) don't like it.
<sorear> arcatan: I'm pretty sure we're about to define semiring operations, so take 0
<Cale> Nah, I'm going to assume that we know how to add and multiply, unless there's a lot of
       interest in it.
<Cale> I suppose I could write the rules down.
<TRWBW> arcatan: it's arbitrary in the same way some people do sin(x) in degrees, some in
        radians, or some people consider 0^0 undefined and some defined as 1. as long as
        in a particular context you are clear which version you are using, it's just a matter
        of taste.
<Cale> Right, it's just a matter of taste, that's a good way to put it :)
<arcatan> yeah
<Cale> So one of the first things you probably bump into with natural numbers is that while
       you can always add a pair of natural numbers and get another natural number, it's not
       always possible to take a pair of natural numbers and subtract one from the other.
<Cale> That is, given natural numbers a and b there is not always a solution to the equation b + x = a
<Cale> So to build the integers, the intuition behind the construction is to make something which
       will satisfy that equation in the end.
<Cale> (once we've defined addition)
<Cale> So I'm going to start off with the set of pairs (a,b) of natural numbers.
<Cale> If we think of the pair (a,b) as standing for the number a - b, then when should two such pairs
       mean the same number?
<Cale> Well, (a,b) should mean the same as (c,d) when a + d = b + c, right?
<jahlin> yes
<Cale> That is, a - b = c - d, when a + d = b + c
<Cale> So we define an equivalence relation on pairs of natural numbers:
<Cale> (a,b) ~ (c,d) when a + d = b + c
<Cale> Now, one thing that we need to know about equivalence relations is that whenever you have an
       equivalence relation on a set S, it partitions that set into   disjoint equivalence classes,
       that is, sets of elements which are all equivalent to one another, and not equivalent to anything
       outside the class.
<Cale> The equivalence class containing x, which I'll denote by [x] is the set of all things equivalent
       to x, that is, the set {y in S: x ~ y}
<Cale> So we define the integers, Z, to be the set of equivalence classes of pairs of natural numbers,
       under this equivalence relation ~
<Cale> Of course, these aren't really numbers until we know how to add and multiply them.
<Cale> So my definition for addition:
<Cale> [(a,b)] + [(c,d)] = [(a+c, b+d)]
<Cale> and for multiplication:
<Cale> [(a,b)] [(c,d)] = [(ac + bd, bc + ad)]
<Cale> There's some work left to do here: we have to see that these are actually well defined:
       that is, if (a,b) ~ (a',b'), and (c,d) ~ (c',d'), then we should get the same results for
       addition [(a,b)] + [(c,d)] = [(a',b')] + [(c',d')], and similarly for multiplication
<Cale> We should also check that this satisfies all the usual properties of numbers.
<Cale> But I don't know, how interested are people in seeing all that? :)
<Cale> Is anyone still following this?
<arcatan> i'm not that interested... but what are "the usual properties of numbers"?
<Cale> Ah, the axioms for a ring.
<Cale> a + (b + c) = (a + b) + c
<Cale> There is some 0, such that (a + 0) = (0 + a) = a, for any a
<Cale> For any a, there is some b such that a + b = b + a = 0
<Cale> For any a and any b, a + b = b + a
<TRWBW> (existance of such a 0 implies its uniqueness, since if you had another contender for the
        title of 0, call it 0', then you necessarily get 0'=0'+0=0)
<Cale> For any a,b,c: (a*b)*c = a*(b*c)
<Cale> There is some 1 such that a*1 = 1*a = a for any a
<Cale> For any a,b,c, we have a*(b+c) = a*b + a*c, and (a+b)*c = a*c + b*c
<Cale> Further, in the case of the integers, we also have that a*b = b*a for any a and b
<arcatan> so it's like a field but it doesn't have, what's that called, inverse?
<TRWBW> given a, the b such that a+b is typically called "-a". again it's unique, because if
       you had another contender, a+b=0 and a+b'=0, you would get b=b+0=b+(a+b')=(b+a)+b'=0+b'=b'
<Cale> It doesn't have inverses under multiplication, (and rings aren't required to be commutative,
       but this one is)
<arcatan> yeah
<Cale> So if we wanted to, we could check all of those things. It's not actually all that hard,
       but it takes time.
<TRWBW> you also get the rest of the properties you expect from these axioms. you don't need to
        special axiom for a*0=0, because a*0=a*0+0 = a*0+(a*0+-a*0) = (a*0+a*  0)+-a*0
        = a*(0+0)+-a*0 = a*0+-a*0 = 0, for example
<Cale> From those things, follow lots of commonsense properties like that if a + c = b + c,
       then a = b, and things like that.
<TRWBW> or you don't need a special axiom for -1*a=-a, since that comes form -1*a = 0+-1*a
        = (-a+a)+-1*a = -a+(a+-1*a) = -a+(1*a+-1*a) = -a+(1+-1)*a = -a+0*a = -a+0 = -a
<TRWBW> things like 0*a=0, -1*a=0, -(a-b)=b-a, a+a=2*a, etc., all follow from applying the
        rules Cale gave in combinations
<Cale> Let's just check that [(1,0)] has an additive inverse. According to my addition:
       [(1,0)] + [(0,1)] = [(1,1)], and we know that (0,0) ~ (1,1) since 0 + 1 =  1 + 0
<TRWBW> hehe, -1*a = -a, typo
<Cale> and so [(1,0)] + [(0,1)] = [(0,0)], and [(0,0)] must be the zero, because adding
       it to anything will (according to the definition I gave for addition), leave anything
       the same.
<Cale> [(1,0)] also acts like 1
<TRWBW> oh, one more property you do need an axiom for, a*b=0 implies a=0 or b=0
<Cale> [(1,0)] * [(a,b)] = [(1*a + 0*b, 0*a + 1*b)] = [(a,b)]
<Cale> In the end, the integer [(n,0)] ends up acting just like the natural number n
<Cale> and [(0,n)] is its additive inverse, -n
<Cale> TRWBW: Do we need an axiom for that? Did I leave out a standard ring axiom?
<Cale> Oh, heh, yeah, we'd need to prove that about Z specifically, right.
<Cale> (I should read things :)
<Cale> Now, for the rational numbers, we pull the same trick again, essentially.
<Cale> This time, our problem is that it's not always possible to divide.
<Cale> (by nonzero elements)
<Cale> So we start with pairs (n,m) of integers
<Cale> where m is not 0
<TRWBW> Cale: you can get it from the order axioms if you prefer, i'm just kibitzing
<Cale> and we define an equivalence relation on them such that the pairs of integers
       (a,b) ~ (c,d) when ad = bc
<Cale> and here the pair (a,b) is used to represent the number a/b
<Cale> and we can define addition and multiplication on equivalence classes again:
<Cale> [(a,b)] + [(c,d)] = [(ad + bc, bd)]
<Cale> [(a,b)] * [(c,d)] = [(ac, bd)]
<Cale> and this ends up being a field -- that is, in addition to all those properties
       we listed for Z, there's one more:
<Cale> for any a in Q (the rational numbers) which is not 0, there is some b in Q so
       that a*b = 1
<Cale> Incidentally, [(n,1)] acts just like the integer n, under those addition and
       multiplication rules.
<Cale> So equivalence relations are a nice tool for making wishes about things.
<Cale> If you ever think "wouldn't it be great if this equation had a solution", then
       there might be a way to build something where it actually does.
<Cale> anyway, that's just a quick overview of everything before the real numbers, it
       was a little rushed, so I hope it's not too incomprehensible :)
<Cale> arcatan / jahlin: still reading?
<arcatan> I'm reading
<Cale> I can pause a bit if you like :)
<arcatan> it was comprehensible, you can go on
<Cale> okay
<Cale> In addition to the properties I talked about with respect to addition and
       multiplication, the natural numbers, integers, and rational numbers are all
       ordered, that is, we have some notion of when one number is less than another.
<TRWBW> Cale: maybe give i=sqrt(-1) as one more infomral example?
<Cale> mm, yeah, I suppose we could do that :)
<Cale> If we already have the reals, we can build the complex numbers by simply taking
       pairs of real numbers (a,b), and defining addition and multiplication directly
       (no need for equivalence classes here)
<Cale> (a,b) + (c,d) = (a+c, b+d)
<Cale> (a,b) * (c,d) = (ac - bd, ad + bc)
<Cale> The numbers (a,0) act just like the real numbers do
<Cale> But we have things like (0,1) * (0,1) = (0*0 - 1*1, 0*1 + 1*0) = (-1,0)
<Cale> That is, (-1,0) has a square root
<Cale> and (-1,0) is the complex number which is -1
<Cale> The complex numbers form a field again, and they're really quite interesting,
       because (apart from the construction of the reals), each of the constructions
       of new kinds of "numbers" were motivated by wanting solutions to polynomial equations
<Cale> For the integers, it was that we wanted solutions to a + x = b
<Cale> For the rationals, we wanted solutions to a * x = b (when a isn't 0)
<Cale> For the complex numbers, we wanted a solution to x^2 = -1
<Cale> But in fact, we get way more than we barained for: it turns out that there is a
       solution to every polynomial equation in the complex numbers.
<Cale> bargained*
<Cale> But what about the real numbers?
<Cale> The motivation for the reals is actually somewhat different.
<Cale> Well, not entirely, I suppose.
<Cale> For example, it can be shown that there is no square root of 2 in the rational numbers.
<Cale> But there are other ways to fix that problem.
<Cale> Hmm, I think I will do Cauchy's construction after all ;)
<Cale> The real problem with the rational numbers is that there are sequences of rational
       numbers which "get close to one another"
<Cale> but which don't get close to any particular rational number.
<Cale> I can make that more formal...
<TRWBW> Cale: oh, can i do Q[sqrt(2)]? (a,b)+(c,d)=(a+c,b+d), (a,b)*(c,d)=(ac+2*bd,ad+bc).
        now you've got sqrt(2), since (0,1)^2=(2,0)
<Cale> yep :)
<Cale> A sequence {x_1,x_2,x_3,...} of rational numbers is called Cauchy if for any (rational)
       e > 0, there is some M such that if n,m > M, we have |x_n - x_m| <  e.
<Cale> That is, no matter how small a distance we take e to be
<Cale> there is some point, far enough out in the sequence
<Cale> so that the distance between any two terms x_n and x_m
<Cale> (that's |x_n - x_m|)
<Cale> is less than e
<Cale> You'd expect that since the terms of such a sequence are getting close to one another,
       that they would approach some number.
<Cale> One more definition:
<Cale> The sequence {x_1,x_2,x_3,...} of rational numbers is said to converge to the limit L,
       if for any e > 0, there is some M such that whenever n > M, we have  |x_n - L| < e
<Cale> That is, for any distance e, no matter how small,
<Cale> there is some point M in the sequence, beyond which
<Cale> every term x_n of the sequence lies within distance e of L.
<Cale> The scary thing is that there are sequences of rational numbers which are Cauchy, but
       don't actually converge to anything.
<Cale> This is what gives us the impression that there are "holes" in the rational numbers.
<ihope_> You mean they don't converge to anything rational?
<Cale> Right. The rationals are all we have at this point.
<Cale> It's easiest to construct examples once we know things about the real numbers.
* ihope_ nods
<Cale> For example, take x_1 = 1, and x_(n+1) = (2 + (x_n)^2)/(2 x_n)
<Cale> This is a sequence of rational numbers, one can actually show that it's Cauchy as well,
       but it actually converges to the real number which we know as       sqrt(2).
<Cale> arcatan: any questions about the definitions there?
<arcatan> no
<Cale> Okay.
<Cale> So what we can do to fix the problem is to start with the set of all Cauchy sequences of
       rational numbers.
<Cale> Naturally, many of these will actually converge to rational numbers, and when they do,
       there won't be one, but many which converge to the same rational.
<Cale> For example, the sequences (0,0,0,0,...), and (1,1/2,1/3,1/4,...,1/n,...) are both
       converging to 0
<Cale> We'll define two Cauchy sequences {x_n} and {y_n} to be equivalent if for any e > 0,
       there is some M so that whenever n > M, we have that |x_n - y_n| < e
<Cale> If {x_n} is converging to L, and {y_n} is equivalent to {x_n}, then {y_n} is converging
       to L as well.
<Cale> Proof:
<TRWBW> Cale: i've lost track. you might want to mentin archimedan before you get into the proof
<Cale> hmm, yeah, we didn't really talk about that. I've just been talking about completeness in
       terms of Cauchy sequences converging.
<Cale> I think that should do, no?
<Cale> What we're going to do is to pull the same trick that we did with the rationals and the
       integers and so on, and just construct the reals as equivalence classes.
<Cale> Note: I'd actually started out thinking of another construction at the beginning, but this
       seems more natural, given the way that we've been headed.
<Crito> 6/nam
<Crito> (oops)
<TRWBW> i missed it, i didn't know if you talked about order axioms at all, or you are just assuming
        them, along with there is an integer greater than any rational
<TRWBW> nvm, just random kibitz
<Cale> ah, yeah, I suppose I haven't said too much about what properties < has on the rationals
<arcatan> hmm, there's an integer greater than any rational?
<Cale> arcatan: there isn't.
<Cale> If n/m is a positive rational number, then n+1 is larger than it.
<TRWBW> arcatan: for all rationals there exists an integer greater than it <=> does not exist an
        integer greater than all rationals
<TRWBW> arcatan: well you gotta throw some order properties in the middle of that <=> but that's
        the two ways to say it
<arcatan> makes sense
<TRWBW> does not exist a rational greater than all integers is another common way
<Cale> The definition is that if you have rational numbers n/m and n'/m', with m and m' positive,
       then n/m < n'/m' whenever n m' < n' m. We probably should have   showed a bunch of things
       about that, as part of our construction of the rationals :)
<Cale> (and then that uses the ordering on the integers, which in turn uses the ordering on the naturals)
<TRWBW> going back to the construction of integers from naturals, you have a < on the naturals,
       it comes down to a-b<c-d <=> a+d<c+b
<Cale> Right, and then on the naturals, you say something like a < b if there is some c
       not equal to 0 such that a + c = b
<arcatan> so what happened to that set of all cauchy sequences of rationals?
<Cale> Right.
<Cale> So I was going to give a little proof of a property about that equivalence, because I
       think it should help to give some feel for how the definition works
<Cale> Well, I don't know how much epsilon/delta type stuff you've done before :)
<arcatan> i think i don't need a proof
<Cale> okay
<Cale> So we can take the set of equivalence classes of Cauchy sequences of rationals,
       and call that the real numbers.
<Cale> and of course, we have to define addition and multiplication
<Cale> We'll do that componentwise
<Cale> So [{x_n}] + [{y_n}] = [{x_n + y_n}]
<Cale> So [{x_n}] [{y_n}] = [{x_n y_n}]
<Cale> We should really check that that's well-defined.
<Cale> So if {x_n} ~ {x'_n}, and {y_n} ~ {y'_n}, we want to show that {x_n + y_n} ~ {x'_n + y'_n}
<Cale> That is, that for any e > 0, we want to show that there is some M such that if n > M,
       we have |(x_n + y_n) - (x'_n + y'_n)| < e
<Cale> We know that there is some M_1 so that if n > M_1 we have |x_n - x'_n| < e/2
<Cale> We know that there is some M_2 so that if n > M_2 we have |y_n - y'_n| < e/2
<Cale> So take M = max(M_1, M_2)
<arcatan> how does that go with multiplication?
<Cale> and then |(x_n + y_n) - (x'_n + y'_n)| = |(x_n - x'_n) - (y_n - y'_n)|
       <= |x_n - x'_n| + |y_n - y'_n| < e/2 + e/2 = e
<Cale> okay
<Cale> Yeah, with multiplication... we'll have
<Cale> hmm :)
<Cale> we need a trick where we introduce some terms to be able to factor that thing :)
<Cale> |x_n y_n - x'_n y'_n|
<Cale> = |x_n y_n + x_n y'_n - x_n y'_n - x'_n y'_n|
<Cale> let's try that :)
<Cale> = |x_n (y_n - y'_n) + (x_n - x'_n) y'_n|
<Cale> <= |x_n (y_n - y'_n)| + |(x_n - x'_n) y'_n|
<Cale> = |y_n - y'_n| |x_n| + |x_n - x'_n| |y'_n|
<Cale> Now, one thing about Cauchy sequences is that they're bounded.
<Cale> That is, if {z_n} is any Cauchy sequence, there is some B such that -B < |z_n| < B,
       for all n
<Cale> er, sorry
<Cale> That is, if {z_n} is any Cauchy sequence, there is some B such that |z_n| < B,
       for all n
<Cale> heh, pick one notation or the other :)
<Cale> So if we pick n large enough that |y_n - y'_n| < e/(2B), where |x_n| < B
<Cale> and large enough that |x_n - x'_n| < e/(2C) where |y_n| < C
<Cale> then
<Cale>  |y_n - y'_n| |x_n| + |x_n - x'_n| |y'_n|
<Cale> < e/(2B) B + e/(2C) C
<Cale> = e/2 + e/2
<Cale> = e
<Cale> and that's just what we need :)
<Cale> (phew)
<arcatan> yeah
<Cale> If you want, I can prove that Cauchy sequences are bounded :)
<Cale> But it's not hard, and it's a good exercise :)
<Cale> So, these operations are well defined.
<Cale> We could go on to check all of the field axioms. In fact, they'll follow
       from the field axioms on the rationals fairly directly.
<Cale> For example, [{x_n}] + ([{y_n}] + [{z_n}]) = [{x_n}] + [{y_n + z_n}]
       = [{x_n + (y_n + z_n)}] = [{(x_n + y_n) + z_n}] = [{x_n + y_n}] + [{z_n}]
       = ([{x_n}] + [{y_n}]) + [{z_n}]
<Cale> That's associativity.
<Cale> You can see that it's just unravelling the definition and then applying
       associativity on rationals.
<Cale> All the field axioms will work out really nicely like that.
<Cale> How about ordering?
<Cale> Well, it seems natural to define [{x_n}] <= [{y_n}] if there is some M so that
       whenever n > M, we have x_n <= y_n.
<Cale> er, no :)
<Cale> Well, it seems natural to define [{x_n}] < [{y_n}] if there is some M so that
       whenever n > M, we have x_n < y_n.
<Cale> It actually matters here :)
<Cale> There are some things we should show that this < satisfies
<TRWBW> coming back the the beginning, the concept of a "relation" ...
<Cale> right :)
<Cale> < isn't an equivalence relation, it's an ordering relation
<Cale> For one, we'd like to know that if p,q,r are real numbers,
       and if p < q, and q < r, then p < r
<Cale> (that is, < should be transitive)
<Cale> and for any real numbers p,q, we want that either p < q, q < p, or p = q
<Cale> Further, if a < b, then a + c < b + c
<Cale> and if 0 < a, and 0 < b, then 0 < a b
<Cale> That is, it should play well with the arithmetic operations too.
<Cale> I'll let arcatan decide how much of this we prove :)
<arcatan> I think I'll actually go to bed now
<Cale> okay :)
<arcatan> but thanks for the lecture, it was quite interesting
<TRWBW> Cale: you might want to be clear that's an exclusive or. exactly one of the 3,
        p < q or q<p or p=q holds, but never more than one
<Cale> right
<Cale> yes
<Cale> and in the end, we'd have one more thing as well: that every Cauchy sequence of
       real numbers converges
<Cale> oh, and another: that there is an natural number larger than any given real number
<TRWBW> Cale: as always, give you kudos for the stamina, but i gotta say when you do these
        things i realize why it takes a week or whatever for them to cover this in school
<Cale> (but that's easy, given that a real number is a bounded sequence of rationals, and
       there's a natural number larger than that)
<Cale> TRWBW: yes :)
<Cale> TRWBW: If you really want to do this properly, there are a lot of details.
<Cale> We were simply asked to read about it on our own ;)
<Cale> Well, that's not entirely true.
<Cale> But many of the details were assigned reading rather than in the lectures.