Justify the existence of a set by using $\Delta_1^0$ comprehension

Question

Here, page $9$, in the proof of Theorem $I.5$, there is this sentence

$$X_k=\{ m | (m \geq k+2) \wedge (b_{m,m} - a_{m,m} \leq 2^{-k+2}) \}$$

exists by $\Delta_1^0$ comprehension.

Question: Why the set exists by $\Delta_1^0$ comprehension? How to express the set $X_k$ using quantifier $\forall$ or $\exists$?

Answer 1

This is the sort of thing that is, on one hand, often routine once you understand it, and, on the other hand, too long to actually write out by hand. To work in Reverse Mathematics, you need to develop a feel for which formulas will be expressible in a $\Delta^0_1$ manner.

The rule of thumb is to rely on Church's thesis: if the definition would be computably decidable in the standard model, it is likely going to fit into the $\Delta^0_1$ comprehension scheme. The formal verification of this for a particular definition requires expanding out the definition into smaller pieces until it is obvious that each piece can be expressed in the appropriate way.

Working formally, the first stage of this expansion gives these two formulas: $$ \begin{split} \phi(m) \equiv & m \geq k + 2 \\ &\land (\forall x)(\forall y)(\forall z)(\forall z)[x = b_{m,m} \land y = a_{m,m} \land z = 2^{-k+2} \to x - y < z] \end{split} $$ and $$ \begin{split} \phi(m) \equiv & m \geq k + 2 \\ & \land (\exists x)(\exists y)(\exists z)[y = b_{m,m} \land y = a_{m,m} \land z = 2^{-k+2} \land x - y < z] \end{split}$$ Here

• $x = b_{m,m}$ is the formula that says the ordered pair $((m,m),x)$ is in $b$
• $y = a_{m,m}$ is a formula that says that the ordered pair $((m,m),y)$ is in $a$
• $z = 2^{-k+2}$ is a formula that says $z = 2^{-k+2}$. The most straightforward way to handle $z$ is to show that there exists a set $P = \{ (k, 2^{-k+2}) : k \in \mathbb{N}\}$, and then use this set as a parameter in the comprehension scheme, so $z = 2^{-k+2}$ can be an abbreviation for $(k,z) \in P$.

Actually, the formulas above are still abbreviations, because $x$ and $y$ are supposed to be rational numbers. So, in the second phase of the expansion, we would replace the quantifier for $x$ with two natural number quantifiers, one for the numerator and one for the denominator, and similarly for $y$. Then the formula $x - y < z$ will be replaced with a more complicated formula using only natural number variables. However, the formulas above indicate to me that it is possible to express the desired definition in a $\Delta^0_1$ manner, which is the goal of the proof, so I will leave the rest of the expansion to someone else.