Can $\mathsf{RCA}_0$ prove that every nonempty c.e. set $A \subseteq \mathbb{N}$ has a least element?

Question

In other words, can $\mathsf{RCA}_0$ prove that for every function $f\colon \mathbb{N} \to \mathbb{N}$, there is $b \in \mathbb{N}$ such that

$$ \exists k \in \mathbb{N},\ f(k) = b\quad \land\quad \forall j \in \mathbb{N},\ f(j) \geq b $$

If so, is there a reference to this result? If not, is this result known to be provable/equivalent over $\mathsf{RCA}_0$ to another subsystem of SOA, and is there a reference for this?

---

More generally (this is more than I need, but out of interest), we could consider the principles $\mathsf{L}\Sigma^i_n$, $\mathsf{L}\Pi^i_n$, $\mathsf{L}\Delta^i_n$ which say that every $\Sigma^i_n$ / $\Pi^i_n$ / $\Delta^i_n$ definable subset of $\mathbb{N}$ has a least element. Where do these fall in the reverse mathematical hierarchy? Is anything known (even for $i=0$)?

Answer 1

As Emil Jeřábek and James Hanson mentioned in comments, this is well-known in the literature of first-order arithmetic as the $\Sigma_1$ least number principle, $\mathsf{L}\Sigma_1$. Simpson doesn't mention it in his book (he doesn't really talk about $\Sigma_n$ bounding either, which is more well known).

Over $\mathsf{PA}^- + \mathsf{I}\Sigma_0$, Kirby and Paris [1] proved that $\mathsf{L}\Sigma_n$, $\mathsf{L}\Pi_n$, $\mathsf{I}\Sigma_n$, $\mathsf{I}\Pi_n$ are all equivalent.

Over $\mathsf{PA}^- + \mathsf{I}\Sigma_0 + \mathsf{exp}$, Slaman [2] proved (building on results of Kirby and Paris) that $\mathsf{L}\Delta_n$, $\mathsf{I}\Delta_n$, $\mathsf{B}\Sigma_n$, are all equivalent.

Both reversals hold over $\mathsf{RCA}_0$, since it proves $\mathsf{PA}^- + \mathsf{I}\Sigma_0 + \mathsf{exp}$. In particular, $\mathsf{L}\Sigma_1$ holds in $\mathsf{RCA}_0$ (as Emil Jeřábek mentioned).

---

[1] L. A. S. Kirby and J. B. Paris. $\Sigma_n$-collection schemas in arithmetic. Angus Macintyre, Leszek Pacholski, Jeff Paris (eds.), Logic Colloquium '77 (proceedings of colloquium held in Wrocław, August 1977). Studies in Logic and the Foundations of Mathematics 96, pp. 199-209. Elsevier North-Holland, NY, 1978.

[2] Theodore A. Slaman. $\Sigma_n$-bounding and $\Delta_n$-induction. Proceedings of the American Mathematical Society 132(8), pp. 2449-2456, 2004.