Nonstandard arithmetic and reverse mathematics. (English) Zbl 1101.03040

Reverse mathematics is based on a hierarchy of fragments of second-order arithmetic. Keisler develops an alternative approach in which the key role is played by the separation of integers into the (standard) natural numbers and hyperintegers. This is done in a hybrid second-order/two-sorted language \(L_2\cup {^*\!L}_1\). Keisler shows that each of the basic theories \(\text{ WKL}_0\), \(\text{ACA}_0\), \(\text{ATR}_0\), and \(\Pi^1_1\)-\(\text{CA}_0\) (which are formulated in the language of second-order arithmetic \(L_2\)) has a natural counterpart in \(L_2\cup {^*\!L}_1\). The language \({^*\!L}_1\) has all the symbols of the first-order arithmetic and variables of two sorts: \(N\) and \(^*\!N\). The universe of sort \(N\) is a subset of the universe of sort \(^*\!N\) and variables and terms of sort \(N\) are allowed in argument places of sort \({^*\!N}\). The role of the basic theory \(\text{ I}\Sigma_1\) is played by \(^*\Sigma \text{PA}\) which includes the basic axioms of \(\text{I}\Sigma_1\) with variables of sort \(^*\!N\), an internal induction axiom for a special class of bounded formulas, and two special axioms. One of the axioms says that \(N\) is a proper initial segment of \(^*\!N\), and the other expresses a property of coded sequences all of whose terms with standard indices are standard (the Finiteness Axiom). This theory is denoted by \(^*\Sigma \text{PA}\). The stronger axiom systems describe properties of structures of the form \((M,\,^*\!N)\), where \(M=(N,P)\) is an \(L_2\) structure and \((N,\,^*\!N)\) is an \(^*\!L_1\) structure. Then, \(^*\text{WKL}_0\) is a theory in the language \(L_2\cup {^*\!L}_1\) defined as \(^*\Sigma + \text{ STP}\), where STP is the Standard Part Principle declaring that \(P\) is the standard system of \(^*\!N\) relative to \(N\). It is shown that \(^*\text{WKL}_0\) implies \(\text{WKL}_0\) and that \(^*\text{WKL}_0\) is conservative with respect to \(\text{WKL}_0\). An important ingredient of the proof is the theorem of K. Tanaka [Ann. Pure Appl. Logic 84, 41–49 (1997; Zbl 0871.03044)], on self-embeddings of countable models of \(\text{WKL}_0\) which are not \(\omega\)-models. The equivalent of \(\text{RCA}_0\) is obtained by weakening STP in \(^*\text{WKL}_0\). The equivalents of \(\text{ACA}_0\) and \(\Pi^1_1\)-\(\text{CA}_0\) are obtained by adding suitable comprehension schemes to \(^*\text{WKL}_0\); \(^*\text{ATR}_0\) involves a \(\Sigma^*_1\)-separation scheme. It is also shown that \(^*\Pi^1_1\)-\(\text{CA}_0\) plus the First-Order Transfer Principle (FOT) is conservative with respect to \(\Pi^1_1\)-\(\text{CA}_0\) proving a conjecture of C. W. Henson, M. Kaufmann and H. J. Keisler [J. Symb. Log. 49, 1039–1058 (1984; Zbl 0587.03048)].


03F35 Second- and higher-order arithmetic and fragments
03H15 Nonstandard models of arithmetic
Full Text: DOI Link


[1] Logic in Tehran 26 (2006)
[2] Model theory (1990)
[3] DOI: 10.1016/S0168-0072(95)00058-5 · Zbl 0871.03044
[4] DOI: 10.2307/2274260 · Zbl 0587.03048
[5] Infinitistic methods pp 257– (1961)
[6] DOI: 10.2307/2274061 · Zbl 0624.03051
[7] Subsystems of second order arithmetic (1999) · Zbl 0909.03048
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.