There are countably many real numbers, and both options are equivalent.

@Mira There may be ℵ₁ many, but it's provable that there aren't countably many.

@JosephNoonan It's also provable that there can be countably many: Downward Lowenheim-Skolem theorem.

@Mira That's not an accurate statement of the Lowenheim-Skolem theorem. All it proves is that there are models of set theory with only countably many real numbers. But within those models, the set of real numbers is still uncountable because the bijection between the model's real numbers and the natural numbers doesn't exist in the model. There's still no way to consistently claim that there are countably many real numbers, unless you reject so much of set theory that it's impossible to even prove Cantor's theorem.

@JosephNoonan The only mathematical objects that exist are the computable ones. Most real numbers aren't computable, so they don't exist. Cantor's argument requires a halting oracle to decide the indices of each real number. The real numbers are defined as the computably-equivalent computer programs that generate a stream of binary digits. You can enumerate "all possible computer programs", but the action of subsetting them to the "programs that emit a stream of binary digits" requires reasoning about the infinite behavior of programs, which is related to the halting problem.

The set of computable real numbers is not in computable bijection with the set of natural numbers, but is still a subset of a countable set.

@Mira Okay, so you are just defining "real numbers" in a non-standard way.

@JosephNoonan I'm working with the same definition of real numbers. It's a first-order theory and the axioms are the same in both cases.

Logics are search algorithms; proofs are search-certificates. You seem to be using a proof-erasing logic, and then getting confused when the proofs are needed to separate the Turing Degree of the objects you're working with.

@Mira You're explicitly only defining the real numbers as the computable real numbers. That's not the standard definition.

Regardless, if you only consider computable objects to be real, then you can't say the real numbers are countable anyway, since there's no computable bijection from the computable reals to the natural numbers. You can only say that your model is countable if you're looking at it from the perspective of a larger model that does include a bijection between the natural numbers and the computable reals, in which case it's not true that the only mathematical objects that exist are computable ones. And that model would also necessarily have noncomputable reals in it, in which case your model of the real numbers isn't countable after all.

@Mira I'm giving your comment a like, not because I agree, but because I appreciate the commitment to the bit.