3 ms·

See the “well ordering theorem”.

• Dylan16807 2y ago
  Okay, I hadn't really picked up on the implications of well-ordering there. Though the (im)possibility of well-ordering all reals doesn't really matter here. Computable reals can by sorted by their programs, and definable reals can be sorted by their definitions. So if you have a "concrete definition of definable reals", then the system you use gives you ways to well-order them. And if you want to "refer to the first real that’s undefinable in that system", you can make a new system2 that encapsulates the old system1. That might prove we can't have a universal system for defining things, which would be disappointing but workable. Or maybe it's just that "the first real that's undefinable in system1" is not concrete, so we can reject it as a description of a number, and then the consequences are much smaller.
• skissane 2y ago
  Which is equivalent to the axiom of choice. If one chooses not to accept that axiom, then the well-ordering theorem is not a theorem. One can even (consistently) append the negation of the axiom of choice to ZF, in which case this theorem is false. Mere negation of the axiom of choice is not a very interesting addition, but there are some interesting alternative axioms, such as the axiom of determinacy, which have negation of the axiom of choice as a consequence People who are fixated on definable/computable reals generally have constructivist sympathies, and many (but not all) constructivist mathematicians reject the axiom of choice. So relying on it in arguments in this context is questionable. https://mathoverflow.net/questions/119561/mathematics-with-the-negation-of-ac https://mathoverflow.net/questions/119561/mathematics-with-t...