I'm not sure you've shown anything. f(x) = x + 1 is a mapping from the reals to the reals. A choice function, with respect to the axiom of choice, is a mapping from the set to an element.
The author's argument relies on "indescribable-ness" somehow blocking the ability to "choose" an element. But that trades on a vague, intuitive understanding of "choosing", which doesn't capture what the AC is about. The AC is about the existence of certain functions. Since the "indescribable-ness" of the domain of a function is not relevant to its existence, the author's argument doesn't successfully attack the AC.
But that is not at issue. What is at issue is whether or not a function exists whose domain is an (infinite) set of indescribable numbers and whose range is a member of the set. The existence of such a function is far less clear.
Of course you can postulate the existence of such a function. But you can also postulate the existence of an oracle for the halting problem. My gut tells me that these two ideas have a lot in common.
> Remember that I am not here trying to argue for the truth of the AC; I'm arguing against the author's argument.
Yep, I get that.
> The author's argument, as I read it, relies on an intuition that "choosing" an element that is not-finitely-describable is problematic.
Not quite. Choosing an element from a set where all of the members are not-finitely-describable is problematic.
> However, the mathematical meaning of "choosing", in the context of the AC, is a statement about the mathematical existence of a certain function.
Yep, I get that.
> To respond to the author's intuition requires only showing that not-finitely-describable domains are not a "problem" for the existence of functions.
No, you would have to show that defining a function on this particular set is not a problem. Note that this is not the same thing as defining a function on elements of this set. That is obviously not a problem. But defining a (non-trivial) function on the set itself is.
It doesn't have anything to do with AoC per se, it has to do (I claim) with people's intuitions about AoC. Specifically, an infinite set of arbitrary subsets of the set of indescribable reals is something for which a reasonable person might be a tad suspicious about postulating the existence of a choice function.
https://mathoverflow.net/questions/44102/is-the-analysis-as-...
The point is there is a lot of nuance and no matter what one believes regarding choice there will be unintuitive results. For instance, when the axiom of choice fails you can have an infinite set with not countably infinite subset. The reals can be a countable union of countable sets. There is a set that can be partitioned into strictly more equivalence classes than the original set has elements, and a function whose domain is strictly smaller than its range. In fact, this is the case in all known models.
A similar result is that there are models of the reals in ZFC that are countable, even though the reals are not countable. How can this be? Well it's similar to the above argument, those models do not represent the actual real numbers.
All this means is that it's not possible to categorically define real numbers in first order ZFC. Any axiomatic definition of the reals in first order ZFC will have some models that satisfy those axioms but are not actually real numbers.
The reason I brought this up is because when you said that there are models of ZFC where every real is definable, those reals are only definable from outside of the model. From within that model there are still undefinable reals and hence I don't think it matters too much to the point lisper is making.
Maybe to put it another way, there is no model of the reals where within that model all reals are definable, and hence lisper's point stands.
I'm not a math expert, but "populating" a set strikes me as an imperative programming mindset. In math, I understand a set more like a function returning a boolean that indicates membership. If the contents of the set change, then it's just a new set.
Set A is the set of all widgets that have a frozz. The existence of Set A doesn't imply that there exists a widget that has a frozz. Perhaps the existence of such a widget is an open question. But the set is perfectly well defined.
By the way, it is worth keeping in mind how Gödel proved the consistency of the axiom of choice. Roughly speaking, the steps are: start with a model of ZF, build from it an inner model where all sets are definable (in a sense) in terms of ordinals, that model (called the "constructible universe") satisfies the axiom of choice. In other words, the axiom of choice holds as soon as you assume that all sets are constructible.
OK, but how are you going to construct a bijection from an arbitrary infinite set of undefinable numbers onto a set with a choice function without the AoC?
Ultimately, you're saying that if we have an indescribable x, then x+1 is conditionally describable (to abuse terminology). But I think that just sidesteps the question. Even then, if we're taking a computability lens, then indescribable(x) implies indescribable(x+1), which would seem to imply that applying your function to indescribable x's is a moot point.
The fact that your function is finitely describable even though we can't describe each of its applications is admittedly a mindfuck.