Return to Answer

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct modulo any typos. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then defining the inverse of $f$ on this set, and then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?)

Let $E$ be the set of even numbers. By the Union Principle, there is a set $I$ such that $E = \bigcup_{(i,j) \in I} S_{(i,j)}$. Note that if $(i,j) \in I$ then $S_{(i,j)} = \{2i\}$. Also note that for every $i$ there is at least one $j$ such that $(i,j) \in I$. Given $i$, let $h(i)$ be the first $j$ such that $(i,j) \in I$. Since $$(\exists k)(f(k) = \ell) \iff (\exists k < h(\ell+1))(f(k) = \ell)$$ we can define the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?) In general, the "bounding principle" for a class of formulas $\Gamma$ says that the image of a bounded set of numbers under a $\Gamma$-definable function is bounded.

Let $E$ be the set of even numbers. By the Union Principle, there is a set $I$ such that $E = \bigcup_{(i,j) \in I} S_{(i,j)}$. Note that if $(i,j) \in I$ then $S_{(i,j)} = \{2i\}$. Also note that for every $i$ there is at least one $j$ such that $(i,j) \in I$. Given $i$, let $h(i)$ be the first $j$ such that $(i,j) \in I$. Since $$(\exists k)(f(k) = \ell) \iff (\exists k < h(\ell+1))(f(k) = \ell)$$ we can define the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct modulo any typos. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then defining the inverse of $f$ on this set, and then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?)

Let $E$ be the set of even numbers. Because $E = \bigcup_{(i,j)} S_{(i,j)}$, using the union principle we can find sequence $(i, j_i)$ such that $S_{(i,j_i)} = \{2i\}$. Then we have, for any $l$, $(\exists k)(f(k) = l) \leftrightarrow (\exists k < j_{l+1})(f(k) = l)$, and so we have a definition of the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct modulo any typos. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then defining the inverse of $f$ on this set, and then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?)

Let $E$ be the set of even numbers. By the Union Principle, there is a set $I$ such that $E = \bigcup_{(i,j) \in I} S_{(i,j)}$. Note that if $(i,j) \in I$ then $S_{(i,j)} = \{2i\}$. Also note that for every $i$ there is at least one $j$ such that $(i,j) \in I$. Given $i$, let $h(i)$ be the first $j$ such that $(i,j) \in I$. Since $$(\exists k)(f(k) = \ell) \iff (\exists k < h(\ell+1))(f(k) = \ell)$$ we can define the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct modulo any typos. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded requires an argument using $\Sigma^0_1$ induction on the formula $\psi(i) \equiv (\exists j)(\forall r)(\forall k < i)(f(r) = k \to k < j)$.

Let $E$ be the set of even numbers. Because $E = \bigcup_{(i,j)} S_{(i,j)}$, using the union principle we can find sequence $(i, j_i)$ such that $S_{(i,j_i)} = \{2i\}$. Then we have, for any $l$, $(\exists k)(f(k) = l) \leftrightarrow (\exists k < j_{l+1})(f(k) = l)$, and so we have a definition of the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct modulo any typos. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then defining the inverse of $f$ on this set, and then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?)

Let $E$ be the set of even numbers. Because $E = \bigcup_{(i,j)} S_{(i,j)}$, using the union principle we can find sequence $(i, j_i)$ such that $S_{(i,j_i)} = \{2i\}$. Then we have, for any $l$, $(\exists k)(f(k) = l) \leftrightarrow (\exists k < j_{l+1})(f(k) = l)$, and so we have a definition of the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.