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

[Martin Davis]

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