NONSTANDARD ARITHMETIC AND REVERSE MATHEMATICS

H. JEROME KEISLER

Abstract. We show that each of the five basic theories of second order arithmetic that play a central role in reverse mathematics has a natural counterpart in the language of nonstandard arithmetic. In the earlier paper [HKK1984] we introduced saturation principles in nonstandard arithmetic which are equivalent in strength to strong choice axioms in second order arithmetic. This paper studies principles which are equivalent in strength to weaker theories in second order arithmetic.

§1. Introduction. Reverse mathematics was introduced by H. Friedman and is developed extensively in the book of Simpson [Si1999]. It shows that many results in classical mathematics are equivalent to one of five basic theories in the language L_{2} of second order arithmetic. These theories, from weakest to strongest, are called Recursive Comprehension (RCA_{0}), Weak Koenig Lemma (WKL_{0}), Arithmetical Comprehension (ACA_{0}), Arithmetical Transfinite Recursion (ATR_{0}), and Π_{1}^{1} Comprehension (Π_{1}^{1}-CA_{0}). In this paper we find natural counterparts to each of these theories in the language ^{∗}L_{1} of nonstandard arithmetic.

The language L_{2} of second order arithmetic has a sort for the natural numbers and a sort for sets of natural numbers, while the language ^{∗}L_{1} of nonstandard arithmetic has a sort for the natural numbers and a sort for the hyperintegers. In nonstandard analysis one often uses first order properties of hyperintegers to prove second order properties of integers. An advantage of this method is that the hyperintegers have more structure than the sets of integers. The method is captured by the Standard Part Principle (STP), a statement in the combined language L_{2} ∪ ^{∗}L_{1} which says that a set of integers exists if and only if it is coded by a hyperinteger.

For each of the basic theories T = WKL_{0}, ACA_{0}, ATR_{0}, Π_{1}^{1}-CA_{0} in the language L_{2} of second order arithmetic, we will find a natural counterpart U in the language ^{∗}L_{1} of nonstandard arithmetic, and prove that:

1) U + STP ⊢ T, and

2) U + STP is conservative with respect to T (that is, any sentence of L_{2} provable from U + STP is provable from T.

We also get a result of this kind for the theory RCA_{0}, but with a weaker form of STP.

For instance, in the case that T = WKL_{0}, the corresponding theory U = ^{∗}ΣPA in the language ^{∗}L_{1} has the following axioms (stated formally in Section 3):

• Basic axioms for addition, multiplication,and exponentiation,

• The natural numbers form a proper initial segment of the hyperintegers,

• Induction for bounded quantifier formulas about hyperintegers,

• If there is a finite n such that (z)_{n} is infinite, then there is a least n such that (z)_{n} is infinite.

In the case that T = Π_{1}^{1}-CA_{0}, our result proves a conjecture stated in the paper [HKK1984]. The missing ingredient was a nonstandard analogue of the Kleene normal form theorem for Σ_{1}^{1} formulas, which is proved here in Section 8 and is also used for the case T = ATR_{0}. In the case T = WKL_{0}, our conservation result uses a self-embedding theorem of Tanaka [Ta1997].

The paper [Ke2005] is a companion to this paper which develops a framework for nonstandard reverse mathematics in the setting of higher order type theory. There is a close relationship between this paper and the paper [En2005] of Enayat. In the earlier papers [HKK1984] and [HK1986] we introduced saturation principles in nonstandard arithmetic which are equivalent in strength to strong choice axioms in second and higher order arithmetic. This paper studies principles which are equivalent in strength to weaker theories in second order arithmetic.

I thank Itay Ben Yaacov, Ali Enayat, Arnold Miller, and Steffen Lempp for helpful discussions in connection with this work.

§2. Preliminaries. We refer to [Si1999] for background in reverse mathematics and second order number theory, and to [CK1990] for background in model theory.

We begin with a brief review of the first order base theory ΣPA (Peano arithmetic with restricted induction) and the second order base theory RCA_{0} (recursive comprehension).

The language L_{1} of ΣPA is a first order language with variables m, n, …, equality =, the order relation <, the constants 0, 1, and the binary operations +, ·. For convenience in coding finite sequences of integers, we also include in the vocabulary of L_{1} the symbols exp, p_{n}, and (m)_{n} for the exponentiation function exp(m, n) = m^{n}, the function p_{n} = the n-th prime, and the function (m)_{n} = the largest k ≤ m such that (p_{n})^{k} divides m. The theory ΣPA without the extra symbols exp, p_{n}, and (m)_{n} is called IΣ_{1} in the literature.

The language L_{2} of RCA_{0} is a two sorted language with the symbols of L_{1} in the number sort N, variables X, Y, … of the set sort P, and the binary operation ∈ of sort N × P.

When we write a formula φ(v⃗), it is understood that v⃗ is a tuple of variables that contains all the free variables of φ. If we want to allow additional free variables we write φ(v⃗, …). The length of v⃗ is denoted by |v⃗|, and v_{i} is a typical element of v⃗. If m⃗ = ⟨m_{0}, …, m_{k}⟩ then (m⃗)_{n} denotes the tuple ⟨(m_{0})_{n}, …, (m_{k})_{n}⟩.

The bounded quantifiers (∀n < t) and (∃n < t) are defined as usual, where t is a term of sort N. By a bounded quantifier formula, or Δ_{0}^{0} formula, we mean a formula of L_{2} built from atomic formulas using propositional connectives and bounded quantifiers. We put Σ_{0}^{0} = Π_{0}^{0} = Δ_{0}^{0}, and

Σ_{k+1}^{0} = {∃m θ : θ ∈ Π_{k}^{0}}, Π_{k+1}^{0} = {∀m θ : θ ∈ Σ_{k}^{0}}.

The arithmetical formulas are the formulas in the set ⋃_{k} Σ_{k}^{0} = ⋃_{k} Π_{k}^{0}. These are the formulas of L_{2} with only first order quantifiers.

Definition 2.1. Axioms of ΣPA.

• The Basic Axioms, a finite set of sentences giving the usual recursive rules for <, +, ·, exp, p_{n}, and (m)_{n}.

• First Order Σ_{1}^{0} Induction Scheme

[φ(0, n⃗) ∧ ∀m[φ(m, n⃗) → φ(m + 1, n⃗)]] → ∀mφ(m, n⃗)

where φ(m, n⃗) is a Σ_{1}^{0} formula of L_{1}.

It is well known that in ΣPA, every primitive recursive relation can be defined in a canonical way by both a Σ_{1}^{0} and a Π_{1}^{0} formula, and that the primitive recursive relations are closed under bounded quantification.

A general L_{2}-structure has the form M = (N , P) where N is an L_{1}- structure, called the first order part of M, and P is a family of subsets of the universe of N.

Definition 2.2. Axioms of RCA_{0}.

• The Basic Axioms of ΣPA.

• Σ_{1}^{0} Induction:

[φ(0, …) ∧ ∀m[φ(m, …) → φ(m + 1, …)]] → ∀mφ(m, …)

where φ is a Σ_{1}^{0} formula of L_{2}.

• Δ_{1}^{0} Comprehension:

∀m[φ(m, …) ↔ ψ(m, …)] → ∃X∀m [m ∈ X ↔ φ(m, …)]

where φ is a Σ_{1}^{0} formula of L_{2} in which X does not occur, and ψ a Π_{1}^{0} formula of L_{2} in which X does not occur.

In RCA_{0} one can define the notion of a binary tree as a set of numbers which code finite sequences of 1’s and 2’s with the natural ordering, as well as the notion of an infinite branch of a tree.

The Weak Koenig Lemma, WKL, is the L_{2} statement that every infinite binary tree X has an infinite branch. The theory WKL_{0} is the defined as

WKL_{0} = RCA_{0} + WKL.

In this paper we will obtain several conservation results in the following sense.

Definition 2.3. Let T be a theory in a language L and T′ be a theory in a language L′ ⊇ L. We say that T′ is conservative with respect to T if every sentence of L which is provable from T′ is provable from T.

This gives an upper bound on the strength of T′; if T′ is conservative with respect to T, then any weakening of T′ is also conservative with respect to T. The following characterization follows easily from the Löwenheim-Skolem theorem.

Proposition 2.4. Suppose L ⊆ L′ and L′ is countable. A theory T′ in L′ is conservative with respect to a theory T in L if and only if every countable model M of T has an elementary extension that can be expanded to a model of T′.

We will need the following conservation results of Friedman and Harrington (see [Si1999], Chapter IX) which show that ΣPA is the first order part of both RCA_{0} and WKL_{0}.

Proposition 2.5. (i) For any model N of ΣPA there is a model M = (N , P) of RCA_{0} with first order part N.

(ii) For any countable model M = (N , P) of RCA_{0} there is a countable model M′ = (N , P′) of WKL_{0} with the same first order part N and with P′ ⊇ P.

Corollary 2.6. For any countable model N of ΣPA there is a countable model M = (N , P) of WKL_{0} with first order part N.

Corollary 2.7. WKL_{0} is conservative with respect to ΣPA.

§3. The theory ^{∗}ΣPA. In this section we define a weak theory ^{∗}ΣPA of nonstandard arithmetic. The language ^{∗}L_{1} has all the symbols of L_{1} plus a new hyperinteger sort ^{∗}N with variables x, y, . . .. In sort ^{∗}N, ^{∗}L_{1} has the symbols =, <, 0, 1, +, ·, exp, p_{y}, (x)_{y} corresponding to the symbols of L_{1}. The sort N has the variables k, m, n, p, q, …, and sort ^{∗}N has the variables u, v, w, x, y, z, . . .. The universe of sort N is to be interpreted as a subset of the universe of sort ^{∗}N. Terms built from variables of sort N are also of sort N. Variables and terms of sort N are allowed in argument places of sort ^{∗}N. Terms which contain at least one variable of sort ^{∗}N are also of sort ^{∗}N. For example, x + n is a term of sort ^{∗}N, and ∃n y < x + n is a formula. We introduce the predicate symbol S for the standard integers, and for each term t we write S(t) for ∃n n = t.

We now build a hierarchy of formulas beginning with the stars of bounded quantifier formulas and applying quantifiers over variables of sort N.

Definition 3.1. In ^{∗}L_{1}, a bounded quantifier is an expression of the form (∀s < t) or (∃s < t) where s is a variable, t is a term, and if s has sort N then t has sort N. (Thus we do not count (∀n < x) as a bounded quantifier).

An internal bounded quantifier formula, or Δ_{0}^{S} formula, is a formula of ^{∗}L_{1} built from atomic formulas using connectives and bounded quantifiers. We put Π_{0}^{S} = Σ_{0}^{S} = Δ_{0}^{S}, and

Π_{k+1}^{S} = {∃nφ : φ ∈ Σ_{k}^{S}}, Σ_{k+1}^{S} = {∀nφ : φ ∈ Π_{k}^{S}}.

A formula is S-arithmetical if it belongs to ⋃_{k} Σ_{k}^{S} = ⋃_{k} Π_{k}^{S}.

In the above definition, The S-prefix indicates that the outer quantifiers are over standard integers.

Definition 3.2. Axioms of ^{∗}ΣPA.

• The Basic Axioms of ΣPA, but with variables of sort ^{∗}N.

• Proper Initial Segment:

∀n∃x(x = n),
∀n∀x[x < n → S(x)],
∃y∀n(n < y).

• Internal Induction:

[φ(0, u⃗) ∧ ∀x[φ(x, u⃗) → φ(x + 1, u⃗)]] → ∀xφ(x, u⃗)

where φ(x, u⃗) is a Δ_{0}^{S} formula.

• Finiteness:

∀z[S((z)_{0}) ∧ ∀m[S((z)_{m}) → S((z)_{m+1})] → ∀mS((z)_{m})].

We let ^{∗}ΔPA be the theory whose axioms are all the axioms of ^{∗}ΣPA except the Finiteness Axiom.

An ^{∗}L_{1} structure will be a structure of the form (N ,^{∗}N) where N is a substructure of ^{∗}N. The usual rules for terms and equality hold. Thus for every term t of sort N we always have ∃nt = n, which we abbreviate as S(t) .

We rely heavily on the convention that k, …, q are variables of sort N and u, …, z are variables of sort ^{∗}N. For example, ^{∗}ΣPA ⊢ ∃y∀n(n < y) but ^{∗}ΣPA ⊢ ¬∃p∀n(n < p). We say that x is finite if S(x), and x is infinite otherwise. We sometimes use H, K for parameters of sort ^{∗}N which are infinite.

We now establish some elementary facts in ^{∗}ΔPA. The following lemma (and its dual with existential quantifiers) will be used without explicit mention.

Lemma 3.3. For every formula φ(x, …) of ^{∗}L_{1} and term t of sort N,

(i) ^{∗}ΔPA ⊢ (∀x < t) φ(x, …) ↔ (∀n < t)φ(n, …).

(ii) ^{∗}ΔPA ⊢ [¬S(H) ∧ (∀x < H)φ(x, …)] → ∀nφ(n, …).

Proof. This follows from the Basic and Proper Initial Segment Axioms. ⊣

Lemma 3.4. (Δ_{0}^{S}-comprehension) For each Δ_{0}^{S} formula φ(m, u⃗) in which y does not occur,

∗ΔPA ⊢ ∃y∀m [(y)_{m} > 0 ↔ φ(m, u⃗)].

Proof. Work in ^{∗}ΔPA. Pick an infinite H. By Internal Induction, there exists y < (p_{H})^{H} such that (∀x < H)(y)_{x} < 2 and

(∀x < H)[(y)_{x} > 0 ↔ φ(x, u⃗)].

Then

∀m [(y)_{m} > 0 ↔ φ(m, u⃗)].
⊣

Lemma 3.5. (Δ_{1}^{S}-comprehension) Let φ(x, u⃗) be a Σ_{1}^{S} formula, and ψ(x, u⃗) be a Π_{1}^{S} formula, in which y does not occur. Then

∗ΔPA ⊢ ∀m [φ(m, u⃗) ↔ ψ(m, u⃗)] → ∃y∀m [(y)_{m} > 0 ↔ φ(m, u⃗)].

Proof. Work in ^{∗}ΔPA. Let φ(x, u⃗) be ∃kφ′(x, k, u⃗) and ψ(x, u⃗) be ∀kψ′(x, k, u⃗) where φ′, ψ′ ∈ Δ_{0}^{S}. Pick an infinite H. Assume that

∀m [φ(m, u⃗) ↔ ψ(m, u⃗)].

Then

∀m [∃k φ′(m, k, u⃗) ↔ (∃z < H)[φ′(m, z, u⃗) ∧ (∀v ≤ z)ψ′(m, v, u⃗)]].

Therefore by Δ_{0}^{S}-comprehension, there exists y such that

∀m [(y)_{m} > 0 ↔ ∃k φ′(m, k, u⃗)].
⊣

Given a Δ_{0}^{S} formula φ(x, u⃗) of ^{∗}L_{1}, the bounded minimum operator (μx < y) φ(x, u⃗) equals the least x < y such that φ(x, u⃗) if there is one, and equals y otherwise. The formal definition is

z = (μx < y) φ(x, u⃗) ↔ [(∀x < z)¬φ(x, u⃗) ∧ [(z < y ∧ φ(z, u⃗)) ∨ z = y]],

where z is a new variable. Note that if φ(x, u⃗) is a Δ_{0}^{S} formula, then so is z = (μx < y) φ(x, u⃗).

Lemma 3.6. (i) For each Δ_{0}^{S} formula φ(x, u⃗),

∗ΔPA ⊢ ∃!z z = (μx < y)φ(x, u⃗).

(ii) For each Δ_{0}^{S} formula ψ(v, x, u⃗),

∗ΔPA ⊢ ∃z(∀v < w)(z)_{v} = (μx < y)ψ(v, x, u⃗).

Proof. (i) Take a new variable v which does not occur in φ(x, u⃗) and prove

(∃!z ≤ v) z = (μx < v)[x ≤ y ∧ φ(x, u⃗)]

by internal induction on v. (It is easily seen that this is equivalent to a Δ_{0}^{S} formula.)

(ii) Prove by internal induction on w that

(p_{w})^{y} < H → (∃z < H^{w})(∀v < w)(z)_{v} = (μx < y)ψ(v, x, u⃗),

and take H so that (p_{w})^{y} < H. ⊣

This lemma allows us to treat (μx < y)φ(x, u⃗) as a term. If φ(x, u⃗) and ψ(x, u⃗) are Δ_{0}^{S} formulas, then ψ((μx < y)φ(x, u⃗), u⃗) is the Δ_{0}^{S} formula

(∃z ≤ y) [z = (μx < y)φ(x, u⃗) ∧ ψ(z, u⃗)].

We may use the bounded minimum operator to introduce new notation in the usual way. For example, we write y ↾ w for

(μx < y)(∀v < w) (x)_{v} = (y)_{v}.

y ↾ w is the code of the first w terms of the sequence coded by y, and for each Δ_{0}^{S} formula ψ(x, u⃗), ψ(y ↾ w, u⃗) is the Δ_{0}^{S} formula

(∃z ≤ y) [z = y ↾ w ∧ ψ(z, u⃗)].

We use the vector notation x⃗ = y⃗ ↾ w to mean that x_{i} = y_{i} ↾ w for each i.

Let us write ∀^{∞}x φ(x, u⃗) for ∀x[¬S(x) → φ(x, u⃗)] and ∃^{∞}x φ(x, u⃗) for ∃x [¬S(x) ∧ φ(x, u⃗)].

Lemma 3.7. (Overspill) Let φ(x, u⃗) be a Δ_{0}^{S} formula. In ^{∗}ΔPA, ∀nφ(n, u⃗) → ∃^{∞}x φ(x, u⃗), and ∀^{∞}x φ(x, u⃗) → ∃nφ(n, u⃗).

Proof. We prove the first statement. Assume ∀nφ(n, u⃗). Pick an infinite H. If φ(H, u⃗) we may take x = H. Assume ¬φ(H, u⃗). By Lemma 3.6 we may take z = (μy < H) ¬φ(y, u⃗). Then ¬S(z). Let x = z − 1. We have x < z, so φ(x, u⃗). But S is closed under the successor function, so ¬S(x). ⊣

Lemma 3.8. (Internal Induction in S) Let φ(x, u⃗) be a Δ_{0}^{S} formula. In ∗ΔPA,

[φ(0, u⃗) ∧ ∀m[φ(m, u⃗) → φ(m + 1, u⃗)]] → ∀m φ(m, u⃗).

Proof. Assume φ(0, u⃗) ∧ ∀m[φ(m, u⃗) → φ(m + 1, u⃗)]. By internal induction, for each k we have ∀x[x < k → φ(x, u⃗)]. Therefore ∀m φ(m, u⃗).

⊣

Proposition 3.9. (Σ_{1}^{S} Induction in S) In ^{∗}ΔPA, the Finiteness Axiom is equivalent to the Σ_{1}^{S} Induction scheme

φ(0, u⃗) ∧ ∀m[φ(m, u⃗) → φ(m + 1, u⃗)] → ∀mφ(m, u⃗) (1)

where φ(m, u⃗) is a Σ_{1}^{S} formula.

Proof. The Finiteness Axiom follows from (1) where φ(m, z) is the formula ∃n n = (z)_{m}. Let φ(m, u⃗) be ∃nψ(m, n, u⃗) where ψ is a Δ_{0}^{S} formula. Pick an infinite H. By Lemma 3.6 we may take z such that

(∀x < H) (z)_{x} = (μy < H)ψ(x, y, u⃗).

Then for all m, we have

∃n ψ(m, n, u⃗) ↔ S((z)_{m}).

The formula (1) now follows from the Finiteness Axiom. ⊣

Theorem 3.10. ^{∗}ΣPA ⊢ ΣPA.

Proof. The basic axioms of ΣPA follow from the basic axioms of^{∗}ΣPA. The Σ_{1}^{0}-Induction scheme follows from the Σ_{1}^{S}-Induction scheme of Proposition 3.9 with the parameters u⃗ in S. ⊣

In the next result, S(y ↾ k) denotes the Σ_{1}^{S} formula ∃p (p = y ↾ k).

Proposition 3.11.

∗ΣPA ⊢ S(y ↾ n) ↔ (∀m < n) S((y)_{m}).

Proof. Work in ^{∗}ΣPA. If S(y ↾ n) and m < n, then (y)_{m} ≤ y ↾ n, so S(y_{m}) by the Proper Initial Segment Axiom. For the converse, assume (∀m < n) S((y)_{m}). We prove by Σ_{1}^{S} induction in S (Lemma 3.9) that for all m,

m ≤ n → S(y ↾ m).

It is trivial that S(y ↾ 0). Assume m ≤ n → S(y ↾ m). If m ≥ n then m + 1 ≤ n → S(y ↾ m + 1) is trivially true. Suppose m < n. Then S(y ↾ m), S(p_{m}), and S((y)_{m}). We have

y ↾ (m + 1) = (y ↾ m) · p_{m}^{(y)_{m}},

so S(y ↾ (m + 1)). This completes the induction. ⊣

§4. Standard Parts. We now combine the languages L_{2} and ^{∗}L_{1} into a common language L_{2} ∪^{∗}L_{1}, and introduce the notions of a standard set and a standard function. They will provide a link between hyperintegers and sets. The language L_{2} ∪^{∗}L_{1} has an integer sort N, a set sort P, and a hyperinteger sort ^{∗}N. L_{2} ∪^{∗}L_{1} has all the symbols of L_{2} and ^{∗}L_{1}. In this language, it will make sense to ask whether a formula of ^{∗}L_{1} implies a formula of L_{2}.

An L_{2} ∪^{∗}L_{1} structure will have the form (M,^{∗}N) where M = (N , P) is an L_{2} structure and (N ,^{∗}N) is a ^{∗}L_{1} structure.

We first define the notion of a standard set, which formalizes a construction commonly used in nonstandard analysis. In the following we work in the language L_{2} ∪^{∗}L_{1} and assume the axioms of ^{∗}ΔPA.

Definition 4.1. We say that X is the standard set of x and that x is a lifting of X, and write X = st(x), if ∀n [n ∈ X ↔ (x)_{n} > 0]. X⃗ = st(x⃗) means that X_{i} = st(x_{i}) for each i.

Thus X = st(x) means that X is the set of all finite n such that p_{n} divides x. We now introduce the Standard Part Principle, which says that every set has a lifting, and every hyperinteger has a standard set. Later on we will introduce several theories that have the Standard Part Principle as an axiom.

Definition 4.2. The Upward Standard Part Principle is the statement that every set has a lifting, formally, ∀X∃x X = st(x).

The Downward Standard Part Principle is the statement that every hyperinteger has a standard set, formally, ∀x∃X X = st(x).

The Standard Part Principle (STP) is the conjunction of the Upward and the Downward Standard Part Principles.

In nonstandard analysis, STP often allows one to obtain results about sets of type P (N) by reasoning about hyperintegers of type ^{∗}N.

The STP is related to H. Friedman’s notion of a standard system, as generalized by Enayat [En2005]. Given a model (N ,^{∗}N) of^{∗}ΔPA, Enayat defined the standard system of ^{∗}N relative to N by

SSy_{N} (^{∗}N) = {st(x) : x ∈ ^{∗}N }.

In an L_{2} ∪^{∗}L_{1}-structure (N , P,^{∗}N), the STP says that P = SSy_{N} (^{∗}N), the Upward STP says that P ⊆ SSy_{N} (^{∗}N), the Downward STP says that P ⊇ SSy_{N} (^{∗}N).

The Standard Part Principles may also be formulated using functions instead of sets. Let us say that X is a total function if ∀m∃!n (m, n) ∈ X. We let f, g, … range over total functions and write f(m) = n instead of (m, n) ∈ f.

We say that x is near-standard, in symbols ns(x), if ∀n S((x)_{n}). Note that ns(x) is a Π_{2}^{S} formula. We employ the usual convention for relativized quantifiers, so that ∀^{ns}x ψ means ∀x[ns(x) → ψ] and ∃^{ns}x ψ means ∃x[ns(x) ∧ ψ]. We write

x ≈ y if ns(x) ∧ ∀n (x)_{n} = (y)_{n}.

We write f = ^{o}x, and say f is the standard function of x and that x is a lifting of f, if

ns(x) ∧ ∀nf(n) = (x)_{n}.

Thus st(x) is a set and ^{o}x is a function. The following is easily checked.

Proposition 4.3. Assume the axioms of ^{∗}ΔPA and that a set exists if and only if its characteristic function exists.

(i) The Upward STP holds if and only if ∀f∃x f = ^{o}x, that is, every total function has a lifting.

(ii) The Downward STP holds if and only if ∀^{ns}x∃f f = ^{o}x, that is, every near-standard hyperinteger has a standard function.

We next show that for liftings of functions one can restrict attention to hyperintegers less than a given infinite hyperinteger H.

Lemma 4.4. In ^{∗}ΔPA, suppose that x is near-standard and H is infinite. Then

(i) If x ≈ y then ns(y) and y ≈ x.

(ii) (∃y < H) x ≈ y.

Proof. (i) Suppose x ≈ y. We have ns(x), so for each n, S((x)_{n}) and (y)_{n} = (x)_{n}, and hence S((y)_{n}). Therefore ns(y), and y ≈ x follows trivially.

(ii) By Overspill there is an infinite K such that K^{K} < H. By Lemma 3.8,

∀n [n < K ∧ (∃y < K^{n})(∀m < n) (y)_{m} = (x)_{m}].

By Overspill,

∃^{∞}u [u < K ∧ (∃y < K^{u})(∀v < u) (y)_{v} = (x)_{v}].

Then y < H ∧ y ≈ x. ⊣

We now define a lifting map from formulas of L_{2} to formulas of ^{∗}L_{1}.

Definition 4.5. Let φ(m⃗, X⃗) be a formula in L_{2}, where m⃗, X⃗ contain all the variables of φ, both free and bound. The lifting \overline{φ}(m⃗, x⃗) is defined as follows, where x⃗ is a tuple of variables of sort ^{∗}N of the same length as X⃗.

• Replace each subformula t ∈ X_{i}, where t is a term, by (x_{i})_{t} > 0.

• Replace each quantifier ∀X_{i} by ∀x_{i}, and similarly for ∃.

It is clear that if φ is a Δ_{0}^{0} formula of L_{2}, then \overline{φ} is a Δ_{0}^{S} formula of ^{∗}L_{1}, and if φ is an arithmetical formula then \overline{φ} is an S-arithmetical formula. The following lemma on liftings of formulas will be used many times.

Lemma 4.6. (i) For each arithmetical formula φ(m⃗, X⃗) of L_{2},

∗ΔPA ⊢ st(x⃗) = X⃗ → [φ(m⃗, X⃗) ↔ \overline{φ}(m⃗, x⃗)].

(ii) For each formula φ(m⃗, X⃗) of L_{2},

∗ΔPA + STP ⊢ st(x⃗) = X⃗ → [φ(m⃗, X⃗) ↔ \overline{φ}(m⃗, x⃗)].

Proof. In the case that φ is atomic, the lemma follows from the definitions involved. The general case is then proved by induction on the complexity of φ, using STP at the quantifier steps in part (ii). ⊣

§5. The theory ^{∗}WKL_{0}. In this section we define the theory ^{∗}WKL_{0} in the language L_{2} ∪^{∗}L_{1}, and show that ^{∗}WKL_{0} implies WKL_{0} and ^{∗}WKL_{0} is conservative with respect to WKL_{0}. A consequence of this result is that ∗ΣPA is conservative with respect to ΣPA.

Definition 5.1. In the language L_{2} ∪^{∗}L_{1}, the theory ^{∗}WKL_{0} is defined by

∗WKL_{0} = ^{∗}ΣPA + STP.

Proposition 5.2. Every model of ^{∗}ΣPA has a unique expansion to a model of ^{∗}WKL_{0}.

Proof. Given a model (N ,^{∗}N) of ^{∗}ΣPA, the unique expansion to a model of ^{∗}WKL_{0} is obtained by taking P = {st(x) : x ∈ ^{∗}N }. ⊣

Proposition 5.3. Let (N , N′) be a model of ^{∗}ΣPA and let ^{∗}N be an end extension of N′ which satisfies Internal Induction.

(i) (N ,^{∗}N) is a model of ^{∗}ΣPA. (ii) If (M, N′) is a model of ^{∗}WKL_{0}, then (M,^{∗}N) is a model of

∗WKL_{0}.

Proof. (i) It is clear that the axioms of ^{∗}ΔPA hold in (N ,^{∗}N). The Finiteness Axiom in (N ,^{∗}N) follows from Lemma 4.4 and the Finiteness Axiom in (N , N′).

(ii) STP in (N ,^{∗}N) follows from Lemma 4.4 and STP in (N , N′). ⊣

Theorem 5.4. ^{∗}WKL_{0} ⊢ WKL_{0}.

Proof. Work in ^{∗}WKL_{0}. We first prove Σ_{1}^{0} Induction. For future reference, we note that this part of the proof will not use the Downward STP.

Let ψ(m, n⃗, X⃗) be a Σ_{1}^{0} formula of L_{2}. Suppose that

ψ(0, n⃗, X⃗) ∧ ∀m[ψ(m, n⃗, X⃗) → ψ(m + 1, n⃗, X⃗)].

By the Upward STP the tuple X⃗ has a lifting x⃗. By Lemma 4.6 (i),

\overline{ψ}(0, n⃗, x⃗) ∧ ∀m [\overline{ψ}(m, n⃗, x⃗) → \overline{ψ}(m + 1, n⃗, x⃗)].

Then by Proposition 3.9, ∀m\overline{ψ}(m, n⃗, x⃗). By Lemma 4.6 (i) again, we have ∀mψ(m, n⃗, X⃗).

We next prove Δ_{1}^{0}-comprehension. Assume that

∀m[∃kφ(m, k, Y⃗) ↔ ∀kψ(m, k, Y⃗)]

where φ and ψ are Δ_{0}^{0} formulas. By the Upward STP there is a lifting y⃗ of Y⃗. By Lemma 4.6,

∀m [∃k \overline{φ}(m, k, y⃗) ↔ ∀k \overline{ψ}(m, k, y⃗)].

By Δ_{1}^{S}-comprehension (Lemma 3.5), there exists x such that

∀m [(x)_{m} > 0 ↔ ∃k \overline{φ}(m, k, y⃗)].

By the Downward STP there is a set X = st(x). By Lemma 4.6,

∀m[m ∈ X ↔ ∃kφ(m, k, Y⃗)].

Finally, we prove WKL. Let ψ(n) be the formula

(∀m < n)[(n)_{m} < 3 ∧ (∀k < m)[(n)_{k} = 0 → (n)_{m} = 0]].

ψ(n) says that n codes a finite sequence of 1’s and 2’s. Write m ⊲ n if

ψ(m) ∧ ψ(n) ∧ (∃k < n)m = n ↾ k].

This says the sequence coded by m is an initial segment of the sequence coded by n. ψ(n) and m ⊲ n are Δ_{0}^{0} formulas, and their stars ^{∗}ψ(u) and v^{∗}⊲ u are in Δ_{0}^{S}. Suppose that T codes an infinite binary tree, that is,

∀m∃n[m < n ∧ n ∈ T]

and

∀n[n ∈ T → ψ(n) ∧ (∀m < n)[m ⊲ n → m ∈ T]].

By the axioms of RCA_{0} (already proved), there is a function f such that for each k, f(k) is the k-th element of T. Then

∀k [k ≤ f(k) ∧ f(k) ∈ T].

By STP, T has a lifting x and f has a lifting y. Then ∀k S((y)_{k}). By Lemma 4.6,

∀n[(x)_{n} > 0 → ^{∗}ψ(n) ∧ (∀m < n)[m^{∗}⊲n → (x)_{m} > 0]]

and

∀k [k ≤ (y)_{k} ∧ (x)_{(y)_{k}} > 0].

Therefore

∀k [k ≤ t∧(x)_{t} > 0∧^{∗}ψ(t)∧(∀m < t)[m^{∗}⊲ t → (x)_{m} > 0]] where t = (y)_{k}.

By Overspill,

∃^{∞}w [w ≤ t∧(x)_{t} > 0∧^{∗}ψ(t)∧(∀u < t)[u^{∗}⊲ t → (x)_{u} > 0]] where t = (y)_{w}.

Then ns(t), and by STP there exists g = ^{o}t. It follows that g codes an infinite sequence of 1’s and 2’s, and each finite initial segment of g belongs to T. Thus g codes an infinite branch of T. ⊣

We now use a result of Tanaka [Ta1997] to show that ^{∗}WKL_{0} is conservative with respect to WKL_{0}.

Definition 5.5. By an ω-model we mean an L_{2}-structure M = (N , P) such that N is the standard model of arithmetic.

Theorem 5.6. (Tanaka [Ta1997]). For every countable model M = (N , P) of WKL_{0} which is not an ω-model, there is a model M_{0} = (N_{0}, P_{0}) such that M_{0} ≅ M, N is a proper end extension of N_{0}, and P_{0} = {X ∩ N_{0} : X ∈ P}.

Theorem 5.7. Every countable model M of WKL_{0} which is not an ωmodel can be expanded to a countable model (M,^{∗}N) of ^{∗}WKL_{0} such that ∗N ≅ N.

Proof. By Theorem 5.6, there is a model M_{1} = (N_{1}, P_{1}) such that M_{1} ≅ M, N_{1} is a proper end extension of N, and P = {X ∩N : X ∈ P_{1}}. Then N_{1} ≅ N. (M, N_{1}) clearly satisfies all the axioms of ^{∗}WKL_{0} except possibly the Finiteness Axiom and STP.

Proof of STP: Let x ∈ N_{1} and let X_{1} = {y ∈ N_{1} : (x)_{y} > 0}. Then X_{1} ∈ P_{1} and st(x) = X_{1} ∩ N ∈ P. Now let X ∈ P. Then X = X_{1} ∩ N for some X_{1} ∈ P_{1}. Pick y ∈ N_{1} \ N. There exists x ∈ N_{1} such that (∀z < y)[(x)_{z} > 0 ↔ z ∈ X_{1}]. Then x is a lifting of X.

Proof of the Finiteness Axiom: Let z ∈ N_{1}. Suppose that S((z)_{0}) and

∀m[S((z)_{m}) → S((z)_{m+1})].

The set Y = {(m, n) ∈ N^{2} : (z)_{m} = n} belongs to P, and using Σ_{1}^{0} Induction with the formula ∃n(m, n) ∈ Y we conclude that ∀mS((z)_{m}).

⊣

Corollary 5.8. ^{∗}WKL_{0} is conservative with respect to WKL_{0}.

Corollary 5.9. Every countable nonstandard model N of ΣPA can be expanded to a countable model (N ,^{∗}N) of ^{∗}ΣPA such that ^{∗}N ≅ N. ∗ΣPA is conservative with respect to ΣPA.

§6. The Theory^{∗}RCA_{0}. In this section we introduce the theory^{∗}RCA_{0} in the language L_{2}∪^{∗}L_{1}, and show that ^{∗}RCA_{0} implies and is conservative with respect to the base theory RCA_{0} of reverse mathematics. ^{∗}RCA_{0} will contain the axioms of ^{∗}ΣPA, the Upward STP, and a weakening of the Downward STP which asserts that certain hyperintegers have standard sets.

We begin with a definability notion which is expressible in the language ∗L_{1}. We say that x is setlike if ∀m (x)_{m} < 2.

Definition 6.1. Suppose that x and each y_{i} is setlike. x is Δ_{1}^{0}-definable from y⃗ if there are a Σ_{1}^{0} formula φ(k, m, p⃗) and a Π_{1}^{0} formula ψ(k, m, p⃗) of L_{1} such that

∀m[∃k φ(k, m, y⃗ ↾ k) ↔ ∀k ψ(k, m, y⃗ ↾ k)]

and

∀m[(x)_{m} > 0 ↔ ∃k φ(k, m, y⃗ ↾ k)].

Definition 6.2. The theory ^{∗}RCA_{0} has the following axioms:

• The axioms of ^{∗}ΣPA,

• The Upward STP, ∀X∃x (X = st(x)),

• Each constant function exists, ∀n∃f∀kf(k) = n.

• Δ_{1}^{0}-STP: If x and each y_{i} is setlike, x is Δ_{1}^{0}-definable from y⃗, and ∃Y⃗ (Y⃗ = st(y⃗)), then ∃X(X = st(x)).

Lemma 6.3. (i)

∗ΔPA ⊢ ∀v∃x [x is setlike ∧ ∀m [(x)_{m} > 0 ↔ (v)_{m} > 0]].

(ii) ^{∗}RCA_{0} ⊢ ∀X [X has a setlike lifting].

(iii) ^{∗}RCA_{0} ⊢ ∀^{∞}H∀X [X has a setlike lifting y < H].

Proof. (i) By internal induction, there exists x ≤ v such that (∀u < v) x_{u} = min((v)_{u}, 1).

(ii) By the Upward STP there is a lifting v of X. Then by (i), there is a setlike x such that st(x) = st(v) = X.

(iii) Take an infinite H and a set X. By (ii), X has a setlike lifting x. Then x is near-standard, and by Lemma 4.4 there exists y ≈ x such that y < H. y is a setlike lifting of X. ⊣

We need the following normal form theorem for Σ_{1}^{0} formulas in ^{∗}ΣPA.

Lemma 6.4. For each Σ_{1}^{0} formula φ(m⃗, Y⃗) in L_{2}, there is a Δ_{0}^{0} formula θ(k, m⃗, r⃗) in L_{1} such that

∗ΣPA ⊢ \overline{φ}(m⃗, y⃗) ↔ ∃kθ(k, m⃗, y⃗ ↾ k).

Proof. We have \overline{φ}(m⃗, y⃗) = ∃nψ(n, m⃗, y⃗) where ψ is Δ_{0}^{S} and each y_{i} occurs only in subformulas of the form (y_{i})_{t} > 0 where t is a term of sort N. Let p⃗ be a tuple containing all free and bound variables of sort N in ψ, and let T be the finite set of all terms t(p⃗) of sort N which occur in ψ. Let m⃗ = ⟨m_{0}, …, m_{j}⟩ and let |q⃗| = |p⃗|. Then the result holds where θ(k, m⃗, y⃗ ↾ k) is

(∃n < k) [ψ(n, m⃗, y⃗ ↾ k) ∧ (∀q⃗ < n + m_{0} + … + m_{j}) ⋀_{t∈T} t(q⃗) < k].

⊣

Theorem 6.5. ^{∗}RCA_{0} ⊢ RCA_{0}.

Proof. Work in ^{∗}RCA_{0}. We have already shown in the proof of Theorem 5.4 that Σ_{1}^{0}-induction follows from the axioms of ^{∗}RCA_{0}. We prove Δ_{1}^{0}-comprehension. The idea is to use Δ_{1}^{S}-comprehension in ^{∗}ΔPA to get a hyperinteger x, and then use the Δ_{1}^{0}-STP axiom to get a set X = st(x). Assume that

∀m[φ(m, Y⃗) ↔ ψ(m, Y⃗)]

where φ ∈ Σ_{1}^{0} and ψ ∈ Π_{1}^{0}. We may suppose that there are no parameters of sort N, because such parameters can replaced by the corresponding constant functions and included in Y⃗. By Lemma 6.3, Y⃗ has a setlike lifting y⃗. By Lemma 4.6,

φ(m, Y⃗) ↔ \overline{φ}(m, y⃗), ψ(m, Y⃗) ↔ \overline{ψ}(m, y⃗).

By Lemma 6.4, there are Δ_{0}^{0} formulas α(k, m, n⃗), β(k, m, n⃗) in L_{1} such that

\overline{φ}(m, y⃗) ↔ ∃k α(k, m, y⃗ ↾ k),
\overline{ψ}(m, y⃗) ↔ ∀k β(k, m, y⃗ ↾ k).

Then

∀m [∃k α(k, m, y⃗ ↾ k) ↔ ∀k β(k, m, y⃗ ↾ k)].

Since y⃗ is setlike, ∀k S(y⃗ ↾ k), and therefore ∃k α(k, m, y⃗ ↾ k) is Σ_{1}^{S} and ∀k β(k, m, y⃗ ↾ k) is Π_{1}^{S}. By Δ_{1}^{S}-comprehension (Lemma 3.5) there exists x such that

∀m [(x)_{m} > 0 ↔ ∃k α(k, m, y⃗ ↾ k)].

By Lemma 6.3 (i), we may take x to be setlike. This shows that x is Δ_{1}^{0}-definable from y⃗. By Δ_{1}^{0}-STP, there exists X with X = st(x). Since

φ(m, Y⃗) ↔ ∃k α(k, m, y⃗ ↾ k)

we have

∀m [m ∈ X ↔ φ(m, Y⃗)].

This proves Δ_{1}^{0}-CA. ⊣

Theorem 6.6. Every countable model M = (N , P) of RCA_{0} which is not an ω-model can be expanded to a countable model (M,^{∗}N) of ^{∗}RCA_{0} such that ^{∗}N ≅ N.

Proof. By Proposition 2.5, there is a countable model M′ = (N , P′) of WKL_{0} with the same first order part N and with P′ ⊇ P. By Theorem 5.7, M′ can be expanded to a countable model (M′,^{∗}N) of ^{∗}WKL_{0} such that ^{∗}N ≅ N.

We work in (M,^{∗}N) and show that all the axioms of ^{∗}RCA_{0} hold. Since P′ ⊇ P, the Upward STP holds. It remains to prove the Δ_{1}^{0}-STP. Suppose x and each y_{i} is setlike, Y⃗ = st(y⃗), and x is Δ_{1}^{0}-definable from y⃗. This means that there are a Σ_{1}^{0} formula φ(k, m, n⃗) and a Π_{1}^{0} formula ψ(k, m, n⃗) of L_{1} such that for each m the formulas

∃kφ(k, m, y⃗ ↾ k), ∀kψ(k, m, y⃗ ↾ k), and (x)_{m} > 0 (2)

are equivalent. There is a Δ_{0}^{0} formula q = Y ↾ k of L_{2} which says that q is the integer which codes the set {j < k : j ∈ Y }. Then ∃kφ(k, m, Y⃗ ↾ k) is equivalent to a Σ_{1}^{0} formula of L_{2}, and ∀kψ(k, m, Y⃗ ↾ k) is equivalent to a Π_{1}^{0} formula of L_{2}.

By Lemma 4.6, Y⃗ ↾ k = y⃗ ↾ k, and it follows that the formulas (2) are equivalent to ∃kφ(k, m, Y⃗ ↾ k) and to ∀kψ(k, m, Y⃗ ↾ k). Since M satisfies Δ_{1}^{0}-comprehension, there is a set X such that

∀m [m ∈ X ↔ ∃kφ(k, m, Y⃗ ↾ k)],

and therefore X = st(x). ⊣

Corollary 6.7. ^{∗}RCA_{0} is conservative with respect to RCA_{0}.

§7. The Theory ^{∗}ACA_{0}. In this section we will find a nonstandard counterpart of the theory ACA_{0} of arithmetical comprehension.

Given a class Γ of formulas in L_{2}, Γ-comprehension (Γ-CA) is the scheme

∃Y ∀m [m ∈ Y ↔ φ(m, …)]

for all formulas φ ∈ Γ in which Y does not occur.

Arithmetical Comprehension (ACA) is Γ-CA where Γ is the class of arithmetical formulas of L_{2}. The theory ACA_{0} is defined by

ACA_{0} = WKL_{0} + ACA.

It is well-known that the axioms of Peano arithmetic (PA) follow from ACA_{0} (see [Si1999], page 7). The following result of Friedman and Harrington (see [Si1999] Theorem IX.1.5) is analogous to Proposition 2.5 (i) and shows that PA is the first order part of ACA_{0}.

Proposition 7.1. For any model N of PA there is a model M = (N , P) of ACA_{0} with first order part N.

We now introduce a scheme corresponding to arithmetical comprehension in the language ^{∗}L_{1} of nonstandard arithmetic.

Definition 7.2. Given a class Γ of formulas of^{∗}L_{1}, Γ-comprehension (Γ-CA) is the scheme

∃y∀m [(y)_{m} > 0 ↔ φ(m, …)],

for all formulas φ(m, …) ∈ Γ in which y does not occur.

Recall that in Lemma 3.4 we proved Δ_{0}^{S} comprehension in ^{∗}ΔPA.

Definition 7.3. S-arithmetical comprehension (S-ACA) is Γ-CA where Γ is the set of S-arithmetical formulas. The theory ^{∗}ACA_{0} is defined by

∗ACA_{0} = ^{∗}WKL_{0} + S-ACA.

The next result is the analogue of the fact that ACA is equivalent to Σ_{1}^{0}-CA in RCA_{0} ([Si1999], page 105).

Proposition 7.4. In ^{∗}ΣPA, S-ACA is equivalent to Σ_{1}^{S}-CA.

Proof. Work in ^{∗}ΣPA and assume Σ_{1}^{S}-CA. We prove Σ_{k}^{S}-CA by induction on k. This is trivial for k = 1. Suppose k ≥ 1 and φ(m, u⃗) ∈ Σ_{k+1}^{S}, and assume Σ_{k}^{S}-CA. Then φ(m, u⃗) = ∃nψ(m, n, u⃗) where ψ ∈ Π_{k}^{S}. By Σ_{k}^{S}-CA,

∃y∀m∀n[(y)_{(m,n)} > 0 ↔ ¬ψ(m, n, u⃗)].

Then by Σ_{1}^{S}-CA,

∃x∀m[(x)_{m} > 0 ↔ ∃n(y)_{(m,n)} = 0].

Therefore

∀m[(x)_{m} > 0 ↔ ∃nψ(m, n, u⃗)].
⊣

Here is a functional version of S-ACA.

Proposition 7.5. In^{∗}ΣPA, S-ACA is equivalent to the following scheme:

∀m∃n ψ(m, n, …) → ∃^{ns}z∀m ψ(m, (z)_{m}, …) (3)

for each S-arithmetical formula ψ.

Proof. Work in ^{∗}ΣPA. First assume S-ACA. Let ψ(m, n, u⃗) be Sarithmetical, and assume that ∀m∃n ψ(m, n, u⃗). By S-ACA there exists y such that ∀m∀n [y_{(m,n)} > 0 ↔ ψ(m, n, u⃗)]. Pick an infinite H. By Lemma 3.6 there exists z such that (∀v < H)(z)_{v} = (μx < H)y_{(v,x)} > 0. Then ∀m ψ(m, (z)_{m}, u⃗), and z is near-standard.

For the converse, assume (3). Let φ(m, u⃗) be S-arithmetical and let ψ(m, u⃗) be the S-arithmetical formula n > 0 ↔ φ(m, u⃗). By (3), we have

∃x∀m[(x)_{m} > 0 ↔ φ(m, u⃗)].

⊣ Theorem 7.6. In ^{∗}WKL_{0}, S-ACA is equivalent to ACA.

Proof. Work in ^{∗}WKL_{0}. We prove that Σ_{1}^{S}-CA is equivalent to Σ_{1}^{0}-CA. Assume Σ_{1}^{S}-CA and let φ(m, n, Y⃗) be Δ_{0}^{0}. By STP, Y⃗ has a lifting y⃗. By Σ_{1}^{S}-CA, ∃x∀m[(x)_{m} > 0 ↔ ∃nφ(m, n, y⃗)]. By STP, there exists X such that X = st(x). Then by Lemma 4.6,

∀m [m ∈ X ↔ ∃n\overline{φ}(m, n, Y⃗)].

Now assume Σ_{1}^{0}-CA and let φ(m, n, u⃗) be Δ_{0}^{S}. By Δ_{0}^{S}-CA, (which holds by Lemma 3.4),

∃z∀m∀n[(z)_{(m,n)} > 0 ↔ φ(m, n, u⃗)].

By STP there exists Z with Z = st(z). By Σ_{1}^{0}-CA,

∃X∀m[m ∈ X ↔ ∃n(m, n) ∈ Z].

By STP, X has a lifting x, and it follows that

∀m[(x)_{m} > 0 ↔ ∃nφ(m, n, u⃗)].
⊣

Corollary 7.7. ^{∗}ACA_{0} ⊢ ACA_{0}.

Proof. By Theorems 5.4 and 7.6. ⊣

Corollary 7.8. ^{∗}ΣPA + S-ACA ⊢ PA.

Definition 7.9. Given a formula φ of L_{1}, a star of φ is a formula ∗φ of ^{∗}L_{1} which is obtained from φ by replacing each bound variable in φ by a variable of sort ^{∗}N in a one to one fashion.

First Order Transfer (FOT) is the scheme

φ(n⃗) → ^{∗}φ(n⃗)

for each formula φ(n⃗) of L_{1}.

FOT says that ^{∗}N is an elementary extension of N.

The following conservation result for ^{∗}ACA_{0} + FOT is a consequence of Theorem B in the paper Enayat [En2005].

Theorem 7.10. Every countable model of ACA_{0} can be expanded to a model of ^{∗}ACA_{0} + FOT.

Corollary 7.11. The theory ^{∗}ACA_{0}+FOT is conservative with respect to ACA_{0}.

This follows in the usual way from Theorem 7.10. It also follows from earlier results in [HKK1984] (Theorem 4.1 and Lemma 4.12), which show that every countable model of ACA_{0} has an elementary extension which can be expanded to a model of ^{∗}ACA_{0} + FOT.

Corollary 7.12. The theory ^{∗}ΣPA + S-ACA + FOT is conservative with respect to PA.

Proof. By Proposition 7.1 and Theorem 7.10. ⊣

It is worth noting that Theorem B in [En2005] is actually stronger than Theorem 7.10 above. Let j be a new unary function symbol and let AUT be the sentence in the language ^{∗}L_{1} ∪ {j} which says that j is an automorphism of ^{∗}N with fixed point set N. In our setting, the result can be stated as follows.

Theorem 7.13. (Enayat [En2005], Theorem B). Every countable model of ACA_{0} can be expanded to a model of ^{∗}ACA_{0} + AUT + FOT.

Hence ^{∗}ACA_{0} + AUT + FOT is conservative with respect to ACA_{0}, and ∗ΣPA + S-ACA + AUT + FOT is conservative with respect to PA.

§8. The Theory ^{∗}ATR_{0}. In this section we find two nonstandard counterparts of the theory ATR_{0} of arithmetic transfinite recursion.

In the language L_{2}, a Σ_{1}^{1} formula is a formula of the form ∃Y ψ(Y, …) where ψ is arithmetical, and a Π_{1}^{1} formula is a formula of the form ∀Y ψ(Y, …) where ψ is arithmetical.

Σ_{1}^{1}-separation (Σ_{1}^{1}-SEP) is the scheme which says that any two disjoint Σ_{1}^{1} properties can be separated by a set. That is, for any two Σ_{1}^{1} formulas ψ(n, …), θ(n, …) in which X does not occur,

¬∃n[ψ(n, …) ∧ θ(n, …)] →
∃X∀n [(ψ(n, …) → n ∈ X) ∧ (θ(n, …) → n ∉ X)].

It is known (see [Si1999], Theorem V.5.1) that in RCA_{0}, Σ_{1}^{1}-SEP is equivalent to the scheme of Arithmetical Transfinite Recursion. Thus the theory ATR_{0} can be defined as

ATR_{0} = WKL_{0} + Σ_{1}^{1}-SEP.

In the language ^{∗}L_{1}, we define Γ-separation (Γ-SEP) as the scheme that for all formulas ψ(n, …), θ(n, …) ∈ Γ in which x does not occur,

¬∃n[ψ(n, …) ∧ θ(n, …)] →
∃x∀n [(ψ(n, …) → (x)_{n} > 0) ∧ (θ(n, …) → (x)_{n} = 0)].

We will consider two classes of formulas in ^{∗}L_{1} analogous to the class Σ_{1}^{1}, which we call Σ_{1}^{b} and Σ_{1}^{∗}. The Σ_{1}^{b} formulas are formed by putting a bounded existential quantifier in front of an S-arithmetical formula, and the Σ_{1}^{∗} formulas are formed by putting an unbounded existential quantifier in front of an S-arithmetical formula. We will then compare Σ_{1}^{1}-SEP with Σ_{1}^{b}-SEP and Σ_{1}^{∗}-SEP.

Definition 8.1. A Σ_{1}^{b} formula is a formula of the form (∃x < H)φ(x, u⃗), and a Π_{1}^{b} formula is a formula of the form (∀x < H)φ(x, u⃗), where φ is S-arithmetical.

The theory ATR_{0}^{b} is defined by

ATR_{0}^{b} = ^{∗}WKL_{0} + Σ_{1}^{b}-SEP.

Definition 8.2. A Σ_{1}^{∗} formula is a formula of the form ∃x φ(x, u⃗), and a Π_{1}^{∗} formula is a formula of the form ∀x, φ(x, u⃗), where φ is Sarithmetical.

The theory ^{∗}ATR_{0} is defined by

∗ATR_{0} = ^{∗}WKL_{0} + Σ_{1}^{∗}-SEP.

Since Σ_{1}^{b} ⊆ Σ_{1}^{∗}, we see at once that

Proposition 8.3. ^{∗}ATR_{0} ⊢ ATR_{0}^{b}.

We do not know whether or not ATR_{0}^{b} ⊢ ^{∗}ATR_{0}. To make a connection between the theories ATR_{0} and ATR_{0}^{b}, we will use an analogue of the Kleene normal form theorem which applies to Σ_{1}^{b} formulas. From Section 3, q = f ↾ m is a Δ_{0}^{0} formula which says that q is the integer which codes the tuple ⟨f(n) : n < m⟩. The Kleene Normal Form Theorem for Σ_{1}^{1} formulas (see [Si1999], page 169) shows that for each Σ_{1}^{1} formula θ(p⃗, U⃗) there is a Π_{1}^{0} formula ψ(m, n, p⃗, U⃗) such that

ACA_{0} ⊢ θ(p⃗, U⃗) ↔ ∃f∀m ψ(m, f ↾ m, p⃗, U⃗).

Here is the analogue for Σ_{1}^{b} formulas.

Theorem 8.4. Let θ(u⃗) be a Σ_{1}^{b} formula. There is a Π_{1}^{S} formula ψ(k, v, u⃗) such that

∗ΣPA + S-ACA ⊢ θ(u⃗) ↔ ∃^{ns}w∀k ψ(k, w ↾ k, u⃗).

Proof. Work in^{∗}ΣPA+S-ACA. Suppose first that θ(u⃗) is S-arithmetical. Then there is a formula ψ ∈ Π_{j}^{S} such that j is minimal and

θ(u⃗) ↔ ∃^{ns}w∀k ψ(k, w ↾ k, u⃗).

We wish to show that j ≤ 1. Suppose j > 1, so that

ψ(k, v, u⃗) ↔ ∀m∃n φ(m, n, k, v, u⃗)

where φ ∈ Π_{j−2}^{S}. Then

∀kψ(k, v, u⃗) ↔ ∀k∀m∃n φ(m, n, k, v, u⃗).

By Proposition 7.5,

∀k ψ(k, v, u⃗) ↔ ∃^{ns}z∀k∀m φ(m, (z)_{(m,k)}, k, v, u⃗),

and therefore

θ(u⃗) ↔ ∃^{ns}w∃^{ns}z∀k∀m φ(m, (z)_{(m,k)}, k, w ↾ k, u⃗).

By combining quantifiers and simplifying, we get a formula ψ′ ∈ Π_{j−2}^{S} such that

θ(u⃗) ↔ ∃^{ns}w∀k ψ′(k, w ↾ k, u⃗),

contradicting the assumption that j is minimal. We conclude that j ≤ 1, so ψ ∈ Π_{1}^{S}, and the result is proved in the case that θ(u⃗) is S-arithmetical.

For the general case, suppose θ(u⃗) is of the form (∃x < H)δ(x, u⃗) where δ is S-arithmetical. Then

δ(x, u⃗) ↔ ∃^{ns}w∀k∀n ψ(x, k, n, w ↾ k, u⃗)

for some Δ_{0}^{S} formula ψ. It follows that

θ(u⃗) ↔ (∃x < H)∃^{ns}w∀k∀n ψ(x, k, n, w ↾ k, u⃗),

so

θ(u⃗) ↔ ∃^{ns}w(∃x < H)∀k∀n ψ(x, k, n, w ↾ k, u⃗).

By Overspill,

(∃x < H)∀k∀n ψ(x, k, n, w ↾ k, u⃗) ↔
∀p(∃x < H)(∀k < p)(∀n < p) ψ(x, k, n, w ↾ k, u⃗).

Therefore

θ(u⃗) ↔ ∃^{ns}w∀p ψ′(p, w ↾ p, u⃗)

where ψ′(p, w ↾ p, u⃗) is the Δ_{0}^{S} formula

(∃x < H)(∀k < p)(∀n < p) ψ(x, k, n, w ↾ k, u⃗).
⊣

Theorem 8.5. In ^{∗}WKL_{0}, Σ_{1}^{1}-SEP is equivalent to Σ_{1}^{b}-SEP.

Proof. Work in^{∗}WKL_{0}. First assume Σ_{1}^{b}-SEP. Let ψ(m, Y, U⃗), θ(m, Y, U⃗) be arithmetical formulas such that

¬∃m [∃Y ψ(m, Y, U⃗) ∧ ∃Y θ(m, Y, U⃗)].

By STP there is a lifting u⃗ of U⃗. By Lemma 4.6 we have

¬∃m [∃y \overline{ψ}(m, y, u⃗) ∧ ∃y \overline{θ}(m, y, u⃗)].

Let H be infinite. Then

¬∃m [(∃y < H) \overline{ψ}(m, y, u⃗) ∧ (∃y < H) \overline{θ}(m, y, u⃗)].

The formulas (∃y < H) \overline{ψ}(m, y, u⃗) and (∃y < H) \overline{θ}(m, y, u⃗) are Σ_{1}^{b}. By Σ_{1}^{b}-SEP there is an x such that

∀m [((∃y < H) \overline{ψ}(m, y, u⃗) → (x)_{m} > 0)∧(∃y < H) \overline{θ}(m, y, u⃗) → (x)_{m} = 0)].

By STP there exists a set X = st(x). By Lemma 6.3, each set Y has a lifting y < H. Thus by Lemma 4.6 we have

∀m [(∃Y ψ(m, Y, U⃗) → m ∈ X) ∧ (∃Y θ(m, Y, U⃗) → m ∉ X)].

This proves Σ_{1}^{1}-SEP.

Now assume Σ_{1}^{1}-SEP. Let ψ(m, …), θ(m, …) be Σ_{1}^{b} formulas such that

¬∃m [ψ(m, …) ∧ θ(m, …)].

By Theorem 8.4, there are Π_{0}^{S} formulas ψ′(m, k, n, …) and θ′(m, k, n, …) such that

ψ(m, …) ↔ ∃^{ns}w∀k ψ′(m, k, w ↾ k, …),
θ(m, …) ↔ ∃^{ns}w∀k θ′(m, k, w ↾ k, …).

It is clear that Σ_{1}^{1}-SEP implies ACA. By Theorem 7.6, S-ACA holds, so there exist y, z such that

∀m∀k∀n [(y)_{(m,k,n)} > 0 ↔ ψ′(m, k, n, …)],
∀m∀k∀n [(z)_{(m,k,n)} > 0 ↔ θ′(m, k, n, …)].

By STP there are sets Y = st(y) and Z = st(z). By Lemma 4.6,

∃^{ns}w∀k (y)_{(m,k,w↾k)} > 0 ↔ ∃f∀k (m, k, f ↾ k) ∈ Y

and

∃^{ns}w∀k (z)_{(m,k,w↾k)} > 0 ↔ ∃f∀k (m, k, f ↾ k) ∈ Z.

By Σ_{1}^{1}-SEP,

∃X∀m [(m ∈ X → ∃f∀k (m, k, f ↾ k) ∈ Y)∧
(m ∉ X → ∃f∀k (m, k, f ↾ k) ∈ Z)].

By STP, X has a lifting x. By Lemma 4.6,

∀m [((x)_{m} > 0 → ∃^{ns}w∀k (y)_{(m,k,w↾k)} > 0)∧
((x)_{m} = 0 → ∃^{ns}w∀k (z)_{(m,k,w↾k)} > 0)].

Then

∀m [(x)_{m} > 0 → ψ(m, …) ∧ ((x)_{m} = 0 → θ(m, …)],

and x is the required witness for Σ_{1}^{b}-SEP. ⊣

Corollary 8.6. ATR_{0}^{b} ⊢ ATR_{0} and ATR_{0}^{∗} ⊢ ATR_{0}.

Theorem 8.7. Every countable model M = (N , P) of ATR_{0} can be expanded to a model (M,^{∗}N) of ATR_{0}^{b} + FOT.

Proof. By Theorem 7.10, every countable model M of ATR_{0} can be expanded to a model (M,^{∗}N) of^{∗}ACA_{0}+FOT. By Theorem 8.5, (M,^{∗}N) also satisfies Σ_{1}^{b}-SEP, and hence is a model of ATR_{0}^{b}. ⊣

This shows that ATR_{0}^{b} + FOT is conservative with respect to ATR_{0}. We now improve this by showing that the larger theory ^{∗}ATR_{0} + FOT is still conservative with respect to ATR_{0}.

Lemma 8.8. Let (N ,^{∗}N) be a model of ^{∗}ΣPA such that ^{∗}N is ω_{1}-like, that is, ^{∗}N has cardinality ω_{1} and every initial segment is countable. Then for every S-arithmetical formula φ(x, m, u⃗),

(N ,^{∗}N) ⊧ ∃H∀m [∃x φ(x, m, u⃗) → (∃x < H)φ(x, m, u⃗)].

Proof. Fix a tuple u⃗ in ^{∗}N. For each m ∈ N such that (N ,^{∗}N) ⊧ ∃x φ(x, m, u⃗), pick an x_{m} such that (N ,^{∗}N) ⊧ φ(x_{m}, u⃗). Since N is countable, and ^{∗}N is ω_{1}-like, there is an H ∈ ^{∗}N such that x_{m} < H for each m ∈ N. ⊣

Theorem 8.9. Every countable model M = (N , P) of ATR_{0} can be expanded to a model (M,^{∗}N) of ^{∗}ATR_{0} + FOT.

Proof. By Theorem 8.7 and the Löwenheim-Skolem theorem, M = (N , P) can be expanded to a countable model (M, N′) of ATR_{0}^{b} + FOT. Since ATR_{0}^{b} ⊢ PA, N′ ⊧ PA. By the MacDowell-Specker theorem (MS1961] and the Löwenheim- Skolem theorem, each countable model of PA has a countable end elementary extension. Applying this ω_{1} times, N′ has an ω_{1}-like end elementary extension ^{∗}N. We show that (M,^{∗}N) ⊧ ^{∗}ATR_{0}. By Proposition 5.3, (M,^{∗}N) ⊧ ^{∗}WKL_{0}. By hypothesis, Σ_{1}^{1}-SEP holds in M. By Theorem 8.5, Σ_{1}^{b}-SEP holds in (M,^{∗}N). FOT holds in (M,^{∗}N) because it holds in (M, N′) and ^{∗}N is an elementary extension of N′. We work in (M,^{∗}N) and show that Σ_{1}^{∗}-SEP holds.

Let ψ(m, u⃗), θ(m, u⃗) be Σ_{1}^{∗} formulas in which x does not occur, and suppose that

¬∃m[ψ(m, u⃗) ∧ θ(m, u⃗)].

We have

ψ(y, u⃗) = ∃z ψ′(z, y, u⃗), θ(y, u⃗) = ∃z θ′(z, y, u⃗)

where ψ′, θ′ are S-arithmetical. By Lemma 8.8, there exists H such that

∀m[∃z ψ′(z, m, u⃗) → (∃z < H)ψ′(z, m, u⃗)],
∀m[∃z θ′(z, m, u⃗) → (∃z < H)θ′(z, m, u⃗)].

Then

∀m[ψ(m, u⃗) ↔ (∃z < H)ψ′(z, m, u⃗)],
∀m[θ(m, u⃗) ↔ (∃z < H)θ′(z, m, u⃗)].

By Σ_{1}^{b}-SEP,

∃x∀m[((∃z < H)ψ′(z, m, u⃗) → (x)_{m} > 0)∧((∃z < H)θ′(z, m, u⃗) → (x)_{m} = 0)].

Therefore

∃x∀m[(ψ(m, u⃗) → (x)_{m} > 0) ∧ (θ(m, u⃗) → (x)_{m} = 0)].
⊣

Corollary 8.10. ^{∗}ATR_{0} + FOT is conservative with respect to ATR_{0}.

§9. The Theory ^{∗}Π_{1}^{1}-CA_{0}. We give two nonstandard counterparts of the theory Π_{1}^{1}-CA_{0} of Π_{1}^{1} comprehension, a theory with a bounded outer quantifier and a larger theory with an unbounded outer quantifier.

In the language L_{2}, Π_{1}^{1}-CA_{0} is defined as the theory

Π_{1}^{1}-CA_{0} = WKL_{0} + Π_{1}^{1}-CA.

Definition 9.1. In the language L_{2} ∪ ^{∗}L_{1}, the theories Π_{1}^{b}-CA_{0} and ∗Π_{1}^{1}-CA_{0} are defined by

Π_{1}^{b}-CA_{0} = ^{∗}WKL_{0} + Π_{1}^{b}-CA,
∗Π_{1}^{1}-CA_{0} = ^{∗}WKL_{0} + Π_{1}^{∗}-CA.

Since Π_{1}^{b} ⊆ Π_{1}^{∗}, we have:

Proposition 9.2. ^{∗}Π_{1}^{1}-CA_{0} ⊢ Π_{1}^{b}-CA_{0}.

As in the preceding section, we do not know whether or not Π_{1}^{b}-CA_{0} ⊢ ∗Π_{1}^{1}-CA_{0}.

Theorem 9.3. In ^{∗}WKL_{0}, Π_{1}^{b}-CA is equivalent to Π_{1}^{1}-CA.

Proof. Work in ^{∗}WKL_{0}. Assume Π_{1}^{b}-CA and let φ(m, Z, U⃗) be arithmetical. By STP, U⃗ has a lifting u⃗. Take an infinite H. By Lemmas 4.6 and 6.3 (iii),

∀m [∀Zφ(m, Z, U⃗) ↔ (∀z < H)\overline{φ}(m, z, u⃗)].

The formula (∀z < H)\overline{φ}(m, z, u⃗) is Π_{1}^{b}. By Π_{1}^{b}-CA, there exists x such that

∀m [(x)_{m} > 0 ↔ (∀z < H)\overline{φ}(m, z, u⃗)].

By STP there exists X = st(x). Then

∀m [m ∈ X ↔ ∀Zφ(m, Z, U⃗)],

and Π_{1}^{1}-CA is proved.

For the converse, assume Π_{1}^{1}-CA, and let θ(v, u⃗) be a Π_{1}^{b} formula. By Theorem 7.6, S-ACA holds, and therefore by Theorem 8.4 there is a Π_{1}^{S} formula ψ(v, k, z, u⃗) such that

θ(v, u⃗) ↔ ∀^{ns}w∃k ψ(v, k, w ↾ k, u⃗).

By ACA there exists a set Y such that

∀m∀k∀n[(m, k, n) ∈ Y ↔ ψ(m, k, n, u⃗)].

Then by Π_{1}^{1}-CA there is a set X such that

∀m[m ∈ X ↔ ∀f∃k (m, k, f ↾ k) ∈ Y].

Using Lemma 4.6 again,

∀f∃k (m, k, f ↾ k) ∈ Y ↔ ∀^{ns}w∃k ψ(v, k, w ↾ k, u⃗).

Therefore

∀m [m ∈ X ↔ θ(m, u⃗)].

By STP, X has a lifting x, and it follows that

∀m[(x)_{m} > 0 ↔ θ(m, u⃗)].
⊣

Corollary 9.4. Π_{1}^{b}-CA_{0} ⊢ Π_{1}^{1}-CA_{0} and Π_{1}^{∗}-CA_{0} ⊢ Π_{1}^{1}-CA_{0}.

Theorem 9.5. Every countable model M = (N , P) of Π_{1}^{1}-CA_{0} can be expanded to a model (M,^{∗}N) of Π_{1}^{b}-CA_{0} + FOT.

Proof. By Theorems 9.3 and 8.7. ⊣

Theorem 9.6. Every countable model M = (N , P) of Π_{1}^{1}-CA_{0} can be expanded to a model (M,^{∗}N) of ^{∗}Π_{1}^{1}-CA_{0} + FOT.

Proof. As in the proof of Theorem 8.9, but using Theorems 9.3 and 9.5 instead of Theorems 8.5 and 8.7, M can be expanded to a model (M,^{∗}N) of Π_{1}^{b}-CA_{0} + FOT such that ^{∗}N is ω_{1}-like. We work in (M,^{∗}N) and show that Π_{1}^{∗}-CA holds.

Let φ(m, u⃗) be a Π_{1}^{∗} formula in which x does not occur. Then φ(m, u⃗) = ∀zφ′(z, m, u⃗) where φ′ is S-arithmetical. By Lemma 8.8, there exists H such that

∀m[∃z¬φ′(z, m, u⃗) → (∃z < H)¬φ′(z, m, u⃗)],

so

∀m[φ(m, u⃗) ↔ (∀z < H)φ′(z, m, u⃗).

By Π_{1}^{b}-CA,

∃x∀m[(x)_{m} > 0 ↔ (∀z < H)φ′(z, m, u⃗)],

so

∃x∀m[(x)_{m} > 0 ↔ φ(m, u⃗)].
⊣

Corollary 9.7. ^{∗}Π_{1}^{1}-CA_{0} + FOT is conservative with respect to Π_{1}^{1}- CA_{0}.

This proves a conjecture stated in [HKK1984], page 1054.

In [HKK1984] and [En2005], conservation results were obtained for induction, choice, and dependent choice schemes in L_{2} which are stronger than Π_{1}^{1}-CA_{0}. To clarify the connection of those results with this paper, we restate the results for dependent choice in our present setting.

In L_{2}, Σ_{k}^{1}-dependent choice (Σ_{k}^{1}-DC) (where k > 0) is the scheme

∀X∃Y φ(X, Y, …) → ∀X∃Y [Y^{(0)} = X ∧ ∀mφ(Y^{(m)}, Y^{(m+1)}, …)] where φ(X, Y, …) ∈ Σ_{k}^{1} and Y^{(m)} = {n : (m, n) ∈ Y }. The theory Σ_{k}^{1}-DC_{0} is defined by

Σ_{k}^{1}-DC_{0} = RCA_{0} + Σ_{k}^{1}-DC.

We also write Σ_{∞}^{1}-DC = ⋃_{k∈ℕ} Σ_{k}^{1}-DC.

The theory Σ_{1}^{1}-DC_{0} implies ACA_{0} and is incomparable with ATR_{0} (H. Friedman; see [Si1999], Section VIII.5). Σ_{2}^{1}-DC_{0} is strictly stronger than Π_{1}^{1}-CA_{0}. The very strong theory Σ_{∞}^{1}-DC_{0} is called second order arithmetic with dependent choice.

Definition 9.8. In ^{∗}L_{1}, we define

Σ_{k+1}^{∗} = {∃xφ(x, …) : φ ∈ Π_{k}^{∗}}, Π_{k+1}^{∗} = {∀xφ(x, …) : φ ∈ Σ_{k}^{∗}}.

Σ_{k}^{∗}-dependent saturation (Σ_{k}^{∗}-DSAT) is the scheme

∀x∃yφ(x, y, …) → ∀x∃y[(y)_{0} = x ∧ ∀mφ((y)_{m}, (y)_{m+1}, …)]

where φ ∈ Σ_{k}^{∗}. We also write Σ_{∞}^{∗}-DSAT = ⋃_{k∈ℕ} Σ_{k}^{∗}-DSAT.

We omit the case k = 0 because Σ_{0}^{1}-DC is equivalent to Σ_{1}^{1}-DC, and Σ_{0}^{∗}-DSAT is equivalent to Σ_{1}^{∗}-DSAT. We now restate two theorems from [HKK1984] in our present setting.

Theorem 9.9. ([HKK1984], Theorem 3.4) Whenever 0 < k ≤ ∞, ∗WKL_{0} + Σ_{k}^{∗}-DSAT ⊢ Σ_{k}^{1}-DC_{0}.

Theorem 9.10. ([HKK1984], Theorem 4.1). Whenever 1 < k ≤ ∞, every countable model of Σ_{k}^{1}-DC_{0} can be expanded to a model of ^{∗}WKL_{0} + Σ_{k}^{∗}-DSAT + FOT.

Whenever 0 < k ≤ ∞, ^{∗}WKL_{0} + Σ_{k}^{∗}-DSAT + FOT is conservative with respect to Σ_{k}^{1}-DC_{0}.

In the case k = ∞ this is a conservation result for second order arithmetic with dependent choice. Theorem C in [En2005] can also be stated as a conservation result for second order arithmetic with dependent choice. Recall from the discussion after Theorem 7.10 that AUT is the sentence in the language ^{∗}L_{1} ∪ {j} which says that j is an automorphism of ^{∗}N with fixed point set N.

Theorem 9.11. ([En2005], Theorem C). Let Γ be the set of all formulas of the language ^{∗}L_{1} ∪ {j}. Every countable model of Σ_{∞}^{1}-DC_{0} can be expanded to a model of ^{∗}WKL_{0} + AUT + Γ-CA + FOT.

Hence the theory ^{∗}WKL_{0} + AUT + Γ-CA + FOT is conservative with respect to Σ_{∞}^{1}-DC_{0}.

References:

[CK1990] C.C. Chang and H.J. Keisler. Model Theory, Third Edition. Elsevier 1990.

[En2005] A. Enayat. From bounded arithmetic to second order arithmetic via automorphisms. To appear, Logic in Tehran: Proceedings of the Conference in Logic, Algebra, and Arithmetic held in Tehran, 2003. Available online at http://academic2.american.edu/∼enayat.

[HKK1984] C.W. Henson, M. Kaufmann, and H.J. Keisler. The strength of nonstandard methods in arithmetic. Journal of Symbolic Logic 49 (1984), pp. 1039-1058.

[HK1986] C.W. Henson and H.J. Keisler. On the strength of nonstandard analysis. Journal of Symbolic Logic 51 (1986), pp. 377-386.

[Ke2005] H.J. Keisler. The strength of nonstandard analysis. To appear. Available online at http://www.math.wisc.edu/∼keisler.

[MS1961] R. MacDowell and E. Specker. Modelle der arithmetic. Pp. 257-263 in Infinitistic Methods, Pergamon Press 1961.

[Si1999] S.G. Simpson. Subsystems of second order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag 1999.

[Ta1997] K. Tanaka. The self-embedding theorem of W KL_{0} and a non-standard method. Annals of Pure and Applied Logic 84 (1997), pp. 41-49.

DEPARTMENT OF MATHEMATICS

UNIVERSITY OF WISCONSIN

480 LINCOLN DRIVE MADISON WI 53706

E-mail: keisler@math.wisc.edu