[scapp]

You sound like you need to read this [0] answer to the question "Are real numbers countable in constructive mathematics?".

> You are using the word "constructive" in an unusual way. It is true that, in ZFC, the set of computable real numbers is countable, but that is not directly a statement about constructive mathematics.

> Not every school of constructive mathematics identifies real numbers with algorithms; that's a characteristic of the "Russian" school as I understand it. In other schools of constructivism that I am more familiar with, real numbers are coded by elements of 2^ω, or by a certain type of Dedekind cut on the rationals. In such schools it is not universally assumed that every real number is associated with a finite algorithm.

> Even in the Russian school, they would not say that the set of real numbers is countable. Because, if you identify real numbers with algorithms, there is no computable enumeration of computable reals that lists all computable reals, and so the translation of "the real numbers are countable" into this setting is false.

> That phenomenon also occurs in classical computable analysis. The subsystem RCA0 of second-order arithmetic has a model in which every real number is computable. But this subsystem still proves that there is no surjection N -> R.

---

It's worth noting that another answer to that question (Andrej Bauer's) gives a constructive proof that the real numbers are uncountable using with the axiom of countable choice. The question of whether it's provable without the axiom of countable choice is open (though see this [1] fairly recent paper on a proof for MacNeille reals).

[0] https://mathoverflow.net/questions/30643/are-real-numbers-co...

[1] https://arxiv.org/abs/1902.07366

[btilly]

Yes, there are multiple constructivist approaches possible. However since my objection to classical approaches is that I want "X exists" to be meaningful, I like mathematical objects that can be written down with a finite number of symbols in a finite space. Which means that I'm only interested in a countable universe of possible mathematical things.

If you say "exists" about anything else, I'll understand you - I do have advanced degrees in math. But I'll think that you're using the word "exists" in a deeply artificial way.

[pdonis]

> I like mathematical objects that can be written down with a finite number of symbols in a finite space.

Which is fine, but I don't think it justifies the claim that there are only countably many real numbers. The only claim it justifies is that there are only a finite (not even countable, since "countable" implies infinitely many) set of numbers that you find useful.

[papandada]

Every integer can be written down with a finite number of symbols....right?

[LudwigNagasena]

What’s the problem with it being “artificial”? Is your problem purely linguistic? You just dislike the word “exists” being used in this context?

[btilly]

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?

[pdonis]

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.

[ummonk]

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).

[papandada]

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.

[btilly]

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.

[LudwigNagasena]

In the usual sense. I don’t see a problem. Just because you don’t have a perfect knowledge of something, it doesn’t mean that the thing isn’t real.

I am not sure where this idea even comes from? To be honest, this sounds completely ridiculous.

[ummonk]

> That phenomenon also occurs in classical computable analysis. The subsystem RCA0 of second-order arithmetic has a model in which every real number is computable. But this subsystem still proves that there is no surjection N -> R.

Huh? It's trivial to create an injection R -> N, by encoding each computational algorithm - whether valid or invalid - as a number.