How many real numbers exist? New proof moves closer to an answer

It's an established result that the Continuum Hypothesis is independent of Zermelo–Fraenkel axioms of set theory. No proof is going change that.

So whatever has been proved here doesn't change that. It will take a second to get the reference but Raymond Smullyan says essentially that "we're not looking for a proof or disproof of CH, we're looking for an assumption that can be shown to be natural enough that we can take it as an axiom".

Just sayin' since the (subheading) writer seems to be playing fast and loose with the concepts involved.

Edit: article goes on to give rigorous explanation but still starting "no one knew" confuses what's going on.

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?

Golf clap on how amazingly effective that was.

I don’t see why that should imply it wouldn't be "okay" to add ¬Con(ZFC).

It may be highly counterintuitive, but the history of mathematics is full of counterintuitive results that nowadays are accepted as true in mainstream mathematics.

Well-known examples are the existence of irrational numbers, the claim that the set of natural numbers has the same size as that of the rational numbers, the existence of hyperbolic geometry, and the Banach-Tarski paradox.