[Prev][Next][Index]
# Re: The real numbers

In article <leavens.816567406@bambam.cs.iastate.edu>, leavens@cs.iastate.edu (Gary Leavens) writes:
|> implies
|> Field(R for T), TotalOrder(R for T)
|> \forall q,r,x,y,z: R
|> (x < y) => (\E z (x < z /\ z < y));
I think that that is such an interesting enough trait that I would
have created it as DenseOrder namely
DenseOrder : trait
includes PartialOrder
asserts \forall x,y,z: R
(x < y) => (\E z (x < z /\ z < y))
implies \forall x,y,z,t,u,: R
(x < y) => \E z \E t(x < z /\ z < t /\ t < y)
(x < y) => \E z \E t \E u(x < z /\ z < t /\ t < u /\ u < y)
Using Seq one should be able to state that any arbitrary long sequence
can be inserted between two numbers in a dense order.
Note also that a RealCloseField is "unbounded" in the sense that you have
implies
\forall x: R \E y (x < y)
Again this could be made a specific trait UnboundedOrder.
In your clause you introduce q and r after \forall, I think they are
superfluous.
Here are implications that can be stated in the traits RealClosedField:
implies \forall x,y : R
x > 0 => x \ne 0;
x > y => x \ne y;
x < 0 => -x > 0;
x * x > 0
I hope this is helpful.
--
Pierre LESCANNE | Tel: (work) (33) 83 59 30 07
CRIN (CNRS) & INRIA-Lorraine & GDR Progra | (home) (33) 83 22 76 92
Centre Charles Hermite | Fax: (33) 83 27 83 19
F54506 VANDOEUVRE-les-NANCY Cedex FRANCE | E-mail: lescanne@loria.fr
more information on www at http://www.loria.fr/~lescanne/

**Reference(s):**

**
**