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

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

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

]]>Just did a little rewriting to make the argument clearer.

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

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.

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

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

]]>Thanks, I’ve added that.

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

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

]]>