{'fraction_non_alphanumeric': 0.0629430395656327, 'fraction_numerical': 0.010289410621218976, 'mean_word_length': 3.5234990903577925, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 42, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Infinitesimal analysis without the Axiom of Choice

It is often claimed that analysis with infinitesimals requires more substantial use of the Axiom of Choice than traditional elementary analysis. The claim is based on the observation that the hyperreals entail the existence of nonprincipal ultrafilters over N, a strong version of the Axiom of Choice, while the real numbers can be constructed in ZF. The axiomatic approach to nonstandard methods refutes this objection. We formulate a theory SPOT which suffices to carry out infinitesimal arguments, and prove that SPOT is a conservative extension of ZF. Thus the methods of Calculus with infinitesimals are just as effective as those of traditional Calculus. This result and conclusion extend to large parts of ordinary mathematics and beyond. We also develop a stronger axiomatic system SCOT, conservative over ZF+ADC, which is suitable for handling such features as an infinitesimal approach to the Lebesgue measure. Proofs of the conservativity results combine and extend the methods of forcing developed by Enayat and Spector.


Introduction
Many branches of mathematics exploit the Axiom of Choice (AC) to one extent or another. It is of considerable interest to gauge how much the Axiom of Choice can be weakened in the foundations of nonstandard analysis. Critics of analysis with infinitesimals often claim that nonstandard methods require more substantial use of AC than their standard counterparts. The goal of this paper is to refute such a claim.
1.1. Axiom of Choice in Mathematics. We begin by considering the extent to which AC is needed in traditional non-infinitesimal mathematics. Simpson [29] introduces a useful distinction between settheoretic mathematics and ordinary or non-set-theoretic mathematics.
The former includes such disciplines as general topology, abstract algebra and functional analysis. It is well known that fundamental theorems in these areas require strong versions of AC. Thus • Tychonoff's Theorem in general topology is equivalent to full AC. • Prime Ideal Theorem asserts that every ring with unit has a (two-sided) prime ideal. PIT is an essential result in abstract algebra and is "almost" as strong as AC (it is equivalent to Tychonoff's Theorem for Hausdorff spaces). It is also equivalent to the Ultrafilter Theorem: Every proper filter over a set S (i.e., in P(S)) can be extended to an ultrafilter.
• Hahn-Banach Theorem for general vector spaces is equivalent to the statement that every Boolean algebra admits a real-valued measure, a form of AC that is somewhat weaker than PIT. Jech [15] and Howard and Rubin [11] are comprehensive references for the relationships between these and many other forms of AC.
Researchers in set-theoretic mathematics have to accept strong forms of AC as legitimate whether or not they use nonstandard methods. Our concern here is with ordinary mathematics, which, according to Simpson, includes fields such as Calculus, countable algebra, differential equations, and real and complex analysis. It is often felt that results in these fields should be effective in the sense of not being dependent on AC. However, even these branches of mathematics cannot do entirely without AC. There is a number of fundamental classical results that rely on it; they include • the equivalence of continuity and sequential continuity for realvalued functions on R; • the equivalence of the ε-δ definition and the sequential definition of closure points for subsets of R; • closure of the collection of Borel sets under countable unions and intersections; • countable additivity of Lebesgue measure. Without an appeal to AC one cannot even prove that R is not a union of countably many countable sets, or that a strictly positive function cannot have vanishing Lebesgue integral (Kanovei and Katz [18]). However, these results follow already from ACC, the Axiom of Choice for Countable collections, a weak version of AC that many mathematicians use without even noticing. 1 Nevertheless, it is true enough that no choice is needed to define the real number system itself, or to develop Calculus and much of ordinary mathematics.
It has to be emphasized that objections to AC are not a matter of ontology, but of epistemology. In other words, the issue is not the existence of objects, but proof techniques and procedures. For better or worse, many mathematicians nowadays believe that the objects of interest to them can be represented by set-theoretic structures in a universe that satisfies ZFC. Nevertheless, they may prefer results that are effective, that is, do not use AC. For the purposes of this discussion, mathematical results are effective if they can be proved in ZF. Much of ordinary mathematics is effective in this sense.
We now consider whether nonstandard methods require anything more. A common objection to infinitesimal methods in the Calculus is the claim that the mere existence of the hyperreals 2 implies the existence of a nonprincipal ultrafilter U over N. The proof is simple: Fix an infinitely large integer ν in N * \ N and define U ⊆ P(N) by X ∈ U ←→ ν ∈ X * , for X ⊆ N. It is easy to see that U is a nonprincipal ultrafilter over N. For example, if X ∪ Y ∈ U, then ν ∈ (X ∪ Y ) * = X * ∪ Y * , where the last step is by the Transfer Principle. Hence either ν ∈ X * or ν ∈ Y * , and so X ∈ U or Y ∈ U. If X is finite, then X = X * , hence ν / ∈ X * and so U is nonprincipal. By the well-known result of Sierpiński [28] (see also Jech [15], Problem 1.10), U is a non-Lebesgue-measurable set (when subsets of N are identified with real numbers in some natural way). In the celebrated model of Solovay [30], ZF + ACC holds (even the stronger ADC, the Axiom of Dependent Choice, holds there), but all sets of real numbers are Lebesgue measurable, hence there are no nonprincipal ultrafilters over N in this model. The existence of nonprincipal ultrafilters over N requires a strong version of AC such as PIT; it cannot be proved in ZF (or even ZF + ADC).

1.2.
Countering the objection. How can such an objection be answered? As in the case of the traditional mathematics, the key is to look not at the objects but at the methods used. Analysis with infinitesimals does not have to be based on hyperreal structures in the universe of ZFC. It can be developed axiomatically; the monograph by Kanovei and Reeken [19] is a comprehensive reference for such approaches. Internal axiomatic presentations of nonstandard analysis, such as IST or BST, extend the usual ∈-language of set theory by a unary predicate st (st(x) reads x is standard ). For reference, the axioms of BST are stated in Section 7.
It is of course possible to weaken ZFC to ZF within BST or IST, but this move by itself does not answer the above objection. It is easily seen, by a modification of the argument given above for hyperreals, that the theory obtained from BST or IST by replacing ZFC by ZF proves PIT (Hrbacek [12]). This argument uses the full strength of the principles of Idealization and Standardization (see Section 7). However, Calculus with infinitesimals can be fully carried out assuming much less. Examination of texts such as Keisler [21] and Stroyan [34] reveals that only very weak versions of these principles are ever used there. Of course one has to postulate that infinitesimals exist (Nontriviality), but stronger consequences of Idealization are not needed. As for Standardization, these textbooks only explicitly postulate a special consequence of it, namely, the following principle: SP (Standard Part) Every limited real is infinitely close to a standard real; see Keisler [21,22], Axioms A -E. However, this is somewhat misleading. Keisler does not develop Calculus from his axioms alone; they describe some properties of the hyperreals, but the hyperreals are considered to be an extension of the field R of real numbers in the universe of ZFC, and the principles of ZFC can be freely used. In particular, the principle of Standardization is not an issue; it is automatically satisfied for any formula. While Standardization for formulas about integers appears innocuous, Standardization for formulas about reals can lead to the existence of nonprincipal ultrafilters. On the other hand, some instances of Standardization over the reals are unavoidable, for example to prove the existence of the function f ′ (the derivative of f ) defined in terms of infinitesimals for a given real-valued function f on R.

SPOT and SCOT.
In the present text, we introduce a theory SPOT in the st-∈-language, a subtheory of IST and BST, and we show that SPOT proves Countable Idealization and enough Standardization for the purposes of the Calculus. We use ∀ st and ∃ st as quantifiers over standard sets. The axioms of SPOT are: ZF (Zermelo -Fraenkel Set Theory) T (Transfer) Let φ be an ∈-formula with standard parameters. Then Our main result is the following.
Theorem A The theory SPOT is a conservative extension of ZF.
Thus the methods used in the Calculus with infinitesimals do not require any appeal to the Axiom of Choice.
The result allows significant strengthenings. We let SN be the Standardization principle for st-∈-formulas with no parameters. The principle allows Standardization of much more complex formulas than SPOT alone.
Theorem B The theory SPOT + SN is a conservative extension of ZF.
It is also possible to add some Idealization. We let BI ′ be Bounded Idealization (see Section 7) for ∈-formulas with standard parameters.
Theorem C The theory SPOT+B+BI ′ is a conservative extension of ZF. This is the theory BST with ZFC replaced by ZF, Standardization weakened to SP and Bounded Idealization weakened to BI ′ ; we denote it BSPT ′ . This theory enables the applicability of some infinitesimal techniques to arbitrary topological spaces. It also proves that there is a finite set S containing all standard reals, a frequently used idea.
As noted above, some important results in elementary analysis and elsewhere in ordinary mathematics require the Axiom of Countable Choice. On the other hand, ACC entails no "paradoxical" consequences, such as the existence of Lebesgue-non-measurable sets, or the existence of an additive function on R different from f a : x → ax for all a ∈ R. Many mathematicians find ACC acceptable. These considerations apply as well to the following stronger axiom.
ADC (Axiom of Dependent Choice) If R is a binary relation on a set A such that ∀a ∈ A ∃a ′ ∈ A (aRa ′ ), then for every a ∈ A there exists a sequence a n | n ∈ N such that a 0 = a and a n Ra n+1 for all n ∈ N.
This axiom is needed for example to prove the equivalence of the two definitions of a well-ordering (Jech [16], Lemma 5.2): (1) Every nonempty subset of a linearly ordered set (A, <) has a least element.
We denote by ZFc ("ZFC Lite") the theory ZF+ADC. This theory is sufficient for axiomatizing ordinary mathematics (and many results of set-theoretic mathematics as well). Let SCOT be the theory obtained from SPOT by adding SN and strengthening SP to Countable st-∈-Choice (CC); see Section 3.
Theorem D The theory SCOT is a conservative extension of ZFc.
In SCOT one can carry out most techniques used in infinitesimal treatments of ordinary mathematics. As examples, we give a proof of Peano's Existence Theorem and an infinitesimal construction of Lebesgue measure in Section 3. Thus the nonstandard methods used in ordinary mathematics do not require any more choice than is generally accepted in traditional ordinary mathematics.
Further related conservative extension theorems can be found in Sections 5, 6 and 7.
2. Theory SPOT and Calculus with infinitesimals 2.1. Some consequences of SPOT. The axioms of SPOT were given in Section 1.3.
Lemma 2.1. The theory SPOT proves the following: Proof. Given a standard n ∈ N and m < n, let A = {k ∈ N | k < m}. By SP there is a standard B ⊆ N such that for all standard k, k ∈ B iff k ∈ A iff k < m. The set B ⊆ N is bounded above by n (Transfer), so it has a greatest element k 0 (< is a well-ordering of N) , which is standard by Transfer. Now we have k 0 < m and k 0 + 1 ≮ m, so k o + 1 = m and m is standard.
Conversely, assume ∀ st n ∈ N ∃x ∀m ∈ N (m ≤ n → φ(m, x)). By the Axiom of Separation of ZF, there is a set S = {n ∈ N | ∃x ∀m ∈ N (m ≤ n → φ(m, x))}, and the assumption implies that ∀ st n ∈ N (n ∈ S).
Assume that S contains standard integers only. Then N \ S = ∅ by the axiom O. Let ν be the least element of N\S. Then ν is nonstandard but ν − 1 is standard, a contradiction.
Let µ be some nonstandard element of S. We have ∃x ∀m ∈ N (m ≤ µ → φ(m, x)); as n ≤ µ holds for all standard n ∈ N, we obtain ∃x ∀ st n ∈ N φ(n, x).
Countable Idealization easily implies the following more familiar form. We use ∀ st fin and ∃ st fin as quantifiers over standard finite sets. Corollary 2.3. Let φ be an ∈-formula with arbitrary parameters. The theory SPOT proves the following: For every standard countable set A ∀ st fin a ⊆ A ∃x ∀y ∈ a φ(x, y) ←→ ∃x ∀ st y ∈ A φ(x, y).
The axiom SP ′ is often stated and used in the form where x is limited iff |x| ≤ n for some standard n ∈ N, and x ≈ r iff |x − r| ≤ 1/n for all standard n ∈ N, n = 0. The unique standard real number r is called the standard part of x or the shadow of x; notation sh(x). We note that in the statement of SP ′ , N can be replaced by any countable standard set A.
Lemma 2.4. The statements SP ′ and SP are equivalent (over ZF + O + T).
As ∀ st q ∈ B (q ≤ n 0 ) holds, the set B is bounded above (apply Transfer to the formula q ∈ B → q ≤ n 0 ) and so it has a supremum r ∈ R, which is standard (Transfer again). We claim that x ≈ r. If not, then |x − r| > 1 n for some standard n, hence either x < r − 1 n or x > r + 1 n . In the first case sup B ≤ r − 1 n and in the second, sup B ≥ r + 1 n ; either way contradicts sup B = r.
SP ⇒ SP ′ : Given A ⊆ N, let χ A be the characteristic function of A. Define a real number x A = Σ ∞ n=0 χ(n) 10 n+1 ; as 0 ≤ x A ≤ 1 9 , there is a standard real number r ≈ x A . Let r = Σ ∞ n=0 an 10 n+1 be the decimal expansion of r where for every n there is k > n such that a k = 9. Note that if n is standard, then there is a standard k with this property, by Transfer. If χ(n) = a n for all n, then A is standard and we let B = A. Otherwise let n 0 be the least n where χ(n) = a n . From r ≈ x A it follows easily that n 0 is nonstandard. In particular, a n ∈ {0, 1} holds for all standard n, hence, by Transfer, for all n ∈ N. Let B = {n ∈ N | a n = 1}. Then B is standard and for all standard n ∈ N, n ∈ B iff a n = 1 iff χ(n) = 1 iff n ∈ A.
As explained in the Introduction, Standardization over uncountable sets such as R, even for very simple formulas, implies the existence of nonprincipal ultrafilters over N, and so it cannot be proved in SPOT (consider a standard set U such that ∀ st X (X ∈ U ←→ X ⊆ N ∧ ν ∈ X), where ν is a nonstandard integer). But we need to be able to prove the existence of various subsets of R and functions from R to R that arise in Calculus and may be defined in terms of infinitesimals. Unlike the undesirable example above, such uses generally involve Standardization for formulas with standard parameters.
where ψ is an ∈-formula and Q stands for ∃ or ∀. This result has twofold importance: • The meaning of every predicate that for standard inputs is defined by a Q st 1 x 1 . . . Q st m x m ψ formula with standard parameters is automatically extended to all inputs, where it it given by the ∈-formula Q 1 x 1 . . . Q m x m ψ.
• Standardization holds for all ∈-formulas with additional predicate symbols, as long as all these additional predicates are defined by ∆ st formulas with standard parameters. In BST all st-∈-formulas are equivalent to ∆ st formulas (see Kanovei and Reeken [19], Theorem 3.2.3). In SPOT the equivalence is true only for certain classes of formulas, but they include the definitions of all the basic concepts of Calculus and much beyond.
We recall that h ∈ R is infinitesimal iff 0 < |h| < 1 n holds for all standard n ∈ N, n > 0. We use ∀ in and ∃ in for quantifiers ranging over infinitesimals and 0. The basic concepts of Calculus have infinitesimal definitions that involve a single alternation of such quantifiers.
The following proposition strengthens a result in Vopěnka [35], p. 148. The variables x, y range over R and m, n, ℓ range over N \ {0}. Proposition 2.6. In SPOT the following is true: Let φ(x, y) be an ∈-formula with arbitrary parameters.
By duality, we also have: Proof. The formula ∀ in h ∃ in k φ(h, k) means: where we assume that the variables m, n do not occur freely in φ(x, y). Using Countable Idealization (Lemma 2.2), we rewrite this as We now use the observation that ∀ℓ ≤ m (|y| < 1/ℓ) is equivalent to |y| < 1/m, and the rules ( , valid assuming that v is not free in α (note that Transfer implies ∃n st(n)). This enables us to rewrite the preceding formula as follows: After exchanging the order of the first two universal quantifiers, we obtain the formula to which we apply (the dual form of) Countable Idealization to get and replacing ∀ℓ ≤ n (|x| < 1/ℓ) by |x| < 1/n, we obtain proving the proposition.
Let Φ(F, c, d) be the formula on the right side of the equivalence in (1). Lemma 2.5 establishes that the formula Φ is equivalent to a ∆ st formula, and φ(F, c, d) provided by the proof of Lemma 2.5 is easily seen to be equivalent to the standard ε-δ definition of derivative. For any standard F , the set Formulas of the form Q 1 h 1 . . . Q n h n φ(h 1 , . . . , h n , v 1 , . . . , v k ) where each Q is either ∀ or ∀ in or ∃ or ∃ in , but all quantifiers over infinitesimals are of the same kind (all existential or all universal), are also ∆ st . As an example, ∃ in h ∀y ∃ in k φ(h, k, x, y) is equivalent to ∃h ∀y ∃k ∀ st m ∀ st n (|h| < 1/m ∧ |k| < 1/n ∧ φ(h, k, x, y)).
The two quantifiers over standard elements of N can be replaced by a single one: and then moved to the front using Countable Idealization.
Klein and Fraenkel proposed two benchmarks for a useful theory of infinitesimals (see Kanovei et al. [17]): • a proof of the Mean Value Theorem by infinitesimal techniques; • a definition of the definite integral in tems of infinitesimals. The theory SPOT easily meets these criteria. The usual nonstandard proof of the Mean Value Theorem (Robinson [26], Keisler [21,22]) uses Standard Part and Transfer, and is easily carried out in SPOT. The familiar infinitesimal definition of the Riemann integral for standard bounded functions on a standard interval [a, b] also makes sense in SPOT and can be expressed by a ∆ st formula. In the next example we outline a treatment inspired by Keisler's use of hyperfinite Riemann sums in [22].
It is easy to show that the value of the integral does not depend on the choice of h. We thus have, The formulas are of the form A E and E E respectively, and therefore equivalent to ∆ st formulas.
The approach generalizes easily to the Riemann integral of bounded functions on [a, b]. We say that These formulas are again equivalent to ∆ st formulas (the first one is of the form A A E and in the second one both quantifiers over standard sets are existential).
The tools available in SPOT enable nonstandard definitions and proofs in parts of mathematics that go well beyond the Calculus.
This definition is equivalent to a ∆ st formula.
In Section 6 we show that Standardization for arbitrary formulas with standard parameters can be added to SPOT and the resulting theory is still conservative over ZF. This result enables one to dispose of any concerns about the form of the defining formula.

Theory SCOT and Lebesgue measure
We recall (see Section 1.3) that SCOT is SPOT + SN + CC, where the principle of Countable st-∈-Choice postulates the following: CC Let φ(u, v) be an st-∈-formula with arbitrary parameters. Then The set N can be replaced by any standard countable set A. We consider also the principle of Countable Standardization.

SC (Countable Standardization) Let ψ(v) be an st-∈-formula with arbitrary parameters. Then
If f is a function provided by CC, let A = {n ∈ N | f (n) = 0}. By SP there is a standard set S such that, for all standard n ∈ N, n ∈ S iff n ∈ A iff ψ(n) holds.
CC st is the following principle: The function F is standard and, for every standard n, the sets F (n) and f (n) have the same standard elements. As they are both standard, it follows by Transfer that F (n) = f (n).
The full principle CC st can conservatively be added to SCOT; see Proposition 5.6.
A useful consequence of SC is the ability to carry out external induction.
be an st-∈-formula with arbitrary parameters. Then SPOT + SC proves the following: Proof. SC yields a standard set S ⊆ N such that ∀ st n ∈ N (n ∈ S ←→ φ(n)). We have 0 ∈ S and ∀ st n ∈ N (n ∈ S → n + 1 ∈ S). Then ∀n ∈ N (n ∈ S → n + 1 ∈ S) by Transfer, and S = N by induction. Hence ∀ st n ∈ N φ(n) holds.
In Example 3.6 it is convenient to use the language of external collections. Let φ(v) be an st-∈-formula with arbitrary parameters. We use dashed curly braces to denote the external collection x ∈ A | φ(x) . We emphasize that this is merely a matter of convenience; writing z ∈ x ∈ A | φ(x) is just another notation for φ(z).
Standardization in BST implies the existence of a standard set S such that ∀ st z (z ∈ S ←→ z ∈ x ∈ A | φ(x) ). We do not have Standardization over uncountable sets is SCOT, but one important case can be proved.
The notation indicates the greatest standard s ∈ R such that s ≤ r for all standard r with the property φ(r) (+∞ if there is no such r).
We give two examples of mathematics in SCOT.
Example 3.5. Peano Existence Theorem. Peano's Theorem asserts that every first-order differential equation of the form y ′ = f (x, y) has a solution (not necessarily a unique one) satisfying the initial condition y(0) = 0, under the assumption that f is continuous in a neighborhood of 0, 0 . The infinitesimal proof begins by constructing the sequences On the face of it one needs Standardization over R to obtain this function, but SC suffices. Consider the It is easy to verify that Y 0 is continuous on Q ∩ [0, a] and that its extension Y to a continuous function on [0, a] is the desired solution.
Example 3.6. Lebesgue measure. In a seminal paper [24] Loeb introduced measures on the external power set of R * which became known as Loeb measures, and used them to construct the Lebesgue measure on R. Substantial use of external collections is outside the scope of this paper, but it is possible to eliminate the intermediate step and give an infinitesimal definitionà la Loeb of the Lebesgue measure in internal set theory. We outline here how to construct the Lebesgue outer measure on R in SCOT.
Let T be a hyperfinite time line (see Example 2.8) and let E ⊆ R be standard.
We define µ µ µ by setting The collection whose infimum needs to be taken is external, but the existence of the infimum is justified by Lemma 3.4. It is easy to see that the value of µ µ µ(E) is independent of the choice of the infinitesimal h in the definition of T. Thus the external function µ µ µ can be defined for standard E ⊆ P(R) by an st-∈-formula with no parameters (preface the formula on the right side of (3) by n=0 m(E n ) = +∞ the claim is trivial, so we assume that m(E n ) = r n ∈ R for all n. Fix a standard ε > 0. For every standard n ∈ N there exists A such that φ(n, A): "A covers E n ∧ |A| · h < r n + ε/2 n+1 " holds. By Countable st-∈-Choice there is a sequence A n | n ∈ N such that for all standard n φ(n, A n ) holds. By Countable Idealization ("Overspill") there is a nonstandard ν ∈ N such that |A n | · h < r n + ε/2 n+1 holds for all n ≤ ν. We let A = ν n=0 A n . Clearly A is finite and covers E. Thus for r = sh(|A| · h) we obtain m(E) ≤ r and |A| · h ≤ Σ ν n=0 |A n | · h < Σ ν n=0 r n + ε. Since the sequence Σ ∞ n=0 r n converges, we have sh(Σ ν n=0 r n ) = Σ ∞ n=0 r n and m(A) ≤ Σ ∞ n=0 r n + ε. As this is true for all standard ε > 0, we . With more work, one can show that m(E) coincides with the conventionally defined Lebesgue outer measure of E for all standard E ⊆ R. See Hrbacek [13] Section 3 for more details and other equivalent nonstandard definitions of the Lebesgue outer measure. 3 One can define Lebesgue measurable sets from m in the usual way. One can also define Lebesgue inner measure for standard E by and prove that a standard bounded E ⊆ R is Lebesgue measurable iff m(E) = m − (E), and the common value is the Lebesgue measure of E; see Hrbacek [14].
4. Conservativity of SPOT over ZF Theorem 4.1. The theory SPOT is a conservative extension of ZF:  Proof of Theorem 4.1. Suppose SPOT ⊢ θ but ZF θ, where θ is an ∈-sentence. Then the theory ZF + ¬θ is consistent, therefore it has a countable model M, by Gödel's Completeness Theorem. Using Proposition 4.2 one obtains its extension M * SPOT, so in particular M * θ and, by Transfer in M * , M θ. This is a contradiction.
The rest of this section is devoted to the proof of Proposition 4.2.
4.1. Forcing according to Enayat and Spector. We combine the forcing notion used by Enayat [7] to construct end extensions of models of arithmetic, with the one used by Spector in [32] to produce extended ultrapowers of models M of ZF by an ultrafilter U ∈ M.
In this subsection we work in ZF, define our forcing notion and prove its basic properties. The next subsection deals with generic extensions of countable models of ZF and the resulting extended ultrapowers. The general reference to forcing and generic models in set theory is Jech [16].
The set of all natural numbers is denoted N and letters m, n, k, ℓ are reserved for variables ranging over N. The index set over which the ultrapowers will eventually be constructed is denoted I. In this section we assume I = N. A subset p of N is called unbounded if ∀m ∃n ∈ p (n ≥ m) and bounded if it is not unbounded. Of course unbounded is the same as infinite, and bounded is the same as finite. We use this terminology with a view to Section 7, where the construction is generalized to I = P fin (S) for any infinite set S. The notation ∀ aa i ∈ p (for almost all i ∈ p) means ∀i ∈ p \ c for some bounded c.
As usual, the symbol V denotes the universe of all sets, and V α (α ranges over ordinals) are the ranks of the von Neumann cumulative hierarchy. We let F be the class of all functions with domain I. The notation ∅ k stands for the k-tuple ∅, . . . , ∅ .
The number k is the rank of q. We note that Q is a proper class. We let 1 = q where q(i) = {∅} for all i ∈ I;1 is the only q ∈ Q of rank 0.
The forcing notion H is defined as follows: H = P×Q and p ′ , q ′ ∈ H extends p, q ∈ H (notation: p ′ , q ′ ≤ p, q ) iff p ′ extends p, rank q ′ = k ′ ≥ k = rank q, and for almost all i ∈ p ′ and all x 0 , . . . , The poset P is used to force a generic filter over I as in Enayat [7], and H forces an extended ultrapower of V by the generic filter U forced by P. It is a modification of the forcing notion from Spector [32], with the difference that in [32] U is not forced but assumed to be a given ultrafilter in V.
A set D ⊆ P is dense in P if for every p ∈ P there is p ′ ∈ D such that p ′ extends p. We note that for any set S ⊆ I, the set The forcing language L has a constant symbolž for every z ∈ V (which we identify with z when no confusion threatens), and a constant symbolĠ n for each n ∈ N. Given an ∈ formula φ(w 1 , . . . , w r , v 1 , . . . , v s ), we define the forcing relation p, q φ(ž 1 , . . . ,ž r ,Ġ n 1 , . . . ,Ġ ns ) for p, q ∈ H by meta-induction on the logical complexity of φ. We use ¬, ∧ and ∃ as primitives and consider the other logical connectives and quantifiers as defined in terms of these. Usually, we suppress the explicit listing in φ of the constant symbolsž for the elements of V.
(1) - (3) are immediate from the definition of forcing and (4) can be proved by induction on the complexity of φ.
Proof. For atomic formulas (cases (1) - (7)) the claim is immediate from the definition. Case (9) is also trivial (union of two bounded sets is bounded).
Lemma 4.8. Let z ∈ V. For every p, q there exist p, q ′ extending p, q and m < k ′ = rank q ′ such that p, q ′ ž =Ġ m .
We abbreviate the relation p, q ž =Ġ m as p, q z =Ġ m , and p, q ž ∈Ġ m as p, q z ∈Ġ m . We say that p, q decides φ if p, q φ or p, q ¬φ. The following lemma is needed for the proof that the extended ultrapower satisfies SP. Lemma 4.9. For every p, q and m < k = rank q there is p ′ , q ′ that extends p, q and is such that for every n ∈ N, p ′ , q ′ decides n ∈Ġ m .
Proof. We first construct a sequence p n , q n | n ∈ N such that p 0 , q o = p, q and for each n, rank q n = k, p n+1 ⊂ p n , p n+1 , q n+1 extends p n , q n , and p n+1 , q n+1 decides n ∈Ġ m .
Given p n , let c = {i ∈ p n | ∀ x 0 , . . . , x k−1 ∈ q n (i) (n ∈ x m )}. If c is unbounded, we let p ′ n+1 = c and q n+1 = q n . Otherwise p n \ c is unbounded and we let p ′ n+1 = p n \ c and q n+1 We obtain p n+1 from p ′ n+1 by omitting the least element of p ′ n+1 . Proposition 4.6 implies that p n+1 , q n+1 decides n ∈Ġ m .
Let i n be the least element of p n . We define p ′ , q ′ as follows: i ∈ p ′ iff i ∈ p n and q ′ (i) = q n (i), where i n ≤ i < i n+1 ; q ′ (i) = {∅ k } otherwise. It is clear from the construction and Proposition 4.6 that p ′ , q ′ ∈ H, it extends p, q , and it decides n ∈Ġ m for every n ∈ N.

Extended ultrapowers.
In this subsection we define the extended ultrapower of a countable model of ZF by a generic filter U, prove some fundamental properties of this structure, and conclude that it is a model of SPOT.
In this section we take Zermelo-Fraenkel set theory as our metatheory, but the proof employs very little of its powerful machinery. Subsection 8.5 explains how the proof given below can be converted into a finitistic proof.
We use ω for the set of natural numbers in the metatheory, and r, s as variables ranging over ω.
Let M = (M, ∈ M ) be a countable model of ZF. Concepts defined in Subsection 4.1 make sense in M and all results of 4.1 hold in M. When M is understood, we use the notation and terminology from 4.1 for the concepts in the sense of M; thus N for N M , "unbounded" for "unbounded in the sense of M", P for P M , for " in the sense of M", etc. The model M need not be well-founded, and ω is isomorphic to an initial segment of N which may be proper. (1) M "p ∈ P" for every p ∈ U; (2) If p ∈ U and M "p ′ ∈ P ∧ p extends p ′ ", then p ′ ∈ U; (3) For eny p 1 , p 2 ∈ U there is p ∈ U such that M "p extends p 1 ∧ p extends p 2 ". A filter U on P is M-generic if for every D ∈ M such that M "D is dense in P" there is p ∈ U for which p ∈ M D.
Since P has only countably many dense subsets in M, M-generic filters are easily constructed by recursion. Let p r | r ∈ ω be an enumeration of P and D r | r ∈ ω be an enumeration of all dense subsets of P in M. Let q 0 = p 0 and for each s ∈ ω let q s+1 = p r for the least r such that M "p r extends q s ∧ p r ∈ D s ".Then let U = {p ∈ M | M "p ∈ P ∧ q s extends p" for some s ∈ ω}.
M-generic filters G ⊆ M × M on H are defined and constructed analogously.
Lemma 4.11. If G is an M-generic filter on H, then U = {p ∈ P | ∃q p, q ∈ G} is an M-generic filter on P.
We now define the extended ultrapower of M by U; we follow closely the presentation in Spector [32].
Let Ω = {m ∈ M | M "m ∈ N"}. We define binary relations = * and ∈ * on Ω as follows: m = * n iff there exists p, q ∈ G such that rank q = k > m, n and p, q Ġ m =Ġ n ; m ∈ * n iff there exists p, q ∈ G such that rank q = k > m, n and p, q Ġ m ∈Ġ n . It is easily seen from the definition of forcing and Proposition 4.6 that = * is an equivalence relation on Ω, and a congruence relation with respect to ∈ * . We denote the equivalence class of m ∈ Ω in the relation = * by G m , define G m ∈ * G n iff m ∈ * n, and let N = {G m | m ∈ Ω}. The extended ultrapower of M by U is the structure N = (N, ∈ * ).
There is a natural embedding j of M into N defined as follows: By Lemma 4.8 for every z ∈ M there exist p, q ∈ G and m < rank q such that p, q z =Ġ m . We let j(z) = G m and often identify j(z) with z. It is easy to see that the definition is independent of the choice of representative from G m , and that j is an embedding of M into N. (1) N φ(G n 1 , . . . , G ns ).

Proof. Statement
for the definition of "dense in" see the sentence preceding Lemma 5.3.) The equivalence of (1) and (2) is the Forcing Theorem. It is proved as usual, by induction on the logical complexity of φ. The cases v 1 = v 2 and v 1 ∈ v 2 follow immediately from the definitions of = * and ∈ * , and the conjunction is immediate from (3) in the definition of a filter.
It remains to prove the Standard Part principle. Let G m ∈ N. By Lemma 4.9 there is p, q ∈ G which decides n ∈Ġ m for all n ∈ Ω. The set E = {n ∈ Ω | p, q n ∈Ġ m } is definable in M, hencethere is e ∈ M such that M "n ∈ e" iff n ∈ E iff N "n ∈ G m ". Thus N " st(e) ∧ ∀ st ν ∈ N (ν ∈ e ←→ ν ∈ G m )".
This proves Proposition 4.2, and hence Theorem A.

Conservativity of SCOT over ZFc
In this section we show that if ZF is replaced by ZFc, the Standard Part principle can be strengthened to Countable st-∈-Choice.
We recall that ZFc implies ACC; this provides enough choice to prove that the ordinary ultrapower of a countable model M of ZFc by an M-generic filter U on P satisfies Loś's Theorem and thus yields an elementary extension of M. A proof that every countable model M = (M, ∈ M ) of ZFc has an extension to a model of SPOT + SC in which M is the class of all standard sets can be obtained by a straightforward adaptation of the arguments in Enayat's paper [7], in particular, of the proofs of Theorems B and C there. Essentially, all one has to do is replace countable models of second-order arithmetic by countable models of ZFc. We followed this approach in an early version of the present paper.
Another proof of conservativity of SCOT over ZFc was suggested to us by Kanovei in a private communication. Its basic idea is to use forcing to add to M a mapping of ω 1 onto R without adding any reals. In the resulting generic extension there are nonprincipal ultrafilters over N, and one can take an ultrapower of M by one of them to obtain an extension that satisfies SCOT. However, this method does not seem adequate for handling Idealization over uncountable sets in Section 7.
We first outline the simplification of the forcing that is possible in the presence of ACC, and then use it to prove that, assuming M is a countable model of ZFc, the structure N from Proposition 4.15 satisfies also CC and SN. The proof can be viewed as a warm-up for similar but more complex arguments of the following sections.
We work in Zermelo-Fraenkel set theory with ADC added. Given I = N and q ∈ Q of rank k, ACC guarantees the existence of a function f such that ∀i ∈ I (f (i) ∈ q(i)); let q(i) = {f (i)} where f (i) = f 0 (i), . . . , f k−1 (i) . For any p, q ∈ H the condition p, q extends p, q . We could replace Q by Q = { q ∈ F | ∃k ∀i ∈ I ( q(i) ∈ V k )}. But there is no need at all for the symbolsĠ k , k ∈ N, and Spector's component Q of the forcing notion H, if our forcing language allows names for all f ∈ F (see below for details).
On the other hand, Standardization and Countable st-∈-Choice, unlike Transfer and Idealization, deal with st-∈-formulas, so we need to generalize our definition of the forcing relation to such formulas.
The forcing notion we use in this section is P. The forcing language L has a constant symbolf for every function f ∈ F (the check is usually suppressed). Forcing is defined for arbitrary st-∈-formulas. Only the following clauses in the definiton of the forcing relation are necessary: (10') p ∃v ψ iff for every p ′ extending p there exist p ′′ extending p ′ and a function f ∈ F such that p ′′ ψ(f ).
The basic properties of forcing from Lemma 4.5 remain valid, but . . , f r ∈ F ", then the following statements are equivalent: (2) There is some p ∈ U such that p φ(f 1 , . . . , f r ) holds in M.
Corollaries 4.13 and 4.14 and Proposition 4.15 remain valid in this modified setting. For ∈-formulas Proposition 5.2 is just a fancy way to state the ordinary Loś's Theorem, but for st-∈-formulas it provides a useful handle on the behavior of N.
We need the following corollary (which can also be proved more tediously directly from the definition of the forcing relation). The statement "D ⊆ P is dense in p" means that ∀p ′′ ≤ p ∃p ′ ≤ p ′′ (p ′ ∈ D).
Proof. We show that the claim holds in every model M of ZFc. For every p ′′ ≤ p in M there is an M-generic filter U such that p ′′ ∈ U. By Proposition 5.2 N ∀ st m φ(m), so, for every m ∈ N, N φ(m). By 5.2 again, there exists p ′ ∈ U such that p ′ φ(m). We can take p ′ ≤ p ′′ .
Lemma 5.4. Let φ(u, v) be an st-∈-formula with parameters from L.. Then ZFc proves the following: If p ∀ st m ∃v φ(m, v), then there is p ′ ∈ P and a sequence f m | m ∈ N such that p ′ extends p and p ′ φ(m, f m ) for every m ∈ N.

Proof. By Lemma 5.3, the set
Applying ADC to the relation R we obtain a sequence p m | m ∈ N such that p 0 ⊆ p and, for each m, p m+1 ⊂ p m and ∃f ∈ F (p m φ(m, f )). We next use ACC to obtain a sequence f m | m ∈ N such that p m φ(m, f m ). Note that the Reflection Principle of ZF provides a set A = V α such that for all m, As in the proof of Lemma 4.9, let i m be the least element of p m and let p ′ = ∞ m=0 p m ∩ (i m+1 \ i m ). Then for every m the set p ′ \ p m is bounded, hence p ′ φ(m, f m ).
Proposition 5.5. If M satisfies ZFc, then N satisfies CC.
We define a function g on I by g Recall thatǧ is the name for g in the forcing language. By Loś's Theorem, p ′ "ǧ is a function with domain N," and, for every m ∈ N, p ′ ǧ(m) = f m . We conclude that N "ǧ is a function with domain N", and N ∀ st m ∈ N φ(m,ǧ(m)). Let p, p ′ ∈ P and let γ be an increasing mapping of p ′ onto p; we extend γ to I = N by defining γ(a) = 0 for a ∈ I \ p.
Corollary 5.8. Let φ be an st-∈-formula with parameters from V. Then p φ iff p ′ φ.
Proposition 5.9. The structure N satisfies the principle of Standardization for st-∈-formulas with no parameters.
The right side is expressible by an ∈-formula.
This completes the proof of Theorem D.
Another principle that can be added to SCOT is Dependent Choice for st-∈-formulas. DC Let φ(u, v) be an st-∈-formula with arbitrary parameters. If b ∈ B and ∀x ∈ B ∃y ∈ B φ(x, y), then there is a sequence b n | n ∈ N such that b 0 = b and ∀ st n ∈ N (b n ∈ B ∧ φ(b n , b n+1 )). Proof. We show that DC holds in the structure N.
Assume that p b ∈ B and p ∀x ∈ B ∃y ∈ B φ(x, y). We now let It is clear from the properties of forcing that for every p ′ , f ′ ∈ A there is p ′′ , f ′′ ∈ A such that p ′ , f ′ R p ′′ , f ′′ . Using ADC we obtain a sequence p n , f n | n ∈ N such that p 0 ≤ p, f 0 = b, and for all n ∈ N p n , f n ∈ A, p n+1 ≤ p n , and p n+1 φ(f n , f n+1 ).
The rest of the proof imitates the arguments in the last paragraphs of the proofs of Lemma 5.4 and Proposition 5.5.

Standardization for parameter-free formulas
In this section we prove that the structure N = (N, ∈ * , M) satisfies the principle of Standardization for parameter-free formulas assuming only that the model M satisfies ZF. Explicitly, the principle postulates: SN Let φ(v) be an st-∈-formula with no parameters. Then Lemma 6.1. The principle SN is equivalent to Standardization for st-∈-formulas with standard parameters.
With the exception of the last proposition, in this section we work in ZF. As in Section 5, we begin with generalizing forcing to st-∈formulas.
Proof. The proof is by induction on the logical complexity of φ.
For ∈-formulas the assertion follows immediately from Proposition 4.6. In particular, it holds for all atomic formulas involving ∈ and = (cases (1) - (7) in the definition of forcing). It is also clear for st (cases (11) and (12)) and for conjunction (case (9)).
Proof. As for Lemma 5.7.
Proposition 6.7. The structure N = (N, ∈ * , M) satisfies the principle of Standardization for st-∈-formulas with no parameters.
Proof. For standard z, N φ(z) iff p, q φ(z) for every p, q ∈ H. The right side is expressible by an ∈-formula.

This completes the proof of Theorem B.
There is yet another principle that can be added to SPOT and keep it conservative over ZF. One of its important consequences is the impossibility to uniquely specify an infinitesimal.
UP (Uniqueness Principle) Let φ(v) be an st-∈-formula with standard parameters. If there exists a unique x such that φ(x), then this x is standard. Theorem 6.8. SPOT + UP is a conservative extension of ZF.
Proof of Claim 1. Let x be such that p x is unbounded. Define Then p x , q x ≤ p, q and p x , q x Ġ m = x, i.e., p x , q x st(Ġ m ), a contradiction.
Claim 2. There exist unbounded mutually disjoint sets p 1 , p 2 ⊂ p and nonempty sets s(i) ⊆ r(i) for all i ∈ p 1 ∪ p 2 such that i∈p 1 s(i) ∩ i∈p 2 s(i) = ∅. We postpone the proof of Claim 2 and complete the proof of the theorem.

Idealization
We recall the axioms of the theory BST; see the references Kanovei and Reeken [19] and Fletcher et al. [8] for motivation and more detail. In addition to the axioms of ZFC, they are: T (Transfer) Let φ(v) be an ∈-formula with standard parameters. Then S (Standardization) Let φ(v) be an st-∈-formula with arbitrary parameters. Then BI (Bounded Idealization) Let φ be an ∈-formula with arbitrary parameters. For every set A ∀ st fin a ⊆ A ∃y ∀x ∈ a φ(x, y) ←→ ∃y ∀ st x ∈ A φ(x, y).
7.1. Idealization over uncountable sets. In order to obtain models with Bounded Idealization, the construction of Subsections 4.1 and 4.2 needs to be generalized from I = N to I = P fin (A), where A is any infinite set. The key is the right definition of "unbounded" subsets of I. We work in ZF.
We use the notation P ≤m (A) for {a ∈ P fin (A) | |a| ≤ m}.
We let ν p (m) denote the least n with this property. The set p is thin if it is not thick.
Clearly {a ∈ P fin (A) | x ∈ a} is thick for every x ∈ A (with ν p (m) = m + 1). We now carry out the developments of Subsections 4.1 and 4.2 with unbounded and bounded replaced by thick and thin, respectively. The definition of forcing and proofs of Lemmas 4.5 and 4.8 are as before. The following observation allows the proof of Proposition 4.6 to go through as well.
Lemma 7.2. If p is thick and S ⊆ P fin (A), then either p ∩ S or p \ S is thick.
Proof. Otherwise there is m 1 such that and there is m 2 such that Let m 1 , m 2 be as above, and let m = m 1 + m 2 . Since p is thick, Fix such n; for a 1 ∈ P ≤m 1 (A) such that ∀b ∈ (p ∩ S) ∩ P ≤n (A) (a 1 b) and a 2 ∈ P ≤m 2 (A) such that ∀b ∈ (p \ S) ∩ P ≤n (A) (a 2 b) we have a 1 ∪ a 2 ∈ P ≤m (A). By ( * * * ) there is b ∈ p ∩ P ≤n (A) such that a 1 ∪ a 2 ⊆ b. Depending on whether b ∈ p ∩ S or b ∈ p \ S, this contradicts (*) or (**).
The next lemma enables a generalization of Lemma 4.9.
Lemma 7.3. Let p n | n ∈ N be such that, for all n, p n ∈ P and p n ⊇ p n+1 . Then there is p ∈ P with the property that for every n there is k ∈ N such that ∀a ∈ (p \ p n ) (|a| ≤ k). In particular, p \ p n is thin.
We show that p is thick. Given m ∈ N, we let n = ν pm (m). If a ∈ P fin (A) and |a| ≤ m, then there is b ∈ p m such that a ⊆ b and |b| ≤ n. By the definition of p, b ∈ p. So n has the required property.
With these changes, the rest of the development of Sections 4.1 and 4.2 goes through and establishes the following strengthening of Proposition 4.15.
Proposition 7.4. The structure N A = (N A , ∈ * , M) for I = P fin (A) satisfies the principles of Transfer, Nontriviality, Boundedness, Standard Part, and Bounded Idealization over A for ∈-formulas with standard parameters.
Proof. To prove that N O one can take d ∈ M such that M "d is a function on I = P fin (A) ∧ ∀a ∈ P fin (A) (d(a) = |a|)". Nontriviality also follows from Bounded Idealization.
Let G m ∈ N and let p, q ∈ G have rank q = k > m. There is some X ∈ M such that M "∀i ∈ I ∀ x 0 , . . . , x k−1 ∈ q(i) (x m ∈ X)." By Proposition 4.6 p, q ∀v (v ∈Ġ m → v ∈X), so ∀v ∈ G m (v ∈ X) holds in N. This proves Boundedness in N.
It remains to prove that Bounded Idealization over A holds in N. Let φ(u, v) be an ∈-formula with parameters from M. Assume that M ∀a ∈ P fin (A) ∃y ∀x ∈ a φ(x, y). By the Reflection Principle in ZF, M "∃ an ordinal α ∀a ∈ P fin (A) ∃y ∈ V α ∀x ∈ a φ(x, y)". We work in the model M.
Let p, q ∈ H be a forcing condition and k = rank q. For i = a ∈ p we let q ′ (a) = q ′ (a) = {∅ k+1 } otherwise. Then p, q ′ extends p, q . For every x ∈ A the set c = p ∩ {a ∈ P fin (A) | x ∈ a} is in P because p \ c is thin (Lemma 7.2), and so, by Proposition 4.6, p, q ′ φ(x,Ġ k ). By the genericity of G there exist p, q ∈ G and k ∈ Ω such that p, q φ(x,Ġ k ) for all x ∈ A. By the Fundamental Theorem 4.12 N φ(x, G k ) for all x ∈ A. This means that the → implication of Idealization over A for ∈-formulas with standard parameters is satisfied in N. The opposite implication follows from SP; see Lemma 2.1 in Section 2.
7.2. Further theories. Nelson's IST postulates a form of Idealization that is even stronger than Bounded Idealization (but it contradicts Boundedness). I Let φ be an ∈-formula with arbitrary parameters.
We let ISPT ′ be the theory obtained from BSPT ′ by deleting Boundedness and replacing Bounded Idealization for formulas with standard parameters by Nelson's Idealization for formulas with standard parameters.
Principle I implies the existence of a finite set that contains all standard sets as elements, and has certain undesirable consequences from the metamathematical point of view. Kanovei and Reeken [19], Theorem 4.6.23, prove that there are countable models M = (M, ∈ M ) of ZFC that cannot be extended to a model of IST in which M would be the class of all standard sets (assuming ZFC is consistent). We do not know whether the same is the case for ISPT ′ . Nevertheless we have the following result.
Theorem 7.5. ISPT ′ is a conservative extension of ZF.
Proof. Let us assume that ISPT ′ ⊢ θ but ZF θ, for some ∈-sentence θ. Let ZF r be ZF with the Axiom Schema of Replacement restricted to Σ r -formulas, and let ISPT ′ r be ISPT ′ with ZF replaced by ZF r . There is r ∈ ω for which ISPT ′ r ⊢ θ. Let M = (M, ∈ M ) be a model of ZF+¬θ. By the Reflection Principle of ZF, valid in M, there is α ∈ M such that M "α is a limit ordinal", M φ Vα for every axiom φ of ZF r , and M (¬θ) Vα .
We let A = V α and use Proposition 7.4 to extend M to a model N A .
On the other hand, (¬θ) Vα holds in M and hence, by Transfer, ¬θ holds in N α . A contradiction.
Kanovei and Reeken [19], Theorem 3.4.5, showed that the class of bounded sets in IST satisfies the axioms of BST. This result holds also for ISPT ′ and BSPT ′ , respectively, and establishes the following theorem.
Theorem 7.6. The theory BSPT ′ is a conservative extension of ZF.
This concludes the proof of Theorem C.
Finally, we prove that if M satisfies ADC, then the model N A constructed in Proposition 7.4 satisfies CC. We note that the definition of forcing for st-∈-formulas in Section 6 and Lemma 6.3 extend to I = P fin (A). Proof. We work in ZFc.
CC: Let us assume that p, q has rank k and p, q By an argument like the one in Lemma 5.3 it follows that for every m and every p ′′ , q ′′ ≤ * p, q there is p ′ , q ′ ≤ p ′′ , q ′′ such that p ′ , q ′ ∈ E m . [We note that the E m may be proper classes, but by the Reflection Principle there is a set S such that p, q ∈ S and for every m and every p ′′ , q ′′ ∈ S there is p ′ , q ′ ≤ p ′′ , q ′′ such that p ′ , q ′ ∈ S ∩ E m . The classes E m can be replaced by the sets S ∩ E m in the argument below.] We let m ′ , p ′ , q ′ R m ′′ , p ′′ , q ′′ iff Applying ADC to the relation R we obtain a sequence p m , q m | m ∈ N such that p 0 , q 0 ≤ p, q and, for each m, p m+1 , q m+1 ≤ p m , q m and p m , q m φ(m,Ġ n ) for some n ∈ N, n > k. Let rank q m = ℓ m and let n m < ℓ m , n m > k, be the least such n.
As in the proof of Lemma 7.3, let p ∞ = ∞ m=0 C m where C m = {a ∈ p m | |a| ≤ ν pm (m)}. We recall that p ∞ \ p m is thin for every m; hence p ∞ , q m φ(m,Ġ nm ). We define a function q ∞ ∈ Q of rank k + 1 as follows: By " Loś's Theorem", p ∞ , q ∞ "Ġ k is a function with domĠ k = N." Now assume that N A ∀ st m ∃v φ(m, v). Then there is p, q ∈ G such that p, q ∀ st m ∃v φ(m, v). By the above discussion, there is a condition of the form p ∞ , q ∞ such that p ∞ , q ∞ ∈ G; hence N "G k is a function with dom G k = N." Fix m ∈ M; let N G k (m) = G ℓ ; we can assume ℓ > k. Then there is some p ′ , q ′ ∈ G, From p ∞ , q m φ(m,Ġ nm ) and Lemma 6.3 it follows that p ∞ , q m ↾ σ m φ(m,Ġ k ). We see from the construction that p ′ ∩ p m , q ′ ↾ σ ′ ≤ p ′ ∩ p m , q m ↾ σ m . As p ′ \ p m is thin, we have p ′ , q ′ ↾ σ ′ φ(m,Ġ k ), and by Lemma 6.3 again, p ′ , q ′ φ(m,Ġ ℓ ). From p ′ , q ′ ∈ G, we conclude that N φ(m, G ℓ ) and hence N φ(m, G k (m)).
CC st : Assuming p, q ∀ st m ∈ N ∃ st v φ(m, v), we can require in the definition of E m that p ′ , q ′ st(Ġ n ), i.e., p ′ , q ′ Ġ n = c zn for a uniquely determined z n . In the definition of q ∞ (a) we can let Let BSCT ′ be the theory obtained from BSPT ′ by adding ADC and strengthening SP to CC; analogously for ISCT ′ . The last two theorems of this section follow by the same arguments as those used to prove Theorems 7.5 and 7.6.
Theorem 7.8. The theory ISCT ′ is a conservative extension of ZFc. Theorem 7.9. The theory BSCT ′ is a conservative extension of ZFc.
We do not know whether N A for I = P fin (A) with uncountable A satisfies SN. In the absence of AC, a way to formulate and prove a suitable analog of Lemma 5.7 is not obvious.
(2) Are the theories BSPT and ISPT conservative extensions of ZF? Are the theories BSCT and ISCT conservative extensions of ZFc?
Here BSPT is obtained from BSPT ′ by strengthening (Bounded) Idealization to allow arbitrary parameters; similarly for the other theories. The likely answer is yes; the obvious approach is to iterate the forcing used to prove the primed versions. Spector develops iterated extended ultrapowers in [33]. His method would require nontrivial adaptations in our framework, but it is likely to work provided the answer to problem (1) is yes. The ultimate result would be that BSCT + SN and ISCT + SN are conservative extensions of ZFc. The likely answer is again yes, using a suitable iteration of extended ultrapowers.
(4) Is SPOT + SC a conservative extension of ZF?
8.2. Forcing with filters. A more elegant and potentially more powerful notion of forcing is obtained by replacing P with P = {P | P is a filter of unbounded subsets of I} where P ′ extends P iff P ⊆ P ′ . " Loś's Theorem" 4.6 then takes the form: P, q φ(Ġ n 1 , . . . ,Ġ ns ) iff rank q = k > n 1 , . . . , n s and ∃p ∈ P ∀i ∈ p ∀ x 0 , . . . , x k−1 ∈ q(i) φ(x n 1 , . . . , x ns ). The forcing notion P we actually use amounts to restricting oneself to principal filters. 8.3. Zermelo set theory. Similar results can be obtained for theories weaker than ZF. Let Z ∞ = ZF − Replacement be the Zermelo set theory, and let BT denote Transfer for bounded formulas. In the proof of Proposition 4.2 the extended ultrapower can be replaced by the extended bounded ultrapower (see Chang and Keisler [5], Sec. 4.4, for a discussion of ordinary bounded ultrapowers). This proves that SPOT − = Z ∞ + O + BT + SP is a conservative extension of Z ∞ . With some modifications, this theory can be taken as an axiomatization of the internal part of nonstandard universes of Keisler [5,22] (the superstructure framework for nonstandard analysis). Analogous results can be obtained for SCOT − , BSPT − and BSCT − . 8.4. Weaker theories. Reverse Mathematics has as its goal the calibration of the exact set-theoretic strength of the principal results in ordinary mathematics. One of its chief accomplishments is the discovery that, with a few exceptions, every theorem in ordinary mathematics is logically equivalent (over S 1 ) to one of the five subtheories S 1 − S 5 of second-order arithmetic Z 2 , known collectively as "The Big Five." Here S 1 is the weakest of the five theories, the second-order arithmetic with recursive comprehension axiom, also denoted RCA 0 , and S 2 , known as WKL 0 , is obtained by adding the Weak König's Lemma to the axioms of RCA 0 . We refer to Simpson [29] for a comprehensive introduction to Reverse Mathematics.
Keisler and others extended the ideas of Reverse Mathematics to the nonstandard realm. In Keisler's paper [23] it is established that if S is any of the "Big Five" theories above, then S has a conservative extension * S to a theory in the language with an additional unary predicate st; the axioms of * S include O, SP and, for the theories stronger than WKL 0 , also FOT (First-Order Transfer). There is an extensive body of work by van den Berg, Sanders and others (see [4], [27] and the references therein) devoted to determining the exact proof-theoretic strength of particular results in infinitesimal ordinary mathematics. Substantial parts of it can be carried out in these and other elementary systems for nonstandard mathematics, for example Nelson [25] and Sommer and Suppes [31]. However, these systems do not enable the natural reasoning as practiced in analysis. They are usually formalized in the language of second-order arithmetic or type theory. Basic objects of ordinary analysis, such as real numbers, continuous functions and separable metric spaces, have to be represented in these theories via suitable codes, and the results may have to be presented "up to infinitesimals," because the full strength of the Transfer principle or the Standard Part principle is not available. The focus of this paper is on theories like SPOT or SPOT − , which axiomatize both the traditional and the nonstandard methods of ordinary mathematics in the way they are customarily practiced. Rather than looking for the weakest principles that enable a proof of a given mathematical theorem, we formulate theories that are as strong as possible while still effective (conservative over ZF) or semi-effective (conservative over ZFc).

8.5.
Finitistic proofs. The model-theoretic proof of Proposition 4.2 as given here is carried out in ZF. Using techniques from Simpson [29], Chapter II, esp. II.3 and II.8, it can be verified that the proof goes through in RCA 0 (w.l.o.g. one can assume that M ⊆ ω).
The proof of Theorem A from Proposition 4.2 requires the Gödel Completeness Theorem and therefore WKL 0 ; see [29], Theorem IV.3.3. We conclude that Theorem A can be proved in WKL 0 .
Theorem A, when viewed as an arithmetical statement resulting from identifying formulas with their Gödel numbers, is Π 0 2 . It is well-known that WKL 0 is conservative over PRA (Primitive Recursive Arithmetic) for Π 0 2 sentences ( [29], Theorem IX.3.16); therefore Theorem A is provable in PRA. Since PRA is generally considered to correctly capture finitistic reasoning as envisioned by Hilbert [10] (see e.g. Simpson [29], Remark IX.3.18), we conclude that Theorem A has a finitistic proof.
These remarks apply equally to Theorems B -D.
8.6. SPOT and CH. Connes (see for example [6], pp. 20-21) objects to the use of ultrafilters but approves of the Continuum Hypothesis (CH). In the absence of full AC, it is important to distinguish (at least) two versions of CH.
CH: Every infinite subset of R is either countable or equipotent to R.
CH + : R is equipotent to ℵ 1 (often written 2 ℵ 0 = ℵ 1 ). The axioms CH and CH + are equivalent in ZFC, but not in ZFc. It is known that ZFc + CH does not imply the existence of any nonprincipal ultrafilters over N (CH holds in the Solovay model). We have: SPOT + CH is a conservative extension of ZF + CH.
Proof. Let φ be an ∈-sentence. Then SPOT However, it seems clear that Connes has CH + in mind. But CH + implies that R has a well-ordering (of order type ℵ 1 ). From this it easily follows that there exist nonprincipal ultrafilters over N (for example, Jech [16], p. 478 proves a much stronger result). Thus Connes's position on this matter is incoherent.
Apart from the issue of CH, Connes's repeated criticisms of Robinson's framework starting in 1994 are predicated on the premise that infinitesimal analysis requires ultrafilters on N (which are incidentally freely used in some of the same works where Connes criticizes Robinson). Our present article shows that Connes's premise is erroneous from the start.

Conclusion
In this paper we observe that infinitesimal methods in ordinary mathematics require no Axiom of Choice at all, or only those weak forms of AC that are routinely used in the traditional treatments. This conclusion follows from the fact that the theory SPOT and its various strengthenings, which do not imply the existence of nonprincipal ultrafilters over N, or other strong forms of AC, are sufficient to carry out infinitesimal arguments in ordinary mathematics (and beyond).
But most users of nonstandard analysis work with hyperreals, and the existence of hyperreals does imply the existence of nonprincipal ultrafilters over N. So it would seem that ultrafilters are needed, after all. However, this view implicitly assumes that set theory like ZFC, based exclusively on the membership predicate ∈, is the only correct framework for Calculus.
Historically, 4 the Calculus of Newton and Leibniz was first made rigorous by Dedekind, Weierstrass and Cantor in the 19th century using the ε-δ approach. It was eventually axiomatized in the ∈-language as ZFC. After Robinson's development of nonstandard analysis it was realized that Calculus with infinitesimals also admits a rigorous formulation, closer to the ideas of Leibniz, Bernoulli, Euler (see [1]) and Cauchy (see [2]). It can be axiomatized in a set theory using the st-∈language. The primitive predicate st can be thought of as a formalization of the Leibnizian distinction between assignable and inassignable quantities. Such theories are obtained from ZFC by adding suitable versions of Transfer, Idealization and Standardization.
Now that it has been established that the infinitesimal methods do not carry a heavier foundational burden than their traditional counterparts, one can ask the following question. Which foundational framework constitutes a more faithful formalization of the techniques of the 17-19 century masters? For all the achievements of Cantor, Dedekind and Weierstrass in streamlining analysis, built into the transformation they effected was a failure to provide a theory of infinitesimals which were the bread and butter of 17-19 century analysis, until Weierstrass. By the yardstick of success in formalization of classical analysis, arguably SPOT, SCOT and other theories developed in the present text are more successful than ZF and ZF + ADC.
One can learn to work in the universe of an st-∈-set theory intuitively. This universe can be viewed as an extension of the standard set-theoretic universe, either by a (soritical) predicate st (the internal picture) or by new ideal objects (the standard picture); see Fletcher et al. [8], Sec. 5.5, for a detailed discussion. 5 This extended universe has a unique set of real numbers, constructed in the usual way, and containing both standard and nonstandard elements. It also of course has choice functions and ultrafilters over N, just as the universe of ZFC does. Mathematicians concerned about AC can analyze their methods of proof and determine whether a particular result can be carried out in one of the theories considered in this paper. For most if not all of ordinary mathematics, both traditional and infinitesimal, the answer is likely to be affirmative. It then follows from Theorems A -D that these results are just as effective as those provable in ZF or ZF+ADC.