Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 definitions 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 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 nforum 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

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexOn [[well-order]] and elsewhere, I've implied that a well-order (a well-founded, extensional, transitive relation) must be [[connected relation|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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIn "Intuitionistic sets and ordinals" Paul Taylor gives the example of the set of truth values as a well-order whose relation $P \lt Q$ holds just when $\neg P \wedge Q$. This is clearly not a linear order intuitionistically.

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

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThanks, I've added that.

   Thanks, I’ve added that.

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 10th 2011
   • (edited Sep 10th 2011)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI 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 $\backslash preceq$ was a valid itex command, but it's not rendering correctly on my screen.

   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 $\backslash preceq$ was a valid itex command, but it’s not rendering correctly on my screen.

5. • CommentRowNumber5.
   • CommentAuthorZhen Lin
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexHere'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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexJust did a little rewriting to make the argument clearer.

   Just did a little rewriting to make the argument clearer.

9. • CommentRowNumber9.
   • CommentAuthorZhen Lin
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexWell, 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...)

   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…)

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, 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).

    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).

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeSep 11th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexNice proof, Todd! I made it a little more obvious (to an alternate version of me reading it) where excluded middle is used (twice).

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