The procedure used within Cantor's diagonalization proof depends on a sequence of choices, each of which is based on whether something is absolutely true, even

The procedure used within Cantor's diagonalization proof depends on a sequence of choices, each of which is based on whether something is absolutely true, even though that truth cannot necessarily be established by any finite set of reasoning from a finite set of axioms. Actually doing this requires making decisions based on absolute truth. The procedure could never be done in practice because there is no reasoning process available in first order logic that can always determine absolute truth. In fact even being able to determine the absolute truth of whether our current axioms are consistent would imply a contradiction. (Thanks, Gödel.) Whether it makes any sense to talk about such constructions at all was the heart of the Formalist vs Constructivist debate about "the law of the excluded middle". The formal first order proofs from ZFC that you mention depend on the axioms of ZFC. Which in turn are assumed. What is actually proven is, "If these are true, then that is the conclusion." But the axioms must be assumed. What is proven is that the axioms lead to the conclusion. And not that the axioms are true or the conclusion matches our naive notions of truth or existence. As to that, a Constructivist can't even get through the first axiom of ZFC before finding problems to question. The axiom of extensionality says that two sets are equal if and only if they have the same elements. In classical mathematics, elements either are or are not in the set. And two sets either do or don't have the same elements. And we can build procedures based on that truth. But such statements based on absolute truth might not be able to be established through any reasoning process. Procedures requiring decisions made on such absolute truths cannot actually be performed. In what way can we establish existence by constructions involving impossible procedures based on information that no reasoning process can ever verify. I will make this problem concrete. Let's let A be the empty set. And B be the set of non-trivial zeros of the Riemann zeta function. According to classical mathematics, either ZFC may prove that A = B, it may prove that A is not B, or the question may be undecidable. If the question is undecidable, then through https://en.wikipedia.org/wiki/Second-order_arithmetic https://en.wikipedia.org/wiki/Second-order_arithmetic you can prove that A = B. (The principle of the proof is the same as how Gödel proved that if ZF is consistent, then so is ZFC.) Classical mathematicians happily accept that claim, even though it rests on a statement that might be true without any possibility of proof. And, furthermore, classical mathematicians will happily accept proofs based on constructions that require an infinite number of decisions that are similarly impossible to make through any form of first-order logic. Constructivism collapses all of that. In that philosophy, we can't talk about the truth of any statement unless a proof as been found for or against it. Procedures may not depend on the impossible task of deciding the undecidable. Nor can we sneak such assumptions in through things like the axiom of extensionality. Which makes the classical proof just pointless symbol manipulation that implies nothing about what does or doesn't exist. Here is the Constructivist view. If we assume things that make no sense, we conclude things that also make no sense. Rather than trying to understand the nonsensical conclusion, we should avoid the nonsensical assumption. There aren't an uncountable number of real numbers who can never be defined, even in principle, in any finite way. Mathematical things that can't be defined, simply don't exist. This view only seems strange to us because it is impossible to study higher mathematics without being indoctrinated into the classical mathematical approach. It is only after learning to think outside of that box that you start to realize how arbitrary the implicit assumptions are.