Nonstandard arithmetic and reverse mathematics. (English) Zbl 1101.03040

Keisler, H. Jerome

Bull. Symb. Log. 12, No. 1, 100-125 (2006).

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)].

Reviewer: Roman Kossak (New York)

MSC:

03F35	Second- and higher-order arithmetic and fragments
03H15	Nonstandard models of arithmetic

Keywords:

reverse mathematics; second-order arithmetic; hyperintegers

Citations:

Zbl 0587.03048; Zbl 0871.03044

References:

[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