Nonstandard arithmetic and recursive comprehension (Q636343)

The main result of the paper concerns the nonstandard counterpart of the fragment of second-order arithmetic \(\mathrm{RCA}_0\). Let \(L_1\) be the language of first-order arithmetic (in this paper it includes \(<\) and truncated subtraction), and let \(L_2\) be the language of second-order arithmetic. \(L_2\) extends \(L_1\) and includes two sorts: \({\mathbb N}\) for natural numbers and \({\mathbb P}\) for sets of natural numbers. Let \(^*L_1\) be the extension of \(L_1\) that has the sort \({\mathbb N}\) for standard integers and the sort \(^*{\mathbb N}\) for hyperintegers. The \(^*L_1\)-theory BNA of Basic Nonstandard Arithmetic includes \(\mathrm{I}\Sigma_1\) in the language of \(L_1\), the sentence saying that \(<\) is a strict linear order, and axioms expressing that \({\mathbb N}\) is a proper initial segment. The Standard Part Principle STP declares that every set of standard integers is coded by a hyperinteger and that every hyperinteger codes a set of natural numbers. Let \(T\) be an \(L_2\)-theory. Keisler calls a theory \(T'\) a nonstandard counterpart of \(T\) if (a) \(T'\) implies and is conservative with respect to \(T\), and (b) \(T'\) is of the form BNA + STP + \(U\), where \(U\) is an \(^*L_1\)-theory. In [``Nonstandard arithmetic and reverse mathematics'', Bull. Symb. Log. 12, No. 1, 100--125 (2006; Zbl 1101.03040)], \textit{H. J. Keisler} gave nonstandard counterparts of four of the five major theories of reverse mathematics, \(\mathrm{WKL}_0\), \(\mathrm{ACA}_0\), \(\mathrm{ATR}_0\), and \(\Pi^1_1\mathrm{-CA}_0\). A candidate for the nonstandard counterpart of \(\mathrm{RCA}_0\) was also defined there, but failed to satisfy (a) above. The present paper rectifies this problem. The theory \(^*\mathrm{RCA}_0'\) is BNA + STP together with induction and comprehension axioms for special classes of \(^*L_1\)-formulas. The main results of the paper are that \(^*\mathrm{RCA}_0'\) implies \(\mathrm{RCA}_0\) and that \(^*\mathrm{RCA}_0\) together with all axioms of the form \(\varphi\rightarrow ^*\varphi\), where \(\varphi\) is a universal sentence of \(L_1\) and \(^*\varphi\) is its natural \(^*L_1\)-translation, is conservative with respect to \(\mathrm{RCA}_0\). The last section includes an interesting list of open problems. In particular, Keisler asks how much \(^*\mathrm{RCA}_0'\) can be strengthened while still remaining conservative over \(\mathrm{RCA}_0\). He shows that some innocuous-looking strengthenings fail to have this property as they imply \(\mathrm{WKL}_0\).