The problem is that exists comes to mean something technical that doesn't match common usage.
Let's take my favorite example.
In graph theory, a minor of a graph is a graph you can get by removing vertices, removing edges, or by replacing an edge-vertex-edge triple with a single edge. Many categories of graphs are closed under the act of taking minors. For example planar graphs, graphs you can draw on the plane with no crossings, are.
The category of planar graphs is entirely described by the fact that any graph that isn't planar must have either K5 or K3,3 as minors. That is, a graph with 5 vertices, all connected. Or a graph with 2 groups of 3 vertices, that all connect to each other. Therefore we call those two graphs the "forbidden minors" for planar graphs.
The Robertson–Seymour theorem says that any category of graphs which is closed under graph minors has a similar description. There is a finite list of forbidden minors which, if none are minors of a given graph, then that graph is in the category.
Since there is a polynomial time algorithm to detect whether a given graph is a minor of another, this immediately means any category of graphs closed under taking minors must have a polynomial time algorithm to test for membership. Just test each forbidden minor.
So far this is straightforward, but here is where things get weird.
The first catch is that the Robertson–Seymour theorem is non-constructive. That is, it says that the list exists and is finite. But it does not bound the number. It does not give us a way to find those minors. It does not give us any way to determine whether we have a complete list. For example we know of thousands of minimal forbidden minors for graphs that can be drawn on a torus, and do not know if our list is complete.
The second catch is that we know that none of those things are possible to do. That is, there are collections of categories of such graphs such that we can prove that no algorithm can bound the number, no algorithm can search for those examples, and no algorithm can verify that a list of forbidden minors is complete.
In what sense does a finite thing that is unfindable, unverifiable, and of unknowable size actually exist? And, if you think that it exists, in what sense is something of unboundable size actually finite?
These concerns don't apply to the claim that the set of real numbers is uncountable. Cantor's diagonal proof is constructive: given any countable set of real numbers, it tells you how to construct a real number that is not in the set. That is sufficient to show that the set of real numbers cannot be countable. Also, even though many real numbers cannot be written down with a finite set of symbols, Cantor's diagonal proof can be.
You're assuming you've been able to construct all those real numbers in the first place, using arbitrary imaginary cauchy sequences (i.e. cauchy sequences that cannot be constructed but rather rely on some magic axiom of infinite choice).
Such an interesting criticism. All of this thread has been enlightening. I sat through traditional undergrad analysis and set theory classes and never imagined there was another option, other than things bothering me for decades since in my subconscious.
Yes, you can write down Cantor's diagonal proof. But if you're careful about it, you find that the diagonalized thing is not a real number. For example a program to list programs that can be proven (by some set of axioms) to create Cauchy sequences can be used to create a Cauchy sequence, but you can't prove that that sequence is a Cauchy sequence without running into Gödel's incompleteness theorem.
Let's take my favorite example.
In graph theory, a minor of a graph is a graph you can get by removing vertices, removing edges, or by replacing an edge-vertex-edge triple with a single edge. Many categories of graphs are closed under the act of taking minors. For example planar graphs, graphs you can draw on the plane with no crossings, are.
The category of planar graphs is entirely described by the fact that any graph that isn't planar must have either K5 or K3,3 as minors. That is, a graph with 5 vertices, all connected. Or a graph with 2 groups of 3 vertices, that all connect to each other. Therefore we call those two graphs the "forbidden minors" for planar graphs.
The Robertson–Seymour theorem says that any category of graphs which is closed under graph minors has a similar description. There is a finite list of forbidden minors which, if none are minors of a given graph, then that graph is in the category.
Since there is a polynomial time algorithm to detect whether a given graph is a minor of another, this immediately means any category of graphs closed under taking minors must have a polynomial time algorithm to test for membership. Just test each forbidden minor.
So far this is straightforward, but here is where things get weird.
The first catch is that the Robertson–Seymour theorem is non-constructive. That is, it says that the list exists and is finite. But it does not bound the number. It does not give us a way to find those minors. It does not give us any way to determine whether we have a complete list. For example we know of thousands of minimal forbidden minors for graphs that can be drawn on a torus, and do not know if our list is complete.
The second catch is that we know that none of those things are possible to do. That is, there are collections of categories of such graphs such that we can prove that no algorithm can bound the number, no algorithm can search for those examples, and no algorithm can verify that a list of forbidden minors is complete.
In what sense does a finite thing that is unfindable, unverifiable, and of unknowable size actually exist? And, if you think that it exists, in what sense is something of unboundable size actually finite?