This is very interesting but I think it relies heavily on interpretation.
For example there exists models of ZFC where all "real numbers" are definable, but said model does not include all the actual real numbers, it excludes any number that is not definable in ZFC. The issue is that the term "real number" is overloaded. In the formal sense it may refer only to numbers that are members of a model in which undefinable numbers are excluded. In another sense the term "real number" refers to actual real numbers as we humans intend for them to exist but do not have a precise formal definition.
This actual set of real numbers does indeed contain members that are not definable in ZFC or any formal system, the issue is that there is no way to formalize this actual definition.
This is similar to what another poster mentioned about Skolem's paradox:
> In another sense the term "real number" refers to actual real numbers as we humans intend for them to exist but do not have a precise formal definition.
Ah a Platonist in the flesh. Don't see many of you on HN. I don't think real numbers truly, objectively exist and think of them more as artifacts of human thought, but that's a deep deep rabbit hole.
I'm kind of curious then, what do you believe the cardinality of the "real" real numbers is?
I think I'm with you on that. Real numbers don't exist in an objective sense, I mean they exist in the same sense that an Escher painting of a hand drawing a hand exists, but they don't exist in the sense that a hand drawing a hand actually exists.
When I was in high school I remember thinking that computers use the discrete to approximate the continuous and that it is the continuum that is real and the discrete that is an imperfect representation of the continuous. Then a high school teacher blew my mind when he told me to consider the opposite, that in fact it's the continuous that is used to approximate the discrete. The discrete is what's real and we humans invented the continuous to approximate the discrete.
That simple twist in thinking had a profound effect on me that influences me to this day 30 years later.
If anything I may have some extreme opinions that frankly no one takes seriously and I'm okay with that. For example I think the finitists had it right and infinity does not exist. There really is such a thing as a largest finite number, a number so large that it's impossible even in principle to add 1 to it. I can't fathom how large that number is, but there's physical justification to believe in it based on something like the Bekenstein bound:
At any rate, I like thinking about this stuff, I do appreciate it, but I don't take it literally. It's poetic, it can inspire new ways of thinking, but I also remind myself to compartmentalize it to some degree and not take these ideas too literally.
If you're sympathetic to the finitist cause, the idea that all mathematical objects are in fact definable is right up that alley. It's nice that this happens to line up acceptance of infinity, but finitism is basically entirely predicated on definability.
For example there exists models of ZFC where all "real numbers" are definable, but said model does not include all the actual real numbers, it excludes any number that is not definable in ZFC. The issue is that the term "real number" is overloaded. In the formal sense it may refer only to numbers that are members of a model in which undefinable numbers are excluded. In another sense the term "real number" refers to actual real numbers as we humans intend for them to exist but do not have a precise formal definition.
This actual set of real numbers does indeed contain members that are not definable in ZFC or any formal system, the issue is that there is no way to formalize this actual definition.
This is similar to what another poster mentioned about Skolem's paradox:
https://news.ycombinator.com/item?id=28767108