Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 3 of 3
In this fom post, Harvey Friedman characterises the unit interval and the real numbers as linearly ordered sets (with top and bottom in the case of [0,1], and no endpoints in the case of R) satisfying the LUB property and having a continuous ’betweeness’ function, , . The proof uses contradiction, but even apart from that I suspect it is highly non-constructive (although I’m happy to be proved any degree of wrong).
The hypotheses are available in a topos (or with even less assumptions), with problems possibly arising with the LUB property, but I don’t know the finer points of what could and couldn’t be done with them.
Any thoughts?
Edit: And further, in this post, Friedman states the result:
An LUB field is an ordered field in which every bounded definable subset has a least upper bound.
THEOREM 1.1. The LUB fields are exactly the real closed fields.
We can strengthen Theorem 1.1 as follows.
THEOREM 1.2. Suppose F is an ordered field with the least upper bound property for all atomic formulas. Then F is a real closed field.
perhaps none of this is surprising, given the characterisation of the reals as a complete ordered field, but is it an improvement to weaken the existence of a LUB to definable subsets/atomic formulae?
Well, the difference is that it gives you more models; the field of algebraic real numbers, for example, is real-closed, as is the field of algebraic expressions in one variable with real constants. I don’t know by what standard to judge that this is an improvement.
Well, not an improvement, then. Poor choice of word, really. But I wonder what bifurcation would happen treating this internally?
1 to 3 of 3