Show that the tree $T$ exists by $\Sigma_0^0$ comprehension

Question

Currently I am reading Simpson's Subsystem of Second Order Arithmetic, Chapter IV Weak Konig Lemma.

Lemma IV.1.1 (Heine/Borel theorem for $[0,1]$). The following is provable in WKL$_0.$ Given a sequence of real numbers $c_i,d_i,i\in\mathbb{N},$ if $$\forall x (0\leq x\leq 1\rightarrow \exists i(c_i<x<d_i) ),$$ then $$\exists n\forall x (0\leq x\leq 1\rightarrow \exists i\leq n(c_i<x<d_i) ),$$

Then the author proceeds to prove it:

Assume that $\langle c_i:i\in\mathbb{N} \rangle$ and $\langle d_i:i\in\mathbb{N} \rangle$ are sequences of rational numbers.

For each $s\in 2^{<\mathbb{N}},$ put $$a_s = \sum_{i<lh(s)}\frac{s(i)}{2^{i+1}}\quad\text{and}\quad b_s = a_s+ \frac{1}{2^{Lh(s)}}.$$

Form a tree $T\subseteq 2^{<\mathbb{N}}$ by putting $s\in T$ if and only if $\neg \exists i\leq lh(s) (c_1<a_s<b_s<d_i).$ $T$ exists by $\Sigma_0^0$ comprehension since $c_i,d_i,a_s,b_s\in\mathbb{Q}.$

I am not able to show that $T$ exists due to $\Sigma_0^0$ comprehension. It would be good if someone can provide a hint.

Answer 1

In the field of reverse mathematics, it is common for authors to write formulas in shorthand, using defined symbols, rather than writing the full formulas in the basic language of second order arithmetic. In particular, symbols such as the relation $<$ on rationals are not part of the basic language, nor is the 'lh' function, so the formula $$\neg \exists i\leq lh(s) (c_1<a_s<b_s<d_i)$$ is not literally a formula of second order arithmetic.

As Derek Elkins wrote in a comment,

The relevance of the parameters being rationals is if they were reals, say, then < would almost certainly expand into some formula that used unbounded quantification somewhere, whereas < for rationals can be encoded without unbounded quantification.

This is the key. As the reader, at this level, you are responsible for translating the shorthand formulas into actual formulas of second-order arithmetic and verifying that the full formulas are of the appropriate syntactic forms. The author may give some general guidance, but unless the translation is especially tricky it is unlikely the author will carry it out explicitly.

In this case, by looking back to the definition of rationals in the book, you will see that no additional quantifiers are needed. The more challenging issue in this case is the 'lh' function and the subscripts, which will lead to additional bounded quantifiers in the full formula.

This is no different, for example, than an analysis paper that carries out somewhat complicated integrals without explanation, or a combinatorics paper that simplifies complicated inequalities.