My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.
Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with.
I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it.
All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.
> Strictly speaking, a programming language doesn't really need comments. "But Lisp has them, and puts them in double quotes."
Lisp has comments, but they aren't generally contained in double quotes, you've tossed a lot of strings into your program and called them comments. Comments are either marked with ; (comment to end of line, like //) with conventions on how many semicolons to use in particular places, or comment blocks with #| comment |# (nestable version of /* */). You can add documentation to many definitions, like functions, using strings which may be what you're thinking of but that happens inside the definition like with this:
(defun constant (x)
"CONSTANT returns a function which always returns X"
(lambda (a) x))
Which is a comment, but it's unusual to use strings as comments outside of contexts like that. Also, if you're going to use strings as comments you can make them multi-line instead of doing
"I thought about calling these car and cdr..."
"...then decided that I'm not really THAT addicted to Lisp"
with:
"I thought about calling these car and cdr...
...then decided that I'm not really THAT addicted to Lisp"
The other reason I'm posting this nit is that if anyone reads your blog/answer and tries to use comments as you've described them inside of expressions they'll be very confused about why it's behaving incorrectly. There's no reason to mislead people, this is not a comment:
(if (= 1 2) "Should never be true" ;; that's not a comment, it's an expression
(print "Never happens")
(print "Always happens")) ;; your interpreter or compiler will complain about this code
And that is why I did think that. I only play with the ideas of Lisp. I've never really had to use it. So I looked at a Lisp example, saw something that looked like it was functioning as a comment, then used that comment style.
In that light, the statement that the reals have greater cardinality than the naturals can be thought of as a statement that _our model of set theory_ happens to contain no injections from the reals to the naturals. Not that they can’t exist in a Platonic sense, or even just in the metatheory.
That does seem extremely relevant. And is a mirror of the fundamental insight behind nonstandard analysis. Which is that that any set containing the integers that follows some set of axioms, has a nonstandard model that follows a nonstandard version of those axioms, and which contains infinite integers.
This can be seen as why it is different for a set of axioms to prove that it proves something, than it is to prove something directly. Because when the axioms prove that they prove, you might be in a nonstandard model where that "proof" is infinitely long, and therefore isn't really a proof!
And that is why, for example, if PA is consistent, then it remains consistent if you extend PA with the axiom, "PA is not consistent". Clearly any model of that extended set of axioms does not describe what we want PA to mean. But that doesn't mean that it logically contradicts itself, either.
From the point of view of proof-theory, you can show that PA (arithmetic) is equivalent to the consistency of the omega cardinal (the countable infinite).
Basically, everything line up quite well between things you want to be true and things that are true in that system.
This equivalence breaks down with higher-order system such as System F, but it gives a system that may feel more natural, especially to programmers.
The problem that explains the endurance of "formalism" is that there are so many things that you "want to be true" that can't be shown to be true in intuitionistic systems is a real issue. For instance, simply proving that a fast-growing function is total. You are fine with recurrence, but not if the function grows too fast? This sounds really stupid. But I don't think many people care that much, they'll just use whatever give them results.
It is certainly easier to prove interesting theorems with formalism. You don't get caught up with such basic things like whether or not it is always possible to tell that one real number is bigger than another.
But formalism leads to having to accept conclusions that some of us don't like. I already referred to the existence of uncountably many things that cannot in any useful way ever be specified. If you include the axiom of choice, you get the Banach-Tarski paradox. Mathematicians debated that one for a while, but now generally accept it.
My favorite example of a weird conclusion comes from https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo.... We can non-constructively prove the following facts. Any class of graphs that is closed under the graph minor operation (for example planar graphs), has a finite set of forbidden graph minors that completely characterize the graph (in the case of planar graphs, K5 and K3,3). In general, there is no way to find those forbidden graph minors. Even if you were given the complete list, you couldn't necessarily verify that the list was correct. You cannot necessarily even find an upper bound on how big this set is.
By "cannot necessarily" I mean, "it is sometimes unprovable".
In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?
To make this concrete, there are 17,523 known forbidden minors for the toroidal graphs. We don't know how to find more. We don't know if we have the full list. And we don't have an upper bound on how many more of them there are to be found.
You're free to accept this ephemeral claim to existence as actual existence. But this existence isn't very useful for us.
> In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?
In the same sense that we could say that every computer program must either eventually terminate or never terminate without most people thinking there's a major philosophical problem here.
And by the way, the very same question can be (and has been) levelled at constructivism: in what sense does a result that would take longer than the lifetime of the universe to compute exist, as it is unfindable and unverifiable?
Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results. It's one thing to say that we can learn interesting things in constructive mathematics and another to say there's a fundamental problem with non-constructive mathematics.
> But formalism leads to having to accept conclusions that some of us don't like.
At least in Hilbert's sense, I don't think formalism says quite what you claim it says. He says that some mathematical statements or results apply to things we can see in the world and could be assigned meaning through, say, correspondence to physics. But other mathematical statements don't say anything about the physical world, and therefore the question of their "actual meaning" is not reason to reject them as long as they don't lead to "real" results (in the first class of statements) that contradict physical reality.
Formalism, therefore, doesn't require you to accept or reject any particular meaning that the second class of statements may or may not have. If a statement in the second class says that some set exists, you don't have to assign that "existence" any meaning beyond the formula itself.
> Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results.
I don't think the point of constructivism is to "philosophically reject non-constructive results". You can accept non-constructive results just fine as a constructivist, so long as they're consistently rephrased as negative statements, i.e. logical statements starting with "NOT ...". This is handy in some ways (you now know instantly what statements correspond to "direct" proofs that can be given a computational semantics and even be reused for all sorts of computer sciencey stuff) and not so handy in others (to some extent, it comes with a kind of denial about the inherently "dual" nature of the fragment of your constructive logic that contains all that negatively-phrased stuff). But these are matters of aesthetics and perceived elegance, more than philosophy.
The duality concern is one that some will want to address by moving even further to linear logics (since these are "dual" like classical logic but also allow for constructive statements) but of course that's yet another can of worms in its own right.
When you talk about the point of constructivism, do you mean currently, or historically?
For me, personally, the point of constructivism is to wind up talking about mathematics in a language that corresponds with what I want words to mean. I personally want mathematical existence to mean something that could be represented in an ideal computer. And existence in classical mathematics means something very different than that.
But historically, the point of constructivism was to try to avoid paradoxes through careful reasoning. At least that is my understanding. You're welcome to read http://thatmarcusfamily.org/philosophy/Course_Websites/Readi... and decide if that is what Brouwer meant.
Unfortunately for this historical motivation, Gödel proved that every classical mathematical proof can be mechanically transformed into a purely constructive proof, possibly of a much more carefully worded statement. With the result that if there is a contradiction within classical mathematics, there is also a contradiction within constructivism.
Luckily it has been so long since our foundations of mathematics fell apart because of someone finding a contradiction, that we no longer worry about it. (Was the set of all sets that do not contain themselves the last such contradiction? I think it might have been.)
You could argue that the early constructivists' notions of "paradoxes" included things such as "statements about the existence of things that we don't know how to explicitly construct, and that may be even impossible to explicitly construct in the general case". Under Gödel's argument, these statements (like other classical statements) become mere negative statements asserting the non-existence of anything that might contradict the aforementioned non-constructive objects. So, they're no longer "paradoxical" in that sense. Stated another way, decidability/computability (perhaps relative to some appropriate oracle, to fully account for the surprising strength of some loosely-"constructive" principles) is not quite the same concern as consistency. Of course, this was all stated in very fuzzy and imprecise terms to begin with (no real notion back then of what "decidable" and "computable" might mean), so there's that.
My understanding of how Hilbert meant it is summed up in this quote from him: "Mathematics is a game played according to certain simple rules with meaningless marks on paper." I think that in part because I read Constance Reid's excellent biography Hilbert! It traces in some detail his thinking over his life, and how he came to formalism. His thinking about the nature of existence was particularly interesting.
If you think that he meant something else, please find somewhere where he said something that didn't boil down to that.
As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about. I know that I didn't.
After you've thought about it, you may well have a dramatically different opinion than I do. For example Gödel thought that mathematical existence was real, since mathematics exists in God's mind. This idea made it important to him to decide which set of axioms was right, where right means, "These are the axioms that God must have settled on, and that therefore exist in His mind." This lead to such ironies as the fact that after proving that the consistency of ZF implies the consistency of ZFC, he then concluded that that the construction was so unnatural that Choice couldn't be one of God's axioms!
I don't agree with Gödel. For a start, I don't believe that God exists. And after I thought about it more, I realized that what I want existence to mean, isn't what mathematicians mean when they say "exists". I'm willing to use language in their way when I'm talking to them. But I'm always aware that it doesn't mean what I want it to mean.
I can't locate my Heijenoort right now, but here's a description from the Stanford Encyclopedia of Philosophy [1] (which points to Heijenoort):
The analogy with physics is striking... In the second half of the 1920s, Hilbert replaced the consistency program with a conservativity program: Formalized mathematics was to be considered by analogy with theoretical physics. The ultimate justification for the theoretical part lies in its conservativity over “real” mathematics: whenever theoretical, “ideal” mathematics proves a “real” proposition, that proposition is also intuitively true. This justifies the use of transfinite mathematics: it is not only internally consistent, but it proves only true intuitive propositions (and indeed all, since a formalization of intuitive mathematics is part of the formalization of all mathematics).
In 1926, Hilbert introduced a distinction between real and ideal formulas. This distinction was not present in 1922b and only hinted at in 1923. In the latter, Hilbert presents first a formal system of quantifier-free number theory about which he says that “The provable formulae we acquire in this way all have the character of the finite”
In other words, Hilbert does not require assigning any sense of truth beyond the symbolic one to those mathematical statements that do not correspond to physical reality, but those statements that can correspond to physical reality (i.e. the "real formulas") must do so, and those "real formulas" are meaningfully true beyond the symbols.
The earlier formalism (mathematics is just symbols) could no longer be justified after Gödel, as consistency was its main justification.
If anything, I think it's constructivism that suffers from a philosophical issue in requiring meaning that isn't physically realisable -- unlike ultrafinitism, for example. Personally, I find both Hilbert's formalism and ultrafinitism more philosophically satisfying than constructivism, as they're both rooted in physical reality, whereas constructivism is based on "computation in principle" (but not in practice!).
> As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about
> Some of the humans who have thought about it do reject them.
I think they reject them only if they misrepresent Hilbert's formalism, because formalism does not assign them any meaning of truth beyond the symbolic. It makes no statement that could be rejected: a mathematical theorem that proves a set "exists" does not necessarily make any claim about its "actual" existence (unlike, say, Platonism). You asked in what sense does such a set exist, and Hilbert would say, great question, which is why I don't claim there necessarily is any such sense.
What those who reject Hilbert's formalism reject is the validity of a system of mathematics where only some but not all propositions are "externally" meaningful, but such a rejection, I think, can only be on aesthetic grounds, because, again, for Hilbert, all "valid" foundations must agree with physical reality when it comes to statements that could be assigned physical meaning. If ZFC led to any result that doesn't agree with physical reality, Hilbert would reject it, too. But it hasn't yet.
I believe that you are misrepresenting Hilbert here.
If ZFC led to a result that doesn't agree with physical reality, Hilbert would not reject that result. Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula. For example, Euclid's geometry doesn't agree with physical reality. Therefore it is an ideal formula, not a real formula. And yet we do not reject this geometry from mathematics.
But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
> Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula.
No. No result, either ideal or real, may contradict reality (it's just that since infinitary statements do not describe reality, they obviously cannot contradict it). You can think about it like this: According to Hilbert, a valid mathematical foundation is any logical theory that is a conservative extension of reality. ZFC, constructive foundations, and ultrafinitist foundations all satisfy that, so they would all be valid foundations according to that principle.
> For example, Euclid's geometry doesn't agree with physical reality.
It may not describe physical reality, but it doesn't contradict it.
> But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
Not only does that disagree with Hilbert's formalism, it also disagrees with constructivism. The question of the philosophy of mathematics is precisely what, if anything, does mathematics describe beyond symbols.
I think what the poster above means is that any formal system in which, say, 1 + 1 = 75, even if internally consistent as a set of symbols, would not be considered a valid logical foundation for mathematics by Hilbert, because it directly contradicts physical reality. Of course, this is under the assumption that 1 and + and 75 are meant to have their usual meanings, not that we've redefined the + operator to mean "the 73rd successor", nor that we're operating in some exotic numerical base where 75 is just a different set of symbols to describe the number 2.
> I have absolutely no idea how physical reality can contradict a statement about a formal symbol game.
Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.
I should clarify that when I talk about "physical reality" that's shorthand for things that are, at least in principle, verifiable using physical means.
> I am also convinced that what you are saying is not what Hilbert actually meant. But he died before I was born, so I can't ask him. Besides, I don't speak German.
Ok, but if you're not sure what a certain philosophical position is, surely you cannot find fault with it. But I was able to locate my Heijenoort, so we can try, assuming you trust Heijenoort's translation.
So here's just a tidbit from Hilbert's 1925 "On The Infinite" (Heijenoort p.367):
And the net result is, certainly, that we do not find anywhere in reality a homogeneous continuum that permits of continued division and hence would realize the infinite in the small. The infinite divisibility of a continuum is an operation that is present only in ourthoughts; it is merely an idea, which is refuted by our observations of nature and by the experience gained in physics and chemistry.
And here are parts of Hilbert, 1927, "The foundations of mathematics" (Heijenoort p.464):
All the propositions that constitute mathematics are converted into formulas, so
that mathematics proper becomes an inventory of formulas.
...even elementary mathematics contains, first, formulas to which correspond contentual communications of finitary propositions (mainly numerical equations or inequalities, or more complex communications composed of these) and which we may
call the real propositions of the theory, and, second, formulas that -just like the numerals of contentual number theory - in themselves mean nothing but are merely things that are governed by our rules and must be regarded as the ideal objects of the theory.
These considerations show that, to arrive at the conception of formulas as ideal propositions, we need only pursue in a natural and consistent way the line of development that mathematical practice has already followed till now.
... Now the fundamental difficulty that we face here can be avoided by the use of ideal propositions. For, if to the real propositions we adjoin the ideal ones, we obtain a system of propositions in which all the simple rules of Aristotelian logic hold and all the usual methods of mathematical inference are valid.
... To be sure, one condition, a single but indispensable one, is always attached to the use of the method of ideal elements, and that is the proof of consistency; for, extension by the addition of ideal elements is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain.
... To make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable; on the contrary, a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument. What the physicist demands precisely of a theory is that particular propositions be derived from laws of nature or hypotheses solely by inferences, hence on the basis of a pure formula game, without extraneous considerations being adduced. Only certain combinations and consequences of the physical laws can be checked by experiment just as in my proof theory only the real propositions are directly capable of verification.
The value of pure existence proofs consists precisely in that the individual construction is eliminated by them and that many different constructions are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the raison d'être of existence proofs.
In other words, "ideal" propositions may mean nothing in and of themselves but they are valid as long as they are a conservative extension of the "real" propositions (the narrower domain), which are necessarily meaningful as they are "directly capable of verification".
> Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.
It would only contradict physical reality if a machine to calculate that algorithm failed to solve the EXPTIME-hard problem as promised. And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
As for your long quote from Hilbert, I understand it very differently from you. He is saying that our interest in ideal mathematics starts with real mathematics. But ideal mathematics is something to engage with on its own terms, whether or not it corresponds with anything real.
Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.
> And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
You can axiomatically add oracles without introducing logical inconsistencies. It is commonly done in complexity theory. The "mistake" is in interpreting such results as directly corresponding to the real world (same as interpreting 2 + 1 = 0 in modular arithmetic as if it were saying something about natural numbers). That is Hilbert's point: we need to be clear about how we map certain mathematical statements to the real world, and "to make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable", i.e. even when we're clear about such a mapping, it is not a requirement that every forumla had such a mapping. Or, perhaps more clear, Hilbert's point is that if in a logical theory not every formula can be assigned a "real meaning", that does not invalidate assigning real meaning to some formulas.
> Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.
He is very explicit that he is not saying that about the "real" propositions. He calls them "contentual", as in carrying content beyond the symbols. From the same talk:
If we now begin to construct mathematics, we shall first set our sights upon elementary number theory; we recognize that we can obtain and prove its truths through contentual intuitive considerations. The formulas that we encounter when we take this approach are used only to impart information.
He is very clear that the justification for the use of formulas that are "just a symbols game" is that they are consistent with formulas that are contentual and are not just a symbols game. That is the debate between Hilbert and Brouwer, or formalism and intuitionism: whether or not all formulas must have an intuitive meaning ("content"). In formalism, not all of them must.
It is precisely because Hilbert's justification was based on consistency, as without it, "real" propositions could be wrong, that the incompleteness results made that justification unprovable.
I'm fine with that. I don't think it's much worse than the quirks of what you call non-formalists systems.
In your original comment, you mention:
All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.
If you wanted to formalize something like that, you'd need the consistency of an absurdly large cardinal. I think it is an interesting type of question to explore, so it's fine to have these large cardinals.
I believe that you're fine with it, simply because that is what you're familiar with. And if you'd grown up with a different way of thinking about these problems, then you wouldn't be fine with it.
Personally, I can work with either system. But, to me, formalism really does feel like a game. And the more that I have thought about the foundations of math, the more dissatisfied I have become with this game. And now I find myself frustrated when people assert the conclusions of the game as truth, instead of as merely being formal statements within a game that mathematicians are choosing to play.
Here is something that I believe.
We owe our current understanding of uncountability to Cantor's metaphor, about figuring out which group of sheep is larger by pairing them off. We would today have a very different kind of mathematics if Cantor had instead made a more careful analogy to the problem of trying to count all of the sheep that have ever existed. Even if you had perfect information about the past, you're doomed to fail because you can't figure out where to draw the line between ancestral sheep, and sheep-like ancestors.
This second metaphor is exactly parallel to uncountability within the computable universe. For example we can implement reals as some kind of Cauchy sequences. For example as programs for functions f, where f(n) is a rational, and |f(n) - f(m)| <= 1/n + 1/m. This works perfectly well. But now Cantor's diagonalization argument clearly does not demonstrate that there are more reals. Instead it demonstrates the limits of what computation can predict about the behavior of other computations.
In other words, I just described a system operating on a notion of truth that is directly tied to the reasoning required to establish that truth. And in that system, uncountable is tied to self-reference. And really doesn't mean more.
I don't know how to really formalize this idea. But I'd be interested if anyone actually has done so.
Mmm, the problem with computable foundations (in my opinion anyway) is that it takes a lot of stuff that is trivial in standard foundations (equivalence relations, basic operations of arithmetic and their laws, quotients, etc) and fills them with subtle logical footguns.
As you say, some view this as a feature, not a flaw. But to my mind mathematics is a tool for dissecting problems with hard formal properties, and for that I'd like the sharpest scalpel I can find.
For me classical foundations strikes a good balance between ease of use and subtlety of reasoning required to get results. I'm not sure the non-constructive and self-referential bits bother me, they don't really get in the way unless you're studying logic (in which case you're interested in computability and other foundations anyway).
> In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?
The way I see it is that an existence of proof isn't required for something to be true. Something being true is a matter of the model, being provable is a matter of axioms and deduction rules. And there comes the distinction between ⊨ and ⊢.
Gödel's incompleteness theorem tells you why it is a good idea to separate semantics (notion of truth) from syntax (reasoning). Because some things are true, although you cannot prove that they are.
Some people now put forward from this the idea that for the natural numbers we know, it is NOT either true or false if for example the twin prime conjecture holds. That is nonsense. It is just that our methods of proof are strictly weaker than our notion of truth is.
That this is so is not even surprising! It is a fact of life that what is true is not necessarily what you can prove to be true. Innocent people imprisoned are an example of that. Guilty people going free another. What is maybe surprising is that what is true in what we perceive as the "real world" is also true in mathematics, which we imagine to be an "ideal realm". But mathematics is ALSO part of the "real world"; if you understand this, it is not so surprising. Yes, I am a platonist, and I think that everybody who isn't is just plain wrong and confused.
Intensional functions are just a special case of extensional functions. Where extensional functions are defined on mathematical objects, intensional functions are extensional functions defined on representations of mathematical objects (which are also mathematical objects, by the way), but pretend to be acting on the mathematical objects themselves, not their representations. That is really all there is to it, it is not a deep philosophical mystery. To do so can of course be very useful!
> there is a single countable list that includes all things that might possibly have any mathematical existence at all.
Help me understand that. Isn't the Cantor diagonialization argument a proof that such a list cannot exist because, supposing it did exist, it could be used to construct an object not on the list? Are you proposing that your list somehow defeats Cantor here?
(Of course, we're using the word "list" loosely here. What we mean is a total function with domain Nat, right?)
> all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.
The universe (in the cosmological sense) can be written down as a single countable list, and anything different would be impossible? Or are you saying that it does not truly exist? I’m not sure how that makes sense.
We can create a countable list that contains every possible description that can ever be created. For example just write down numbers in base ASCII, using a programmable markup language (like TeX) that lets us represent anything that we want. (OK, TeX can only describe shapes down to the wavelength of visible light, but that's good enough for me.)
In what sense does an idea exist when it cannot be described by anything on that list?
To quote an old adage, the map isn’t the territory. That we can’t fully write it down (which we can’t even for countable infinities, or even something like 10^10^10 symbols) doesn’t mean that it doesn’t exist. All of the territory still exists, even if any map that we can draw will only capture certain aspects of it.
Regarding “ideas”, to me math is primarily exploration and discovery, rather than invention. That’s one way how it corresponds to the territory analogy.
My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.
(By internet coincidence, I recently wrote https://math.stackexchange.com/questions/5074503/can-pa-prov... which ends with the beginning of the construction of that list, starting with the Peano axioms. https://news.ycombinator.com/item?id=44269822 is about that answer.)
Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with.
I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it.
All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.