TobyBartels comments on Harry Potter and the Methods of Rationality discussion thread, part 8 - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (653)
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).
Assuming you accept classical logic, then P(N) may be constructed as a subset of R: that famous fractal the Cantor set.
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.
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
Edit: Nevermind, this line was asking what J_2 was, you've given a reference elsewhere.
Oh, that works. Should have thought of that.
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?