NONSTANDARD ARITHMETIC AND RECURSIVE COMPREHENSION

H. JEROME KEISLER

Abstract. First order reasoning about hyperintegers can prove things about sets of integers. In the author’s paper Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic Logic 12 (2006), it was shown that each of the “big five” theories in reverse mathematics, including the base theory RCA_{0}, has a natural nonstandard counterpart. But the counterpart ^{∗}RCA_{0} of RCA_{0} has a defect: it does not imply the Standard Part Principle that a set exists if and only if it is coded by a hyperinteger. In this paper we find another nonstandard counterpart, ∗RCA_{0}′, that does imply the Standard Part Principle.

1. Introduction

In the paper [3], it was shown that each of the “big five” theories of second order arithmetic in reverse mathematics has a natural counterpart in the language of nonstandard arithmetic. In this paper we give another natural counterpart of the weakest these theories, the theory RCA_{0} of Recursive Comprehension.

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} that says that a set of integers exists if and only if it is coded by a hyperinteger. We say that a theory T′ in L_{2} ∪^{∗}L_{1} is conservative with respect to a theory T in L_{2} if every sentence of L_{2} provable from T′ is provable from T.

For each of the theories T = WKL_{0}, ACA_{0}, ATR_{0}, Π_{1}^{1}-CA_{0} in the language L_{2} of second order arithmetic, [3] gave a theory U of nonstandard arithmetic in the language ^{∗}L_{1} such that:

(1)  U + STP implies T and is conservative with respect to T.

The nonstandard counterpart ^{∗}RCA_{0} for RCA_{0} in [3] does not have property (1). The theory ^{∗}RCA_{0} + STP is not conservative with respect to RCA_{0}, and ∗RCA_{0} has only a weakened form of the STP. In this paper we give a new nonstandard counterpart ^{∗}RCA_{0}′ of RCA_{0} that does have property (1). That is, we give a theory U of nonstandard arithmetic in ^{∗}L_{1} such that the theory ∗RCA_{0}′ = U + STP implies RCA_{0} and is conservative with respect to RCA_{0}.

Date: January 31, 2010.

Section 2 contains background material. Our main results are stated in Section 3. In Section 4 we give the easy proof that ^{∗}RCA_{0}′ implies RCA_{0}. In Section 5 we give the more difficult proof that ^{∗}RCA_{0}′ is conservative with respect to RCA_{0}. Section 6 contains complementary results showing that various enhancements of ^{∗}RCA_{0}′ imply the Weak Koenig lemma, and thus are not conservative with respect to RCA_{0}. We also discuss some related open questions.

The results in this paper were presented at the Conference in Computability, Reverse Mathematics, and Combinatorics held at the Banff International Research Station in December 2008. I wish to thank the organizers and participants of that conference for helpful discussions on this work.

2. Preliminaries

We refer to [2] for background on models of arithmetic, and to [4] for a general treatment of reverse mathematics in second order arithmetic.

We follow the notation of [3], with one exception. We take the vocabulary of the first order language L_{1} of arithmetic to be {<, 0, 1, +, −^{·} , ·}. The operation −^{·} is cutoff subtraction, defined by n + (m −^{·} n) = max(m, n). Thus m −^{·} n = m − n if m ≥ n, and m −^{·} n = 0 if m < n. The additional function symbols p_{n} and (m)_{n} will be introduced here as defined symbols. (In [3] they were part of the underlying vocabulary of L_{1}.)

The language L_{2} of second order arithmetic is an extension of L_{1} with two sorts, N for natural numbers and P for sets of natural numbers. In L_{2}, the symbols of L_{1} are taken to be of sort N. L_{2} has variables X, Y, … of sort P and a membership relation ∈ of sort N × P. In either L_{1} or L_{2}, Δ_{0}^{0} is the set of all bounded quantifier formulas, Σ_{1}^{0} is the set of formulas of the form ∃m φ where φ ∈ Δ_{0}^{0}, and so on.

The expressions m ≤ n, m > n, m ≥ n will be used in the obvious way. We will sometimes use the expression m = n/r as an abbreviation for m · r = n. We let ℕ be the set of (standard) natural numbers. We sometimes also use ℕ to denote the structure (ℕ, <, 0, 1, +, −^{·} , ·).

The theory IΣ_{1}, Peano Arithmetic with Σ_{1}^{0} induction, has the usual axioms for linear order with first element 0, and the recursive rules for 0, 1, +, −^{·} , and ·, and the Σ_{1}^{0} Induction scheme

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

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

The theory RCA_{0} of arithmetic with restricted comprehension is the usual base theory for reverse mathematics. It is the theory in L_{2} that has the axioms of IΣ_{1}, and the Σ_{1}^{0} Induction scheme and Δ_{1}^{0} Comprehension scheme for formulas of L_{2}. Each model of RCA_{0} will be a pair (N , P) where P is a set of subsets of N. The theory WKL_{0} is RCA_{0} plus the Weak Koenig Lemma. It is well-known that WKL_{0} is not conservative with respect to RCA_{0} (see [4]).

The language ^{∗}L_{1} is the extension of L_{1} that has the sort N for standard integers and the sort ^{∗}N for hyperintegers. It has variables m, n, … of sort N and x, y, z, … of sort ^{∗}N. The universe of sort N is to be interpreted as a subset of the universe of sort ^{∗}N. ^{∗}L_{1} has the same vocabulary {< , 0, 1, +, −^{·} , ·} as L_{1}. All terms are considered to be terms of sort ^{∗}N, and terms built from variables of sort N are also considered to be terms of sort N. The atomic formulas are s = t, s < t where s, t are terms.

A bounded quantifier of sort N is an expression (∃m < s) or (∀m < s) where m is a variable of sort N and s a term of sort N. A bounded quantifier of sort ^{∗}N is an expression (∃x < t) or (∀x < t) where x is a variable of sort ^{∗}N which is not of sort N, and t a term. Thus (∃x < m) is a bounded quantifier of sort ^{∗}N, but (∃m < x) is not a bounded quantifier.

A Δ_{0}^{S} formula is a formula of ^{∗}L_{1} built from atomic formulas using connectives and bounded quantifiers of sorts N and ^{∗}N. A Σ_{1}^{S} formula is a formula of the form ∃n φ where φ is a Δ_{0}^{S} formula. (The superscript S indicates that the unbounded quantifiers are of the standard sort N.)

Definition 2.1. The theory BNA of Basic Nonstandard Arithmetic has the following axioms in the language ^{∗}L_{1}:

• The axioms of IΣ_{1} in the language L_{1},

• The sentence saying that < is a strict linear order.

• The Proper Initial Segment Axioms:

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

Note that the theory BNA by itself says nothing about the operations +, −^{·} , · on the nonstandard hyperintegers. We will work with theories that contain BNA and additional axioms.

For each formula φ if L_{1}, we let ^{∗}φ be a formula of ^{∗}L_{1} that is obtained from φ by replacing each bound variable in φ by a variable of sort ^{∗}N in a one to one fashion. A universal sentence in L_{1} is a sentence of the form ∀m⃗ φ(m⃗) where φ has no (bounded or unbounded) quantifiers.

Definition 2.2. Given a set Γ of formulas of L_{1}, Γ-Transfer (or Transfer for Γ) is the set of formulas φ → ^{∗}φ where φ ∈ Γ.

∀ Transfer, or ∀T, is Transfer for the set of all universal sentences in L_{1}.

A model of BNA will be an ordered structure of the form (N ,^{∗}N) where N is a model of IΣ_{1}, and ^{∗}N is a proper end extension of N. In a model (N ,^{∗}N) of BNA + ∀T, ^{∗}N will be the non-negative part of an ordered ring. In particular, the commutative, associative, distributive, and order laws will hold for +, ·, <, and −^{·} will have the property that y + (x −^{·} y) = max(x, y).

The theory ^{∗}ΔPA introduced in [3] has the axioms of BNA plus the following axiom scheme, called Internal Induction:

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

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

The theory ^{∗}ΣPA in [3] has the axioms of ^{∗}ΔPA plus the following axiom, called Σ_{1}^{S} Induction:

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

where φ(m, u⃗) is a Σ_{1}^{S} formula. (See [3], Definition 3.2 and Proposition 3.9).

Note that Internal Induction is an induction over a variable x of sort ^{∗}N, while Σ_{1}^{S} Induction is an induction over a variable m of sort N.

In this paper we will work in the combined language L_{2} ∪^{∗}L_{1}. We use the notation (x|y) (x divides y) as an abbreviation for the formula ∃z[x · z = y]. Using the axioms of IΣ_{1}, we can define p_{n} as the n-th prime in the usual way, and treat p_{n} as a function symbol of sort N → N. However, we will never write p_{x} where x is a variable of sort ^{∗}N. Following [3], we define the standard set relation X = st(x) by the formula

(∀n ≥ 0) [n ∈ X ↔ (p_{n}|x)].

The Upward Standard Part Principle (Upward STP) is the sentence

∀X∃x[X = st(x)]

which says that every set in P is coded by a hyperinteger. The Downward Standard Part Principle (Downward STP) is the sentence

∀x∃X[X = st(x)]

which says that every hyperinteger codes a set in P. The Standard Part Principle STP is the sentence

∀X∃x[X = st(x)] ∧ ∀x∃X[X = st(x)].

This is the conjunction of the Upward STP and the Downward STP.

As in [3], we say that a theory T′ in a language L′ is conservative with respect to a theory T in a language L ⊆ L′ if every sentence of L that is provable from T′ is provable from T.

It is shown in [3], Section 5, that the theory ^{∗}WKL_{0} = ^{∗}ΣPA + STP implies and is conservative with respect to WKL_{0}. In fact, ^{∗}WKL_{0} + ∀T is still conservative with respect to WKL_{0}.

There are two possible options for weakening ^{∗}WKL_{0} to get a theory that implies and is conservative with respect to RCA_{0}: either weaken STP or weaken ^{∗}ΣPA. The theory ^{∗}RCA_{0} introduced in [3] took the first option. The axioms of ^{∗}RCA_{0} are ^{∗}ΣPA plus the Upward STP and a very weak form of the Downward STP, called Δ_{1}^{0}-STP. As mentioned in the introduction, it was proved in [3] that ^{∗}RCA_{0} implies and is conservative with respect to RCA_{0}.

Yokoyama [6], [7] introduced a theory that is stronger than ^{∗}RCA_{0} but, like ^{∗}RCA_{0}, is conservative with respect to RCA_{0} and has a very weak form of the Downward STP.

In [1], Avigad considered several theories that extend RCA_{0} without the STP, and can be formulated in the combined language L_{2} ∪^{∗} L_{1} or in higher order analogues. When comparing the results of [1] with the present paper, note that the sort N in [1] corresponds to the sort ^{∗}N in this paper, and the standardness predicate S in [1] corresponds to the sort N in this paper. Thus the induction axiom for quantifier-free formulas of Primitive Recursive Arithmetic in [1] is the same thing as Internal Induction in this paper.

3. Statements of the Main Results

In this section we introduce a theory ^{∗}RCA_{0}′ that does what ^{∗}RCA_{0} does but contains the full Standard Part Principle. ^{∗}RCA_{0}′ takes the second option for weakening ^{∗}WKL_{0}; it is stronger than BNA + STP but weaker than ^{∗}WKL_{0}. We will prove that ^{∗}RCA_{0}′ implies and is conservative with respect to RCA_{0}.

We remark that the theory BNA + STP by itself says very little about sets of natural numbers. It does not even imply that there are infinite sets of sort P. One can get a model (N , P,^{∗}N) of BNA + STP with no infinite sets by taking N to be ℕ, taking P to be the set of finite subsets of ℕ, and taking ^{∗}N to be the non-negative part of the ring of polynomials over ℤ in a variable x such that ∀n n < x.

In order to get a theory that is strong enough to imply RCA_{0}, we will add nonstandard induction and comprehension principles. We will see in Section 6 that too strong a comprehension principle will give a theory that already implies WKL_{0}, and thus cannot be conservative with respect to RCA_{0}. For this reason, we need to introduce the class of special Δ_{0}^{S} formulas.

Definition 3.1. By a special Δ_{0}^{S} formula we mean a formula of ^{∗}L_{1} that is built from atomic formulas s = t, s < t, and divisibility formulas (n|t) where s, t are terms, using connectives and bounded quantifiers of sort N. A special Σ_{1}^{S} formula is a formula of the form ∃m φ where φ is a special Δ_{0}^{S} formula.

Every special Δ_{0}^{S} formula is a Δ_{0}^{S} formula, because the formula (n|t) is an abbreviation for the Δ_{0}^{S} formula (∃x < t + 1) n · x = t. Note that for each term s of sort N, the formula (s|t) is equivalent in BNA to the special Δ_{0}^{S} formula (∃n < s + 1)[n = s ∧ (n|t)].

Given a formula φ(m, u⃗) of ^{∗}L_{1}, the expression st(x) = φ(·, u⃗) stands for the formula

∀m [(p_{m}|x) ↔ φ(m, u⃗)].

Intuitively, st(x) = φ(·, u⃗) means that x codes the class {m : φ(m, u⃗)}.

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

• The axioms of BNA, • Special Σ_{1}^{S} Induction:

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

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

• Special Δ_{1}^{S} Comprehension:

∀m[φ(m, u⃗) ↔ ¬ψ(m, u⃗)] → ∃x st(x) = φ(·, u⃗)

where φ, ψ are special Σ_{1}^{S} formulas in which x does not occur.

• The Standard Part Principle STP.

Proposition 3.3. ^{∗}WKL_{0} implies ^{∗}RCA_{0}′.

Proof. The axioms of ^{∗}WKL_{0} already include BNA + STP. Σ_{1}^{S} Induction already contains Special Σ_{1}^{S} Induction. By Lemma 3.5 in [3], ^{∗}WKL_{0} implies the Δ_{1}^{S} Comprehension scheme, which contains Special Δ_{1}^{S} Comprehension.

□  □

We now state our main results.

Theorem 3.4. ^{∗}RCA_{0}′ implies RCA_{0}.

Theorem 3.5. ^{∗}RCA_{0}′ + ∀T is conservative with respect to RCA_{0}.

The proofs of these theorems will be given in the next two sections.

Before embarking on the proofs, we make some comments on the theory ∗RCA_{0}′. Theorems 3.4 and 3.5 show that ^{∗}RCA_{0}′ can serve as a base theory for reverse mathematics in the combined language L_{2} ∪^{∗} L_{1}. It implies the axioms of RCA_{0}, and can be express implications between stronger theories in the nonstandard setting.

The coding of sets by means of prime divisors that is used in ^{∗}RCA_{0}′ is inconvenient for some purposes. One can write down theories with the analogous axioms but a different coding of sets. The problem is that a different coding may result in a theory that is not conservative with respect to RCA_{0}. The coding by means of prime divisors has the major advantage of giving a theory that is conservative with respect to RCA_{0}. This coding also has the following nice properties:

st(x) ∩ st(y) ⊆ st(x + y), st(x) ∪ st(y) ⊆ st(xy), st(x) ∩ st(x + 1) = ∅.

One might also ask whether ^{∗}RCA_{0}′, or ^{∗}RCA_{0}′ + ∀T, can be used in its own right to carry out certain kinds of nonstandard arguments. We give some heuristic arguments suggesting the answer is yes, to a limited extent. Consider first the weaker theory BNA + ∀T in the language ^{∗}L_{1}. In BNA + ∀T, the hyperintegers can be extended in the usual way to the ordered field of hyperrational numbers (quotients of hyperintegers). One can define an infinitesimal as a hyperrational number whose absolute value is less than every positive rational, and a finite hyperrational number as one whose absolute value is less than some positive rational. In this theory one can develop Robinson’s infinitesimal treatment of limits and derivatives for rational functions.

As we will see in Section 6, in^{∗}RCA_{0}′ one can use special Δ_{1}^{S}-Comprehension and then the Downward STP to build sets, and in this way prove that for every finite hyperrational number x there is a unique real number r, the shadow of x, such that for each rational q,

q < r ⇒ q ≤ x and q < x ⇒ q ≤ r.

This opens up the possibility of proving theorems for hyperrational numbers and taking shadows to draw conclusions about real numbers.

One can also begin with a proof in a theory that is stronger than ^{∗}RCA_{0}′ and convert it to a proof in^{∗}RCA_{0}′, with the particular instance of the axiom in the stronger theory that was needed in the original proof replaced by a hypothesis in the new proof in ^{∗}RCA_{0}′. Section 6 has some examples of this.

Many methods that are available in ^{∗}WKL_{0} and are commonly used in nonstandard analysis are not available in ^{∗}RCA_{0}′ + ∀T. Internal induction and the overspill principle are not available. The comprehension axioms of ^{∗}RCA_{0}′ do not allow bounded quantifiers of sort ^{∗}N. Transfer for Π_{1}^{0} sentences is not available. All of these methods were left out for a good reason. We will show in Section 6 that under ^{∗}RCA_{0}′, each of them implies the Weak Koenig Lemma.

4. Proof that ^{∗}RCA_{0}′ Implies RCA_{0}

In this section we prove Theorem 3.4. Note that the Special Σ_{1}^{S} Induction and Special Δ_{1}^{S} Comprehension Axioms for ^{∗}RCA_{0}′ are sentences in the language ^{∗}L_{1} which has variables of sort ^{∗}N but no variables of sort P, and we must prove the Σ_{1}^{0}-Induction and Δ_{1}^{0}-Comprehension Axioms of RCA_{0}, which have variables of sort P but no variables of sort ^{∗}N.

Lemma 4.1. For every formula φ(x, …) of ^{∗}L_{1},

BNA ⊢ ∀x φ(x, …) → ∀n φ(n, …).
Proof. This follows at once from the axiom ∀n∃x(x = n).  □  □

The notation S(t) (meaning “t is standard”) is an abbreviation for the Σ_{1}^{S} formula ∃n n = t. For a tuple of terms t⃗ = (t_{1}, …, t_{k}), S(t⃗) means S(t_{1}) ∧ ⋯ ∧ S(t_{n}).

Lemma 4.2. For any term t(x⃗),

BNA ⊢ S(x⃗) → S(t(x⃗)).

Proof. Assume S(x⃗). This means that there exists a tuple m⃗ such that m⃗ = x⃗. By definition, t(m⃗) has sort N. By the rules of two-sorted logic, we

have S(t(m⃗)) and t(x⃗) = t(m⃗), and thus S(t(x⃗)).  □  □

We need the following definition from [3] (modified by replacing the expression (x_{i})_{t} > 0 by the equivalent expression (p_{t}|x_{i})).

Definition 4.3. 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 the formula of ^{∗}L_{1} 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 (p_{t}|x_{i}).

• 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 a Σ_{1}^{0} formula then \overline{φ} is a Σ_{1}^{S} formula. The next lemma is a lifting theorem from formulas of L_{2} to formulas of ^{∗}L_{1}. It was stated for ^{∗}ΔPA as Lemma 4.6 in [3], but also holds for BNA.

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

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

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

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

Proof. We first prove the result in the case that φ is an atomic formula. Work in BNA and assume that st(x⃗) = X⃗. If φ(m⃗) is an atomic formula of the form t(m⃗) = u(m⃗) or t(m⃗) < u(m⃗), then \overline{φ}(m⃗) is the same as φ(m⃗), so φ(m⃗) ↔ \overline{φ}(m⃗). If φ(m⃗, X) is an atomic formula of the form t(m⃗) ∈ X, then \overline{φ}(m⃗, x) is (p_{t(m⃗)}|x). By Lemma 4.2, ∃n n = t(m⃗). Therefore t(m⃗) ∈ X ↔ (p_{t(m⃗)}|x), as required.

The general case is now follows by induction on the complexity of φ, using the Proper Initial Segment Axioms for bounded quantifiers, and using STP

for second order quantifiers.  □  □

Proof of Theorem 3.5 from Theorem 5.1. Work in ^{∗}RCA_{0}′, and prove the axioms of RCA_{0}. The axioms of IΣ_{1} already belong to ^{∗}RCA_{0}′. For each instance θ of Σ_{1}^{0} Induction, \overline{θ} is an instance of special Σ_{1}^{S} Induction, which is obtained by replacing each subformula of the form t ∈ X_{i} by (p_{t}|x_{i}). Therefore by Lemma 4.4, Σ_{1}^{0} Induction holds. The argument for Δ_{1}^{0} Com-

prehension is similar.  □  □

5. Proof that ^{∗}RCA_{0}′ is Conservative With Respect to RCA_{0}

In this section we prove Theorem 3.5. Theorem 3.5 is a consequence of the following theorem and a result in [3].

Theorem 5.1. Let (N , P, N_{1}) be a model of ^{∗}ΣPA+Upward STP+∀T such that N_{1} has cofinality at least |P|. Then N_{1} has a substructure ^{∗}N such that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′ + ∀T.

Note that if (N , P, N_{1}) is countable, then N_{1} automatically has cofinality ℵ_{0} = |P|. So Theorem 5.1 shows in particular that for every countable model (N , P, N_{1}) of ^{∗}ΣPA+Upward STP + ∀T, N_{1} has a substructure ^{∗}N such that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′ + ∀T.

We first show that Theorem 3.5 follows from Theorem 5.1 above and Theorem 5.7 in [3].

Proof of Theorem 3.5 from Theorem 5.1. Assume Theorem 5.1. Let θ be a sentence of L_{2} that is consistent with RCA_{0}. Then RCA_{0} +θ has a countable model (N , P) such that N is not isomorphic to ℕ. By Theorem IX.2.1 in [4], there is a set P′ ⊇ P such that (N , P′) is a model of WKL_{0}. By Theorem 5.7 in [3], (N , P′) can be expanded to a countable model (N , P′, N_{1}) of ∗WKL_{0} such that N_{1} ≅ N. We now replace P′ by P and consider the structure (N , P, N_{1}). Since P ⊆ P′ and N_{1} ≅ N, (N , P, N_{1}) is a model of ∗ΣPA+Upward STP + ∀T + θ. By Theorem 5.1, N_{1} has a substructure ^{∗}N such that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′ + ∀T. Since θ holds in (N , P), it holds in (N , P,^{∗}N). This shows that θ is consistent with ^{∗}RCA_{0}′ + ∀T, so ^{∗}RCA_{0}′ + ∀T is conservative with respect to RCA_{0}, and Theorem 3.5

holds.  □  □

The remainder of this section is devoted to the proof of Theorem 5.1. Assume the hypotheses of Theorem 5.1.

For x, y ∈ N_{1}, write x ∼ y if there exists r ∈ N such that x ≤ ry and y ≤ rx. Write x ≪ y if rx < y for all r ∈ N. Note that in N_{1},

x ≪ y → x < y,
u ≤ x ≪ y ≤ z → u ≪ z,
u ∼ x ≪ y ∼ z → u ≪ z,
x ∼ y ↔ [¬x ≪ y ∧ ¬y ≪ x],
[x ≪ z ∧ y ≪ z] → x + y ≪ z.

We write x ≪ y if x^{k} ≪ y for each 0 < k ∈ ℕ. Note that in N_{1},

∀x∃y x ≪ y,
x ≪ y → x ≪ y,
u ≤ x ≪ y ≤ z → u ≪ z,
u ∼ x ≪ y ∼ z → u ≪ z,
[x ≪ z ∧ y ≪ z] → xy ≪ z.

We say that a set X ∈ P is bounded if (N , P) ⊧ ∃m∀n [n ∈ X → n < m].

We now show that there is a sequence ⟨U_{α}, α < κ⟩ of length κ ≤ |P| such that each U_{α} is an unbounded element of P, and for each unbounded X ∈ P there is a unique α < κ such that XΔU_{α} is bounded. To see that such a sequence exists, let P′ be the set of unbounded elements of P. Let P′′ be a subset of P′ that contains exactly one element of each equivalence class under the relation “XΔY is bounded”. Since P′′ ⊆ P, the elements of P′′ can be arranged in a sequence U_{α}, α < κ of length κ ≤ |P|. Then U_{α} has the required properties.

We claim that there is a sequence ⟨u_{α}, α < κ⟩ of elements of N_{1} \ N such that whenever α < β < κ:

• u_{α} ≪ u_{β}.

• N_{1} ⊧ (u_{α} is a product of distinct primes).

• For each n ∈ N, (p_{n}|u_{α}) in N_{1} if and only if n ∈ U_{α}. Given u_{α} for all α < β, we obtain u_{β} as follows. By the Upward STP, there

is an element u ∈ N_{1} such that st(u) = U_{β}. Take an element x ∈ N_{1} \ N. By Internal Induction in (N , N_{1}), there is an element y such that

N_{1} ⊧ y = Π{z : z < x ∧ z is prime ∧ (z|u)}.

At this point we use the hypothesis that |P| is at most the cofinality of N_{1}. Since β < κ ≤ |P| ≤ the cofinality of N_{1}, we may take an element v in N_{1} that is greater than u_{α} for all α < β, and take a prime w in N_{1} such that v ≪ w. Then u_{β} = wy has the required properties.

Let f be the unique function from P into N_{1} such that:

• f(∅) = 1.

• For each bounded Y ∈ P,

f(Y) = Π{p_{n} : n ∈ Y } ∈ N .

• f(U_{α}) = u_{α} for each α < κ.

• Whenever X, Y ∈ P, X ∩ Y = ∅, and Y is bounded,

f(X ∪ Y) = f(X)f(Y).

Note that whenever X, Y ∈ P and XΔY is bounded, f(X) ∼ f(Y), and in fact bf(X) = af(Y) where a = f(X \ Y) and b = f(Y \ X).

Lemma 5.2. Whenever X ∈ P and n ∈ N, n ∈ X if and only if (p_{n}|f(X)) in N_{1}.

Proof. The result is clear if X is bounded, and also if X = U_{α} for some α. If X is unbounded, then XΔU_{α} is bounded for some α < κ. We observe that bf(X) = af(U_{α}) where a is the product of primes p_{n} with n ∈ X \ U_{α} and b is the product of primes p_{n} with n ∈ U_{α} \ X. The result follows from

this observation.  □  □

Let

Q = {f(X) : X ∈ P and X is unbounded}.

Then for each x ∈ Q there exist a, b ∈ N and α < κ such that bx = au_{α}, and hence x ∼ u_{α}.

It will be convenient to have the freedom to subtract elements of N_{1} from each other. By ∀ Transfer, N_{1} satisfies the associative, commutative, and distributive laws for + and ·. We may therefore we introduce the ordered ring Z generated by N, and the ordered ring Z_{1} generated by N_{1}, with the vocabulary of L_{1} and the additional binary operation −. Thus N is the non-negative part of Z, and N_{1} is the non-negative part of Z_{1}.

Definition 5.3. We define ^{∗}Z to be the substructure of Z_{1} generated by Z ∪ Q, and ^{∗}N to be the non-negative part of ^{∗}Z.

Note that^{∗}Z is again an ordered ring. Since ∀ Transfer holds in (N , P, N_{1}) and ^{∗}N ⊆ N_{1}, ∀ Transfer holds in (N , P,^{∗}N). We show that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′. It is clear that the axioms of BNA hold in (N , P,^{∗}N). The next several lemmas will be used to prove that STP holds in (N , P,^{∗}N).

We call a finite subset P_{0} ⊆ P neat if each X ∈ P_{0} is unbounded and for each X, Y ∈ P_{0}, if XΔY is bounded then X = Y. A finite subset Q_{0} ⊆ Q is called neat if Q_{0} = {f(X) : X ∈ P_{0}} for some neat set P_{0} ⊆ P. We collect some easy observations about neat sets in a lemma.

Lemma 5.4. (i) For every finite set Q_{1} ⊆ Q there is a neat finite set Q_{0} ⊆ Q such that

Q_{1} ⊆ {ny : n ∈ N and y ∈ Q_{0}}.

(ii) Suppose Q_{0} is neat, x, y ∈ Q_{0}, and x < y. Then x ≪ y,

(iii) Suppose Q_{0} is neat, x, y are finite products of elements of Q_{0}, and x < y. Then x ≪ y.

Proof. (i) Let P_{1} be the finite subset of P such that f maps P_{1} onto Q_{1}. The relation “XΔY is bounded” partitions P_{1} into finitely many equivalence classes Q_{1}, …, Q_{k}. For each i let X_{i} = ⋂ Q_{i}. Then the set Q_{0} = {f(X_{1}), ⋯ f(X_{k})} has the required properties.

(ii) Let x = f(X), y = f(Y). For some α, β < κ, XΔU_{α} and Y ΔU_{β} are bounded. Therefore x ∼ u_{α} and y ∼ u_{β}. If α = β then XΔY is bounded, and since Q_{0} is neat we would have x = y, contradicting x < y. If β < α, then y ∼ u_{β} ≪ u_{α} ∼ x, so y ≪ x, again contradicting x < y. We must therefore have α < β, and by the above argument, x ≪ y.

(iii) Write x and y as finite products of elements on Q_{0} in decreasing order,

x = x_{0} ⋯ x_{k}, x_{0} ≥ ⋯ ≥ x_{k}, y = y_{0} ⋯ y_{ℓ}, y_{0} ≥ ⋯ ≥ y_{ℓ}.

Since x ≠ y, there must be a least j such that x_{j} ≠ y_{j} (adding 1’s to the end of the shorter product if necessary). Then x = zx′ and y = zy′ where z = 1 if j = 0, and z = x_{0} ⋯ x_{j−1} = y_{0} ⋯ y_{j−1} if j > 0. Hence x′ < y′. We cannot have x_{j} > y_{j}, because then by (ii), y_{i} ≪ x_{j} whenever j ≤ i ≤ ℓ, so y′ ≪ x_{j} ≤ x′, contradicting x′ < y′. Therefore x_{j} < y_{j}. Using (ii) again, we have x_{i} ≪ y_{j} for each i ≥ j, so x′ ≪ y_{j} ≤ y′ and hence x′ ≪ y′. Then for each r ∈ N, rx′ < y′, so rx = zrx′ < zy′ = y. Therefore x ≪ y, as

required.  □  □

We now give a useful representation for an arbitrary element of ^{∗}Z.

Definition 5.5. Let Q_{0} be a neat subset of Q and let x ∈ Z_{1}. An equation

x = m_{0}x_{0} + ⋯ + m_{k}x_{k}

is said to be neat for x over Q_{0} if k ∈ ℕ and:

• The equation is true.

• m_{i} ∈ Z for each i ≤ k.

• Each x_{i} is a finite product of elements of Q_{0} (counting 1 as the empty product).

• x_{0} < ⋯ < x_{k}.

Lemma 5.6. Each element x ∈ ^{∗}Z has a neat equation.

Proof. We show that the set of x ∈ Z_{1} that have neat equations contains Z ∪ Q and is closed under +, −, and ·. If m ∈ Z, then m = m · 1 itself is a neat equation for m with k = 0. If x ∈ Q, then x = 0 · 1 + 1 · x is a neat equation for x with k = 1. Suppose

x = m_{0}x_{0} + ⋯ + m_{k}x_{k}, y = n_{0}y_{0} + ⋯ + n_{ℓ}y_{ℓ}

are neat equations over neat sets Q_{0} and Q_{1} respectively. By Lemma 5.4 (i), we can assume without loss of generality that the union Q_{0} ∪ Q_{1} is neat. Since ^{∗}Z is an ordered ring, we may collect terms in the usual way to obtain

neat equations for x + y, x − y, and x · y over Q_{0} ∪ Q_{1}.  □  □

The next lemma shows that the set of non-zero values of m_{i}x_{i} is unique in a neat equation for an element x ∈ ^{∗}Z.

Lemma 5.7. Suppose x ∈ ^{∗}Z and

x = m_{0}x_{0} + ⋯ + m_{k}x_{k}, x = m′_{0}x′_{0} + ⋯ + m′_{ℓ}x′_{ℓ}

are two neat equations for x. Then

{m_{i}x_{i} : i ≤ k} ∪ {0} = {m′_{j}x′_{j} : j ≤ ℓ} ∪ {0}.

Proof. The result is trivial if x = 0. Assume x ≠ 0. By removing zero terms, we may assume that m_{i} ≠ 0 for each i ≤ k, and m′_{j} ≠ 0 for each j ≤ ℓ. We argue by induction on k, and prove that ℓ = k and m_{i}x_{i} = m′_{i}x′_{i} for each i ≤ k.

We assume the result holds for all k′ < k and prove it for k. We first prove that m_{k}x_{k} = m′_{ℓ}x′_{ℓ}. We have m_{k} ≠ 0 and m′_{ℓ} ≠ 0. By Lemma 5.4 (iii), for each i < k we have x_{i} ≪ x_{k}. Let y = x − m_{k}x_{k} and y′ = x − m′_{ℓ}x′_{ℓ}. If k = 0 then y = 0. If k > 0 then

y = m_{0}x_{0} + … + m_{k−1}x_{k−1}

is a sum of elements u such that |u| ≪ x_{k}. Therefore |y| ≪ x_{k}, and

|x| = |y + m_{k}x_{k}| ≤ |y| + |m_{k}|x_{k} < x_{k} + |m_{k}|x_{k} = (1 + |m_{k}|)x_{k}.

We also have

x_{k} ≤ |m_{k}|x_{k} = |x − y| ≤ |x| + |y| ≤ 2|x|.

The analogous results also holds for x′_{ℓ},

|x| < (1 + |m′_{ℓ}|)x′_{ℓ}, x′_{ℓ} < 2|x|.

It follows that

x′_{ℓ} ≤ 2|x| < (1 + |m_{k}|)x_{k}, x_{k} ≤ 2|x| < (1 + |m′_{ℓ}|)x′_{ℓ},

so x_{k} ∼ x′_{ℓ}. Using Lemma 5.4, we can find a neat subset Q_{0} of Q, a finite product z of elements of Q_{0}, and elements a, b ∈ N such that x_{k} = az and x′_{ℓ} = bz. It follows that

|m_{k}x_{k} − m′_{ℓ}x′_{ℓ}| = |(x − y) − (x − y′)| = |y − y′| ≪ x_{k}.

Then |(m_{k}a − m′_{ℓ}b)z| ≪ az, so we must have m_{k}a = m′_{ℓ}b. This proves that

m_{k}x_{k} = m′_{ℓ}x′_{ℓ}.

If k = 0 we are done. Suppose that k > 0. Then y = y′, and we have two neat equations for y. The desired conclusion now follows from the induction

hypothesis. This completes the proof.  □  □

We will use the above lemma to characterize the divisibility relation (m|x) where m ∈ N and x ∈ ^{∗}N. It is clear that if m divides x in ^{∗}N, then m divides x in N_{1}. That is, if ^{∗}N ⊧ ∃z mz = x then N_{1} ⊧ ∃z mz = x. However, the converse is false. For example, if f(X) ∈ Q and 2 ∉ X, then 2 divides 1 + f(X) in the sense of N_{1} but Lemma 5.11 below shows that 2 does not divide 1 + f(X) in the sense of ^{∗}N.

Note that for n, m ∈ N, n divides m in ^{∗}N if and only if n divides m in N_{1}, and also if and only if n divides m in N.

From now on, the expression (y|x) will be used in the sense of ^{∗}N, so that (y|x) means ^{∗}N ⊧ ∃z yz = x. When x and y belong to ^{∗}Z, we will use (y|x) to mean that |y| divides |x| in ^{∗}N.

It is clear that (0|x) if and only if x = 0, and that (m|0) for all m. This observation reduces the question of whether (m|x) to the case that m > 0 and x > 0.

The next four lemmas together will give a criterion for (m|x) when m ∈ N and x ∈ ^{∗}N.

Lemma 5.8. Suppose q ∈ N, X ∈ P, and x = f(X). Then (p_{q}|x) if and only if q ∈ X.

Proof. If (p_{q}|x), then q ∈ X by Lemma 5.2. If q ∈ X, then Y = X \ {q}

belongs to P, and x = f({q})f(Y) = p_{q}f(Y), so (p_{q}|x).  □  □

For q, n ∈ N and 0 < n let (n)_{q} be the largest m such that (p_{q})^{m} divides n.

Lemma 5.9. Suppose r ∈ N and y_{i} = f(Y_{i}) ∈ Q for each i ≤ k. Let y = y_{0} ⋯ y_{k}. Then (r|y) if and only if 0 < r and

(∀q < r)(r)_{q} ≤ |{i ≤ k : q ∈ Y_{i}}|.

Proof. Assume 0 < r. For each i ≤ k let U_{i} = {q ∈ Y_{i} : (p_{q}|r)} and Z_{i} = Y_{i} \ U_{i}. U_{i} is bounded and U_{i}, Z_{i} ∈ P by Δ_{1}^{0} Comprehension. Let n_{i} = f(U_{i}) ∈ N, and let z_{i} = f(Z_{i}). Let n = n_{0} ⋯ n_{k} and z = z_{0} ⋯ z_{k}. Note that n_{i} ≤ r, so n < r^{k+1} + 1. We have y_{i} = n_{i}z_{i} and thus y = nz. Since U_{i} ∩ Z_{i} is empty for each i, z is relatively prime to r in N_{1}. Therefore (r|y) if and only if (r|n), which in turn holds if and only if (r)_{q} ≤ (n)_{q} for each q. By Lemma 5.8, for each q we have (n)_{q} = |{i ≤ k : q ∈ Y_{i}}| if (p_{q}|r),

and (n)_{q} = 0 otherwise. This proves the lemma.  □  □

Lemma 5.10. Suppose m, r ∈ N and y_{i} = f(Y_{i}) ∈ Q for each i ≤ k. Let y = y_{0} ⋯ y_{k}. Then (r|my) if and only if either m = 0, or 0 < r and there exists n < r^{k+1} + 1 such that (r|mn) and (n|y).

Proof. Assume 0 < m and 0 < r. It is clear that (r|mn) and (n|y) implies (r|my). Suppose (r|my). Let n and z be as in the proof of Lemma 5.9. Then n < r^{k+1} + 1, and y = nz, so (n|y). Moreover, z is relatively prime to

r in N_{1} and (r|mnz), so (r|mn).  □  □

Lemma 5.11. Let x ∈ ^{∗}Z and let

x = m_{0}x_{0} + ⋯ + m_{k}x_{k}

be a neat equation for x. If r ∈ N, then (r|x) if and only if (r|m_{i}x_{i}) for each i ≤ k.

Proof. We prove the nontrivial direction. Suppose (r|x), and take z ∈ ^{∗}Z such that rz = x. z has a neat equation

z = n_{0}z_{0} + ⋯ + n_{ℓ}z_{ℓ}.

Then

rz = rn_{0}z_{0} + ⋯ + rn_{ℓ}z_{ℓ}.

is a neat equation for rz. By Lemma 5.7, k = ℓ, and rn_{i}z_{i} = m_{i}x_{i} for each

i ≤ k, and the result follows.  □  □

We now work in (N , P,^{∗}N) and prove the axioms of ^{∗}RCA_{0}′. We have already shown that the axioms of BNA hold.

Lemma 5.12. The STP holds in (N , P,^{∗}N).

Proof. Lemma 5.8 shows that X = st(f(X)) for every X ∈ P. This proves the upward STP.

For the Downward STP, we must show that for each x ∈ ^{∗}N the set st(x) = {q ∈ N : (p_{q}|x)} belongs to P. For x ∈ ^{∗}Z we write st(x) = st(|x|). Let

x = m_{0}x_{0} + ⋯ + m_{k}x_{k}

be a neat equation for x. By Lemma 5.11,

st(x) = st(m_{0}x_{0}) ∩ ⋯ ∩ st(x_{k}m_{k}).

For each i, st(m_{i}) ∈ P by Δ_{1}^{0} Comprehension in (N , P). Fix a positive i ≤ k and let x_{i} = y_{0} ⋯ y_{ℓ} where each y_{j} ∈ Q. Then y_{j} = f(Y_{j}) for some Y_{j} ∈ P. By Lemmas 5.9 and 5.10, (p_{q}|m_{i}x_{i}) if and only if either (p_{q}|m_{i}) or q ∈ Y_{j} for some j ≤ ℓ. Therefore

st(m_{i}x_{i}) = st(m_{i}) ∪ st(y_{0}) ∪ ⋯ ∪ st(y_{ℓ}).

We have st(m_{i}) ∈ P and st(y_{j}) ∈ P for each j ≤ ℓ. Since P is closed under finite unions and finite intersections, it follows that st(x) ∈ P, and

the Downward STP is proved.  □  □

For Theorem 5.1, it remains to prove Special Σ_{1}^{S} Induction and Special Δ_{1}^{S} Comprehension. To prepare for this we prove two more lemmas. The next lemma says that each term of sort ^{∗}N with constants from ^{∗}N and variables m⃗ can be represented as one of a finite set of “neat polynomials”.

Let Q_{0} be a neat subset of Q. By a neat polynomial over Q_{0} we mean an expression P (m⃗, d⃗) of the form

P_{0}(m⃗, d⃗)z_{0} + ⋯ + P_{h}(m⃗, d⃗)z_{h},

where h ∈ ℕ, d⃗ is a tuple of constants from N, each P_{i}(m⃗, d⃗) is a polynomial in m⃗ with coefficients in Z, each z_{i} is a finite product of elements of Q_{0}, and z_{0} < … < z_{h}. For readability, we will suppress the parameters d⃗, writing P (m⃗) instead of P (m⃗, d⃗).

Recall that by Lemmas 5.4 and 5.6, for each tuple x⃗ of elements of ^{∗}N there is a neat set Q_{0} such that each member of x⃗ has a neat equation over Q_{0}.

Lemma 5.13. Let x⃗ be a tuple of constants from ^{∗}N, m⃗ be a tuple of variables of sort N, and t(m⃗, x⃗) be a term in ^{∗}L_{1}. Let Q_{0} be a neat set such that each member of x⃗ has a neat equation over Q_{0}. Then there is a finite sequence P^{(0)}(m⃗), …, P^{(k)}(m⃗) of neat polynomials over Q_{0}, and a finite sequence ψ_{0}(m⃗), …, ψ_{k}(m⃗) of quantifier-free formulas of L_{1} with constants from N, such that

N ⊧ ∀m⃗[ψ_{0}(m⃗) ∨ ⋯ ∨ ψ_{k}(m⃗)]

and for each i ≤ k,

(N ,^{∗}N) ⊧ ∀m⃗[ψ_{i}(m⃗) → t(m⃗, x⃗) = P^{(i)}(m⃗)].

Proof. We argue by induction on the complexity of t(m⃗, x⃗). If t(m⃗, x⃗) is a single variable m of sort N, the result holds with P^{(0)} = m and ψ_{0} being the true formula. If t(m⃗, x⃗) is a single constant x ∈ ^{∗}N, the result holds with P^{(0)} being a neat equation for x over Q_{0}. Assume the result holds for a term t(m⃗, x⃗) with the neat polynomials and formulas

P^{(0)}(m⃗), …, P^{(k)}(m⃗), ψ_{0}(m⃗), …, ψ_{k}(m⃗),

and also holds for a term u(m⃗, x⃗) with the neat polynomials and formulas

R^{(0)}(m⃗), …, R^{(ℓ)}(m⃗), θ_{0}(m⃗), …, θ_{ℓ}(m⃗).

Then the lemma holds for the sum t(m⃗, x⃗) + u(m⃗, x⃗) with the neat polynomials and quantifier-free formulas

P^{(i)} + R^{(j)}, ψ_{i} ∧ θ_{j}, i ≤ k and j ≤ ℓ.

Similarly, the lemma holds for the product t(m⃗, x⃗) · u(m⃗, x⃗) with the neat polynomials and quantifier-free formulas

P^{(i)} · R^{(j)}, ψ_{i} ∧ θ_{j}, i ≤ k and j ≤ ℓ.

To deal with the cutoff difference of two terms, we need a quantifier-free formula that expresses the property that the value of one neat polynomial is greater than the value of another. By adding terms with zero coefficients, each pair of neat polynomials P^{(i)}(m⃗), R^{(j)}(m⃗) over Q_{0} can be put in the form

P_{0}(m⃗, c⃗)z_{0} + ⋯ + P_{h}(m⃗, c⃗)z_{h},
R_{0}(m⃗, c⃗)z_{0} + ⋯ + R_{h}(m⃗, c⃗)z_{h},

with the same sequence z_{0}, …, z_{h} of finite products of elements of Q_{0}. There is a quantifier-free formula φ_{i,j}(m⃗) with parameters in N that states that for some a ≤ h, P_{a}(m⃗, c⃗) > R_{a}(m⃗, c⃗), and P_{b}(m⃗, c⃗) = R_{b}(m⃗, c⃗) whenever a < b ≤ h. We have z_{0} < … < z_{h}, and by Lemma 5.4, z_{0} ≪ … ≪ z_{h}. It follows that for all m⃗ in N, φ_{i,j}(m⃗) holds if and only if P^{(i)}(m⃗) > R^{(j)}(m⃗). Therefore the lemma holds for the cutoff difference t(m⃗, x⃗) −^{·} u(m⃗, x⃗) with the sequence of neat polynomials

P^{(i)} − R^{(j)}, i ≤ k and j ≤ ℓ

followed by the zero polynomial, and the sequence of quantifier-free formulas

ψ_{i} ∧ θ_{j} ∧ φ_{i,j}, i ≤ k and j ≤ ℓ

followed by the “otherwise” formula

¬ ⋁_{i=0}^{k} ⋁_{j=0}^{ℓ} ψ_{i} ∧ θ_{j} ∧ φ_{i,j}.

□  □

The next lemma reduces a special Δ_{0}^{S} formula with constants from ^{∗}N and variables of sort N to a Δ_{0}^{0} formula in L_{2} with constants from N and P and variables of sort N.

Lemma 5.14. Let x⃗ be a tuple of constants from ^{∗}N, and m⃗ be a tuple of variables of sort N. For each special Δ_{0}^{S} formula φ(m⃗, x⃗) there is a tuple d⃗ of constants from N, a tuple Y⃗ of sets in P, and a Δ_{0}^{0} formula φ̂(m⃗, d⃗, Y⃗) in L_{2} such that in (N , P,^{∗}N),

∀m⃗ [φ(m⃗, x⃗) ↔ φ̂(m⃗, d⃗, Y⃗)].

Proof. By Lemma 5.4, there is a neat set Q_{0} such that each member of x⃗ has a neat equation over Q_{0}. Let P_{0} = f^{−1}(Q_{0}) and let Y⃗ be a tuple of sets that enumerates P_{0}.

Let t(m⃗, x⃗) be a term of sort ^{∗}N in ^{∗}L_{1}. Let

P^{(0)}(m⃗), …, P^{(k)}(m⃗), ψ_{0}(m⃗), …, ψ_{k}(m⃗)

be as in Lemma 5.13, and let d⃗ be the tuple of constants from ^{∗}N that occur in these polynomials and formulas. Let

P^{(ℓ)}(m⃗) = P_{0}^{(ℓ)}(m⃗, d⃗)z_{0} + ⋯ + P_{h_{ℓ}}^{(ℓ)}(m⃗, d⃗)z_{h_{ℓ}}.

We first prove the lemma for atomic formulas of the form 0 < t(m⃗, x⃗). Let φ̂(m⃗, d⃗, Y⃗) be the quantifier-free formula that says that for each ℓ ≤ k, if ψ_{ℓ}(m⃗) then there is an i ≤ h such that P_{i}^{(ℓ)}(m⃗, d⃗) > 0 and P_{j}^{(ℓ)}(m⃗, d⃗) = 0 whenever i < j ≤ h_{ℓ}. Then the lemma holds when φ is 0 < t(m⃗, x⃗), with the formula φ̂(m⃗, d⃗, Y⃗). Note that in this case, Y⃗ does not occur at all in the formula φ̂(m⃗, d⃗, Y⃗).

Using the facts that s < t if and only if 0 < t −^{·} s, and s = t if and only if ¬(s < t) ∧ ¬(t < s), we see that the lemma holds for all atomic formulas of the forms s < t and s = t.

We next deal with the formulas of the form (r|t(m⃗, x⃗)). We may assume that r belongs to the tuple of variables m⃗. Fix an assignment a⃗ for m⃗ in N. Let b be the resulting assignment for r. In the case that t(a⃗, x⃗) = 0, the formula (b|t(a⃗, x⃗)) is true. In the case that b = 0 and t(a⃗, x⃗) ≠ 0, the formula (b|t(a⃗, x⃗)) is false. Suppose that b ≠ 0 and t(a⃗, x⃗) ≠ 0. By Lemma 5.13, there is an ℓ ≤ k such that ψ_{ℓ}(a⃗, d⃗) holds. Then t(a⃗, x⃗) = P^{(ℓ)}(a⃗). For each i ≤ h_{ℓ}, let t_{i} = P_{i}^{(ℓ)}(a⃗, d⃗). We have t_{i} ∈ Z. Since Q_{0} is neat, we have a neat equation

t(a⃗, x⃗) = t_{0}z_{0} + ⋯ + t_{h}z_{h}

over Q_{0}.

For each i ≤ h_{ℓ}, z_{i} is a finite product z_{i} = z_{i,0} ⋯ z_{i,k_{i}} of elements of Q_{0}, and for each j ≤ k_{i}, z_{i,j} = f(Z_{i,j}) for some Z_{i,j} in the sequence Y⃗. Applying Lemma 5.11, we see that (b|t(a⃗, x⃗)) if and only if (b|P_{i}^{(ℓ)}(a⃗, d⃗)z_{i}) for each i ≤ h_{ℓ}. Fix an i ≤ h_{ℓ}. By Lemma 5.10, we have (b|P_{i}^{(ℓ)}(a⃗, d⃗)z_{i}) if and only if either P_{i}^{(ℓ)}(a⃗, d⃗) = 0, or there exists n < (c^{k_{i}+1}) + 1 such that (b|nP_{i}^{(ℓ)}(a⃗, d⃗)) and (n|z_{i}). By Lemma 5.9, we have (n|z_{i}) if and only if

(∀q < n)(n)_{q} ≤ |{j ≤ k_{i} : q ∈ Z_{i,j}}|.

This shows that (r|t(m⃗, x⃗)) is expressible by a Δ_{0}^{0} formula φ̂(m⃗, d⃗, Y⃗) in L_{2}, so the lemma is proved for the case that φ(m⃗, c⃗, x⃗) is of the form (r|t(m⃗, x⃗)).

The lemma for an arbitrary special Δ_{0}^{S} formula φ(m⃗, c⃗, x⃗) now follows by

a straightforward induction on the complexity of φ.  □  □

Lemma 5.15. Special Σ_{1}^{S} Induction holds in (N , P,^{∗}N).

Proof. Let φ(n⃗, x⃗) be a special Σ_{1}^{S} formula where x⃗ is a tuple of constants from ^{∗}N. Then φ(n⃗, x⃗) is ∃m ψ(m, n⃗, x⃗) where ψ is a special Δ_{0}^{S} formula. By Lemma 5.14 there is a tuple d⃗ of constants from N, a tuple Y⃗ of sets in P, and a Δ_{0}^{0} formula ψ̂(m, n⃗, d⃗, Y⃗) in L_{2} such that

∀m∀n⃗ [ψ(m, n⃗, x⃗) ↔ ψ̂(m, n⃗, d⃗, Y⃗)].

Let φ̂(n⃗, d⃗, Y⃗) be the Σ_{1}^{0} formula ∃m ψ̂(m, n⃗, d⃗, Y⃗). Then

∀n⃗ [φ(n⃗, x⃗) ↔ φ̂(n⃗, d⃗, Y⃗)].

Thus Special Σ_{1}^{S} Induction for φ(n⃗, x⃗) follows from Σ_{1}^{0} Induction for φ̂(n⃗, d⃗, Y⃗)

in (N , P).  □  □

Lemma 5.16. Special Δ_{1}^{S} Comprehension holds in (N , P,^{∗}N).

Proof. This is proved by an argument similar to the preceding lemma, using

Δ_{1}^{0} Comprehension in (N , P) and the upward STP.  □  □

It now follows from Lemmas 5.12, 5.15 and 5.16 that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′, so Theorem 5.1 is proved.

6. Open Questions and Complementary Results

6.1. Open Questions. A general question is: How much one can strengthen ∗RCA_{0}′ and still be conservative with respect to RCA_{0}? Here are some natural cases.

Question 6.1. If one strengthens ^{∗}RCA_{0}′ or ^{∗}RCA_{0}′ + ∀T by adding Σ_{1}^{S} Induction, is the resulting theory still conservative with respect to RCA_{0}?

Question 6.2. If one strengthens ^{∗}RCA_{0}′ by adding Transfer for universal formulas (rather than sentences), is the resulting theory still conservative with respect to RCA_{0}?

The above two theories do not imply WKL_{0}. To see this, let (N , P) be a model of RCA_{0} plus the negation of the Weak Koenig Lemma whose first order part is N = ℕ. An example of such a model is the minimal model where P is the set of recursive subsets of ℕ (see [4], Section VIII.1). By the compactness theorem, N has an elementary extension N_{1} of cofinality at least |P| such that (N , P, N_{1}) satisfies the Upward STP. Since N = ℕ, (N , P, N_{1}) is also a model of^{∗}ΣPA+∀T. Theorem 5.1 gives us a substructure ∗N of N_{1} such that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′ + ∀T. Using N = ℕ, it is easily seen that (N , P,^{∗}N) also satisfies Σ_{1}^{S} Induction and Transfer for universal formulas.

Question 6.3. If one strengthens ^{∗}RCA_{0}′ + ∀T by adding a symbol for exponentiation to the vocabulary, is the resulting theory still conservative with respect to RCA_{0}?

Our results in this paper depend on the particular way we code sets of natural numbers by hyperintegers, via prime divisors. Another general question is

Question 6.4. What are the nonstandard counterparts of RCA_{0} when one uses a different method of coding sets of natural numbers by hyperintegers?

6.2. Coding Real Numbers by Hyperrational Numbers. In this subsection we consider a question related to Question 6.4, concerning the representation of real numbers as shadows of hyperrational numbers. Following [4], in RCA_{0} the rational numbers are introduced in the usual way as quotients of integers, and a real number is defined as a sequence ⟨q_{n}⟩ of rational numbers such that |q_{k} − q_{n}| ≤ 2^{−k} whenever k < n ∈ N, and two real numbers ⟨q_{n}⟩, ⟨r_{n}⟩ are defined to be equal if (∀n)|q_{n} − r_{n}| ≤ 2^{1−n}. In ^{∗}RCA_{0}′ + ∀T, the hyperrational numbers are introduced in the usual way as quotients of hyperintegers. Both the real numbers and the hyperrational numbers are ordered fields which contain the rational numbers. A hyperrational number x/y is finite if ∃n |x/y| < n.

Definition 6.5. In ^{∗}RCA_{0}′ + ∀T, a real number r is a shadow of a hyperrational number x/y if for all rational numbers q,

q < r ⇒ q ≤ x and q < x ⇒ q ≤ r.

By the Upward Shadow Principle we mean the statement that every real number is the shadow of some hyperrational number.

By the Downward Shadow Principle we mean the statement that every finite hyperrational number has a shadow.

We will see below that the Downward Shadow Principle is provable in ∗RCA_{0}′ + ∀T. Our question concerns the Upward Shadow Principle.

Question 6.6. Is the theory

∗RCA_{0}′ + ∀T + Upward Shadow Principle

conservative with respect to RCA_{0}? Does it imply WKL_{0}?

It is obvious that in ^{∗}RCA_{0}′ +∀T, every hyperrational number has at most one shadow (up to equality).

Proposition 6.7. The Downward Shadow Principle is provable in ^{∗}RCA_{0}′+ ∀T.

Proof. Work in ^{∗}RCA_{0}′ + ∀T. Let x/y be a finite hyperrational number. By Special Δ_{1}^{S}-comprehension, there exists z such that

st(z) = {(n, k) : (k/2^{n}) ≤ (x/y) < ((k + 1)/2^{n})}.

By the Downward STP, there is a set Z such that Z = st(z). For each n let q_{n} = k/2^{n} where k is the unique number such that (n, k) ∈ Z. By Theorem 3.4, Δ_{1}^{0}-Comprehension holds. By Δ_{1}^{0}-Comprehension, the sequence ⟨q_{n}⟩ exists. It is easily seen that whenever n < m, q_{n} ≤ q_{m} ≤ (x/y) < q_{n} + 2^{−n}, so ⟨q_{n}⟩ is a real number. It is clear that ⟨q_{n}⟩ is a shadow of (x/y). □ □

Proposition 6.8. The Upward Shadow Principle is provable in ^{∗}WKL_{0}.

Proof. Work in ^{∗}WKL_{0}. It follows from Internal Induction that the hyperrational numbers form an ordered field. Let ⟨q_{n}⟩ be a real number. We may assume that ⟨q_{n}⟩ is positive. By STP, there exists u such that st(u) = ⟨q_{n}⟩. Let z be a positive infinite hyperinteger. Then

(∀n)(∃x < z)(∃y < z)(∀m < n)(q_{m} ≤ (x/y) < q_{m} + 2^{−m}),

and the inner part

(∃x < z)(∃y < z)(∀m < n)(q_{m} ≤ (x/y) < q_{m} + 2^{−m})

is expressible as a Δ_{0}^{S} formula θ(n, u, z). By Overspill, there is an infinite v such that θ(v, u, z). Therefore

(∃x < z)(∃y < z)(∀m)(q_{m} ≤ (x/y) < q_{m} + 2^{−m}).
It follows that ⟨q_{n}⟩ is a shadow of (x/y).  □  □

Proposition 6.9. The theory

∗RCA_{0}′ + ∀T + (Every shadow is rational)

is conservative with respect to RCA_{0}. Hence the Upward Shadow Principle is not provable in ^{∗}RCA_{0}′ + ∀T.

Proof. It is enough to show that in the model of ^{∗}RCA_{0}′ + ∀T constructed in the proof of Theorem 3.5, the shadow of each finite hyperrational number (x/y) is rational. By Lemmas 5.4 and 5.6, x and y have neat equations

x = m_{0}x_{0} + ⋯ + m_{k}x_{k}, y = n_{0} + ⋯ + n_{ℓ}y_{ℓ}

over the same neat set Q_{0}. If x ≪ y, then the shadow of (x, y) is zero. Suppose not x ≪ y. We cannot have y ≪ x, because (x/y) is finite. Therefore x ∼ y, and x_{k} ∼ y_{ℓ}. Since x_{k} and y_{ℓ} are finite products of elements of Q_{0}, we must have x_{k} = y_{ℓ}. We say that a hyperrational number x/y is infinitesimal if |x| ≪ |y|. One can now show that there are infinitesimal hyperrational numbers ε, δ such that

x = (m_{k} + ε)x_{k}, y = (n_{ℓ} + δ)x_{k},

and hence that |(x/y) − (m_{k}/n_{ℓ})| is infinitesimal, so (m_{k}/n_{ℓ}) is the shadow

of (x/y).  □  □

6.3. Theories that Imply WKL_{0}. In this subsection we will show that several theories that appear to be only slightly stronger than^{∗}RCA_{0}′ actually imply WKL_{0}. Let T_{0} be the theory

T_{0} = RCA_{0} + BNA + STP.

We shall give some rather weak statements U in the language ^{∗}L_{1} such that

T_{0} + U implies WKL_{0}.

For any such statement U, it follows from Theorem 3.4 that ^{∗}RCA_{0}′ + U implies WKL_{0}, and thus ^{∗}RCA_{0}′ + U cannot be conservative with respect to RCA_{0}.

A key idea in these results will be to keep track of the Overspill scheme. Recall from [3] that Overspill is the set of formulas

∀n φ(n, y⃗) → ∃x [¬S(x) ∧ φ(x, y⃗)],

where φ(x, y⃗) is a Δ_{0}^{S} formula of ^{∗}L_{1}.

It is sometimes helpful to interpret Overspill as a statement about the undefinability of S(x). In a model (N ,^{∗}N) of BNA, we say that S(x) is definable by a Δ_{0}^{S} formula φ(x, y⃗) if ∃y⃗∀x[S(x) ↔ φ(x, y⃗)].

Remark 6.10. In a model of BNA, Overspill holds if and only if S(x) is not definable by a Δ_{0}^{S} formula.

Proof. Let φ(x, y⃗) be a Δ_{0}^{S} formula. Then the following are equivalent in BNA:

Overspill holds for φ(x, y⃗).

∀y⃗[∀n φ(n, y⃗) → ∃x [¬S(x) ∧ φ(x, y⃗)]].

¬∃y⃗[∀nφ(n, y⃗) ∧ ∀x[φ(x, y⃗) → S(x)]].

¬∃y⃗∀x[φ(x, y⃗) ↔ S(x)].

S(x) is not definable by φ(x, y⃗).  □  □

The following result shows that ^{∗}RCA_{0}′+Transfer for Π_{1}^{0} sentences implies WKL_{0}. This can be compared with Theorem 3.5 and the discussion after Question 6.2, which give other forms of Transfer that do not imply WKL_{0} in ^{∗}RCA_{0}′.

Proposition 6.11. In the theory T_{0}, each scheme in the following list implies the next.

(1) Transfer for Π_{1}^{0} sentences

(2) Internal Induction

(3) Overspill

(4) WKL_{0}

Proof. We work in T_{0}. First assume Transfer for Π_{1}^{0} sentences. Let φ(y, u⃗) be a Δ_{0}^{S} formula, and assume that

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

Then

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

By Σ_{1}^{0} Induction,

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

By Transfer for Π_{1}^{0} sentences,

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

Therefore ∀x (∀y < x) φ(y, u⃗), and hence ∀y φ(y, u⃗), so Internal Induction holds.

The proof of Lemma 3.7 in [3], with minor changes, shows that in BNA, Internal Induction implies Overspill.

The proof of Theorem 5.4 in [3] shows that Overspill implies the Weak

Koenig Lemma.  □  □

Remark 6.12. It follows from Theorem 5.7 in [3] that ^{∗}WKL_{0}+Transfer for first order sentences is conservative with respect to WKL_{0}, so ^{∗}RCA_{0}′ plus each of the theories in Proposition 6.11 is conservative with respect to WKL_{0}.

By Proposition 6.11, any extension of ^{∗}RCA_{0}′ which is conservative with respect to RCA_{0} must have models (N , P,^{∗}N) such that Δ_{0}^{0}-Induction fails in ^{∗}N. The next proposition shows that in the model of ^{∗}RCA_{0}′ constructed in the proof of Theorem 3.5, Δ_{0}^{0}-Induction fails dramatically in ^{∗}N.

Proposition 6.13. In the model (N , P,^{∗}N) constructed in Theorem 5.1, S(x) is definable by a Δ_{0}^{S} formula φ(x) whose only free variable is x, and thus Overspill fails. In particular, S(x) is definable by the Δ_{0}^{S} formula

(∀y < x)[(2|y) ∨ (2|y + 1)].

Proof. The sentence ∀m[(2|m) ∨ (2|m + 1)] is provable from IΣ_{1} and thus holds in N, Therefore ∀x[S(x) → φ(x)].

For the other direction, suppose ¬S(x), that is, x ∈ ^{∗}N but x ∉ N. By definition, the set U_{0} belongs to P and is unbounded. Then st(u_{0}) = U_{0}, so u_{0} ∉ N. Let z = min(x − 1, u_{0}). Then z < x and z ∉ N. By Lemma 5.6, z must have a neat equation z = m_{0} + m_{1}z_{1} where m_{0} ∈ Z, 0 < m_{1} ∈ N, z_{1} = u_{0}/a where a ∈ N, a is a product of distinct primes in N, and a divides u_{0}. We may assume that z_{1} is not divisible by 2, because if it is we can replace a by 2a and m_{1} by 2m_{1}. In N we may write m_{1} = bn_{1} where b is a power of 2 and n_{1} is not divisible by 2. Let y = m_{0} + n_{1}z_{1}. Then y < x, n_{1}z_{1} is not divisible by 2, and y = m_{0} + n_{1}z_{1} is a neat equation. By Lemma 5.11, neither y nor y + 1 is divisible by 2. Therefore ¬φ(x), and the result

is proved.  □  □

We now look at what happens when a weak comprehension axiom is added to ^{∗}RCA_{0}′. We recall some notation from [3]. An S-arithmetical formula is a finite string of quantifiers of sort N followed by a Δ_{0}^{S} formula. Δ_{0}^{S} Comprehension (Δ_{0}^{S}-CA) is the scheme

(2)  ∃z∀m[(p_{m}|z) ↔ φ(m, u⃗)]

where φ(m, u⃗) is a Δ_{0}^{S} formula in which z does not occur. S-ACA is the stronger scheme (2) where φ(m, u⃗) is an S-arithmetical formula. It is shown in [3], Lemma 3.4, that Δ_{0}^{S}-CA is provable in ^{∗}ΔPA, and hence in ^{∗}WKL_{0}. It is shown in [3], Section 7, that the theory ^{∗}ACA_{0} = ^{∗}WKL_{0} + S-ACA implies and is conservative with respect to ACA_{0}.

The next result shows that Theorem 3.5 would fail if we added the Δ_{0}^{S}-CA scheme to ^{∗}RCA_{0}′.

Proposition 6.14. Let T_{1} be the theory

T_{1} = T_{0} + Δ_{0}^{S}-CA.

(i) Any model of T_{1} in which Overspill fails satisfies S-ACA and ACA_{0}. (ii) T_{1} implies WKL_{0}.

Proof. It is clear that (i) and Proposition 6.11 implies (ii). To prove (i), we work in T_{1} and prove S-ACA. Suppose that some instance of the Overspill scheme fails. By Remark 6.10, S(x) is definable by a Δ_{0}^{S} formula φ(x, y⃗). Then for some y⃗ we have ∀x[S(x) ↔ φ(x, y⃗)]. By the Proper Initial Segment Axioms, there is an H such than ¬S(H). It follows that each Σ_{1}^{S} formula ∃m ψ(m, n, u⃗) with parameters u⃗ is equivalent to the Δ_{0}^{S} formula

(∃x < H)[ψ(x, n, u⃗) ∧ φ(x, y⃗)].

Call this formula θ(n, u⃗, H). Then by Δ_{0}^{S}-CA,

∃z∀n[(p_{n}|z) ↔ θ(n, u⃗, H)],

and hence

∃z∀n[(p_{n}|z) ↔ ∃m ψ(m, n, u⃗)].

This proves Σ_{1}^{S}-CA. By the proof of Proposition 7.4 in [3], BNA + Σ_{1}^{S}- CA implies S-ACA. ACA_{0} now follows from the proof of Theorem 7.6 in

[3].  □  □

Remark 6.15. By Lemma 3.4 in [3], ^{∗}WKL_{0} implies T_{1}, so ^{∗}RCA_{0}′ + T_{1} is conservative with respect to WKL_{0}.

Proposition 6.14 shows that any model of T_{1} either satisfies Overspill or satisfies ACA_{0}. We note that T_{1} does not imply ACA_{0}, because ^{∗}WKL_{0} implies T_{1} but does not imply ACA_{0}. We will see that T_{1} also does not imply Overspill. In fact, Proposition 6.16 will show that a much stronger theory T_{2} does not imply Overspill.

We consider some stronger comprehension and induction schemes. Π_{∞}^{∗}- CA is the scheme

∃x∀m[(p_{m}|x) ↔ φ(m, u⃗)]

where φ(m, u⃗) is any formula of ^{∗}L_{1} in which x does not occur.

Π_{∞}^{∗}-IND is the scheme

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

where φ(m, u⃗) is any formula of ^{∗}L_{1}.

Proposition 6.16. The theory

T_{2} = ^{∗}RCA_{0}′ + Π_{∞}^{∗}-CA + Π_{∞}^{∗}-IND + ∀T

does not imply Overspill.

Proof. We build a model of T_{2} in which Overspill fails. Let (N , P) be the standard model of second order arithmetic where N = ℕ and P is the power set of ℕ. By the compactness theorem, N has an elementary extension N_{1} of cofinality at least |P| = 2^{ℵ_{0}}. By Theorem 5.1 and Proposition 6.13, there is a substructure ^{∗}N of N_{1} such that (N , P,^{∗}N) is a model of ^{∗}RCA_{0}′ + ∀T and Overspill fails. Since N = ℕ, (N , P,^{∗}N) also satisfies the other axioms

of T_{2}.  □  □

Our final result shows that Theorem 3.5 would fail if we added a symbol for every primitive recursive function to the vocabulary. In fact, when we do this we get a theory that implies WKL_{0}.

Let L_{1}(PR) be the language L_{1} with a new function symbol for every primitive recursive function, and similarly for L_{2} and ^{∗}L_{1}. Let RCA_{0}(PR) be the theory obtained by adding to RCA_{0} the defining equation for each primitive recursive function. It is well-known that RCA_{0}(PR) is conservative with respect to RCA_{0}. Let ∀T(PR) be Transfer for the set of all universal sentences of L_{1}(PR).

Proposition 6.17. The theory RCA_{0}(PR) + ∀T(PR) + BNA + STP implies Overspill and WKL_{0}.

Proof. We will give a proof of Overspill that uses ∀T(PR). This can be contrasted with the proof of Overspill in Lemma 3.7 of [3] using Internal Induction.

By the Proper Initial Segment axioms, it suffices to prove Overspill for Δ_{0}^{S} formulas in ^{∗}L_{1}(PR) all of whose variables have sort ^{∗}N. Every such formula is the star of a Δ_{0}^{0} formula of L_{1}(PR). Let φ(n, m⃗) be a Δ_{0}^{0} formula of L_{1}(PR). We work in ^{∗}RCA_{0}′(PR) and prove Overspill for the starred formula ^{∗}φ(y, x⃗).

Every Δ_{0}^{0} formula ψ(r⃗) of L_{1}(PR) defines a primitive recursive predicate. So L_{1}(PR) has a function symbol α_{ψ}(r⃗) such that

∀r⃗[ψ(r⃗) ↔ α_{ψ}(r⃗) = 0].

We show by induction on the complexity of ψ that

(3)  ∀z⃗[^{∗}ψ(z⃗) ↔ α_{ψ}(z⃗) = 0].

If ψ is an atomic formula, then (3) follows from ∀T(PR). If (3) holds for φ and ψ, then it follows from ∀T(PR) that (3) holds for φ ∧ ψ, φ ∨ ψ, and ¬φ. Suppose ψ(r⃗) is (∀n < r_{i}) φ(n, r⃗). Then

∀n∀r⃗[φ(n, r⃗) ↔ α_{φ}(n, r⃗) = 0]
∀r⃗[ψ(r⃗) ↔ α_{ψ}(r⃗) = 0]
∀r⃗[α_{ψ}(r⃗) = 0 ↔ (∀n < r_{i})α_{φ}(n, r⃗) = 0].

By ∀T(PR),

∀z⃗[α_{ψ}(z⃗) = 0 → (∀y < z_{i})α_{φ}(y, z⃗) = 0].

Let β(r⃗) be the function

β(r⃗) = (μn < r_{i})α_{φ}(n, r⃗) > 0.

Then β is primitive recursive, and using ∀T(PR) again we have

∀r⃗[α_{ψ}(r⃗) > 0 → [β(r⃗) < r_{i} ∧ α_{φ}(β(r⃗), r⃗) > 0]],
∀z⃗[α_{ψ}(z⃗) > 0 → [β(z⃗) < z_{i} ∧ α_{φ}(β(z⃗), z⃗) > 0]],
∀z⃗[α_{ψ}(z⃗) = 0 ↔ (∀y < z_{i})α_{φ}(y, z⃗) = 0].

Now suppose (3) holds for φ(n, r⃗), that is,

∀y∀z⃗[^{∗}φ(y, z⃗) ↔ α_{φ}(y, z⃗) = 0].

Then the following are equivalent:

∗ψ(z⃗), (∀y < z_{i})^{∗}φ(y, z⃗), (∀y < z_{i})α_{φ}(y, z⃗) = 0, α_{ψ}(z⃗) = 0.

This proves that (3) holds for ψ, and completes the induction.

Now let φ(n, m⃗) be a Δ_{0}^{0} formula, and assume that

∀n^{∗}φ(n, x⃗).

We must prove

(4)  ∃y[¬S(y) ∧^{∗}φ(y, x⃗)].

We have ∀n α_{φ}(n, x⃗) = 0. Let γ(m, r⃗) be the primitive recursive function

γ(m, r⃗) = (μn < m)α_{φ}(n, r⃗) > 0.

Then the following universal sentences hold:

∀r⃗ γ(0, r⃗) = 0,
∀m∀r⃗∀n[[γ(m, r⃗) = m ∧ α_{φ}(m, r⃗) = 0] → γ(m + 1, r⃗) = m + 1].

By ∀T(PR), the stars of these sentences hold. Therefore by Special Σ_{1}^{S} Induction,

∀m γ(m, x⃗) = m.

We note that the following universal sentences hold, and by ∀T(PR) their stars hold:

∀m∀r⃗∀n [[n < γ(m, r⃗) ∧ n < m] → α_{φ}(n, r⃗) = 0],
∀m∀r⃗∀n[α_{φ}(γ(m, r⃗), r⃗) = 0 → γ(m, r⃗) = m].

By the proper Initial Segment axioms there exists z such that ¬S(z). Let u = γ(z, x⃗). We cannot have S(u), because then α_{φ}(u, x⃗) = 0 and u = z, contradicting ¬S(z). So ¬S(u). Hence 0 < u, and there exists y = u − 1. We have ¬S(y). Since y < u = γ(z, x⃗), we have α_{φ}(y, x⃗) = 0. Then by (3), ∗φ(y, x⃗). This shows that (4) holds, and proves Overspill.

WKL_{0} now follows by Proposition 6.11.  □  □

Remark 6.18. The proof of Theorem 5.7 in [3] goes through when symbols for the primitive recursive functions are added to the vocabulary. It follows that the analogue of ^{∗}WKL_{0} + ∀T in this vocabulary is conservative with respect to WKL_{0}, and hence the theory RCA_{0}(PR) + ∀T(PR) + BNA + STP is conservative with respect to WKL_{0}.

Since the proof of a single sentence is finite, there is a finite set of primitive recursive functions such that the corresponding fragment of RCA_{0}(PR) + ∀T(PR) + BNA + STP already implies the Weak Koenig Lemma, and hence implies WKL_{0}. Question 6.3 asks whether this happens for the fragment obtained by adding just the exponential function.

7. Conclusion

This paper and [3] together show that for each of the “big five” theories T of reverse mathematics there is a theory T′ such that:

(a) T′ implies and is conservative with respect to T,

(b) T′ is of the form BNA + STP + U where U is a theory in the language ∗L_{1} of nonstandard arithmetic.

Let us call such a theory T′ a nonstandard counterpart of T. The paper [3] gave nonstandard counterparts of each of the theories WKL_{0}, ACA_{0}, ATR_{0}, and Π_{1}^{1}-CA_{0}. For RCA_{0}, [3] gave a nonstandard theory ^{∗}RCA_{0} which had property (a) but did not have property (b). In this paper give a nonstandard counterpart of RCA_{0}, namely the theory

∗RCA_{0}′ = BNA + STP+ Special Σ_{1}^{S}-IND + Special Δ_{1}^{S}-CA. Moreover, the stronger theory ^{∗}RCA_{0}′ + ∀T, where ∀T is the Transfer

scheme for universal sentences, is also a nonstandard counterpart of RCA_{0}. The main arguments were in Section 5, where we showed that ^{∗}RCA_{0}′ + ∀T is conservative with respect to RCA_{0}. To do this we used a result of Tanaka [5] and a special algebraic construction to show that every countable model (N , P) of RCA_{0} can be expanded to a model (N , P,^{∗}N) of ^{∗}RCA_{0}′ + ∀T.

As mentioned in the Introduction, in nonstandard analysis one often uses first order properties of hyperintegers to prove second order properties of integers, and the hyperintegers have more structure than the sets of integers. The objective of the theory ^{∗}RCA_{0}′ + ∀T is to capture the structure that the hyperintegers can have in a nonstandard counterpart of RCA_{0}.

In Section 6 we asked how much one can strengthen ^{∗}RCA_{0}′ +∀T and still be conservative with respect to RCA_{0}. We showed that several theories that appear to be only slightly stronger than ^{∗}RCA_{0}′ already imply WKL_{0} and thus cannot be conservative with respect to RCA_{0}. We also posed some open questions asking whether certain other theories stronger than RCA′_{0} +∀T are conservative with respect to RCA_{0}.

References

[1] Jeremy Avigad, Weak theories of nonstandard arithmetic and analysis. Pages 19-46 in Reverse Mathematics 2001, ed. by S. Simpson. A.K. Peters 2005.

[2] Richard Kaye, Model of Peano Arithmetic. Oxford 1991.

[3] H. Jerome Keisler, Nonstandard Arithmetic and Reverse Mathematics. Bulletin of Symbolic 12 (2006), pages 100–125.

[4] Stephen G. Simpson, Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer-Verlag, 1999.

[5] Kazuyuki Tanaka, The self-embedding theorem of WKL_{0} and a non-standard method. Annals of Pure and Applied Logic 84 (1997), pp. 41–49.

[6] Keita Yokoyama, Non-standard analysis within second order arithmetic. Lecture presented at the Conference on Computability, Reverse Mathematics, and Combinatorics, Banff 2008.

[7] Keita Yokoyama, Formalizing non-standard arguments in second order arithmetic. Preprint, 2008.

Department of Mathematics, University of Wisconsin, 480 Lincoln Drive, Madison WI 53706

   E-mail address: keisler@math.wisc.edu