I would be interested in knowing if there is any second-order system which is strong enough to talk about continuity, but not to prove the existence of a first uncountable ordinal.
I can do better. I can give you a complete, decidable, axiomatized system that does that: first order real arithmetic. However, in this system you can’t talk about integers in any useful way.
We can do better than that: first order real arithmetic + PA + a set of axioms embedding the PA integers into R in the obvious way. This is a second order system where I can’t talk about uncountable ordinals. However, this system doesn’t let us talk about sets.
Note that in both these cases we’ve done this by minimizing how much we can talk about sets. Is there some easy way to do this where we can talk about set a reasonable amount?
I’m not sure. Answering that may be difficult (I don’t think the question is necessarily well-defined.) However, I suspect that the following meets one’s intuition as an affirmative answer: Take ZFC without regularity, replacement or infinity, choice, power set or foundation. Then add as an axiom that there exists a set R that has the structure of a totally ordered field with the least-upper bound property.
This structure allows me to talk about most things I want to do with the reals while probably not being able to prove nice claims about Hartogs numbers which should make proving the existence of uncountable ordinals tough. It would not surprise me too much if one could get away with this system with the axiom of the power set thrown also. But it also wouldn’t surprise me either if one can find sneaky ways to get info about ordinals.
Note that none of these systems are at all natural in any intuitive sense. With the exception of first-order reals they are clear attempts to deliberately lobotomize systems. (ETA: Even first order reals is a system which we care about more for logic and model theoretic considerations than any concrete natural appreciation of the system.) Without having your goal in advance or some similar goal I don’t think anyone would ever think about these systems unless they were a near immortal who was passing the time by examining lots of different axiomatic systems.
While thinking about this I realized that I don’t know an even more basic question: Can one deal with what Eliezer wants by taking out the axiom schema of replacement, choice, and foundation? The answer to this is not obvious to me, and in some sense this is a more natural system. If this is the case then one would have a robust system in which most of modern mathematics could be done but you wouldn’t have your solution. However, I suspect that this system is enough to prove the existence of the least uncountable ordinal.
Note that without replacement, you can’t construct the von Neumann ordinal omega*2, or any higher ones, so certainly not omega_1. Of course, this doesn’t prevent uncountable well-ordered sets (obviously these follow from choice, though I guess you’re taking that out as well), but you need replacement to show that every well-ordered set is isomorphic to a von Neumann ordinal.
So I don’t think that this should prevent the construction of an order of type omega_1, even if it can’t be realized as a von Neumann ordinal. Of course losing canonical representatives means you have to talk about equivalence classes, but if all we want to do is talk about omega_1, it suffices to consider well-orderings of subsets of N, so that the equivalence classes in question will in fact be sets. Maybe there’s some other technical obstacle I’m missing here (like it somehow wouldn’t be the first uncountable ordinal despite being the right order?) -- this isn’t really my area and I haven’t bothered to work through it, I can try that later—but I wouldn’t expect one.
Maybe there’s some other technical obstacle I’m missing here
There’s not. The Hartog’s number construction gives us the set H(N) of all isomorphism classes of well-orders on subsets of any fixed countably infinite set, and we can prove that H(N) is uncountable and every proper initial segment of H(N) is countable, using power set and separation (but only bounded separation) but not replacement. I verified this just now by looking at Wikipedia’s article on Hartog’s number and checking through the proof myself.
The next step (step 4 in Wikipedia, ETA: which can be saved for the end, although WP did not do so) is to replace the elements of H(N) with von Neumann ordinals, but this is really beside the point. You already have a representation of the least uncountable ordinal, and this step is just making it canonical in a certain way.
It’s not clear to me that ZFC without regularity, replacement, infinity, choice, power set or foundation with a totally ordered field with the LUB property does allow you to talk about most things you want to do with the reals : without replacement or powerset you can’t prove that cartesian products exist, so there doesn’t seem to be any way of talking about the plane or higher-dimensional spaces as sets. If you add powerset back in you can carry out the Hartogs number construction to get a least uncountable ordinal
Hmm, that’s a good point. Lack of cartesian products is annoying. We don’t however need the full power set axiom to get them. We can simply have an axiom that states that cartesian products exist. Or even weaker do the following (ad hoc axioms) with a new property of being Cartesian: 1. The cartesian product of any two Cartesian sets exist. 2. Any subset of R is Cartesian. 3. The cartesian product of two Cartesian sets is Cartesian. 4. If A and B are Cartesian then A union B, A intersect B, and A\B are all Cartesian. That should be enough and is a lot weaker than general power set I think.
van den Dries, “Tame topology and o-minimal structures,” Cambridge U Press 1998
develops a lot of 20th century geometry in a first order theory of real numbers. You can do enough differential geometry in this setting to do e.g. general relativity.
I would be interested in knowing if there is any second-order system which is strong enough to talk about continuity, but not to prove the existence of a first uncountable ordinal.
I can do better. I can give you a complete, decidable, axiomatized system that does that: first order real arithmetic. However, in this system you can’t talk about integers in any useful way.
We can do better than that: first order real arithmetic + PA + a set of axioms embedding the PA integers into R in the obvious way. This is a second order system where I can’t talk about uncountable ordinals. However, this system doesn’t let us talk about sets.
Note that in both these cases we’ve done this by minimizing how much we can talk about sets. Is there some easy way to do this where we can talk about set a reasonable amount?
I’m not sure. Answering that may be difficult (I don’t think the question is necessarily well-defined.) However, I suspect that the following meets one’s intuition as an affirmative answer: Take ZFC without regularity, replacement or infinity, choice, power set or foundation. Then add as an axiom that there exists a set R that has the structure of a totally ordered field with the least-upper bound property.
This structure allows me to talk about most things I want to do with the reals while probably not being able to prove nice claims about Hartogs numbers which should make proving the existence of uncountable ordinals tough. It would not surprise me too much if one could get away with this system with the axiom of the power set thrown also. But it also wouldn’t surprise me either if one can find sneaky ways to get info about ordinals.
Note that none of these systems are at all natural in any intuitive sense. With the exception of first-order reals they are clear attempts to deliberately lobotomize systems. (ETA: Even first order reals is a system which we care about more for logic and model theoretic considerations than any concrete natural appreciation of the system.) Without having your goal in advance or some similar goal I don’t think anyone would ever think about these systems unless they were a near immortal who was passing the time by examining lots of different axiomatic systems.
While thinking about this I realized that I don’t know an even more basic question: Can one deal with what Eliezer wants by taking out the axiom schema of replacement, choice, and foundation? The answer to this is not obvious to me, and in some sense this is a more natural system. If this is the case then one would have a robust system in which most of modern mathematics could be done but you wouldn’t have your solution. However, I suspect that this system is enough to prove the existence of the least uncountable ordinal.
Note that without replacement, you can’t construct the von Neumann ordinal omega*2, or any higher ones, so certainly not omega_1. Of course, this doesn’t prevent uncountable well-ordered sets (obviously these follow from choice, though I guess you’re taking that out as well), but you need replacement to show that every well-ordered set is isomorphic to a von Neumann ordinal.
So I don’t think that this should prevent the construction of an order of type omega_1, even if it can’t be realized as a von Neumann ordinal. Of course losing canonical representatives means you have to talk about equivalence classes, but if all we want to do is talk about omega_1, it suffices to consider well-orderings of subsets of N, so that the equivalence classes in question will in fact be sets. Maybe there’s some other technical obstacle I’m missing here (like it somehow wouldn’t be the first uncountable ordinal despite being the right order?) -- this isn’t really my area and I haven’t bothered to work through it, I can try that later—but I wouldn’t expect one.
There’s not. The Hartog’s number construction gives us the set H(N) of all isomorphism classes of well-orders on subsets of any fixed countably infinite set, and we can prove that H(N) is uncountable and every proper initial segment of H(N) is countable, using power set and separation (but only bounded separation) but not replacement. I verified this just now by looking at Wikipedia’s article on Hartog’s number and checking through the proof myself.
The next step (step 4 in Wikipedia, ETA: which can be saved for the end, although WP did not do so) is to replace the elements of H(N) with von Neumann ordinals, but this is really beside the point. You already have a representation of the least uncountable ordinal, and this step is just making it canonical in a certain way.
Heh, I’d forgotten how simple Hartogs number was in general.
It’s not clear to me that ZFC without regularity, replacement, infinity, choice, power set or foundation with a totally ordered field with the LUB property does allow you to talk about most things you want to do with the reals : without replacement or powerset you can’t prove that cartesian products exist, so there doesn’t seem to be any way of talking about the plane or higher-dimensional spaces as sets. If you add powerset back in you can carry out the Hartogs number construction to get a least uncountable ordinal
Hmm, that’s a good point. Lack of cartesian products is annoying. We don’t however need the full power set axiom to get them. We can simply have an axiom that states that cartesian products exist. Or even weaker do the following (ad hoc axioms) with a new property of being Cartesian: 1. The cartesian product of any two Cartesian sets exist. 2. Any subset of R is Cartesian. 3. The cartesian product of two Cartesian sets is Cartesian. 4. If A and B are Cartesian then A union B, A intersect B, and A\B are all Cartesian. That should be enough and is a lot weaker than general power set I think.
van den Dries, “Tame topology and o-minimal structures,” Cambridge U Press 1998
develops a lot of 20th century geometry in a first order theory of real numbers. You can do enough differential geometry in this setting to do e.g. general relativity.
The J_2 referenced in this subthread shoud do the trick. (See in particular number 6 in the page linked to by shinoteki there).