Can we give an equivalent definition for computable numbers without mentioning turing machines?

Question

Let $\mathbb{R}$ be the set of all real numbers, as defined by dedekind cuts. Given $\mathbb{R}\subset\mathscr{P}(\mathbb{Q})$, and we have a construction of $\mathbb{Q}$ as as a set of equivalence classes on $\mathbb{Z}$ which is itself a set of equivalence classes on $\mathbb{N}$ and of course we can take $\mathbb{N}$ to be the set of finite von neumann ordinals, which means that $\mathbb{R}$ is a genuine set that exists in any model of ZF. Lets define the set of 'provable real numbers' $\mathbb{R}_p$ in some second order meta theory, to be the set of all sets which are real numbers, and are sets in every model of ZF. So we know that $\mathbb{R}_p$ is going to be countable, my question however is: Is $\mathbb{R}_p$ at all related to the set of all computable real numbers? Is it equivalent to, a subset of, or a super set of the set of computable real numbers? or is it none of those?

Answer 1

Unfortunately this is one of those situations where a very natural question has a surprisingly technical answer. Right now I'm erring on the side of concision, but let me know if there's a particular point you'd like me to expand on. Some points however really can't be treated elementarily - e.g. the proof that $\mathsf{HYP}$ is an upper bound for $\mathbb{R}_p$ really requires some work.

---

It takes a bit of work to make your notion of $\mathbb{R}_p$ fully precise. I think the following definition captures your intuition, however:

Let $\mathbb{R}_p$ be the set of reals whose corresponding Dedekind cuts are in every $\omega$-model of $\mathsf{ZF}$.

(To make this nontrivial we assume that $\mathsf{ZF}$ does in fact have $\omega$-models.)

An $\omega$-model of $\mathsf{ZF}$ is a model which is "correct about $\omega$:" all the things that model thinks are finite are actually finite. By the compactness theorem, not all models are $\omega$-models, and in non-$\omega$-models we have "nonstandard rational numbers" which makes the definition of $\mathbb{R}_p$ no longer clear.

The key here is absoluteness: there are certain facts which all $\omega$-models are correct about, and so any real defined entirely in terms of those facts will be in $\mathbb{R}_p$. For example, all computable reals are in $\mathbb{R}_p$ since Turing machine computations are ultimately just statements about natural numbers, and all $\omega$-models agree on what the natural numbers look like. But this immediately pushes us far beyond the computable: for the same reason we get all the arithmetic reals such as the (highly non-computable) Chaitin's $\Omega$, and with a bit of thought we get the hyperarithmetic reals as well. A general argument (which is unfortunately a bit technical) also establishes the set of hyperarithmetic reals as an upper bound, so in fact we get exactly that $\mathbb{R}_p$ is the set of hyperarithmetic reals.

Incidentally, this characterization is extremely robust. For any set theory $T$ we can similarly define $\mathbb{R}_p^T$ to be the set of reals in every $\omega$-model of $T$. It turns out that basically any reasonable $T$ will yield $\mathbb{R}_p^T=\mathsf{HYP}$ as above, for the same reason: as long as $T$ has $\omega$-models in the first place, is reasonably simple (= hyperarithmetically axiomatizable), and can prove basic facts about the Turing jump operation, the argument hinted at above goes through. So for example we can add choice, or large cardinals, or drop all the way down to something like $\mathsf{KP}$, and we won't change the answer.

---

You mention in the comments the possibility of shifting to a more "proof-theoretic" notion, of the real numbers which "provably exist." Here we run into a serious problem:

What does it mean for $\mathsf{ZF}$ to prove that a real number $r$ exists?

The problem is that it only makes sense to ask whether $\mathsf{ZF}$ proves a sentence in the language of set theory. So to even ask whether $\mathsf{ZF}$ proves "$r$ exists," we need to already have some fixed definition of $r$ in the language of set theory. This motivates the following definition:

Let $\mathbb{R}_{named}$ be the set of reals of the form $\varphi^V$, for $\varphi$ a formula which $\mathsf{ZF}$ proves defines some real number.

Here "$\varphi^V$" is the interpretation of $\varphi$ in the set-theoretic univere $V$: that is, the thing $\varphi$ actually names.

The problem is that this is highly undetermined. For example, and shifting attention to binary sequences for simplicity, let $c:\mathbb{N}\rightarrow\{0,1\}$ be the continuum pattern: $$c(n)=1\quad\iff\quad 2^{\aleph_{2n}}=\aleph_{2n+1}.$$ Obviously $\mathsf{ZF}$ proves that $c$ exists, but Easton's theorem says that $\mathsf{ZF}$ can't prove any particular facts about $c$! As far as $\mathsf{ZF}$ knows, $c$ could be any sequence whatsoever.

(Moreover, $\mathbb{R}_{named}$ can't even be defined in set theory per Tarski, unlike $\mathbb{R}_p$. So the "models-only" definition is actually much better behaved.)

---

EDIT: Let me say a bit more about the proof that $\mathbb{R}_p\subseteq \mathsf{HYP}$ that I alluded to above. The real result being proved is:

Suppose $r$ is a non-hyperarithmetic real. Then there is a countable $\omega$-model of $\mathsf{ZFC}$ not containing $r$.

Note the restriction to countable models. This is a situation where strengthening the goal makes the result easier to prove: countable structures live in the realm of descriptive set theory, and we can use powerful tools there.

Basically, we look at the relations $R\subseteq\mathbb{N}^2$ such that $(\mathbb{N};R)$ is a (necessarily countable) $\omega$-model of $\mathsf{ZFC}$. The set of all binary relations on $\mathbb{N}$ whatsoever is naturally viewed as a topological space (indeed, one homeomorphic to the Cantor space), and the set $\mathfrak{X}$ of relations representing $\omega$-models of $\mathsf{ZFC}$ is $\Sigma^1_1$ in the sense of that space. A result of Gandy says that for every non-hyperarithmetic real $r$, any nonempty $\Sigma^1_1$ set has an element $s$ to which $r$ is not hyperarithmetically reducible. Now the point is this: if $R\in\mathfrak{X}$ and $r$ is a real in the model represented by $R$ in the appropriate sense, we can "read off" $r$ from the relation $R$ itself - precisely, we have that $r$ is hyperarithmetic relative to $R$ (in fact we can strengthen that to "computable relative to," but that takes a bit of thought). This means that we can apply Gandy to get the result stated above.

(Actually, Gandy's result is even stronger: see Gandy's basis theorem. But we only need the "cone-avoiding" aspect of it here.)

Now this really is a technical argument: not only have I not even remotely sketched how to prove Gandy's result, I also haven't defined "$\Sigma^1_1$." But I think the above is still worth writing down, if only to motivate the blackboxed bits by demonstrating how they can be used.