Arithmetic comprehension

(1 ⇒ 2), (2 ⇒ 3) and (2 ⇒ 4) are instances of comprehension: the jump and the range $\{ m : \exists i\ f(i) = m \}$ are defined by $\Sigma^0_1$ formulas.

(4 ⇒ 2) Let $\varphi(n) \equiv \exists k\, \theta(n, k)$ with $\theta$ bounded, possibly with parameters. Let $f(\langle n, k \rangle) = 2n + 1$ if $\theta(n, k)$ holds and no $k' < k$ satisfies $\theta(n, k')$, and $f(\langle n, k \rangle) = 2 \langle n, k \rangle$ otherwise. The function $f$ exists by $\Delta^0_1$ comprehension, and it is injective: an odd value $2n+1$ is taken at most once, at the least witness $k$, and an even value $2\langle n, k \rangle$ at most once. Its range $R$ exists by (4), and $\{ n : \varphi(n) \} = \{ n : 2n + 1 \in R \}$ exists by $\Delta^0_1$ comprehension.

(3 ⇒ 2) Let $\varphi(n)$ be $\Sigma^0_1$ with set parameters $A_1, \dots, A_k$, and $A = A_1 \oplus \cdots \oplus A_k$. By the formalized $s$-$m$-$n$ theorem, there is a primitive recursive $h$ such that $\Phi^A_{h(n)}(h(n))\converge$ if and only if $\varphi(n)$; so $\{ n : \varphi(n) \} = \{ n : h(n) \in A' \}$, which exists by $\Delta^0_1$ comprehension relative to $A'$.

(2 ⇒ 1) We show by induction on $m$ in the metatheory that $\Sigma^0_1$ comprehension proves $\Sigma^0_m$ comprehension. Let $\varphi(n) \equiv \exists k\, \psi(n, k)$ with $\psi$ a $\Pi^0_{m}$ formula. By $\Sigma^0_m$ comprehension applied to $\neg \psi$, which is equivalent to a $\Sigma^0_m$ formula, the set $Y = \{ \langle n, k \rangle : \neg \psi(n, k) \}$ exists. Then $\{ n : \varphi(n) \} = \{ n : \exists k\, \langle n, k \rangle \notin Y \}$ exists by $\Sigma^0_1$ comprehension with parameter $Y$. Every arithmetic formula is equivalent to a $\Sigma^0_m$ formula for some $m$, by the prenex normal form.

By Friedman and Theorem 1.2 (3), using absoluteness: $Y$ is the jump of $X$ in the model if and only if $Y = X'$. A jump ideal contains $\emptyset^{(n)}$ for every $n$, hence every arithmetic set, and $\mathrm{ARITH}$ is a jump ideal by Post’s theorem (Post).

($\Rightarrow$) Rescaling, we may assume $0 \leq x_n \leq 1$. By arithmetic comprehension, the set $S$ of rationals $q$ such that $x_n > q$ for some $n$ exists. For each $k$, let $q_k$ be the largest number of the form $j 2^{-k}$, with $-1 \leq j \leq 2^k$, that belongs to $S$; it exists since $-2^{-k} < x_0$, and the sequence $(q_k)$ exists by $\Delta^0_1$ comprehension relative to $S$. Some $x_n$ exceeds $q_k$, and no $x_n$ exceeds $q_k + 2^{-k}$: either $q_k + 2^{-k} \notin S$, or $q_k = 1$. For $k \leq l$, $q_k \leq q_l$, since $q_k$ is also of the form $j 2^{-l}$, and $q_l < q_k + 2^{-k}$, since some $x_n$ exceeds $q_l$. So $x = (q_k)$ is a real, with $q_k \leq x \leq q_k + 2^{-k}$. It is the limit: every $x_n$ satisfies $x_n \leq q_k + 2^{-k} \leq x + 2^{-k}$ for all $k$, hence $x_n \leq x$; and for each $k$ some $x_n > q_k \geq x - 2^{-k}$, so $x - x_m < 2^{-k}$ for all $m \geq n$, since the sequence is non-decreasing.

($\Leftarrow$) We prove (4) of Theorem 1.2. Let $f$ be injective, and $x_n = \sum_{i \leq n} 2^{-f(i)-1}$, as in Specker. It is non-decreasing and bounded by $1$; let $x$ be its limit. For each $m$, there is $n$ with $x - x_n < 2^{-m-1}$, and then $m$ is in the range of $f$ if and only if $m = f(i)$ for some $i \leq n$: an $i > n$ with $f(i) = m$ would give $x - x_n \geq x_i - x_n \geq 2^{-m-1}$. The condition $x - x_n < 2^{-m-1}$ is $\Sigma^0_1$ in $x$ and $(x_n)$. Hence

two $\Sigma^0_1$ formulas. In both lines, the left-to-right direction holds with any $n$ such that $x - x_n < 2^{-m-1}$, by the observation above for the first line; the right-to-left direction is immediate for the first line and is the observation above for the second. So the range exists by $\Delta^0_1$ comprehension.

($\Rightarrow$) Let $T$ be infinite and finitely branching. By arithmetic comprehension, the set $E$ of nodes of $T$ with infinitely many extensions in $T$ exists. The root belongs to $E$. If $\sigma \in E$, one of its finitely many immediate successors belongs to $E$: otherwise each of them has finitely many extensions, and so would $\sigma$, by arithmetic induction on the number of successors. Define the path $P$ by $P \uh 0 = \varepsilon$ and $P \uh (n+1) =$ the first immediate successor of $P \uh n$ in $E$, in the order of codes; this is a search relative to $T \oplus E$ that terminates, so $P$ exists by $\Delta^0_1$ comprehension.

($\Leftarrow$) We prove (4) of Theorem 1.2. Let $f$ be injective. Let $T$ be the set of sequences $\sigma \in \nat^{<\nat}$ such that, for every $m < |\sigma|$, either $\sigma(m) = i + 1$ with $f(i) = m$, or $\sigma(m) = 0$ and $f(i) \neq m$ for every $i < |\sigma|$. It is a tree, defined by a bounded formula, and each node has at most two immediate successors, since $f$ is injective. It is infinite: for each $n$, the sequence $\sigma$ of length $n$ with $\sigma(m) = i + 1$ if $f(i) = m$ for some $i < n$, and $\sigma(m) = 0$ otherwise, belongs to $T$. Let $P$ be a path. If $P(m) = i + 1$, then $f(i) = m$. If $P(m) = 0$, then $f(i) \neq m$ for every $i$, since $P \uh n \in T$ for every $n > i$. So $\mathrm{ran}(f) = \{ m : P(m) \neq 0 \}$, which exists by $\Delta^0_1$ comprehension.