Warning: this is an htmlized version!
The original is across this link, 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{eduardoochs@gmail.com} \\ \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: