ZF is consistent with many negations of strong choice. For example, ZF is consistent with Lebesgue measurability of every subset in R. Well-ordering of R is enought to create unmeasurable set.
So, if ZF could prove existence of such a formula, ZF+measurability would prove contradiction, but ZF+neasurability is equiconsistent with ZF and ZF would be inconsistent.
It is very hard to say anything about any well-ordering of R, they are monster constructions...
Constructible version of R (if it is inside R and not the whole R) is just like Q: dense, small part of the whole, and usually zero-measure. So, this construction will yield something of measure zero if you define measure on the whole R.
Here’s a sort of related argument (very much not a math expert here): Any well ordering on the real numbers must be non-computable. If there was a computable order, you could establish a 1-1 correspondence between the natural numbers and the reals (since each real would be emitted on the nth step of the algorithm).
Well, yes, but mostly because most real numbers cannot ever be specified to an algorithm or received back from it. So you are right, ordering of R is about incomputable things.
The difference here is that we talk about ZFC formulas which can include quite powerful tricks easily.
This is true, but not, I think, the corect point to focus on.
The big obstacle is that the real numbers are uncountable. Of course, their uncountability is also why there exist uncomputable reals, but let’s put that aside for now, because the computability of individual reals is not the point.
The point is that computers operate on finite strings over finite alphabets, and there are only countably many of these. In order to do anything with a computer, you must first translate it into a problem about finite strings over a finite alphabet. (And the encoding matters, too—“compute the diameter of a graph” is not a well-specified problem, because “compute the diameter of a graph, specified as an adjacency matrix” and “compute the diameter of a graph, specified with connectivity lists” are different problems. And if of course I was implicitly assuming here the output was in binary—if we wanted it in unary, that would again technically be a different problem.)
So the whole idea of an algorithm that operates on or outputs real numbers is nonsensical, because there are only countably many finite strings over a given finite alphabet, and so no encoding is possible. Only specified subsets of real numbers with specified encodings can go into computers.
Notice that the whole notion of the computability of a real number appears nowhere in the above. It’s also a consequence of uncountability, but really not the point here.
I’m going to go into your original comment a bit more here:
If there was a computable order, you could establish a 1-1 correspondence between the natural numbers and the reals (since each real would be emitted on the nth step of the algorithm).
You seem to be under the impression that a countably infinite well-ordering must be isomorphic to omega, or at least that a computable one must be. I don’t think that would make for a useful definition of a computable well-ordering. Normally we define a well-ordering to be computable if it is computable as a relation, i.e. there is an algorithm that given two elements of your set will compare them according to your well-ordering. We can then define a well-order type (ordinal) to be computable if it is the order type of some computable well-ordering. By this definition, omega+1, and basically all the countable ordinals you usually see, are computable (well, except for the ones explicitly made not to be).
So the whole idea of an algorithm that operates on or outputs real numbers is nonsensical
You can work with programs over infinite streams in certain situations. For example, you can write a program that divides a real number by 2, taking an infinite stream as input and producing another infinite stream as output. Similarly, you can write a program that compares two unequal real numbers.
True, I forgot about that. I guess that would allow extending the notion of “computable well-ordering” to sets of size 2^aleph_0. Of course that doesn’t necessarily mean any of them would actually be computable, and I expect none of them would. Well, I guess it has to be the case that none of them would, or else we ought to be able to prove “R is well-orderable” without choice, but there ought to be a simpler argument than that—just as computable ordinals in the ordinary sense are downclosed, I would expect that these too ought to be downclosed, which would immediately imply that none of the uncountable ones are computable. Now I guess I should actually check that they are downclosed...
Upvoted on reflection for the part I quoted, which either answers the question or gives us some reason to distinguish R-in-L (the set we’d call the real numbers if we endorsed the statement “V=L”) from “the-real-numbers-as-we-know-them”.
Nope.
ZF is consistent with many negations of strong choice. For example, ZF is consistent with Lebesgue measurability of every subset in R. Well-ordering of R is enought to create unmeasurable set.
So, if ZF could prove existence of such a formula, ZF+measurability would prove contradiction, but ZF+neasurability is equiconsistent with ZF and ZF would be inconsistent.
It is very hard to say anything about any well-ordering of R, they are monster constructions...
Does a well-ordering on the constructable version of R provably do this? I fear I can’t tell if you’ve addressed my question yet.
Constructible version of R (if it is inside R and not the whole R) is just like Q: dense, small part of the whole, and usually zero-measure. So, this construction will yield something of measure zero if you define measure on the whole R.
Here’s a sort of related argument (very much not a math expert here): Any well ordering on the real numbers must be non-computable. If there was a computable order, you could establish a 1-1 correspondence between the natural numbers and the reals (since each real would be emitted on the nth step of the algorithm).
Is that remotely right?
Well, yes, but mostly because most real numbers cannot ever be specified to an algorithm or received back from it. So you are right, ordering of R is about incomputable things.
The difference here is that we talk about ZFC formulas which can include quite powerful tricks easily.
Oh right, I forgot that real numbers could be individually non-computable in the first place.
This is true, but not, I think, the corect point to focus on.
The big obstacle is that the real numbers are uncountable. Of course, their uncountability is also why there exist uncomputable reals, but let’s put that aside for now, because the computability of individual reals is not the point.
The point is that computers operate on finite strings over finite alphabets, and there are only countably many of these. In order to do anything with a computer, you must first translate it into a problem about finite strings over a finite alphabet. (And the encoding matters, too—“compute the diameter of a graph” is not a well-specified problem, because “compute the diameter of a graph, specified as an adjacency matrix” and “compute the diameter of a graph, specified with connectivity lists” are different problems. And if of course I was implicitly assuming here the output was in binary—if we wanted it in unary, that would again technically be a different problem.)
So the whole idea of an algorithm that operates on or outputs real numbers is nonsensical, because there are only countably many finite strings over a given finite alphabet, and so no encoding is possible. Only specified subsets of real numbers with specified encodings can go into computers.
Notice that the whole notion of the computability of a real number appears nowhere in the above. It’s also a consequence of uncountability, but really not the point here.
I’m going to go into your original comment a bit more here:
You seem to be under the impression that a countably infinite well-ordering must be isomorphic to omega, or at least that a computable one must be. I don’t think that would make for a useful definition of a computable well-ordering. Normally we define a well-ordering to be computable if it is computable as a relation, i.e. there is an algorithm that given two elements of your set will compare them according to your well-ordering. We can then define a well-order type (ordinal) to be computable if it is the order type of some computable well-ordering. By this definition, omega+1, and basically all the countable ordinals you usually see, are computable (well, except for the ones explicitly made not to be).
You can work with programs over infinite streams in certain situations. For example, you can write a program that divides a real number by 2, taking an infinite stream as input and producing another infinite stream as output. Similarly, you can write a program that compares two unequal real numbers.
True, I forgot about that. I guess that would allow extending the notion of “computable well-ordering” to sets of size 2^aleph_0. Of course that doesn’t necessarily mean any of them would actually be computable, and I expect none of them would. Well, I guess it has to be the case that none of them would, or else we ought to be able to prove “R is well-orderable” without choice, but there ought to be a simpler argument than that—just as computable ordinals in the ordinary sense are downclosed, I would expect that these too ought to be downclosed, which would immediately imply that none of the uncountable ones are computable. Now I guess I should actually check that they are downclosed...
What does it mean to be downclosed?
I mean closed downwardly—if one is computable, then so is any smaller one. (And so the Church-Kleene ordinal is the set of all computable ordinals.)
Upvoted on reflection for the part I quoted, which either answers the question or gives us some reason to distinguish R-in-L (the set we’d call the real numbers if we endorsed the statement “V=L”) from “the-real-numbers-as-we-know-them”.