[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