# [FOM] characterization of Real numbers? (by Saeed Salehi)

Jesse Alama alama at stanford.edu
Fri Feb 11 23:51:37 EST 2005

```Hi Saeed,

Your ordered set X has the least upper bound property (this is
inherited from the least upper bound property of R) and a countable
dense subset (namely, Q x ([0,1] & Q)).  If the standard
characterization of R (an ordered set that has the least upper bound
property and a countable dense subset) is accurate , then it would seem
that your X is order-isomorphic to the real line.  Perhaps I'm missing
something; I would be grateful if you would discuss your counterexample
in more detail.

Warm regards,

Jesse

On Feb 10, 2005, at 12:14, Martin Davis wrote:

> I'm posting this message for Saeed Salehi <saeed at cs.utu.fi> because
> his attempts to post it contained unacceptable formatting codes.
>
> Martin
> -----------------------------------------------------------------------
> ----------------------------------------------------
> Hi everybody.
>
> I tried to prove the below theorem posted by Prof. Friedman for
> answering the second question of Prof. Shipman to myself, but came up
> with a counter example. I might be wrong in some point, can anybody
> please tell me where I am making a mistake?
> Let X=R x [0,1] be the direct product of the reals with the closed
> interval [0,1] equipped with the lexicographical order. It has the
> properties mentioned in the theorem with the F function defined by F(
> (a,i) , (b,j) ) = ( (a+b)/2 , (i+j)/2 ). But X is not order isomorphic
> to R.
> ****************
> That's a really nice theorem, which is just what I was looking for;
> just 2 questions:
>
> 1) what's the simplest way to formally define "order continuous" for a
> function from X^2 to X where X is an ordered space?
> 2) How do you prove this?
>
> -- JS
>
> *****************
> THEOREM. Let X be a linear ordering without endpoints. Then X is order
> isomorphic to the real line if and only if
>
> i) X has the least upper bound property;
> ii) there is an order continuous F:X^2 into X such that for all x,y, x
> < y
> implies x < F(x,y) < y.
>
> Harvey Friedman
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

```