Re: The real numbers

Subject: Re: The real numbers
From: lescanne@loria.fr (Pierre Lescanne)
Date: 17 Nov 1995 11:20:33 +0100
Keywords: reals, LSL, specification
Newsgroups: comp.specification.larch
Organization: CRIN & INRIA-Lorraine - Nancy - FRANCE
References: <leavens.816567406@bambam.cs.iastate.edu>


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):

The real numbers

From: leavens@cs.iastate.edu (Gary Leavens)