CronoDAS comments on Harry Potter and the Methods of Rationality discussion thread, part 8 - Less Wrong

8 Post author: Unnamed 25 August 2011 02:17AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (653)

You are viewing a single comment's thread. Show more comments above.

Comment author: CronoDAS 05 September 2011 08:37:20AM 2 points [-]

Wikipedia seems to be saying that you can prove the existence of the first uncountable ordinal in pure ZF without the axiom of choice. Is that correct?

Comment author: TobyBartels 05 September 2011 08:59:47AM 3 points [-]

Yes, and in fact it can be proved in weaker axiom systems than that.

Comment author: Psy-Kosh 05 September 2011 02:15:53PM 1 point [-]

Okay, are there any decent foundational theories that won't prove it?

Comment author: shinoteki 05 September 2011 03:23:19PM 3 points [-]

It is basically the main point of the definition of ordinals that for any property of ordinals , there is a first ordinal with that property. There are, however, foundational theories without uncountable ordinals , for instance Nik Weaver's Mathematical Conceptualism.

Comment author: TobyBartels 08 September 2011 08:38:03PM *  1 point [-]

Well, that depends on what you take to be decent. In the sibling, shinoteki has pointed (via Nik Weaver) to J_2. As Weaver argues, this is plenty strong enough to do ordinary mathematics: the mathematics that most mathematicians work on, and the mathematics that (almost always, perhaps absolutely always) is used in real-world applications. On the other hand, I find it difficult to work with, and prefer explicit reasoning about sets (but I'm a mathematician, so maybe I'm just used to that). That said, I think that properly limiting the impredicativity of set-based constructions should allow one to create a set-like theory that corresponds to something like J_2. (I'm being vague here because I don't know better; it's possible, I'd even say likely, that other mathematicians know better responses.)