I think we may have something of a clash of backgrounds here. The reason I’m inclined to take the real continuum seriously is that there are numerous physical quantities that seem to be made of real or complex numbers. The reason I take mathematical induction seriously is that it looks like you might always be able to add one minute to the total number of minutes passed. The reason I take second-order logic seriously is that it lets me pin down a single mathematical referent that I’m comparing to the realities of space and time.
The reason I’m not inclined to take the least uncountable ordinal seriously is because, occupying as it does a position above the Church-Kleene ordinal and all possible hypercomputational generalizations thereof, it feels like talking about the collection of all collections—the supremum of an indefinitely extensible quality that shouldn’t have a supremum any more than I could talk about a mathematical object that is the supremum of all the models a first-order set theory can have. If set theory makes the apparent continuum from physics collide with this first uncountable ordinal, my inclination is to distrust set theory.
The reason I take second-order logic seriously is that it lets me pin down a single mathematical referent that I’m comparing to the realities of space and time.
How can you say this after having read this thread?
If you believe in second-order model theory, then you believe in set theory. (However, by limiting it to second order over the natural numbers, without going on to third order, you are not obligated to believe in uncountable ordinals.)
ETA: It is very imprecise to compare second-order model theory and set theory like this. Already model theory is set theory, of course, albeit (potentially, not in practice) set theory without power sets. I should just leave the model theory out of it and say:
If you believe in second-order logic, then you believe in set theory. (However, ….)
The reason I take second-order logic seriously is that it lets me pin down a single mathematical referent that I’m comparing to the realities of space and time.
I have my problems with the other two, but this is the only one I don’t understand. What do you mean?
it feels like talking about the collection of all collections—the supremum of an indefinitely extensible quality that shouldn’t have a supremum any more than I could talk about a mathematical object that is the supremum of all the models a first-order set theory can have
You seem to accept the notion that all finite numbers have a supremum. Why not just iterate whatever process accounts for that?
You seem to accept the notion that all finite numbers have a supremum. Why not just iterate whatever process accounts for that?
First of all, I’ve never seen an aleph-null, just one, two, three, etc. Accepting that the integers have a supremum is a whole different kettle of fish from accepting that the collection of finite integers seems to go on without bound. Second, taking a supremum once, using a clearly defined computable notation and a halting machine that can compare any two representations, is a whole different kettle of fish than talking about the supremum of all possible ways to define countable well-orderings to and beyond computable recursion.
you can’t talk about the integers or the reals in first-order logic.
It’s more accurate to say that you can’t talk about arbitrary subsets of the integers or the reals in first-order logic.
Accepting that the integers have a supremum is a whole different kettle of fish from accepting that the collection of finite integers seems to go on without bound.
I agree. This is the difference between completed and potential infinity. Nelson.
Second, taking a supremum once, using a clearly defined computable notation and a halting machine that can compare any two representations, is a whole different kettle of fish than talking about the supremum of all possible ways to define countable well-orderings to and beyond computable recursion.
I’m not so sure. Everything you’ve ever talked about, uncountable ordinals and all, you’ve talked about using computable notation. Computable, period is a whole different kettle of fish.
OK, you say you don’t accept that sort of uncomputable leap to the end. The problem is that, AIUI, you’re already accepting it as soon as you accept the power set of N. (Of the various “axioms of power” of ZFC, power set is the only one needed here. And if you just want omega_1, you don’t need arbitrary power sets, just that of N. I mean really you want P(N x N), but since N is in an easily-described bijection with N x N, it shouldn’t make a difference; just use a pairing function instead of proper ordered pairs.) The construction of omega_1 from P(N) is pretty straightforward, really, and doesn’t use any of ZFC’s other powerful axioms. Maybe you can somehow have the reals without P(N)? I.e. without binary expansions? shrug This is getting rather far away from what I know. Constructivists—well, not the milder ones who just reject excluded middle, but the stricter ones who don’t like impredicativity (whatever that might be, don’t ask me) -- don’t accept the axiom of power sets; they consider it just as much an unjustified leap to the end.
Of course you could always try summoning TobyBartels and ask him how the constructivists do it. When you say these sorts of things I’m a little of surprised you haven’t gone constructivist already. But I guess you like classical logic. :)
(By the “axioms of power”, I mean replacement, power set, and choice; the ones anyone might object to. Well, foundation is objectionable too, but it’s more of an axiom of weakness. Healing Salve as opposed to Ancestral Recall. :P Also looking things up apparently the no-impredicativity constructivists insist on weakening axiom of separation as well? Well, I think their weaker version should suffice here. Again, I am saying these things without carefully checking them because hopefully TobyBartels will show up and correct me if I am wrong. :) )
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.
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?
I think we may have something of a clash of backgrounds here. The reason I’m inclined to take the real continuum seriously is that there are numerous physical quantities that seem to be made of real or complex numbers. The reason I take mathematical induction seriously is that it looks like you might always be able to add one minute to the total number of minutes passed. The reason I take second-order logic seriously is that it lets me pin down a single mathematical referent that I’m comparing to the realities of space and time.
The reason I’m not inclined to take the least uncountable ordinal seriously is because, occupying as it does a position above the Church-Kleene ordinal and all possible hypercomputational generalizations thereof, it feels like talking about the collection of all collections—the supremum of an indefinitely extensible quality that shouldn’t have a supremum any more than I could talk about a mathematical object that is the supremum of all the models a first-order set theory can have. If set theory makes the apparent continuum from physics collide with this first uncountable ordinal, my inclination is to distrust set theory.
How can you say this after having read this thread?
If you believe in second-order model theory, then you believe in set theory. (However, by limiting it to second order over the natural numbers, without going on to third order, you are not obligated to believe in uncountable ordinals.)
ETA: It is very imprecise to compare second-order model theory and set theory like this. Already model theory is set theory, of course, albeit (potentially, not in practice) set theory without power sets. I should just leave the model theory out of it and say:
I have my problems with the other two, but this is the only one I don’t understand. What do you mean?
You seem to accept the notion that all finite numbers have a supremum. Why not just iterate whatever process accounts for that?
http://en.wikipedia.org/wiki/Second-order_logic#Expressive_power—you can’t talk about the integers or the reals in first-order logic. You can have first-order theories with the integers as a model, but they’ll have models of all other cardinalities too. http://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem
First of all, I’ve never seen an aleph-null, just one, two, three, etc. Accepting that the integers have a supremum is a whole different kettle of fish from accepting that the collection of finite integers seems to go on without bound. Second, taking a supremum once, using a clearly defined computable notation and a halting machine that can compare any two representations, is a whole different kettle of fish than talking about the supremum of all possible ways to define countable well-orderings to and beyond computable recursion.
It’s more accurate to say that you can’t talk about arbitrary subsets of the integers or the reals in first-order logic.
I agree. This is the difference between completed and potential infinity. Nelson.
I’m not so sure. Everything you’ve ever talked about, uncountable ordinals and all, you’ve talked about using computable notation. Computable, period is a whole different kettle of fish.
OK, you say you don’t accept that sort of uncomputable leap to the end. The problem is that, AIUI, you’re already accepting it as soon as you accept the power set of N. (Of the various “axioms of power” of ZFC, power set is the only one needed here. And if you just want omega_1, you don’t need arbitrary power sets, just that of N. I mean really you want P(N x N), but since N is in an easily-described bijection with N x N, it shouldn’t make a difference; just use a pairing function instead of proper ordered pairs.) The construction of omega_1 from P(N) is pretty straightforward, really, and doesn’t use any of ZFC’s other powerful axioms. Maybe you can somehow have the reals without P(N)? I.e. without binary expansions? shrug This is getting rather far away from what I know. Constructivists—well, not the milder ones who just reject excluded middle, but the stricter ones who don’t like impredicativity (whatever that might be, don’t ask me) -- don’t accept the axiom of power sets; they consider it just as much an unjustified leap to the end.
Of course you could always try summoning TobyBartels and ask him how the constructivists do it. When you say these sorts of things I’m a little of surprised you haven’t gone constructivist already. But I guess you like classical logic. :)
(By the “axioms of power”, I mean replacement, power set, and choice; the ones anyone might object to. Well, foundation is objectionable too, but it’s more of an axiom of weakness. Healing Salve as opposed to Ancestral Recall. :P Also looking things up apparently the no-impredicativity constructivists insist on weakening axiom of separation as well? Well, I think their weaker version should suffice here. Again, I am saying these things without carefully checking them because hopefully TobyBartels will show up and correct me if I am wrong. :) )
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?