Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 6th 2011
    • (edited Jun 6th 2011)

    In this fom post, Harvey Friedman characterises the unit interval and the real numbers as linearly ordered sets XX (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, f:X 2Xf:X^2 \to X, x<f(x,y)<yx\lt f(x,y)\lt y. 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?

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJun 7th 2011

    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.

    • CommentRowNumber3.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 7th 2011

    Well, not an improvement, then. Poor choice of word, really. But I wonder what bifurcation would happen treating this internally?