|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008filterp.tex")
% (find-dn4ex "edrx08.sty")
% (defun e () (interactive) (eev "cd ~/LATEX/ && ~/dednat4/dednat41 2008filterp.tex && latex 2008filterp.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008filterp.tex && latex 2008filterp.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008filterp.tex && bibtex 2008filterp && latex 2008filterp.tex"))
% (defun c () (interactive) (find-zsh "F=2008filterp; cd ~/LATEX/ && ~/dednat4/dednat41 $F.tex && latex $F.tex && bibtex $F && latex $F.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008filterp.tex && pdflatex 2008filterp.tex"))
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008filterp.ps 2008filterp.dvi")
% (find-pspage "~/LATEX/2008filterp.ps")
% (find-dvipage "~/LATEX/2008filterp.dvi")
% (find-pspage "~/LATEX/2008filterp.pdf")
% (ee-cp "~/LATEX/2008filterp.dvi" (ee-twusfile "LATEX/2008filterp.dvi") 'over)
% (ee-cp "~/LATEX/2008filterp.pdf" (ee-twusfile "LATEX/2008filterp.pdf") 'over)
% (ee-cp "/tmp/2008filterp-texsrc.tar.gz" (ee-twusfile "LATEX/2008filterp-texsrc.tar.gz") 'over)
% «.intro-nsa-1» (to "intro-nsa-1")
% «.filters» (to "filters")
% «.intro-nsa-2» (to "intro-nsa-2")
% «.ultrafilters-evil» (to "ultrafilters-evil")
% «.example-1» (to "example-1")
% «.filtered-spaces» (to "filtered-spaces")
% «.natural-infinitesimals» (to "natural-infinitesimals")
% «.translating» (to "translating")
% «.future-directions» (to "future-directions")
% «.related-work» (to "related-work")
% «.final-note» (to "final-note")
% «.stuff» (to "stuff")
% «.meanings» (to "meanings")
%\documentclass[oneside]{book}
\documentclass[oneside]{article}
\usepackage[latin1]{inputenc}
\usepackage{indentfirst}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008filterp.dnt
{\myttchars
\footnotesize
\begin{verbatim}
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.
\end{verbatim}
}
% Mention lifting thorugh the quotient?
% The quotient /F is enoguh?
%*
% (eedn4a-bounded)
\def\Opens{\mathcal{O}}
\def\calN{{\mathcal{N}}}
\def\calM{{\mathcal{M}}}
\def\calR{{\mathcal{R}}}
\def\calV{{\mathcal{V}}}
\def\calX{{\mathcal{X}}}
\def\calY{{\mathcal{Y}}}
\def\calZ{{\mathcal{Z}}}
\def\Seti#1{\Set^{(-#1,#1)}}
\def\Setf#1{\Set^{(-\frac{1}{#1},\frac{1}{#1})}}
\def\simnat{\overset{î}{\sim}}
\def\iff{\Leftrightarrow}
% (find-2000ufffile "edrx.sty")
\def\hli{\mathstrut \\ \hline \mathstrut \\}
\def\To{\Rightarrow}
% \def\ot{\leftarrow}
\def\calN{{\mathcal{N}}}
\def\aw{{\textstyle \frac{a}{Ï}}}
\def\an{{\textstyle \frac{a}{n}}}
\def\tE{\mathscr{E}}
\def\tF{\mathscr{F}}
\def\Filt{\mathbf{Filt}}
\def\diam{\mathrm{diam}}
\def\IF{(\I,\F)}
\def\IU{(\I,\U)}
\def\NN{(\N,\calN)}
\def\RRz{(\R,\calR_0)}
\def\XX{(X,\X)}
\def\YY{(Y,\Y)}
\def\XXz{(X,\X_{x_0})}
\def\YYz{(Y,\Y_{y_0})}
\def\SetI{\Set^\I}
\def\SetN{\Set^\N}
\def\SetIF{\Set^\I/\F}
\def\SetIU{\Set^\I/\U}
\def\SetNN{\Set^\N/\calN}
\def\SetNU{\Set^\N/\N}
\def\calA{\mathcal{A}}
\def\calN{\mathcal{N}}
\def\up{{\uparrow}}
\def\False{�}
\def\mysection#1#2{\section{#1}\label{#2}}
\def\iffdef{\overset{\text{def}}{\iff}}
\title{Natural Infinitesimals in Filter-Powers}
\author{Eduardo Ochs \\
% Pólo Universitário de Rio das Ostras (PURO-UFF)
\url{[email protected]} \\
\url{http://angg.twu.net/} \\
}
\date{Preliminary version - 2008jul13}
\maketitle
% --------------------
% «intro-nsa-1» (to ".intro-nsa-1")
% (sec "A very quick introduction to NSA" "intro-nsa-1")
% \mysection {A very quick introduction to NSA} {intro-nsa-1}
% (sec "Introduction" "intro-nsa-1")
Proofs in non-standard analysis are done by moving back and forth
between two universes, the standard universe, $\Set$, and the
non-standard universe, $\SetIU$. Here we will work also with two other
universes between $\Set$ and $\SetIU$: $\SetI$, the universe of
($\I$-indexed) sequences, and $\SetIF$, the ``semi-standard
universe'', in which sequences are identified when the set of indices
where they coincide is ``$\F$-big''.
% ; $\F$ is a filter contained in the ultrafiler $\U$..
Intuitively, the filter-power $\SetIF$ is a generalization of
$\SetNN$, where $\calN$ is the filter of cofinite sets of naturals.
Let's use the prefixes ``pre-hyper-'' and ``hyper-'' to refer to
elements of a $\SetI$ and of a $\SetIF$ respectively. Sequences of
reals tending to zero are pre-hyperreals (in $\SetN$) whose
corresponding hyperreals in $\SetNN$ --- or in a $\SetNU$, where $U$
is a ultrafilter extending $\calN$ --- behave as infinitesimals.
In a certain sense, ultrapowers are much more well-behaved than
filter-powers: the logic of a $\SetIU$ is two-valued, and we have
certain ``transfer theorems'' that transfer truths from $\Set$ to a
$\SetIU$ 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 $\SetIF \to \SetIU$, yielding proofs in a
filter-power $\SetIF$ that can be immediately reinterpreted as being
standard proofs in disguise; ``infinitesimality'' becomes
``continuity''.
\msk
Important: {\sl 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.
% \msk
%
% In Non-Standard Analysis we construct a new universe, $\Set^\I/\U$,
% from the standard universe, $\Set$. Intuitively, this is a
% generalization of the construction $\Set^\N/\calN$: the index set
% $\I$ (or $\N$) is used to make the objects of $\Set^\I$ be
% ``sequences'' (indexed by $\I$) of objects of $\Set$ ; there is a
% mapping $\Set \to \Set^\I$ that takes entities of $\Set$ to constant
% sequences in $\Set^\I$ --- the ``standard'' entities of $\Set^\I$.
% $\Set^\I$ contains a copy of $\Set$, but it also has lots of new
% elements... for example, $(1, \frac{1}{2}, \frac{1}{3}, \frac{1}{4},
% \ldots)$, that should behave as an infinitesimal somehow...
%
% The quotient ``$/\U$'', or ``$/\calN$'', identifies sequences that
% coincide at ``almost every index'', or, in the terminology that we
% will use, ``in a big set of indices''. The filters $\U \subset
% \Pts(\I)$ and $\calN \subset \Pts(\N)$ {\sl define} which sets of
% indices are ``$\U$-big'' and ``$\calN$-big'': to test if two
% sequences $(a_i)$ and $(b_i)$ should be identified, we construct the
% set $I' := \sst{i \in \I}{a_i = b_i}$ and if $\I' \in \U$ --- i.e.,
% if $I'$ is ``$\U$-big'' --- then they are identified.
% --------------------
% «filters» (to ".filters")
% (sec "A very quick introduction to filters" "filters")
\mysection {A very quick introduction to filters} {filters}
A {\sl filter} $\F$ on an index set $\I$ is a family of subsets of
$\I$, $\F \subset \Pts(\I)$, such that:
\begin{itemize}
\item $\I � \F$;
\item if $I, I' � \F$ and $I�I' \subseteq I'' \subseteq \I$ then $I''
� \F$.
\end{itemize}
These two conditions are exactly what it is needed to make
%
$$ (a_i) \sim (b_i) \quad \iffdef \quad \sst{i�\I}{a_i=b_i} � \F $$
%
an equivalence relation: we want $(a_i) \sim (a_i)$, so $\I � \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'' \supset I � I'$, so we need the second condition to
make `$\sim$' transitive.
\msk
This will be our archetypical filter (the ``filter of cofinites''):
%
$$\calN := \sst{I \subset \N}{I \text{ is cofinite (i.e., $\N \bsl 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 \in X$; an {\sl open
neighborhood} of $x$ in $X$ is an open set $U \subseteq X$ containg
$x$; a {\sl neighborhood} of $x$ in $X$ is a set $V \subseteq X$
containing some open neighborhood of $x$; a {\sl punctured
neighborhood} of $x$ is a set $V \subset X$ such that $V \cup \{x\}$
is a neighborhood of $x$; and a {\sl strictly punctured
neighborhood} of $x$ is a set $V \subseteq X \bsl \{x\}$ such that
$V \cup \{x\}$ is a neighborhood of $x$.
\msk
These filters will also be useful later: if $x�X$ is a point in a
topological space $(X, \Opens(X))$, then:
%
$$\begin{array}{rcl}
\calV_x &:=& \sst{V}{ �U�\Opens(X). \; x�U \subseteq V \subseteq X } \\
\calV^-_x &:=& \sst{V}{ �U�\Opens(X). \; x�U \subseteq (V�\sof{x}) \subseteq X } \\
\end{array}
$$
%
$\calV_x$ is the {\sl filter of neighborhoods} of $x$; $\calV^-_x$ is
the {\sl filter of punctured neighborhoods} of $x$. Sometimes
``$\calV^-_x$'' will stand for a filter on $X$, sometimes for a filter
on $X \bsl \sof{x}$.
(By the way: $\calN$ is the filter of punctured neighborhoods of
$\infty$ in the one-point compactification of $\N$.)
\msk
Let's define two operations on families of subsets of $\I$:
$$\begin{array}{rcl}
\up \calA & := & \sst{A' \subseteq \I}{�A�\calA. A \subseteq A' \subseteq \I} \\
\interfin \calA & := & \sst{A_1�\ldots�A_n}{n�\N, A_i � \calA} \\
\end{array}
$$
In $\interfin \calA$ we consider that when $n=0$ the intersection
``$A_1�\ldots�A_n$'' is $\I$.
Fact: for any family $\calA$ of subsets of $\I$, the family $\interfin
\up \A$ (that is equal to $\up \interfin \A$) is a filter on $\I$ ---
the ``filter generated by $\A$''.
\msk
Let's call a filter $\F$ on $\I$ {\sl bad} when $\F = \Pts(\I)$.
A non-bad filter $\F$ divides the sets in $\Pts(\I)$ in three classes:
\begin{itemize}
\item The {\sl $\F$-big} sets are the ones in $\F$;
\item The {\sl $\F$-small} sets sets are the ones whose complements
are $\F$-big;
\item The {\sl $\F$-medium} sets are the other sets in $\Pts(\I)$ -
the ones that are neither $\F$-big nor $\F$-small.
\end{itemize}
The cofinite subsets of $\N$ are $\calN$-big; the finite subsets are
$\calN$-small; and for any $k \in \sof{2, 3, 4, \ldots}$ the set of
multiples of $k$ (``$k\N$'') is $\calN$-medium.
An {\sl ultrafilter} $\U$ on $\I$ is a (non-bad) filter on $\I$ that
divides the subsets of $\I$ in just $\U$-big and $\U$-small subsets;
there are no $\U$-medium subsets.
We will reserve the notation `$\U$' for ultrafilters.
\msk
A non-bad filter $\F$ on $\I$ is said to be {\sl principal} when
$\bigcap \F \neq \emptyset$. For each non-empty set $I \subset \I$,
$\up \{I\}$ is a principal filter; $\up \{I\}$ is an ultrafilter iff
$I$ has exactly one element. $\calN$ is not principal. Filters and
ultrafilters of the form $\up \{I\}$ induce trivial equivalence
relations; we are more interested in non-principal filters and
ultrafilters.
\msk
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 {\sl prove} this
(which is very hard; reference?) but it is easy enough, and quite
enlightening.
% \msk
\begin{quotation}
Take a denumerable set $\calA = \sof{A_1, A_2, A_s, \ldots}$ of
generators; form the sequence $A'_1 := A_1$, $A'_2 := A_1 � A_2$,
$A'_3 := A_1 � A_2 � A_3$, $\ldots$, and then form the sequence
$A''_1, A''_2, A''_3, \ldots$ by removing the repetitions from $A'_1,
A'_2, A'_3, \ldots$ . Clearly, $\up \interfin \calA = \up \interfin
\calA' = \up \calA' = \up \calA''$, where $\calA'' := \sof{A''_1,
A''_2, \ldots}$; if $\calA''$ is finite, $\calA'' = \sof{A''_1,
\ldots, A''_n}$, then $\up \calA'' = \up \sof{A''_n}$; if $A''_n =
\emptyset$ then $\up \calA''$ is bad, and if $A''_n \neq \emptyset$
then $\up \calA''$ is principal.
If $\calA''$ is infinite, take the sequence of ``differences'' $D_1 =
A''_1 \bsl A''_2$, $D_2 = A''_2 \bsl A''_3$, $\ldots$; both $D_1 � D_3
� D_5 � \ldots$ and $D_2 � D_4 � D_6 � \ldots$ are $\up
\calA''$-medium sets, and so $\up \calA''$ is not an ultrafilter.
\end{quotation}
% --------------------
% «intro-nsa-2» (to ".intro-nsa-2")
% (sec "A very quick introduction to NSA" "intro-nsa-2")
\mysection {A very quick introduction to NSA} {intro-nsa-2}
More terminology:
\msk
$\Set$ is the {\sl standard universe}.
$\Set^\I/\U$ is the {\sl non-standard universe}.
$\Set^\I/\F$ (here $\F$ can be just a filter) is the {\sl semi-standard universe}.
A {\sl pre-hyperpoint} is a point of $\Set^\I$, i.e., an $\I$-indexed
sequence.
A {\sl hyperpoint} is a point of $\Set^\I/\F$ or $\Set^\I/\U$, i.e.,
the image of a sequence by the quotients `$/\F$' or `$/\U$' --- i.e.,
an equivalence class of sequences.
A {\sl standard element} of $\Set^\I$ or $\Set^\I/\F$ is a constant
sequence (modulo the equivalence relation, maybe).
\msk
%D diagram unnamed-arrows
%D 2Dx 100 +30 +30
%D 2D 100 \Set ---> \Set^\I --> \Set^\I/\F
%D 2D \ :
%D 2D \ :
%D 2D v v
%D 2D +30 \Set^\I/\U
%D 2D
%D (( \Set \Set^\I \Set^\I/\F
%D \Set^\I/\U
%D @ 0 @ 1 -> @ 1 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 .>
%D ))
%D enddiagram
The obvious maps
%
$$\diag{unnamed-arrows}$$
%
will not usually be named. When $\F \subset \U$ the map $\Set^\I/\F
\to \Set^\I/\U$ exists; it takes each equivalence class of sequences
into a bigger equivalence class.
\msk
Now take this (pre-)hyperreal: $\ee := (1, \frac{1}{2}, \frac{1}{3},
\ldots)$. For any standard interval containing 0, say, $U :=
(-\frac{1}{4}, \frac{1}{4})$, the sentence ``$\ee � U$'' is true in
$\Set^\N/\calN$: the sequence of truth-values
%
$$\textstyle (1�U, \frac{1}{2}�U, \frac{1}{3}�U, \ldots)$$
%
is false for the first indices, but true from some point on, and so it
coincides with $(�, �, �, \ldots)$ in a big set of indices.
We will say that a pre-hyperpoint $x'$ is {\sl 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, $\ee := (1, \frac{1}{2}, \frac{1}{3}, \ldots)$
is infinitely close to 0 --- but $\ee > 0$.
\msk
Typical proofs in NSA work a part of the time in $\Set$ and part in a
$\Set^\I/\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:
\begin{quotation}
In a $\Set^\I/\U$ every ($\I$-indexed) sequence of truth-values is
either equivalent to `true' or to `false'; but in a $\Set^\I/\F$ we
may have more truth-values. For example, $(�, \False, �, \False, �,
\False, \ldots)$ only coincides with $(�, �, �, \ldots)$ and with
$(\False, \False, \False, \ldots)$ in medium sets of indices.
\end{quotation}
So, in a `$\Set^\I/\U$' we have transfer theorems, and a two-valued
logic. Everything seems to indicate that `$\Set^\I/\U$'s are better
than `$\Set^\I/\F$'s, but...
% --------------------
% «ultrafilters-evil» (to ".ultrafilters-evil")
% (sec "Ultrafilters are evil (in a sense)" "ultrafilters-evil")
\mysection {Ultrafilters are evil (in a sense)} {ultrafilters-evil}
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 \cite{Halpern64}. What matters here is: {\sl
ultrafilters are a source of non-intuitiveness in the semantics};
proofs done in $\Set^\I/\U$ may be hard to translate to standard
proofs in $\Set$. On the other hand, proofs done in a $\Set^\I/\F$ ---
especially proofs in $\Set^\N/\calN$ --- 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
\cite{HensonKeisler}). 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^\I/\U$ is especially interesting:
the ones that ``lift'' to a filter-power $\Set^\I/\F$, from where they
can be translated quickly to standard proofs.
\msk
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:
% --------------------
% «example-1» (to ".example-1")
% (sec "A proof with infinitesimals" "example-1")
\mysection {A proof with infinitesimals} {example-1}
Definition (tentative, and sketchy): a {\sl purely calculational
proof} with infinitesimals is one made of a series of steps of the
forms:
``$�x_1 \sim x_0.f(x_1)=g(x_1)$'' or
``$�x_1 \sim x_0.�!y_1 \sim y_0. f(x_1)=h(x_1,y_1)$'',
\noindent where $x_0$, $y_0$, $f$, and $g$ are standard.
\ssk
These steps can be composed in several ways. Let's look at an example.
Suppose that we want to prove that $\lim_{n \to +�} (1 +
\frac{a}{n})^n = e^a$; it is enough to prove that for any infinitely
big natural number $Ï$, $(1 + \aw)^{Ï} \sim 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.
\def\lis{
\li { \aw }={ \o } { g_1 }={ g_2 } {\\}
\li { f(b + \o) }={ f(b) + f'(b) \; \o + \O\o^2 } { g_3 }={ g_4 } { }
\li { }={ f(b) + f'(b) \; \o + \o'\o } { }={ g_5 } { }
\li { }={ f(b) + (f'(b) + \o')\o } { }={ g_6 } {\\}
\li { \log(1 + \o) }={ (1 + \o')\o } { g_7 }={ g_8 } {\\}
\li { \log\,(1 + \aw)^Ï }={ Ï \; \log\, (1 + \aw) } { h_1 }={ h_2 } { }
\li { }={ Ï \; ((1 + \o') \; \aw) } { }={ h_3 } { }
\li { }={ (1 + \o') \; a } { }={ h_4 } {\\}
\li { (1 + \aw)^Ï }={ e^{((1 + \o') \; a)} } { h_5 }={ h_6 } { }
\li { }={ e^{(a + \o' a)} } { }={ h_7 } { }
\li { }={ e^{(a + \o'')} } { }={ h_8 } { }
\li { }={ e^a + \o'''. } { }={ h_9 } { }
}
$$
\def\li#1=#2#3=#4#5{#1&= && #3&= \\ #5}
\def\li#1=#2#3=#4#5{#1&= && #3&= \\}
\begin{array}{rclcrcl}
\lis
\end{array}
$$
\msk
%D diagram wo
%D 2Dx 100 +10 +10 +20 +20 +10 +10 +10 +10 +20
%D 2D 100 {}Ï |-> {}\o \o |--> \o,\O |-----> \o,\o'
%D 2D - - - - - /
%D 2D | | | | | \
%D 2D v v v v v v
%D 2D +20 g_1 ==== g_2 g_3 ==== g_4 ===== g_5 === g_6
%D 2D
%D 2D
%D 2D
%D 2D +20 Ï |-----> Ï,\o' |-----------> \o'
%D 2D - - - - / /
%D 2D / \ | | \ \
%D 2D v v v v \ \
%D 2D +20 h_1 ==== h_2 == h_3 ==== h_4 \ \-------> \o'' |--> \o'''
%D 2D - - \ - -
%D 2D | | \ | |
%D 2D v v v v v
%D 2D +20 h_5 ==================== h_6 ===== h_7 === h_8 |---> h_9
%D 2D
%D (( {}Ï {}\o g_1 g_2
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =
%D ))
%D (( \o \o,\O \o,\o'
%D g_3 g_4 g_5 g_6
%D @ 0 @ 1 |-> @ 1 @ 2 |->
%D @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |-> @ 2 @ 6 |->
%D @ 3 @ 4 = @ 4 @ 5 = @ 5 @ 6 =
%D ))
%D (( Ï Ï,\o' \o' \o'' \o'''
%D @ 0 @ 1 |-> @ 1 @ 2 |-> @ 2 @ 3 |-> @ 3 @ 4 |->
%D ))
%D (( h_1 h_2 h_3 h_4
%D @ 0 @ 1 = @ 1 @ 2 = @ 2 @ 3 =
%D ))
%D (( h_5 h_6 h_7 h_8 h_9
%D @ 0 @ 1 = @ 1 @ 2 = @ 2 @ 3 = @ 3 @ 4 =
%D ))
%D (( Ï h_1 |-> Ï h_2 |-> Ï,\o' h_3 |-> \o' h_4 |-> \o' h_7 |-> \o''
%D h_8 |-> \o''' h_9 |->
%D ))
%D (( h_1 h_5 |-> .plabel= l �{exp}
%D h_4 h_6 |-> .plabel= l �{exp}
%D ))
%D enddiagram
%D
$$\diag{wo}$$
When we compose all cells we get this:
%D diagram wo2
%D 2Dx 100 +25 +25 +35
%D 2D 100 {}Ï |-> {}\o''' Ï |-----> \o'''
%D 2D - - - -
%D 2D | | | |
%D 2D v v v v
%D 2D +20 h_5 ==== h_9 h_5(Ï) == h_9(\o''')
%D 2D
%D (( {}Ï {}\o''' h_5 h_9
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =
%D ))
%D (( Ï \o''' h_5(Ï) .tex= (1+\aw)^Ï h_9(\o''') .tex= e^a+\o'''
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =
%D ))
%D enddiagram
%D
$$\diag{wo2}$$
We will see how to lift this proof to a standard proof.
% --------------------
% «filtered-spaces» (to ".filtered-spaces")
% (sec "Filtered spaces" "filtered-spaces")
\mysection {Filtered spaces} {filtered-spaces}
\def\V{{\mathcal{V}}}
\def\X{{\mathcal{X}}}
\def\Y{{\mathcal{Y}}}
\def\mathbblow{\mathbbold}
Definitions: a {\sl filtered space} is a pair $(X,\X)$ where $X$ is a
set and $\X$ is a filter over $X$; a {\sl function} from $(X,\X)$ to
$(Y,\Y)$ is a function from an $\X$-big subset of $X$ to $Y$; a {\sl
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) \to (Y,\Y)$ is
{\sl 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 {\sl equivalent} when they coincide on some $\X$-big set.
If $f, f': (X,\X) \to (Y,\Y)$ are equivalent and continuous, and $g,
g': (Y,\Y) \to (Z,\mathcal{Z})$ are also equivalent and continuous,
then $(f;g)$ and $(f';g')$ are also equivalent and continuous.
%D diagram filtermapcomp
%D 2Dx 100 +30
%D 2D 100 (X,\X)
%D 2D
%D 2D +20 (Y,\Y) (Z,\mathcal{Z})
%D 2D
%D (( (X,\X) (Y,\Y) (Z,\mathcal{Z})
%D @ 0 @ 1 -> sl_ .plabel= l f
%D @ 0 @ 1 -> sl^ .plabel= r f'
%D @ 1 @ 2 -> sl^ .plabel= a g'
%D @ 1 @ 2 -> sl_ .plabel= b g
%D @ 0 @ 2 .>
%D ))
%D enddiagram
%D
$$\diag{filtermapcomp}$$
A topological space $(X,\Opens(X))$ with a chosen point $x_0 \in X$
has a natural filtered space structure: take $\X := \X_{x_0}$, the
filter of neighborhoods of $x_0$.
A function $f:X \to 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 \to Y$ is continuous at $x_0$ iff $f:(X,\X_{x_0}) \to
(Y,\Y_{y_0})$ is continuous.
\msk
Now fix an index set $\I$ and a filter $\F$ on it; our semi-standard
universe will be $\Set^\I/\F$.
A {\sl pre-hyperpoint} of $(X,\X)$ is a function from $(\I,\F) \to
(\X,\X)$. A {\sl total pre-hyperpoint} of $(X,\X)$ is a function whose
domain is the whole $\I$. Two pre-hyperpoints $(\I,\F) \to (X,\X)$ are
{\sl equivalent} when they coincide in an $\F$-big set of indices.
{\sl Hyperpoints} are pre-hyperpoints modulo equivalence.
A {\sl pre-infinitesimal} in $(X,\X_{x_0})$, for us, will be a
pre-hyperpoint $x_1:(\I,\F) \to (X,\X_{x_0})$ ``infinitely close to
the chosen point'' $x_0$, in the sense that for each standard
neighborhood $X' \ni x_0$ the $x_1$ belongs to $X'$ for a big set of
indices --- formally, $�X' \in \X_{x_0}. x_1^{-1}(X') \in \F$. {\sl
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=\infty$).
% Note that with this definition of ``infinitesimal'', where the chosen
% point doesn't need to be 0,
%
% Note that with this definition of ``infinitesimal'', where the chosen
% point doesn't need to be 0, we will call an ``infinite
% pre-hypernatural'' like $(1, 2, 3, \ldots)$ a ``pre-infinitesimal'' if
% the chosen point is $\infty$.
\msk
These definitions were all chosen to make this work:
\begin{center}
{\bf Key idea:} {\sl infinitesimality is the same
as continuity at the chosen point.}
\end{center}
\msk
When we look at things in this way then it becomes obvious that a
standard continuous function $f:X \to Y$ taking $x_0$ to $y_0$ takes
any infinitesimal $x_1 \sim x_0$ to an infinitesimal $f(x_1) \sim
y_0$.
%D diagram comp1
%D 2Dx 100 +15 +35
%D 2D 100 (\I,\F)
%D 2D
%D 2D +20 (X,\X_{x_0}) --> (Y,\Y_{y_0})
%D 2D
%D (( (\I,\F) (X,\X_{x_0}) (Y,\Y_{y_0})
%D @ 0 @ 1 -> .plabel= l x_1
%D @ 1 @ 2 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{comp1}$$
As this holds for and index set $\I$, any filter $\F$ on $\I$, and any
infinitesimal $x_1 \sim x_0$, we can do much more.
% --------------------
% «natural-infinitesimals» (to ".natural-infinitesimals")
% (sec "Natural Infinitesimals" "natural-infinitesimals")
\mysection {Natural Infinitesimals} {natural-infinitesimals}
Definition: the {\sl natural infinitesimal} on a (standard) filtered
space $(X,\X_{x_0})$, that we will denote by $x_1^î \simnat x_0$, is
the identity function $x_1^î = \id: (X,\X_{x_0}) \to (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 \sim
x_0$ --- in the diagram below we take an $x_1$ living in $\Set^\I/\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.
%D diagram nat-infinitesimal
%D 2Dx 100 +35
%D 2D 100 (\I,\F) ..> (X,\X_{x_0}){}
%D 2D \ |
%D 2D v v
%D 2D +20 (X,\X_{x_0})
%D 2D
%D (( (\I,\F) (X,\X_{x_0}){} (X,\X_{x_0})
%D @ 0 @ 1 .> .plabel= a x_1
%D @ 0 @ 2 -> .plabel= l x_1
%D @ 1 @ 2 -> .plabel= r x_1^î=\id
%D ))
%D enddiagram
%D
$$\diag{nat-infinitesimal}$$
% Our notation for it will be: $x_1 \simnat x_0$.
Now, for any $f: (X,\calX_{x_0}) \to (Y,\calY_{y_0})$ taking $x_0$ to
$y_0$, this holds:
% \smallskip
\begin{quotation}
{\bf Key theorem:}
(i) $f$ is continuous at $x_0$
$\iff$ (ii) for $(\I,\F) := (X,\calX_{x_0}),$ $x^î_1 \simnat x_0$, we have $f(x^î_1) \sim f(x_0)$
$\iff$ (iii) for all $(\I,\F)$ and $x_1 \sim x_0$, we have $f(x_1) \sim f(x_0)$.
% $\iff$ (iv) for all $(\I,\U)$ and $x_1 \sim x_0$, we have $f(x_1) \sim f(x_0)$.
\end{quotation}
%D diagram keyth-diags-1
%D 2Dx 100 +20 +35 +15 +20 +30
%D 2D 100 A0 a0
%D 2D | |
%D 2D x1î | x1î |
%D 2D v f v f
%D 2D +25 A1 -> A2 a1 -> a2
%D 2D
%D 2D +20 B0 b0
%D 2D \ \
%D 2D x1 \ x1 \
%D 2D v f v f
%D 2D +25 B1 -> B2 b1 -> b2
%D 2D
%D (( A0 .tex= (X,\X_{x_0}) A1 .tex= (X,\X_{x_0}) A2 .tex= (Y,\Y_{y_0})
%D B0 .tex= (\I,\F) B1 .tex= (X,\X_{x_0}) B2 .tex= (Y,\Y_{y_0})
%D a0 .tex= x a1 .tex= x a2 .tex= y
%D b0 .tex= i b1 .tex= x b2 .tex= y
%D A0 A1 -> .plabel= l x_1^î A0 A2 -> .plabel= a y_1 A1 A2 -> .plabel= r f
%D B0 B1 -> .plabel= l x_1 B0 B2 -> .plabel= a y_1 B1 B2 -> .plabel= r f
%D a0 a1 |-> .plabel= l x_1^î a0 a2 |-> .plabel= a y_1 a1 a2 |-> .plabel= r f
%D b0 b1 |-> .plabel= l x_1 b0 b2 |-> .plabel= a y_1 b1 b2 |-> .plabel= r f
%D ))
%D enddiagram
%D
$$\diag{keyth-diags-1}$$
% \smallskip
Proof: (i) $\funto$ (ii) and (i) $\funto$ (iii) are obvious from what
we've seen before --- that the composite of continuous maps between
filtered spaces is continuous. For $�$(i) $\funto$ $�$(ii), as $f$ is
not continuous at $x_0$, we can choose a $Y' \in \Y_{y_0}$ such that
$f^{-1}(Y') \notin \X_{x_0}$; but then $y_1^{-1}(Y') =
x_1^{î^{-1}}(f^{-1}(Y')) \notin \X_{x_0}$, and $f(x_1^î) \not\sim
f(x_0)$. For $�$(i) $\funto$ $�$(iii), take $(\I,\F) := (X,\X_{x_0})$,
$x_1 := x_1^î$, and reuse the proof of $�$(i) $\funto$ $�$(ii).
\msk
In texts about Non-Standard Analysis the infinitesimal
characterization of continuity is presented in another form:
\begin{quotation}
(i) $f$ is continuous at $x_0$
$\iff$ (iv) for all $(\I,\U)$ and $x_1 \sim x_0$, we have $f(x_1) \sim f(x_0)$.
\end{quotation}
Clearly, (iii)$\funto$(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.]
% --------------------
% «translating» (to ".translating")
% (sec "Translating a proof with infinitesimals" "translating")
\mysection {Translating a proof with infinitesimals} {translating}
\msk
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 \neq 0$, i.e., $\lim_{\ee \to
0} \frac{g(b + \o)}{\o}$.
What really matters, when we look at the diagrams, is that for any
$(\I,\F)$ and for any infinitesimal $x_1: (\I,\F) \to (X,\X_{x_0})$
--- maybe obeying some condition, like $\o \neq 0$ --- there is a
unique ``adequate'' infinitesimal $y_1: (\I,\F) \to (Y,\Y_{y_0})$; we
want to ``represent'' the operation $x_1 \mapsto y_1$ as a function
$f: (X,\X_{x_0}) \to (Y,\Y_{y_0})$, and we can do that trivially by
setting $(\I,\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.
%D diagram obtaining-f
%D 2Dx 100 +35 +40 +40
%D 2D 100 a0 b0
%D 2D
%D 2D +30 a1 a2 b1 b2
%D 2D
%D (( a0 .tex= \IF a1 .tex= \XXz a2 .tex= \YYz
%D b0 .tex= \XXz b1 .tex= \XXz b2 .tex= \YYz
%D a0 a1 -> .plabel= l x_1
%D a0 a2 -> .PLABEL= ^(0.61) y_1
%D a1 a2 .> .plabel= b f
%D a0 a1 midpoint a0 a2 midpoint |-> sl_
%D b0 b1 -> .plabel= l x_1^î
%D b0 b2 -> .plabel= r y_1
%D b1 b2 -> .plabel= b f:=y_1
%D ))
%D enddiagram
%D
$$\diag{obtaining-f}$$
Applying this idea to the composite of all cells in the example in
sec.\ 5, we get this:
%
%D diagram wo3
%D 2Dx 100 +25 +25 +35 +35 +40
%D 2D 100 {}i n n{}
%D 2D - / - / -
%D 2D | \ | \ |
%D 2D v v v v |
%D 2D +20 {}Ï |-> {}\o''' Ï |-----> \o''' |
%D 2D - - - - |
%D 2D | | | | |
%D 2D v v v v v
%D 2D +20 h_5 ==== h_9 h_5(Ï) == h_9(\o''') h_5(n) == h_9(n)
%D 2D
%D (( {}i {}Ï {}\o''' h_5 h_9
%D @ 0 @ 1 |-> @ 0 @ 2 |->
%D @ 1 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 4 =
%D ))
%D (( n Ï \o''' h_5(Ï) .tex= (1+\aw)^Ï h_9(\o''') .tex= e^a+\o'''
%D @ 0 @ 1 |-> @ 0 @ 2 |->
%D @ 1 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 4 =
%D ))
%D (( n{} h_5(n) .tex= (1+\an)^n h_9(n) .tex= e^a+\o'''(n)
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 2 =
%D ))
%D enddiagram
%D
$$\diag{wo3}$$
%
where $i \in \IF$, $n, Ï \in \NN$, and all the other ``points'' live
in $\RRz$. Note that the `$\mto$' 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.
% ----------
% \mysection{A proof that lifts to a filter-power}
% \begin{align*}
% \log \, (1 + \aw)^{Ï}
% & = Ï \; \log\, (1 + \aw) \\
% & = Ï \; (\log 1 + ((\log' 1) + \o) \; \aw) \\
% & = Ï \; (0 + (1 + \o) \; \aw) \\
% & = Ï \; (1 + \o) \; \aw \\
% & = (1 + \o) \; a \\
% \\
% (1 + \aw)^{Ï} & = e^{((1 + \o) \; a)} \\
% & = e^{(a + \o a)} \\
% & = e^{(a + \o')} \\
% & = e^a + \o''. \\
% \end{align*}
% --------------------
% «meanings» (to ".meanings")
% (s "Meanings" "meanings")
% \myslide {Meanings} {meanings}
% \mysection {Meanings}
% Finite hyperreals: $f(a+\o) = f(a) + f'(a)\o + \O\o^2$.
%
% How do we handle this $\O$ (topologically)?
%
% \ssk
%
% It is from this that we derive $f(a+\o) = f(a) + (f'(a) + \o')\o$,
%
% and $\log(1+\o) = \log(1) + (\log'(1) + \o')\o = (1 + \o')\o$.
% \begin{align*}
% \log \, (1 + \aw)^{Ï}
% & = Ï \; \log\, (1 + \aw) \\
% & = Ï \; ((1 + \o') \; \aw) \\
% & = (1 + \o') \; a \\
% \\
% (1 + \aw)^{Ï} & = e^{((1 + \o') \; a)} \\
% & = e^{(a + \o' a)} \\
% & = e^{(a + \o'')} \\
% & = e^a + \o'''. \\
% \end{align*}
%
% $$
% \begin{array}{rcl}
% \aw &=& \o \\
% f(b + \o) &=& f(b) + f'(b) \; \o + \O\o^2 \\
% &=& f(b) + f'(b) \; \o + \o'\o \\
% &=& f(b) + (f'(b) + \o')\o \\
% \log(1 + \o) &=& (1 + \o')\o \\
% \log\,(1 + \aw)^Ï &=& Ï \; \log\, (1 + \aw) \\
% &=& Ï \; ((1 + \o') \; \aw) \\
% &=& (1 + \o') \; a \\
% (1 + \aw)^Ï &=& e^{((1 + \o') \; a)} \\
% &=& e^{(a + \o' a)} \\
% &=& e^{(a + \o'')} \\
% &=& e^a + \o'''. \\
% \end{array}
% $$
% --------------------
% «future-directions» (to ".future-directions")
% (sec "Future directions" "future-directions")
\mysection {Future directions} {future-directions}
Let $\Filt$ be the category of filtered spaces (in $\Set$). For each
filtered space $(\I,\F)$, the filter-power $\Set^\I/\F$ can be seen as
the fiber of some bigger category (a fibration, of course!), over the
object $(\I,\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^\I/\F \to \Set^\I/\U$
described in [...] (for $\F \subset \U$) is associated to seeing $\id:
\I \to \I$ as a continuous function $\IU \to \IF$.
\msk
Take a filter $\F$ over $\I$, and add the empty set to it: this new
set of subsets, $\F \cup \emptyset \subset \Pts(\I)$, is a topology on
$\I$ --- a funny one, in which there are no ``divisors of zero'': the
intersection of two non-empty open sets is always another non-empty
set. Now regard the topology $\F \cup \{\emptyset\}$ as a Heyting
algebra; the double-negation operation takes $\emptyset$ to itself,
and all non-empty open sets to $X$. I have the impression that if we
sheafify $\Set^{(\I,\F\cup\{\emptyset\})}$ (using the `$��$'
modality?) we get $\Set^\I/\F$ --- and then geometric morphims, etc.
But (as my terminology reveals!) I know far less about sheaves than
I should...
\bsk
Define the ``diameter'' of a set in $\R$ in the obvious way. A
standard function $f: \R \to \R$ 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: \R \to
\Pts(\R)$, or to a relation $R \subset \R×\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$.
\msk
Take some function $g: \R^2 \to \R^2$ that has two derivatives at a
point $a \in \R^2$. For infinitesimals $o$ in $\R^2$, we have that
$g(a+\o) = g(a) + (g'(a)+\o')\o$ --- i.e., there exists an
infinitesimal non-standard function $\o':\R^2 \to \R^2$ that makes the
equation hold... but this $\o'$ is by no means unique!
\msk
I have only described cases where the new infinitesimals are related
to the previous ones by ``unique existentials'', as in $�Ï \sim
\infty.�!\o \sim 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 \sim x_0. \; �y_1 \sim y_0. \; R(x_1, y_1) \text{---}$$
%
a sentence like that one is exactly when for any (standard)
neighborhood $Y' \in \calY_{y_0}$ of $y_0$ its inverse image
%
$$X' := \sst{x�X}{�y�Y'.\; R(x,y)}$$
%
is a neighborhood of $x_0$ --- i.e., this operation $Y' \mto X'$ is
continuous... it seems that in these cases the natural infinitesimal
should have $R \subseteq X \subseteq Y$ as its index set.
% \msk
%
% Big-O: $f(a+\o) = f(a) + (f'(a)+\o')\o$
%
% Exists without the bang: if $f: \R^2 \to \R$ is smooth in a
% neighborhood of 0, then $f(a+\o) = f(a) + (f'(a)+\o')\o$, where
% $\o'$ is a function of $\o$ (and an operator)
% --------------------
% «related-work» (to ".related-work")
% (sec "Related work" "related-work")
\mysection {Related work} {related-work}
{\sl [Remember: this is a preliminary version...]}
\msk
If I remember correctly, \cite{Davis77} proves ``(iv)$\funto$(i)''
from sec.\ \ref{natural-infinitesimals} 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 \cite{BeesonWiedijk05} 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
\cite{Beeson95} there's a procedure for ``elimination of
infinitesimals'' in a ``neighborhood semantics''.
% (find-beesonnsaecpage 28 "neighborhood semantics")
% (find-beesonnsaectext "neighborhood semantics")
In the papers \cite{Nelson77}, \cite{Nelson88}, 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 \cite{Robinson73}
(\S11) Abraham Robinson states the need for tools to analyze lengths
of proofs.
Jonas Eliasson uses a category of filters in his \cite{EliassonUSCU},
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, his reference for the category of filters is
% \cite{KoubekReiterman}. I need to take a look at all that...
Also: \cite{ButzFilter}, \cite{AvigadHelzner}
In Johnstone's ``Topos Theory'' book (\cite{Johnstone77}) 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.\ \ref{example-1} 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
\url{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''.
% --------------------
% «final-note» (to ".final-note")
% (sec "A final note" "final-note")
\mysection {A final note} {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
\cite{Bell98} {\sl (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 $\SetIF$ shouldn't be an obstacle, and that most proofs in
Calculus, being constructive, should lift through the quotient $\SetIF
\to \SetIU$...
\msk
{\sl Why can't I find the ideas in this paper published anywhere else?
Am I missing something, or are they new?}
\bibliography{filters}
\bibliographystyle{alpha}
% Laugwitz (early papers, in German)
% Ehresmann
% Nelson (IST paper, removal)
\end{document}
% --------------------
% «stuff» (to ".stuff")
% (sec "Stuff" "stuff")
\mysection {Stuff} {stuff}
\bigskip
A simple case:
$(1+\frac{a}{Ï}) = 1 + \o$
\bigskip
Every proof of
$�Ï \sim +\infty.�!\o \sim 0. (1+\frac{a}{Ï}) = 1+\o$
corresponds to a standard continuous function $(\N,\calN) \to
(\R,\calR_0)$ in a filter-power $\Set^\F$; and all such proofs and
filter-functions factor in an unique way through a proof of
for $Ï^î \simnat +\infty, �!\o \sim 0. (1+\frac{a}{Ï}) = 1+\o$
in $\Set^\N$.
Each fragment of the big proof corresponds to a proof in a canonical
filter-power
The case $�x_1 \sim x_0. �y_1 \sim y_0. R(x_1,y_1)$ generalizes the
previous ``$�Ï�!\o$'' case; but note that if we take $R := X×Y$ then
things are different (why?), and in the general case $\I:=R \subseteq
X×Y$ the ``continuity condition'' becomes $�Y'�\calY_{y_0}. R^{-1}(Y')
� \calX_{x_0}$.
There's one infinitesimal on a filtered space $(X,\X_{x_0})$
We've seen how to characterize (pre-)hyperpoints $x_1: (\I,\F) \to
(X,\calX_{x_0})$ that are ``infinitesimals'', i.e., ``infinitely close
to $x_0$'' (notation: $x_1 \sim x_0$). But we are usually free to
choose any index set $\I$ and filter $\F$ on it, and then any
topological space with a chosen point (any filtered space, even) has a
``natural infinitesimal'': the identity map. In a diagram:
%D diagram natinf
%D 2Dx 100
%D 2D 100 (\I,\F):=(X,\calX_{x_0})
%D 2D |
%D 2D x_1:=id |
%D 2D v
%D 2D +30 (X,\calX_{x_0})
%D 2D
%D (( (\I,\F):=(X,\calX_{x_0})
%D (X,\calX_{x_0})
%D @ 0 @ 1 -> .plabel= l x_1:=\id
%D ))
%D enddiagram
%D
$$\diag{natinf}$$
By an abuse of language, an ``infinitesimal'' in $(X,\X_{x_0})$ will
also mean a {\sl hyperpoint} infinitely close to the chosen point;
this makes sense because if a pre-hyperpoint is infinitesimal, then
all pre-hyperpoints equivalent to it are also infinitesimals.
[By this convention infinitely big numbers are infinitesimals.]
[Another convention: referring to pre-hyperpoints as hyperpoints.]
[Some examples of non-constant pre-hyperpoints: (1,2,3,...),
(1,1/2,1/3,...), the identity on a topological space.]
% We will think that chosen point $x_0 \in (X, \calX_{x_0})$ plays the
% role of ``zero'', and we will refer to (pre-)hyperpoints that are
% infinitely close to $x_0$ as ``infinitesimals''.
Let's see what this means.
A pre-hyperpoint $x_1$ of $X$ can be seen as a function from the index
set $\I$ to $X$; it is infinitely close to $x_0$ when for all
neighborhoods $X'$ of $x_0$ the sentence ``$x_1 \in X'$'' is true at a
big set of indices --- i.e., when $x_1^{-1}(X') \in \F$.
A function $f: X \to Y$ that takes $x_0$ to $y_0$ is is continuous at
$x_0$ when the inverse image of each neighborhood of $y_0$ by $f$ is a
neighborhood of $x_0$ --- i.e., when $�Y' \in \calY_{y_0}. f^{-1}(Y')
\in \calX_{x_0}$.
In a diagram:
%D diagram IXY
%D 2Dx 100 +40
%D 2D 100 (\I,\F)
%D 2D |
%D 2D x_1 |
%D 2D v f
%D 2D +30 (X,\calX_{x_0}) --> (Y,\calY_{y_0})
%D 2D
%D (( (\I,\F)
%D (X,\calX_{x_0}) (Y,\calY_{y_0})
%D @ 0 @ 1 -> .plabel= l x_1
%D @ 1 @ 2 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{IXY}$$
% {\myttchars
% \footnotesize
% \begin{verbatim}
% I n {n}
% v - - /
% | | | \
% v v | \
% \N --> \R Ï |--> \o''' | \
% | | - - | \
% | | | | | \
% v v v v v v
% {}\R = \R{} h_5 === h_9 (1+\an)^n == e^a+o'''(n)
%
% Categorically, this is a ``triangle'' that says that two mappings
% I --> \R are equal
% \end{verbatim}
% }
%D diagram INXY
%D 2Dx 100 +35 +40
%D 2D 100 (\I,\F) (X,\calX_{x_0}){}
%D 2D \ |
%D 2D x_1 \ | x^î_1
%D 2D v v f
%D 2D +30 (X,\calX_{x_0}) --> (Y,\calY_{y_0})
%D 2D
%D (( (\I,\F) (X,\calX_{x_0}){}
%D (X,\calX_{x_0}) (Y,\calY_{y_0})
%D @ 0 @ 2 -> .plabel= l x_1
%D @ 1 @ 2 -> .plabel= r x^î_1
%D @ 2 @ 3 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{INXY}$$
%D diagram factors1
%D 2Dx 100 +35 +40
%D 2D 100 (\I,\F)
%D 2D |
%D 2D Ï |
%D 2D v f
%D 2D +30 (\N,\calN) --> (\R,\calR_0)
%D 2D
%D (( (\I,\F)
%D (\N,\calN) (\R,\calR_0)
%D @ 0 @ 1 -> .plabel= l Ï #
%D @ 1 @ 2 -> .plabel= a \o
%D ))
%D enddiagram
%D
$$\diag{factors1}$$
%D diagram factors2
%D 2Dx 100 +35 +40
%D 2D 100 (\I,\F) --> (\N,\calN){}
%D 2D \ |
%D 2D Ï \ | Ï^î=id
%D 2D v v f
%D 2D +30 (\N,\calN) --> (\R,\calR_0)
%D 2D
%D (( (\I,\F) (\N,\calN){}
%D (\N,\calN) (\R,\calR_0)
%D @ 0 @ 1 -> .plabel= a Ï #
%D @ 0 @ 2 -> .plabel= l Ï #
%D @ 1 @ 2 -> .plabel= r Ï^î=\id
%D @ 2 @ 3 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{factors2}$$
$�Ï \sim +\infty.�!\o \sim 0. (1+\frac{a}{Ï}) = 1+\o$
$\lim_{n \to +\infty} (1+\frac{a}{Ï}) = 1+\o$
for $Ï^î \simnat +\infty, �!\o \sim 0. (1+\frac{a}{Ï}) = 1+\o$
\bsk
Interesting fragments:
\msk
$\dbrnat{\aw = \o}$
$\dbrnat{f(b + \o) = f(b) + f'(b) \; \o + \O \o^2}$
$\dbrnat{f(b + \o) = f(b) + f'(b) \; \o + \o' \o}$
$\dbrnat{f(b + \o) = f(b) + (f'(b) + \o') \; \o}$
$\dbrnat{\log\, (1 + \o) = (1 + \o') \; \o}$
$\dbrnat{\log\, (1 + \aw) = (1 + \o') \; \aw}$
\msk
$\dbrnat{\log \, (1 + \aw)^{Ï} = Ï \; \log\, (1 + \aw)}$
$\dbrnat{Ï \; \log\, (1 + \aw) = Ï \; ((1 + \o') \; \aw)}$
$\dbrnat{Ï \; ((1 + \o') \; \aw) = (1 + \o') \; a}$
\msk
$\dbrnat{(1 + \aw)^{Ï} = e^{((1 + \o') \; a)}}$
$\dbrnat{e^{((1 + \o') \; a)} = e^{(a + \o' a)}}$
$\dbrnat{{(a + \o' a)} = e^{(a + \o'')}}$
$\dbrnat{{(a + \o'')} = e^a + \o'''}$
%%*
%% (eedn4-51-bounded)
% (find-2000uffpage 1)
% (find-2000ufffile "2000uff.tex" "Exemplo da exponencial")
% (fooi "\\xww" "xÏ" "\\ww" "Ï")
% (fooi "x" "a")
% \begin{align*}
% \log \, (1 + aÏ)^{Ï}
% & = Ï \; \log\, (1 + aÏ) \\
% & = Ï \; (\log 1 + ((\log' 1) + \o) \; aÏ) \\
% & = Ï \; (0 + (1 + \o) \; aÏ) \\
% & = Ï \; (1 + \o) \; aÏ \\
% & = (1 + \o) \; a \\
% \\
% (1 + aÏ)^{Ï} & = e^{((1 + \o) \; a)} \\
% & = e^{(a + \o a)} \\
% & = e^{(a + \o')} \\
% & = e^a + \o''. \\
% \end{align*}
%
% $�Ï \sim +\infty.$
%
% $\qquad \log \, (1 + aÏ)^{Ï} = Ï \, \log\, (1 + aÏ)$
%
% $�Ï \sim +\infty. \; �!\o \sim 0.$
%
% $\qquad Ï \, \log\, (1 + aÏ) = Ï \; (\log 1 + ((\log' 1) + \o_1) \; aÏ)$
%
% $�Ï \sim +\infty. \; �\o \sim 0.$
%
% $\qquad Ï \; (\log 1 + ((\log' 1) + \o_1) \; aÏ) = (1 + \o) \; a$
%
% $�\o \sim 0. \; �!\o' \sim 0.$
%
% $\qquad (\ldots)$
%
% % ------------------
% \bsk
%
% $�Ï \sim +\infty. \; �!\o \sim 0.$
%
% $\qquad P(Ï,\o)$
%
% $�Ï \sim +\infty. \; �\o \sim 0.$
%
% $\qquad Q(Ï,\o)$
%
% $�\o \sim 0.$
%
% $\qquad R(\o)$
%
% $�\o \sim 0. \; �!\o' \sim 0.$
%
% $\qquad S(\o,\o')$
%
% \bsk
$(\N, \calN) \diagxyto/->/^{\o:=\o(Ï)} (\R, \calR_0)$
$(\N×\R, \uparrow(\calN×\calR_0)) \diagxyto/->/^{P} (�, \calV_�)$
\msk
$(\N×\R, \uparrow(\calN×\calR_0)) \diagxyto/->/^{Q} (�, \calV_�)$
\msk
$(\R, \calR_0) \diagxyto/->/^{R} (�, \calV_�)$
\msk
$(\R, \calR_0) \diagxyto/->/^{\o:=\o'(\o)} (\R, \calR'_0)$
$(\R×\R', \uparrow(\calR_0×\calR'_0)) \diagxyto/->/^{S} (�, \calV_�)$
% \def\mymot{\diagxyto/<-|/<100>}
%\newpage
% ------------------
\mysection{Attic}
%:*>=*\ge *
%L forths["="] = function () pusharrow("=") end
%D diagram SetNM
%D 2Dx 100 +40 +40 +40 +40
%D 2D 100 \Set^{\N_{>=3}} <-- \Set^{\N_{>=2}} <-- \Set^\N
%D 2D <-------/ | | ||
%D 2D +25 \Set^\calN | | ||
%D 2D | | | ||
%D 2D | v | ||
%D 2D +20 | \Set^{3\N} <-----------|----------- \Set^\N{}
%D 2D | / | /
%D 2D | v v <----/
%D 2D +20 | \Set^{6\N} <-------------- \Set^{2\N}
%D 2D v <--/
%D 2D +10 \Set^\calM
%D 2D
%D (( \Set^{\N_{>=3}} \Set^{\N_{>=2}} \Set^\N # 0 1 2
%D \Set^\calN # 3
%D \Set^{3\N} \Set^\N{} # 4 5
%D \Set^{6\N} \Set^{2\N} # 6 7
%D \Set^\calM # 8
%D @ 0 @ 1 <- @ 1 @ 2 <-
%D @ 0 @ 3 ->
%D @ 3 @ 8 -> @ 0 @ 4 -> @ 1 @ 7 -> @ 2 @ 5 =
%D @ 4 @ 5 <- @ 4 @ 6 -> @ 5 @ 7 -> @ 6 @ 7 <-
%D @ 6 @ 8 ->
%D ))
%D enddiagram
%D
$$\diag{SetNM}$$
%D diagram Set()
%D 2Dx 100 +50 +50 +50 +30
%D 2D 100 \Setf3 <---- \Setf2 <---- \Set^\R \R
%D 2D <----
%D 2D +20 \Set^{\calR_0}
%D 2D
%D 2D +20 \Set^{I''} <- \Set^{I'} <- \Set^\I \I
%D 2D <----
%D 2D +20 \Set^\F
%D 2D
%D (( \Setf3 \Setf2 \Set^\R # 0 1 2
%D \Set^{\calR_0} # 3
%D \Set^{I''} \Set^{I'} \Set^\I # 4 5 6
%D \Set^\F # 7
%D @ 0 @ 1 <- @ 1 @ 2 <-
%D @ 0 @ 3 ->
%D @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 -> @ 3 @ 7 ->
%D @ 4 @ 5 <- @ 5 @ 6 <-
%D @ 4 @ 7 ->
%D \I \R ->
%D ))
%D enddiagram
%D
$$\diag{Set()}$$
%D diagram SetXYZ
%D 2Dx 100 +30 +30 +20 +20 +20 +20
%D 2D 100 \Set^\calX <--- \Set^{X'} <--- \Set^X X x_0 x_1 X'
%D 2D | | | | - - ^|
%D 2D | | | | | | ||
%D 2D v v v v v v -v
%D 2D +30 \Set^\calY <--- \Set^{Y'} <--- \Set^Y Y y_0 y_1 Y'
%D 2D | | | | - - ^|
%D 2D | | | | | | ||
%D 2D v v v v v v -v
%D 2D +30 \Set^\calZ <--- \Set^{Z'} <--- \Set^Z Z z_0 z_1 Z'
%D 2D
%D (( \Set^\calX \Set^{X'} \Set^X
%D \Set^\calY \Set^{Y'} \Set^Y
%D \Set^\calZ \Set^{Z'} \Set^Z
%D @ 0 @ 1 <- @ 1 @ 2 <-
%D @ 3 @ 4 <- @ 4 @ 5 <-
%D @ 6 @ 7 <- @ 7 @ 8 <-
%D @ 0 @ 3 -> @ 1 @ 4 -> @ 2 @ 5 ->
%D @ 3 @ 6 -> @ 4 @ 7 -> @ 5 @ 8 ->
%D ))
%D (( X Y -> Y Z ->
%D ))
%D (( x_0 y_0 |-> y_0 z_0 |->
%D ))
%D (( x_1 y_1 |-> y_1 z_1 |->
%D ))
%D (( X' Y' -> sl_ Y' Z' -> sl_
%D X' Y' <-| sl^ Y' Z' <-| sl^
%D ))
%D enddiagram
%D
$$\diag{SetXYZ}$$
$f$ is continuous at $x_0$
$\iff$ for all $\I$, $\U$, $x_1 \sim x_0$, we have $f(x_1) \sim f(x_0)$
$\iff$ for all $\I$, $\F$, $x_1 \sim x_0$, we have $f(x_1) \sim f(x_0)$
$\iff$ for $\I:=X$, $\F:=\calX_{x_0}$, $x_1 \overset{î}{\sim} x_0$, we have $f(x_1) \sim f(x_0)$
% ------------------
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% modes: (latex-mode fundamental-mode)
% ee-anchor-format: "«%s»"
% End: