See the article 21e in *Annals
of Pure and Applied Logic* by Karel Hrbacek and Mikhail Katz.

It turns out that 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. This enables
*effective infinitesimals* in ℝ.

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 a conservative extension of 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".

Since SPOT incorporates the axioms of ZF, the natural numbers ℕ and the real numbers ℝ are developed as usual.

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 such a μ, 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 *limited*, and otherwise *unlimited*. SPOT
proves that every nonstandard natural number is unlimited.

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

Then the derivative of *f* (*x*) is
**sh**((*f*(*x*+ε) - *f*(*x*))/ε).
In more detail, a standard number *L* is the slope of
*f* at a standard point *x* if
(∀^{in}ε) (∃^{in} ℓ)
*f*(*x*+ε) - *f*(*x*) =
(*L*+ℓ)ε. Here ∀^{in} and
∃^{in} denote quantification over infinitesimals.

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 approach (conservative over ZF) to analysis with infinitesimals. SPOT is a subtheory of axiomatic (syntactic) theories developed in the 1970s independently by Hrbacek and Nelson. In addition the the axioms of ZF, SPOT has the following three axioms:

**T** (Transfer) Let φ be an ∈-formula with
standard parameters. Then ∀^{st} x φ(x) →
∀x φ(x).

The intuitive meaning of the transfer axiom is that a statement known
to be true for all standard inputs of the variables, should be true
for all inputs. Thus, knowing that a relation
cos^{2}*x*+sin^{2}*x*=1 holds for
all standard *x* should entail its validity for all *x*.
In Leibnizian terminology, whatever is true in the finite realm,
should remain true in the infinite realm (in the context of axiomatic
systems such as SPOT, it is preferable to use the term "unlimited
integer" rather than "infinite integer").

**O** (Nontriviality) ∃ν ∈ ℕ
∀^{st} n ∈ ℕ (n ≠ ν).

Nontriviality asserts that an unlimited natural number exists (or equivalently that a nonzero infinitesimal exists).

**SP** (Standard Part) Every limited real is infinitely
close to a standard real.

Equivalently,
**SP'** (Standard Part) ∀A ⊆ ℕ
∃^{st} B ⊆ ℕ ∀^{st} n ∈
ℕ (n ∈ B ↔ n ∈ A).

Intuitively, the equivalence of SP and SP' can be understood in terms
of the binary expansion of a real number *x*. If A denotes the set of
ranks at which the corresponding digit of *x* is 1, and B denotes the
set of ranks at which the corresponding digit
of **sh**(*x*) is 1, then the fact that *x*
and **sh**(*x*) are infinitely close corresponds to the
fact that A and B agree at all standard (limited) ranks.

See also

Effective infinitesimals in R (MOPA)

Fermat

Leibniz

Euler

Cauchy

Skolem

Robinson

Nelson

Hrbacek

More on infinitesimals

Return to homepage