Equivalences between statements of (seemingly) different order

Question

In Steve Simpson's excellent monograph SOSOA, we find Theorem X.4.4 which contains an equivalence (over RCA$_0^*$) between the following statements:

1. The induction axiom for $\Sigma_1^0$-formulas (with set parameters, of course).

2. For every countable field $K$, every polynomial $f(x)$ in $K[x]$ has only finitely many roots in $K$.

Such equivalences seem rare as they involve a first-order statement (with set parameters) and a 'truly' second-order statement. My question is then as follows:

Are there more equivalences of this kind, i.e. between first-order statements (with set parameters) and 'truly' second-order ones?

I also welcome criticism of my premise, i.e. perhaps 2) is deemed not 'truly' second-order by all? Perhaps there is a philosophy of math angle too/even?

Answer 1

When we say "with set parameters" I take it that what we really mean is something of the form: the axioms of (e.g.) the $\Sigma^0_1$ induction scheme are the universal closures of all formulas of the form $$(\varphi(0) \wedge \forall{n}\varphi(n) \rightarrow \varphi(n+1)) \rightarrow \forall{n}\varphi(n),$$ where $\varphi$ is $\Sigma^0_1$ and may contain free number and set variables—in other words, a set of $\Pi^1_1$ statements.

This muddies the waters somewhat, since e.g. statements asserting that some computable linear order is a well-ordering are also $\Pi^1_1$. For example, $\mathrm{WO}(\omega^\omega)$ is equivalent to Hilbert's basis theorem (Simpson 1988). These sorts of statements (perhaps) don't have quite the same 'feeling' as the example Sam gives.

Another philosophical issue relates to the fact that, according to Simpson, induction schemes like $\mathrm{I}\Sigma^0_1$ are set existence principles, in virtue of their equivalence to bounded comprehension schemes (remark II.3.11 in SoSOA). This is important in light of the view that reverse mathematics is about determining which set existence principles are necessary in order to prove a given theorem. I push back against Simpson's views on induction schemes a bit in a 2019 paper (see particularly pages 171–172), in the context of a more general inquiry into whether this is a good way of understanding RM.

Other examples in the vein Sam describes, of equivalences of mathematical statements to $\mathrm{I}\Sigma^0_1$ over $\mathsf{RCA}_0^*$ can be found in (Simpson and Smith 1986),(Hatzikiriakou 1989a), and (Hatzikiriakou 1989b), e.g. that every finitely generated vector space over $\mathbb{Q}$ has a basis; that every torsion-free, finitely generated abelian group is free; the structure theorem for finitely generated abelian groups; and the theorem that for every countable field $K$, every polynomial $f(x) \in K[x]$ has only finitely many roots in $K$.

Another one, this time over $\mathsf{RCA}_0$ rather than $\mathsf{RCA}_0^*$, is the equivalence of $\mathsf{RT}^1_{<\infty}$ to the $\Sigma^0_2$ bounding scheme (Hirst 1987). There has been a lot of recent work on the first-order strength of (weakenings of) Ramsey's theorem, both over $\mathsf{RCA}_0$ and $\mathsf{RCA}_0^*$, for example Kołodziejczyk and Yokoyama (2021).