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$)?

  • 1
    $\begingroup$ This is $L\Sigma^0_1$, which is equivalent to $I\Sigma^0_1$, which is included in $\mathrm{RCA}_0$ by definition. $\endgroup$ Apr 13 at 6:10
  • $\begingroup$ @EmilJeřábek: do you have a reference for the equivalence? I couldn't find it in Simpson's book or online. $\endgroup$ Apr 13 at 6:41
  • 2
    $\begingroup$ @JordanMitchellBarrett I think this isn't that hard to show directly, but if you want a reference this is Theorem 2.4 in "Metamathematics of First-Order Arithmetic" by Hájek and Pudlák. $\endgroup$ Apr 13 at 7:10
  • $\begingroup$ I'll have a look at that. If you have a direct proof, I'd love to see it. $\endgroup$ Apr 13 at 7:31
  • $\begingroup$ So a kind of minimization principle can be found in SOSOA: II.3.5 on page 70. I think this answers your question. $\endgroup$ Apr 13 at 17:43

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.