Infinitesimal analysis without the axiom of choice

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.

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". 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. 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.

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 ε) (∃0in ℓ) f(x+ε) - f(x) = (L+ℓ)ε. Here ∀in denotes quantification over nonzero infinitesimals, whereas ∃0in 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 (xi)ε as i runs from 1 to μ, where the xi 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).

O (Nontriviality) ∃ν ∈ ℕ ∀st n ∈ ℕ (n ≠ ν).

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).

SPOT as a conservative extension of Zermelo-Fraenkel (MO)
More on infinitesimals
Return to homepage