See the article 21d in *Annals
of Pure and Applied Logic* by Karel Hrbacek and myself.

Analysis with infinitesimals does not require the axiom of choice any
more than traditional non-infinitesimal analysis. There are two
popular approaches to Robinson's mathematics (including analysis with
infinitesimals): model-theoretic and axiomatic/syntactic. The
model-theoretic approach (including the construction of the
ultrapower) typically relies on strong forms of the axiom of choice.
The axiomatic/syntactic approach turns out to be more economical in
the use of foundational material, and exploits a richer
**st**-∈-language, as explained below.

The traditional set-theoretic foundation for mathematics is Zermelo-Fraenkel set theory (ZF). The theory ZF is a set theory in the ∈-language. Here "∈" is the two-place membership relation. In ZF, all mathematical objects are built up step-by-step starting from ∅ and exploiting the one and only relation ∈.

For instance, the inequality 0<1 is formalized as the membership relation ∅∈{∅}, the inequality 1<2 is formalized as the membership relation {∅}∈{∅,{∅}}, etc. Eventually ZF enables the construction of the set of natural numbers ℕ, the ring of integers ℤ, the field of real numbers ℝ, etc.

The following questions are meant as motivation for the sequel:

1. Why should all of mathematics be based on a single relation?

2. Could such a foundational choice have been the result of historical contingency rather than mathematical necessity?

3. Do other set-theoretic foundational possibilities exist?

For the purposes of mathematical analysis, a more congenial set theory
SPOT has been developed in the more versatile
**st**-∈-language, exploiting a predicate
**st** in addition to the relation ∈. The theory SPOT
is proved to be conservative over ZF. Thus SPOT does not require any
additional foundational commitments beyond ZF. In particular, the
axiom of choice is not required, and nonprincipal ultrafilters are not
required. Here "**st**" is the one-place predicate
*standard* so that **st**(*x*) is read
"*x* is standard". The predicate **st**
formalizes the distinction already found in
Leibniz
between *assignable* and *inassignable* numbers. An
inassignable (nonstandard) natural number μ∈ℕ is greater
than every assignable (standard) natural number in ℕ.

The reciprocal of μ, denoted ε=1/μ∈ℝ, is an
example of a positive infinitesimal (smaller than every positive
standard real). Such an ε is a nonstandard real number. A
real number smaller in absolute value than some standard real number
is called *finite*, and otherwise *infinite*. Every
nonstandard natural number is infinite.

The theory SPOT enables one to take the standard part, or
*shadow*, of every finite real number *r*, denoted
**sh**(*r*). This means that the difference
*r* - **sh**(*r*) is
infinitesimal.

The derivative of *f* (*x*) is then
**sh**((*f*(*x*+ε) - *f*(*x*))/ε).
In more detail, a standard number *L* is the derivative of
*f* at a standard point *x* if (∀^{in}
ε) (∃_{0}^{in} ℓ)
*f*(*x*+ε) - *f*(*x*) =
(*L*+ℓ)ε. Here ∀^{in} denotes
quantification over nonzero infinitesimals, whereas
∃_{0}^{in} denotes quantification over all
infinitesimals (including 0).

The definite integral of *f* over [*a*,*b*] (with
*a*, *b* standard) is the shadow of the infinite sum
Σ_{i=1}^{μ} *f*
(*x*_{i})ε as i runs from 1 to μ,
where the *x*_{i} are the partition points of
an equal partition of [*a*,*b*] into μ subintervals.

We will present the axioms that enable this effective (i.e., ZF-based)
approach to analysis with infinitesimals. SPOT is a subtheory of
axiomatic (syntactic) theories developed in the 1970s independently by
Hrbacek and Nelson.