\(\Pi_1^1\)-CA\(_0\) and order types of countable ordered groups (Q2732274)

The author deals with the classification problem of all admissible order types for orderable groups from the point of view of the Friedman-Simpson program of reverse mathematics [cf. \textit{S. G. Simpson}, ``Reverse mathematics'', Proc. Symp. Pure Math. 42, 461-471 (1985; Zbl 0578.03005), Subsystems of second order arithmetic, Springer, Berlin-Heidelberg (1999; Zbl 0909.03048)]. It is well known that in the abelian case a basic tool is the classical theorem of Hölder (stating that every archimedean ordered group is isomorphic to a subgroup of the additive ordered group of the reals), which can be proven in the weakest system of reverse mathematics, namely recursive analysis \(\text{RCA}_0\) [cf. \textit{R. Solomon}, ``Ordered groups: a case study in reverse mathematics'', Bull. Symb. Log. 5, No.~1, 45-58 (1999; Zbl 0922.03078)]. In the case of countable ordered groups, the fundamental classification theorem is due to Mal'tsev: if \(G\) is a countable ordered group, then the order type of \(G\) has the form \(Z^\alpha Q^\varepsilon\), for some wellorder \(\alpha\) and \(\varepsilon \in \{0,1\}\) (where \(Z\) is the additive group of the integers and \(Q\) the field of the rationals). The main content of this paper is the proof that Mal'tsev 's theorem is indeed much stronger, and in fact equivalent with the strongest subsystem investigated so far in reverse mathematics, namely \(\Pi ^1_1\text{-CA}_0\). Therefore, Mal'tsev's theorem is not predicatively reducible (e.g. provable in the system based on arithmetical transfinite recursion \(\text{ATR}_0\)). We recall that \(\Pi ^1_1\text{-CA}_0\) is based on the schema postulating the existence of a set of natural numbers in correspondence to arbitrary formulas of the form \(\forall X A(X,u)\), \(A\) being first order (no set quantifier). The result should be especially appreciated, since, as the reader can check from Simpson's book, the number of known equivalences of mathematical results with the subsystem \(\Pi ^1_1\text{-CA}_0\) is rather meager in comparison with systems like \(\text{ATR}_0\) or \(\text{WKL}_0\).