Hello list,
I am looking for references on the following facts about interpreting
some sentences involving infinitesimals in filter-powers instead of in
ultrapowers...
Notation:
\I is an index set;
\F is a filter on \I;
\U is an ultrafilter on \I, possibly extending \F;
if X is a topological space and x is a point of X, then
\V_x is the filter of neighborhoods of x in X;
Set^\F is a shorthand for the filter-power (Set^\I)/\F;
Set^\U is a shorthand for the ultrapower (Set^\I)/\U;
Terminology:
Set is the "standard universe";
Set^\U is the "non-standard universe";
Set^\F is the "semi-standard universe";
points of Set^\I are called "sequences", or "pre-hyperpoints";
points of Set^\F or Set^\U are called "hyperpoints".
Well, the facts. Here they are:
(1) For any (standard) function f:X->Y from a topological space to
another, and for any standard point x in X, the following three
statements are equivalent:
(a) f is continuous at x;
(b) for all choices of a triple (\I, \F, x_1), where \I is an
    index set, \F is a filter on \I, and x_1 is a hyperpoint
    infinitely close to x, then f(x_1) is infinitely close to f(x);
(c) for the "natural infinitesimal" (\I, \F, x_1) := (X, \V_x, id),
    the hyperpoint f(x_1) is infinitely close to f(x).
(2) Any filter-infinitesimal (\I, \F, x_1) infinitely close to x
factors through the natural infinitesimal (X, \V_x, id) in a unique
way.
(3) We can use these ideas to lift proofs done in a certain "strictly
calculational fragment" of the language of non-standard analysis to
constructions done in a filter-power; and then, if we replace the
free variables that stand for infinitesimals in our formulas by
natural infinitesimals, we get (by (c)<=>(a) in (1)) a translation
of our proof with infinitesimals to a standard proof, in terms of
limits and continuity.
On the one hand, I have never seen anything published about
filter-infinitesimals, and it took me a long time to find the right
formulations for this... on the other hand, ideas similar to these
seem to be implicit in many places (see the last sections of the PDF).
However, my guess is that at least parts of (3) are new.

Natural Infinitesimals in Filter-Powers

Eduardo Ochs

                 eduardoochs@gmail.com
                  http://angg.twu.net/

Preliminary version - 2008jul13

Proofs in non-standard analysis are done by moving back and forth between two universes, the standard universe, Set, and the non-standard universe, Set^{𝕀}/U. Here we will work also with two other universes between Set and Set^{𝕀}/U: Set^{𝕀}, the universe of (𝕀-indexed) sequences, and Set^{𝕀}/F, the “semistandard universe”, in which sequences are identified when the set of indices where they coincide is “F-big”.

Intuitively, the filter-power Set^{𝕀}/F is a generalization of Set^{ℕ}/N, where N is the filter of cofinite sets of naturals. Let’s use the prefixes “pre-hyper-” and “hyper-” to refer to elements of a Set^{𝕀} and of a Set^{𝕀}/F respectively. Sequences of reals tending to zero are pre-hyperreals (in Set^{ℕ}) whose corresponding hyperreals in Set^{ℕ}/N — or in a Set^{ℕ}/ℕ, where U is a ultrafilter extending N — behave as infinitesimals.

In a certain sense, ultrapowers are much more well-behaved than filterpowers: the logic of a Set^{𝕀}/U is two-valued, and we have certain “transfer theorems” that transfer truths from Set to a Set^{𝕀}/U and back. The logic of a non-trivial filter-power, however, is boolean but not two-valued; what we will show here is that certain “purely calculational” proofs involving infinitesimals can be lifted through the quotient Set^{𝕀}/F → Set^{𝕀}/U, yielding proofs in a filterpower Set^{𝕀}/F that can be immediately reinterpreted as being standard proofs in disguise; “infinitesimality” becomes “continuity”.

Important: I don’t know how much of this is new. This preliminary version has two main intents: (1) to request feedback and pointers to the literature from people who know the subject infinitely more than me, and (2) to give some elementary motivation for topos theory to the regular attendants of the local Logic seminar — the logic of a filter-power, being boolean, is much easier to grasp than the one of a non-boolean topos. Intent (2) made me write this in a very elementary way; I apologize in advance to the “(1)” people for the length of the text, and for the obviousness of some parts.

1 A very quick introduction to filters

A filter F on an index set 𝕀 is a family of subsets of 𝕀, F ⊂ P(𝕀), such that:

• 𝕀 ∈ F;

• if I, I′ ∈ F and I ∩ I′ ⊆ I′′ ⊆ 𝕀 then I′′ ∈ F.

These two conditions are exactly what it is needed to make

(a_{i}) ∼ (b_{i}) ⇔^{def} { i ∈ 𝕀 | a_{i} = b_{i} } ∈ F

an equivalence relation: we want (a_{i}) ∼ (a_{i}), so 𝕀 ∈ F; and if (a_{i}) and (b_{i}) coincide when i ∈ I, and (b_{i}) and (c_{i}) coincide when i ∈ I′, then (a_{i}) and (c_{i}) coincide at some set of indices I′′ ⊃ I ∩ I′, so we need the second condition to make ‘∼’ transitive.

This will be our archetypical filter (the “filter of cofinites”):

N := { I ⊂ ℕ | I is cofinite (i.e., ℕ\I is finite) }.

We will also need “filters of neighborhoods”, “filters of punctured neigborhoods”, and “filters of strictly punctured neighborhoods”. Fix a topological space X and a point x ∈ X; an open neighborhood of x in X is an open set U ⊆ X containg x; a neighborhood of x in X is a set V ⊆ X containing some open neighborhood of x; a punctured neighborhood of x is a set V ⊂ X such that V ∪ {x} is a neighborhood of x; and a strictly punctured neighborhood of x is a set V ⊆ X\{x} such that V ∪ {x} is a neighborhood of x.

These filters will also be useful later: if x ∈ X is a point in a topological space (X, O(X)), then:

\begin{aligned}V_{x} & := & \{ V | ∃U ∈ O(X). x ∈ U ⊆ V ⊆ X \} \\ V_{x}^{−} & := & \{ V | ∃U ∈ O(X). x ∈ U ⊆ (V ∪ \{ x \}) ⊆ X \} \end{aligned}

V_{x} is the filter of neighborhoods of x; V_{x}^{−} is the filter of punctured neighborhoods of x. Sometimes “V_{x}^{−}” will stand for a filter on X, sometimes for a filter on X\{ x }.

(By the way: N is the filter of punctured neighborhoods of ∞ in the onepoint compactification of ℕ.)

Let’s define two operations on families of subsets of 𝕀:

\begin{aligned}↑A & := & \{ A′ ⊆ 𝕀 | ∃A ∈ A.A ⊆ A′ ⊆ 𝕀 \} \\ ⋂_{fin} A & := & \{ A_{1} ∩ … ∩ A_{n} | n ∈ ℕ, A_{i} ∈ A \} \end{aligned}

In ⋂_{fin} A we consider that when n = 0 the intersection “A_{1} ∩ … ∩ A_{n}” is 𝕀. Fact: for any family A of subsets of 𝕀, the family ⋂_{fin} ↑A (that is equal to

↑ ⋂_{fin} A) is a filter on 𝕀 — the “filter generated by A”.

Let’s call a filter F on 𝕀 bad when F = P(𝕀).

A non-bad filter F divides the sets in P(𝕀) in three classes:

• The F-big sets are the ones in F; • The F-small sets sets are the ones whose complements are F-big;

• The F-medium sets are the other sets in P(𝕀) - the ones that are neither F-big nor F-small.

The cofinite subsets of ℕ are N -big; the finite subsets are N -small; and for any k ∈ { 2, 3, 4, … } the set of multiples of k (“kℕ”) is N -medium.

An ultrafilter U on 𝕀 is a (non-bad) filter on 𝕀 that divides the subsets of 𝕀 in just U-big and U-small subsets; there are no U-medium subsets.

We will reserve the notation ‘U’ for ultrafilters.

A non-bad filter F on 𝕀 is said to be principal when ⋂ F ≠ ∅. For each nonempty set I ⊂ 𝕀, ↑{I} is a principal filter; ↑{I} is an ultrafilter iff I has exactly one element. N is not principal. Filters and ultrafilters of the form ↑{I} induce trivial equivalence relations; we are more interested in non-principal filters and ultrafilters.

All naïve attempts to construct non-principal ultrafilters explicitly — say, by enlarging filters until no more medium sets are left — are bound to fail. The following argument does not prove this (which is very hard; reference?) but it is easy enough, and quite enlightening.

Take a denumerable set A = { A_{1}, A_{2}, A_{s}, … } of generators; form the sequence A′_{1} := A_{1}, A′_{2} := A_{1} ∩ A_{2}, A′_{3} := A_{1} ∩ A_{2} ∩ A_{3}, …, and then form the sequence A′′_{1}, A′′_{2}, A′′_{3}, … by removing the repetitions from A′_{1}, A′_{2}, A′_{3}, …. Clearly, ↑ ⋂_{fin} A = ↑ ⋂_{fin} A′ = ↑A′ = ↑A′′, where A′′ := { A′′_{1}, A′′_{2}, … }; if A′′ is finite, A′′ = { A′′_{1}, …, A′′_{n} }, then ↑A′′ = ↑{ A′′_{n} }; if A′′_{n} = ∅ then ↑A′′ is bad, and if A′′_{n} ≠ ∅ then ↑A′′ is principal.

If A′′ is infinite, take the sequence of “differences” D_{1} = A′′_{1}\A′′_{2}, D_{2} = A′′_{2}\A′′_{3}, …; both D_{1} ∪ D_{3} ∪ D_{5} ∪ … and D_{2} ∪ D_{4} ∪ D_{6} ∪ … are ↑A′′-medium sets, and so ↑A′′ is not an ultrafilter.

2 A very quick introduction to NSA

More terminology:

Set is the standard universe. Set^{𝕀}/U is the non-standard universe. Set^{𝕀}/F (here F can be just a filter) is the semi-standard universe. A pre-hyperpoint is a point of Set^{𝕀}, i.e., an 𝕀-indexed sequence. A hyperpoint is a point of Set^{𝕀}/F or Set^{𝕀}/U, i.e., the image of a sequence

by the quotients ‘/F’ or ‘/U’ — i.e., an equivalence class of sequences.

A standard element of Set^{𝕀} or Set^{𝕀}/F is a constant sequence (modulo the equivalence relation, maybe).

The obvious maps

[figure: Set; Set^{𝕀}; Set^{𝕀}; Set^{𝕀}/F; Set^{𝕀}; Set^{𝕀}/U; Set^{𝕀}/F; Set^{𝕀}/U]

will not usually be named. When F ⊂ U the map Set^{𝕀}/F → Set^{𝕀}/U exists; it takes each equivalence class of sequences into a bigger equivalence class.

Now take this (pre-)hyperreal: ϵ := (1, \frac{1}{2}, \frac{1}{3}, …). For any standard interval containing 0, say, U := (−\frac{1}{4}, \frac{1}{4}), the sentence “ϵ ∈ U” is true in Set^{ℕ}/N: the sequence of truth-values

(1 ∈ U, \frac{1}{2} ∈ U, \frac{1}{3} ∈ U, …)

is false for the first indices, but true from some point on, and so it coincides with (⊤, ⊤, ⊤, …) in a big set of indices.

We will say that a pre-hyperpoint x′ is infinitely close to a standard point x when for any standard open set U containing x the sentence “x′ ∈ U” is true in a big set of indices.

Following these ideas, ϵ := (1, \frac{1}{2}, \frac{1}{3}, …) is infinitely close to 0 — but ϵ > 0.

Typical proofs in NSA work a part of the time in Set and part in a Set^{𝕀}/U, using certain “transfer theorems” to “transfer truths” between the standard and the non-standard universe; the details are complex, and not relevant now. This observation, however, is crucial:

In a Set^{𝕀}/U every (𝕀-indexed) sequence of truth-values is either equivalent to ‘true’ or to ‘false’; but in a Set^{𝕀}/F we may have more truth-values. For example, (⊤, ⊥, ⊤, ⊥, ⊤, ⊥, …) only coincides with (⊤, ⊤, ⊤, …) and with (⊥, ⊥, ⊥, …) in medium sets of indices.

So, in a ‘Set^{𝕀}/U’ we have transfer theorems, and a two-valued logic. Everything seems to indicate that ‘Set^{𝕀}/U’s are better than ‘Set^{𝕀}/F’s, but...

3 Ultrafilters are evil (in a sense)

The existence of non-principal ultrafilters is a consequence of the Axiom of Choice, and it is independent of ZF, but the proof of this is quite hard; see [Hal64]. What matters here is: ultrafilters are a source of non-intuitiveness in the semantics; proofs done in Set^{𝕀}/U may be hard to translate to standard proofs in Set. On the other hand, proofs done in a Set^{𝕀}/F — especially proofs in Set^{ℕ}/N — are easy to translate; when the filters are explicilty presented, they are standard proofs in disguise.

One of the reasons why NSA never gained very wide acceptance was because it has been proved that by using NSA one “cannot prove anthing new” (this is only true for some

One of the reasons why NSA never gained very wide acceptance was because it was believed that by using NSA one “cannot prove anthing new” (actually this is only true for some classes of formulas; see [HK86]). Proofs using infinitesimals may be clearer and shorter, but infinitesimals are like objects that we are not supposed to play with (because they are “unnecessary”?!), and we may need to hide them quickly when the grown-ups approach... From this point of view, one class of proofs in Set^{𝕀}/U is especially interesting: the ones that “lift” to a filter-power Set^{𝕀}/F, from where they can be translated quickly to standard proofs.

I don’t know how to characterize the full class of “liftable” proofs yet — but it seems that “purely calculational” proofs can be lifted. I am going to give a definition of “purely calculational” proofs — that may be overly restrictive —, and show how to lift and translate proofs of that form. We will focus on a single example, that seems to be rich enough:

4 A proof with infinitesimals

Definition (tentative, and sketchy): a purely calculational proof with infinitesimals is one made of a series of steps of the forms:

“∀x_{1} ∼ x_{0}.f(x_{1}) = g(x_{1})” or

“∀x_{1} ∼ x_{0}.∃!y_{1} ∼ y_{0}.f(x_{1}) = h(x_{1}, y_{1})”, where x_{0}, y_{0}, f, and g are standard.

These steps can be composed in several ways. Let’s look at an example. Suppose that we want to prove that lim_{n→+∞}(1 + \frac{a}{n})^{n} = e^{a}; it is enough to

prove that for any infinitely big natural number ω, (1 + \frac{a}{ω})^{ω} ∼ e^{a}. The calculations are the ones below, at the left; the right side shows some abbreviations. Note that we write just “g_{1}” for “g_{1}(ω)”, “h_{3}” for “h_{3}(ω, o′)”, etc.

At some steps new symbols — o, o′, o′′ — are introduced. Their names (“little ‘o’ ”s) imply that they are infinitesimals, and there are implicit quantifiers: “there is a unique value for o (or o′, or o′′) here making the equality hold”. At g_{4} we introduce an ‘O’, that stands for a “finite hyperreal”. Readers who are not familiar with this concept ([SL76], sec.4.4.1) should just skip this step.

\frac{a}{ω} = o  g_{1} = g_{2}
f(b + o) = f(b) + f′(b) o + Oo^{2}  g_{3} = g_{4}
= f(b) + f′(b) o + o′o  = g_{5}
= f(b) + (f′(b) + o′)o  = g_{6}
log(1 + o) = (1 + o′)o  g_{7} = g_{8}
log (1 + \frac{a}{ω})^{ω} = ω log (1 + \frac{a}{ω})  h_{1} = h_{2}
= ω ((1 + o′) \frac{a}{ω})  = h_{3}
= (1 + o′) a  = h_{4}
(1 + \frac{a}{ω})^{ω} = e^{((1+o′) a)}  h_{5} = h_{6}
= e^{(a+o′a)}  = h_{7}
= e^{(a+o′′)}  = h_{8}
= e^{a} + o′′′.  = h_{9}
[figure: ω; o; ω; g_{1}; o; g_{2}; g_{1}; g_{2}; o; o, O; o, O; o, o′; o; g_{3}; o, O; g_{4}; o, o′; g_{5}; o, o′; g_{6}; g_{3}; g_{4}; g_{4}; g_{5}; g_{5}; g_{6}; ω; ω, o′; ω, o′; o′; o′; o′′; o′′; o′′′; h_{1}; h_{2}; h_{2}; h_{3}; h_{3}; h_{4}; h_{5}; h_{6}; h_{6}; h_{7}; h_{7}; h_{8}; h_{8}; h_{9}; ω; h_{1}; ω; h_{2}; ω, o′; h_{3}; o′; h_{4}; o′; h_{7}; o′′; h_{8}; o′′′; h_{9}; h_{1}; h_{5}; exp; h_{4}; h_{6}; exp]

When we compose all cells we get this:

[figure: ω; o′′′; ω; h_{5}; o′′′; h_{9}; h_{5}; h_{9}; ω; o′′′; ω; (1 + \frac{a}{ω})^{ω}; o′′′; e^{a} + o′′′; (1 + \frac{a}{ω})^{ω}; e^{a} + o′′′]

We will see how to lift this proof to a standard proof.

5 Filtered spaces

Definitions: a filtered space is a pair (X, X) where X is a set and X is a filter over X; a function from (X, X) to (Y, Y) is a function from an X -big subset of X to Y; a total function from (X, X) to (Y, Y) is a function defined on the whole set X. We say that a function f : (X, X) → (Y, Y) is continuous when the inverse image by f of each Y-big set is an X -big set, and we say that two functions f, g : (X, X) to (Y, Y) are equivalent when they coincide on some X -big set.

If f, f′ : (X, X) → (Y, Y) are equivalent and continuous, and g, g′ : (Y, Y) → (Z, Z) are also equivalent and continuous, then (f; g) and (f′; g′) are also equivalent and continuous.

[figure: (X, X); (Y, Y); f; (X, X); (Y, Y); f′; (Y, Y); (Z, Z); g′; (Y, Y); (Z, Z); g; (X, X); (Z, Z)]

A topological space (X, O(X)) with a chosen point x_{0} ∈ X has a natural filtered space structure: take X := X_{x_{0}}, the filter of neighborhoods of x_{0}.

A function f : X → Y between two topological spaces can be seen as a (total) function between filtered spaces. If f takes x_{0} to y_{0}, then f : X → Y is continuous at x_{0} iff f : (X, X_{x_{0}}) → (Y, Y_{y_{0}}) is continuous.

Now fix an index set 𝕀 and a filter F on it; our semi-standard universe will be Set^{𝕀}/F.

A pre-hyperpoint of (X, X) is a function from (𝕀, F) → (X , X). A total pre-hyperpoint of (X, X) is a function whose domain is the whole 𝕀. Two prehyperpoints (𝕀, F) → (X, X) are equivalent when they coincide in an F-big set of indices. Hyperpoints are pre-hyperpoints modulo equivalence.

A pre-infinitesimal in (X, X_{x_{0}}), for us, will be a pre-hyperpoint x_{1} : (𝕀, F) → (X, X_{x_{0}}) “infinitely close to the chosen point” x_{0}, in the sense that for each standard neighborhood X′ ∋ x_{0} the x_{1} belongs to X′ for a big set of indices — formally, ∀X′ ∈ X_{x_{0}}.x_{1}^{−1}(X′) ∈ F. Infinitesimals are pre-infinitesimals modulo equivalence.

Note that as the chosen point doesn’t need to be 0, “infinitesimal” becomes an umbrella term that can mean “infinitely small” (x_{0} = 0), “infinitely close to”, and even “infinitely big” (x_{0} = ∞).

These definitions were all chosen to make this work:

Key idea: infinitesimality is the same as continuity at the chosen point.

When we look at things in this way then it becomes obvious that a standard continuous function f : X → Y taking x_{0} to y_{0} takes any infinitesimal x_{1} ∼ x_{0} to an infinitesimal f(x_{1}) ∼ y_{0}.

[figure: (𝕀, F); (X, X_{x_{0}}); x_{1}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); f]

As this holds for and index set 𝕀, any filter F on 𝕀, and any infinitesimal x_{1} ∼ x_{0}, we can do much more.

6 Natural Infinitesimals

Definition: the natural infinitesimal on a (standard) filtered space (X, X_{x_{0}}), that we will denote by x_{1}^{♮} ∼^{♮} x_{0}, is the identity function x_{1}^{♮} = id : (X, X_{x_{0}}) → (X, X_{x_{0}}); seen as an infinitesimal, it lives in Set^{X}/X_{x_{0}}. As it corresponds to the identity map, any other infinitesimal x_{1} ∼ x_{0} — in the diagram below we take an x_{1} living in Set^{𝕀}/F — factors through x_{1}^{♮} it in a unique way; this suggests that there is a kind of “change of base” operation between filter-powers.

[figure: (𝕀, F); (X, X_{x_{0}}); x_{1}; (𝕀, F); (X, X_{x_{0}}); x_{1}; (X, X_{x_{0}}); (X, X_{x_{0}}); x_{1}^{♮}=id]

Now, for any f : (X, X_{x_{0}}) → (Y, Y_{y_{0}}) taking x_{0} to y_{0}, this holds:

Key theorem:

(i) f is continuous at x_{0}

⇔ (ii) for (𝕀, F) := (X, X_{x_{0}}), x_{1}^{♮} ∼^{♮} x_{0}, we have f(x_{1}^{♮}) ∼ f(x_{0})

⇔ (iii) for all (𝕀, F) and x_{1} ∼ x_{0}, we have f(x_{1}) ∼ f(x_{0}).

[figure: (X, X_{x_{0}}); (X, X_{x_{0}}); x_{1}^{♮}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); y_{1}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); f; (𝕀, F); (X, X_{x_{0}}); x_{1}; (𝕀, F); (Y, Y_{y_{0}}); y_{1}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); f; x; x; x_{1}^{♮}; x; y; y_{1}; x; y; f; i; x; x_{1}; i; y; y_{1}; x; y; f]

Proof: (i) ⇒ (ii) and (i) ⇒ (iii) are obvious from what we’ve seen before — that the composite of continuous maps between filtered spaces is continuous. For ¬(i) ⇒ ¬(ii), as f is not continuous at x_{0}, we can choose a Y′ ∈ Y_{y_{0}} such that f^{−1}(Y′) ∉ X_{x_{0}}; but then y_{1}^{−1}(Y′) = x_{1}^{♮^{−1}}(f^{−1}(Y′)) ∉ X_{x_{0}}, and f(x_{1}^{♮}) ≁ f(x_{0}). For ¬(i) ⇒ ¬(iii), take (𝕀, F) := (X, X_{x_{0}}), x_{1} := x_{1}^{♮}, and reuse the proof of ¬(i) ⇒ ¬(ii).

In texts about Non-Standard Analysis the infinitesimal characterization of continuity is presented in another form:

(i) f is continuous at x_{0}

⇔ (iv) for all (𝕀, U) and x_{1} ∼ x_{0}, we have f(x_{1}) ∼ f(x_{0}).

Clearly, (iii)⇒(iv); but to show that (iv) implies the rest we need to be in a universe with enough ultrafilters; [Ban83] is probably a good reference.

[B. Banaschewski, The Power of the Ultrafilter Theorem, Journal of the London Mathematical Society (2) 27, 193–202, 1983.]

7 Translating a proof with infinitesimals

Each of the cells in the diagram in sec. 5 is an instance of the key theorem — maybe slightly disguised. For example, to prove that g(b + o) = (g′(b) + o′)o we may start with \frac{g(b+o)}{o} −g′(b) = o′, for an infinitesimal o ≠ 0, i.e., lim_{ϵ→0} \frac{g(b+o)}{o}.

What really matters, when we look at the diagrams, is that for any (𝕀, F) and for any infinitesimal x_{1} : (𝕀, F) → (X, X_{x_{0}}) — maybe obeying some condition, like o ≠ 0 — there is a unique “adequate” infinitesimal y_{1} : (𝕀, F) → (Y, Y_{y_{0}}); we want to “represent” the operation x_{1} ↦ y_{1} as a function f : (X, X_{x_{0}}) → (Y, Y_{y_{0}}), and we can do that trivially by setting (𝕀, F) := (X, X_{x_{0}}), x_{1} := x_{1}^{♮}; then we can take f := y_{1}, and the f obtained in this way works in the general case.

[figure: (𝕀, F); (X, X_{x_{0}}); x_{1}; (𝕀, F); (Y, Y_{y_{0}}); y_{1}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); f; (X, X_{x_{0}}); (X, X_{x_{0}}); x_{1}^{♮}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); y_{1}; (X, X_{x_{0}}); (Y, Y_{y_{0}}); f:=y_{1}]

Applying this idea to the composite of all cells in the example in sec. 5, we get this:

[figure: i; ω; i; o′′′; ω; o′′′; ω; h_{5}; o′′′; h_{9}; h_{5}; h_{9}; n; ω; n; o′′′; ω; o′′′; ω; (1 + \frac{a}{ω})^{ω}; o′′′; e^{a} + o′′′; (1 + \frac{a}{ω})^{ω}; e^{a} + o′′′; n; (1 + \frac{a}{n})^{n}; n; e^{a} + o′′′(n); (1 + \frac{a}{n})^{n}; e^{a} + o′′′(n)]

where i ∈ (𝕀, F), n, ω ∈ (ℕ, N), and all the other “points” live in (ℝ, R_{0}). Note that the ‘↦’ arrows in this diagram do not stand for functions in the usual sense, but for functions between filtered spaces (not necessarily total). Incidentally, all of them are continuous.

8 Future directions

Let Filt be the category of filtered spaces (in Set). For each filtered space (𝕀, F), the filter-power Set^{𝕀}/F can be seen as the fiber of some bigger category (a fibration, of course!), over the object (𝕀, F) of the base category Filt.

I have not attempted (yet) to define precisely this fibration, or to study it — but it seems to be the right place to interpret “change of base” steps, like the passage from h_{5} = h_{6} to h_{6} = h_{8} n the example. By the way, the quotient Set^{𝕀}/F → Set^{𝕀}/U described in [...] (for F ⊂ U) is associated to seeing id : 𝕀 → 𝕀 as a continuous function (𝕀, U) → (𝕀, F).

Take a filter F over 𝕀, and add the empty set to it: this new set of subsets, F ∪ ∅ ⊂ P(𝕀), is a topology on 𝕀 — a funny one, in which there are no “divisors of zero”: the intersection of two non-empty open sets is always another nonempty set. Now regard the topology F ∪ {∅} as a Heyting algebra; the doublenegation operation takes ∅ to itself, and all non-empty open sets to X. I have the impression that if we sheafify Set^{(𝕀,F∪{∅})} (using the ‘¬¬’ modality?) we get Set^{𝕀}/F — and then geometric morphims, etc. But (as my terminology reveals!) I know far less about sheaves than I should...

Define the “diameter” of a set in ℝ in the obvious way. A standard function f : ℝ → ℝ is continuous at a iff for any infinitesimal o, diam(f([a−o, a+o])) is an infinitesimal. It is easy to adapt this idea to a set-valued function F : ℝ → P(ℝ), or to a relation R ⊂ ℝ × ℝ. We may then consider a variation of the set-valued function F, which will take a real x and a “hint”, and then return an element of F (x); the hint selects which one. If we move the hint parameter to the index set we get a point-valued non-standard function that in some senses represents the behavior of the standard set-valued function F.

Take some function g : ℝ^{2} → ℝ^{2} that has two derivatives at a point a ∈ ℝ^{2}. For infinitesimals o in ℝ^{2}, we have that g(a + o) = g(a) + (g′(a) + o′)o — i.e., there exists an infinitesimal non-standard function o′ : ℝ^{2} → ℝ^{2} that makes the equation hold... but this o′ is by no means unique!

I have only described cases where the new infinitesimals are related to the previous ones by “unique existentials”, as in ∀ω ∼ ∞.∃!o ∼ 0.R(ω, o). I have the impression that it should be possible to deal with steps that introduce new infinitesimals with just ‘∃’, like:

∀x_{1} ∼ x_{0}. ∃y_{1} ∼ y_{0}. R(x_{1}, y_{1})—

a sentence like that one is exactly when for any (standard) neighborhood Y′ ∈ Y_{y_{0}} of y_{0} its inverse image

X′ := { x ∈ X | ∃y ∈ Y′. R(x, y) }

is a neighborhood of x_{0} — i.e., this operation Y′↦X′ is continuous... it seems that in these cases the natural infinitesimal should have R ⊆ X ⊆ Y as its index set.

9 Related work

[Remember: this is a preliminary version...]

If I remember correctly, [Dav77] proves “(iv)⇒(i)” from sec. 6 by starting with a filter of neighborhoods, and then enlarging it to an ultrafilter on the same index set; I got the inspiration for trying to work with filters from his “Concurrence Theorem” — and from my difficulties in developing a good intuition about NSA’s infinitesimals.

In [BW05] filters are used in a way that seems to be closely related to the one that I use in this paper; and in sec. 8 of [Bee95] there’s a procedure for “elimination of infinitesimals” in a “neighborhood semantics”.

In the papers [Nel77], [Nel88], Edward Nelson discusses — among many other things — automatic ways to translate non-standard proofs to standard; his setting and his techniques are very different from the ones that I use here. In [Rob73] (§11) Abraham Robinson states the need for tools to analyze lengths of proofs.

Jonas Eliasson uses a category of filters in his [Eli01], and its bibliography points to several papers by Palmgren and Blass that look interesting, but that I have not yet been able to get.

Also: [But99], [AH02]

In Johnstone’s “Topos Theory” book ([Joh77]) there’s a section about the “filter-power construction” (9.4), and another one about sheaves as categories of fractions (3.4). I need to thank Peter Arndt for helping me to understand them; I still don’t understand them as much as I should (far from it!), but I can assure him his efforts have not been in vain...

I described the example in sec. 4 briefly in my MsC thesis (1999) and in a presentation that I gave about it in 2000; the text and the slides for the

presentations are available from http://angg.twu.net/math-b.html#MsC, but

they are in Portuguese, and at that point I didn’t know how to generalize the method, or how to characterize “purely calculational proofs”.

10 A final note

The idea of filter-infinitesimals is not new, the proof of the key theorem is obvious, and “infinitesimals as sequences tending to zero” should be one of the basic intuitive ways to understand infinitesimals, especially if we use some kind of “physicists’ notation” and we omit the index variable... also, somewhere in his [Bel98] (oh no, I lost the page again... 8-() Bell says something along the lines of: “all proofs in Calculus are constructive”. It should be clear, then, that the non-two-valuedness of Set^{𝕀}/F shouldn’t be an obstacle, and that most proofs in Calculus, being constructive, should lift through the quotient Set^{𝕀}/F → Set^{𝕀}/U...

Why can’t I find the ideas in this paper published anywhere else? Am I missing something, or are they new?

References

[AH02] Jeremy Avigad and Jeffrey Helzner. Transfer principles in nonstandard intuitionistic arithmetic. Archive for Mathematical Logic, 41:581–602, 2002.

[Bee95] Michael Beeson. Using nonstandard analysis to verify the correctness of computations. International Journal of Foundations of Computer Science, 6(3):299–338, 1995.

[Bel98] John. L. Bell. A Primer of Infinitesimal Analysis. Cambridge University Press, 1998.

[But99] Carsten Butz. The filter construction revisited. Preprint, 1999.

[BW05] Michael Beeson and Freek Wiedijk. The meaning of infinity in calculus and computer algebra systems. Journal of Symbolic Computation, 39(5):523–538, 2005.

[Dav77] Martin Davis. Applied Nonstandard Analysis. John Wiley, New York, 1977.

[Eli01] Jonas Eliasson. Ultrapowers as sheaves on a category of ultrafilters. Technical report, Uppsala University, 2001.

[Hal64] J. D. Halpern. The independence of the axiom of choice from the boolean prime ideal theorem. Fundamenta Mathematicae, pages 57– 66, 1964.

[HK86] C. Ward Henson and H. Jerome Keisler. On the strength of nonstandard analysis. The Journal of Symbolic Logic, 51(2):377–386, 1986.

[Joh77] P. T. Johnstone. Topos Theory. Academic Press, 1977.

[Nel77] Edward Nelson. Internal set theory; a new approach to nonstandard analysis. Bulletion of the American Mathematical Society, 83:1165– 1198, 1977.

[Nel88] Edward Nelson. The syntax of nonstandard analysis. Annals of Pure and Applied Logic, 38:123–134, 1988.

[Rob73] Abraham Robinson. Metamathematical problems. Journal of Symbolic Logic, 38(3):500–516, 1973.