That is very interesting (have an upvote!) but I don't see how it invalidates my argument. If every real is definable then the set of non-definable reals is empty and AoC does not apply at all.

The notion of countable and not countable does have some nuance. In the models that every real is definable that model, from within, believes it is uncountable since there is no bijection with a countable set from within that model. However, from the outside that model is countable.

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.

We need to be careful with the language here. It's not true that there are models of ZFC where the real numbers are actually definable. What's true is there are models of ZFC where what is considered a "real number" from within that model is always definable (but will not be definable within that model). However, those sets do not form the actual real numbers, they are simply sets that from within the model satisfy a given definition of the reals without actually being the reals.

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.

I’m not a logician or set theorist. I studied commutative algebra and, naturally, accept the axiom of choice. When you say, ”the actual reals” I think you mean the standard notion of a real number that we all are used to using. But those models that we are talking about are models of the axioms of the reals. So, they are the actual real numbers as far as that model is concerned, right?

You got it, absolutely. So yes there are models where as far as the model is concerned there is a set that satisfies the axioms of real numbers, and furthermore all elements of that set are actually definable (but not definable from within that model), but that set is not the standard notion of real numbers. It's just that it's impossible to provide a set of axioms that defines the real numbers and only the real numbers (in first order logic), so for any definition of the real numbers you end up with a model that will satisfy that definition but doesn't actually model the "standard notion of 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.

Understood. I wasn’t trying to address lisper’s directly as such. My poorly stated goal was to point out that intuition regarding uncountable sets is shaky at best. There are weird results regardless of one’s views because of nonstandard models.