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 k-theory lie-theory limit limits linear linear-algebra locale localization logic mathematics 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 subobject 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.
    • CommentAuthorTobyBartels
    • CommentTimeSep 9th 2011

    On well-order and elsewhere, I’ve implied that a well-order (a well-founded, extensional, transitive relation) must be connected (and thus a linear order). But this is not correct; or at least I can’t prove it, and I’ve read a few places claiming that well-orders need not be linear. So I fixed well-order, although the claim may still be on the Lab somewhere else.

    Of course, all of this is in the context of constructive mathematics; with excluded middle, the claim is actually true. I also rewrote the discussion of classical alternatives at well-order to show more popular equivalents.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 9th 2011

    In “Intuitionistic sets and ordinals” Paul Taylor gives the example of the set of truth values as a well-order whose relation P<QP \lt Q holds just when ¬PQ\neg P \wedge Q. This is clearly not a linear order intuitionistically.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeSep 9th 2011

    Thanks, I’ve added that.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 10th 2011
    • (edited Sep 10th 2011)

    I wasn’t aware of the result that well-founded, extensional, transitive relations are linear (in classical logic). I added a subsection which purports to prove this, but the proof should be checked, or better yet, improved if possible. (And I imagine it is possible – it’s something I wrote off the top of my head.)

    BTW: I though \preceq\backslash preceq was a valid itex command, but it’s not rendering correctly on my screen.

    • CommentRowNumber5.
    • CommentAuthorZhen Lin
    • CommentTimeSep 10th 2011

    Here’s a cheap way of doing it, if I haven’t made any mistakes: by Mostowski collapse, any set equipped with a well-founded extensional relation is isomorphic to a set (in the material set theory sense) equipped with the \in relation; if we further demand that \in is transitive on this set, then this set must in fact be a set of von Neumann ordinals (because it is a set of hereditarily transitive sets). And ordinals are well-ordered, of course.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 10th 2011

    Thanks, Zhen. Please feel free to add that if you’d like. My only comment is that it’s addressed to someone with a certain background, whereas I wanted to record an argument based directly on the given definition.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011

    And [von Neumann] ordinals are well-ordered, of course

    I presume you mean that von Neumann ordinals are linearly ordered. But is that really easier to prove than that arbitrary well-orders are so? I just looked through all my books on material set theory, and the only one I could find that doesn’t define a von Neumann ordinal to be linearly ordered by \in proves that they are linearly ordered by an argument that works just as well for any well-orders.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 10th 2011

    Just did a little rewriting to make the argument clearer.

    • CommentRowNumber9.
    • CommentAuthorZhen Lin
    • CommentTimeSep 10th 2011

    Well, at least for me, reducing to the case of ordinals made it conceptually clearer why the claim is true. I haven’t yet found a direct proof I’m happy with though; it feels like there ought to be a proof using the principle of well-founded induction. (Perhaps this is a symptom of the fact that the claim is not constructively true…)

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011

    Yes, if there were a proof using only the principle of well-founded induction, then it would probably work constructively…

    I like Todd’s proof very much! It also has the advantage of not requiring any form of the axiom of replacement, which is not true of any proof that constructs something by well-founded recursion (including Mostowski’s collapsing lemma).

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeSep 11th 2011

    Nice proof, Todd! I made it a little more obvious (to an alternate version of me reading it) where excluded middle is used (twice).