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?