TobyBartels 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: TobyBartels 11 September 2011 09:53:39PM *  3 points [-]

The construction of omega_1 from P(N) is pretty straightforward, really, and doesn't use any of ZFC's other powerful axioms.

You either need P(P(N)) or something like an axiom of quotient sets to take the equivalence classes that are the actual elements of this version of omega_1. I presume (but haven't checked) that this is why J_2 has R but not omega_1 (although J_2 is not written in set-theoretic language, so you have to encode these).

Maybe you can somehow have the reals without P(N)?

Assuming you accept classical logic, then P(N) may be constructed as a subset of R: that famous fractal the Cantor set.

I am saying these things without carefully checking them because hopefully TobyBartels will show up and correct me if I am wrong.

Just about everything that I know about predicative mathematics is distilled here. There I describe two schools, and the constructive one (which is less predicative than the classical one!) is the only one that I know well.

Comment author: Sniffnoy 11 September 2011 10:21:20PM *  2 points [-]

You either need P(P(N)) or something like an axiom of quotient sets to take the equivalence classes that are the actual elements of this version of omega_1.

Crap, looks like I should have checked that after all! OK, I guess if Eliezer accepts R but not P(R) then there's less of a problem here than I thought. :P

I presume (but haven't checked) that this is why J_2 has R but not omega_1 (although J_2 is not written in set-theoretic language, so you have to encode these).

Edit: Nevermind, this line was asking what J_2 was, you've given a reference elsewhere.

Maybe you can somehow have the reals without P(N)?

Assuming you accept classical logic, then P(N) may be constructed as a subset of R: that famous fractal the Cantor set.

Oh, that works. Should have thought of that.

The constructive one (which is less predicative than the classical one!)

Huh, so there's two separate things going on here. Constructivism in the sense of no-excluded-middle, and I guess "predicativism" in the sense of, uh, things should be predicative? I probably should have realized those were largely independent, but didn't. How is the constructive version less predicative? Is it just the function set issue?