\documentclass[jsco]{academic}
\usepackage{amssymb,url}
\newcommand{\R}{{\mathbb R}}
\newcommand{\OR}{{\cal O}(\R)}
\newcommand{\dom}{\mathop{\rm dom}\nolimits}
\newcommand{\Lim}{\mathop{\rm Lim}}
\let\littleskip=\smallskip
\begin{document}
\title{The meaning of infinity in calculus\\and computer algebra systems}
\shorttitle{The meaning of infinity}
\shortauthor{Beeson and Wiedijk}
\author[1]{Michael Beeson}
\author[2]{Freek Wiedijk}
\address[1]{San Jos\'e State University}
\address[2]{University of Nijmegen}
\maketitle
\begin{abstract}
We use filters of open sets to provide a semantics justifying the use of infinity
in informal limit calculations in calculus, and in the
same kind of calculations in computer algebra.
We compare the behavior of these filters to the way
Mathematica behaves when calculating with infinity.
We stress the need to have a proper semantics for computer
algebra expressions, especially if one wants to use
results and methods from computer algebra in theorem provers.
The computer algebra method under discussion
in this paper is the use of rewrite rules to evaluate limits involving infinity.
\end{abstract}
\section{Introduction}
\subsection{Problem}
In calculus, when calculating limits, one often first uses the
heuristic of `calculating with infinity' before trying to evaluate
the limit in a more formal way. For instance one `calculates':
$$\lim_{x\to\infty} {1\over x + 1} = {1\over\infty + 1} = {1\over\infty} = 0$$
which indeed gives the correct answer.
However, it is not clear what the {\em meaning\/} of this use
of the symbol `$\infty$' is, and why this method works. This problem
arises in calculus textbooks, which usually avoid examples of such calculations for
fear of `lack of rigor', although students are taught these methods at the blackboard.
It arose in the design of the first author's software, MathXpert
\cite{beeson-mathpert,beeson-hisc,beeson-ste}. This software, which is designed to assist a
student in producing step-by-step solutions to calculus problems, had to be able to produce
`ideal' step-by-step solutions of limit problems.
Are such `ideal solutions' allowed to
use calculations involving infinity? Or are those calculations just private preliminary considerations
intended to guide a rigorous proof?
MathXpert does allow calculations involving infinity, but not the full system justified
in this paper, since that goes beyond what one finds in calculus textbooks.
In the Mathematica system \cite{wol:96} the approach of calculating with
infinity is used.
Since Mathematica gives answers, rather than step-by-step solutions,
one will not notice the calculations with infinity, in cases where the limit turns out to
exist (and be a finite number). But in fact, in Mathematica
there is a complete `calculus of infinity'
(and some related symbols):
\begin{flushleft}\label{example}
\verb|In[1]:= 1/(Infinity + 1)|\\
\littleskip
\verb|Out[1]= 0|\\
\littleskip
\verb|In[2]:= Sqrt[Infinity]|\\
\littleskip
\verb|Out[2]= Infinity|\\
\littleskip
\verb|In[3]:= Infinity - Infinity|\\
\littleskip
\verb|Infinity::indet: |\\
\verb| Indeterminate expression (-Infinity) + (Infinity) encountered.|\\
\littleskip
\verb|Out[3]= Indeterminate|\\
\littleskip
\verb|In[4]:= Indeterminate + Infinity|\\
\littleskip
\verb|Out[4]= Indeterminate|\\
\littleskip
\verb|In[5]:= Sin[Infinity]|\\
\littleskip
\verb|Out[5]= Interval[{-1, 1}]|\\
\littleskip
\verb|In[6]:= 1/Interval[{-1, 1}]|\\
\littleskip
\verb|Out[6]= Interval[{-Infinity, -1}, {1, Infinity}]|\\
\littleskip
\verb|In[7]:= Interval[{-1, 1}]*Interval[{-1, 1}]|\\
\littleskip
\verb|Out[7]= Interval[{-1, 1}]|\\
\littleskip
\verb|In[8]:= Interval[{-1, 1}]^2|\\
\littleskip
\verb|Out[8]= Interval[{0, 1}]|\\
\littleskip
\verb|In[9]:= 0*Sin[Infinity]|\\
\littleskip
\verb|Out[9]= Interval[{0, 0}]|
\littleskip
\verb|In[10]:= Infinity/Sin[Infinity]|\\
\littleskip
\verb|Out[10]= Interval[{-Infinity, -Infinity}, {Infinity, Infinity}]|\\
\littleskip
\verb|In[11]:= Infinity/Sin[Infinity]^2|\\
\littleskip
\verb|Out[11]= Interval[{Infinity, Infinity}]|\\
\end{flushleft}
Other computer algebra systems implement similar calculi.
For instance, the Maple system \cite{mon:ged:hea:lab:vor:97} uses the symbols {\tt infinity} and {\tt undefined} in answers to limit problems.%
\footnote{There is also some notion of interval in Maple,
written as {\tt 1} {\tt ..} {\tt 2}, but our attempts to calculate with these terms
led only to error messages. These terms seem primarily to be used for generating integer sequences,
although the answer to $\lim_{x\to\infty} \sin x$ comes out as {\tt -1} {\tt ..} {\tt 1}.}
It is well known that many computer algebra packages make
errors.
One of the reasons for that is that they fail to check the pre-conditions or `side conditions'
that must be satisfied for a simplification rule to be applicable. For example,
before applying $\sqrt{x^2} = x$ we need to check that $x \ge 0$. Systematically
keeping track of such assumptions is difficult.
The errors in computer algebra systems sometimes
give the impression that those systems place a higher priority
on performing as many simplifications as possible than on ensuring that only
correct computations are performed.
Generally, `evaluation errors' which users complain about are taken care of
on an ad hoc basis only,
to get rid of the most embarrassing ones.
Related to these errors is the fact that these systems
have no unified semantics for their expression language. In this paper
we focus on the apparatus for limits and offer a solution: a semantics
explaining and supporting the use of infinities in limit calculations.
We will present a formal semantics of limits, which not only explains the
calculations usually performed with infinities, but offers some extensions
by introducing some other symbols for common ways in which a function can fail
to have a limit. Thus, we will be able to get an answer by calculation for such
a limit as
$ \lim_{x \to \infty} {{ 1}/({2 + \sin x})} $
which will be `oscillations through the interval $[{1\over 3},1]$'.
We then compare the resulting semantics to the behavior of Mathematica as
illustrated above. There is a rough general correspondence, and our semantics
agrees with some of the examples above, but in
some instances Mathematica does give incorrect answers, and in some cases
we are able to
distinguish between identical Mathematica expressions
which are different in our semantics.
\subsection{Approach}
We will represent $\infty$ and its cousins {\sf indeterminate\/}
and {\sf interval\/} by {\em filters\/} over
some underlying topological space (which in calculus textbooks and Mathematica is the space of
real numbers, but could also be the complex numbers or more general spaces).
For each point of the space there will be a filter associated with
it, which is called the {\sf principal\/} filter of the point.
For each function on the space there will be a {\em lifted\/} version that
works on the filters instead of on the points.
Furthermore we will
define classes of filters called the {\em interval\/} filters and the
{\em connected\/} filters.
It will turn out that those two classes coincide and that
connectedness of filters is preserved under continuous mappings.
Also we will define the {\em join\/} and the {\em meet\/} of
two filters.
It turns out that the calculus used in Mathematica
corresponds directly to the set of finite joins of interval filters.
\subsection{Related work}
First, in topology, the two standard
approaches for defining limits in topological spaces make use of
{\em nets\/} or {\em filters}. There is therefore nothing original
in the use of filters to analyze the notion of limits. However,
our focus to use them in an applied setting, and identify specific
filters associated with `extra-mathematical' symbols such as $\infty$,
seems to be new.
Second, the interval filters are directly related to the
active field of {\em interval arithmetic}. We throw a new light on the calculations with
intervals by looking at them as filters.
Third, justifying `calculations with infinite objects' rigorously
is close to doing the same with `calculations with infinitesimal
objects', which is the domain of {\em nonstandard analysis}.
In nonstandard analysis one also has infinity as a first class
citizen,
but in nonstandard analysis there is not {\em one}, designated,
infinity;
instead there are many infinite nonstandard numbers, without
a `canonical' one.
In our case there {\em is} a canonical infinity.
To illustrate
this difference concretely, let $\omega$ be the
infinity of nonstandard analysis and let $\infty$ be
the infinity of our filter calculus.
Then we have
$\omega + 1\ne\omega$, but $\infty + 1 = \infty$.
The simplest way to get non-standard objects also employs a filter,
but this has to be a special kind of filter called an {\em ultrafilter}.
Also this filter contains arbitrary sets instead of only open sets
(as is the case for the filters that are studied in this paper).
Another important difference is that, in contrast to our approach,
in this construction there is only {\em one\/} filter involved.
The non-standard objects in this construction are not filters themselves.
Nonstandard analysis has been used in \cite{beeson-nsa} to help in the
computation of limits in a computer algebra system.
\section{Filters, lifting, refinement and limits}\label{basic}
\begin{definition}
Let $X$ be a topological space.
Denote the open sets of $X$ by ${\cal O}(X)$.
A {\em filter on $X$\/} is a set $A \subseteq {\cal O}(X)$ that satisfies:
$$\begin{array}{c}
\forall U\in A.\,\forall V\in{\cal O}(X).\,U \subseteq V \Rightarrow V\in A\\
\noalign{\smallskip}
\forall U\in A.\,\forall V\in A.\,U\cap V\in A
\end{array}$$
In words: a filter is a set of open sets that is
closed under supersets and finite intersections.
The collection of filters on $X$ is written $\bar{X}$.
A filter that does not contain the empty set is called {\em proper}.
A filter that does not contain any set at all is called {\em empty}.
\end{definition}
Often the property of being proper is made part of the definition
of a filter.
We did not do this, because then we would be unable to define
the notion of {\em meet} on page \pageref{meet} below.
Sometimes the property of being non-empty is made part of the
definition of a filter too.
However the empty filter, which is called {\sf domain-error\/} below,
is essential to our application.
We found variants of the definition of filter in the literature,
both allowing for improper \cite{kur:66} and for empty \cite{sim:76} filters.
Therefore we feel free to define the concept of filter to suit our purposes.
In the topological literature a filter is generally
not defined on a topological space but on an
arbitrary set. In that case the restriction to open sets is not present.
However, for our application it is more natural to restrict ourselves
to filters of open sets.
\begin{definition}\label{specific}
Here are some common filters on the real numbers,
where $a\in\R$ is an arbitrary real number:
\begin{eqnarray*}
\mbox{\sf improper} \equiv \dagger &\equiv& \OR\\
\mbox{\sf domain-error} \equiv \bot &\equiv& \emptyset\\
\mbox{\sf indeterminate} \equiv \mathord{\leftrightarrow} &\equiv& \{\R\}\\
\mbox{\sf principal}(a) \equiv \bar{a} &\equiv& \{U\in\OR \,|\, a\in U\}\\
&=& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(a-\varepsilon,a+\varepsilon)\subseteq U\}\\
\mbox{\sf left}(a) \equiv {a}^- &\equiv& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(a-\varepsilon,a)\subseteq U\}\\
\mbox{\sf right}(a) \equiv {a}^+ &\equiv& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(a,a+\varepsilon)\subseteq U\}\\
\mbox{\sf punctured}(a) \equiv {a}^{\pm} &\equiv& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(a-\varepsilon,a)\cup(a,a+\varepsilon)\subseteq U\}\\
\mbox{\sf infinity} \equiv \infty &\equiv& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(1/\varepsilon,\infty)\subseteq U\}\\
\mbox{\sf minus-infinity} \equiv -\infty &\equiv& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(-\infty,-1/\varepsilon)\subseteq U\}\\
\mbox{\sf bi-infinity} \equiv \pm\infty &\equiv& \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,(-\infty,-1/\varepsilon)\cup(1/\varepsilon,\infty)\subseteq U\}\\
\mbox{\sf positive} \equiv \mathord{\rightarrow} &\equiv& \{U\in\OR \,|\, (0,\infty)\subseteq U\}\\
\mbox{\sf negative} \equiv \mathord{\leftarrow} &\equiv& \{U\in\OR \,|\, (-\infty,0)\subseteq U\}\\
\mbox{\sf non-zero} \equiv \pm\mathord{\rightarrow} &\equiv& \{U\in\OR \,|\, (-\infty,0)\cup(0,\infty)\subseteq U\}
\end{eqnarray*}
\end{definition}
For each of these filters we have a `long' and a `short' notation.
The first four filters can be defined for any topological space.
The other filters have analogues in any order topology.
\begin{definition}
Let again $X$ be a topological space.
Let $A$ be a collection of subsets of $X$ (not necessarily open)
that satisfies:
$$\forall U\in A.\,\forall V\in A.\,\exists W\in A.\,W \subseteq U\cap V\eqno{\mbox{\rm ($\ast$)}}$$
The {\em filter generated by $A$\/} is defined to be:
$$\mbox{\sf generated-by\/}(A) \equiv \{U\in{\cal O}(X) \,|\, \exists V\in A.\,V\subseteq U\}$$
The collection of sets $A$ is called the {\em basis\/} of the
filter $\mbox{\sf generated-by\/}(A)$.
\end{definition}
Being closed under finite intersections implies ($\ast$).
If all elements of $A$ are open sets,
the filter generated by $A$ is the intersection of all filters
that contain $A$ as a subset.
The filters defined on page \pageref{specific} can be defined
more naturally
using the notion of a generated filter.
For instance, we have:
$$\begin{array}{rcl}
\mbox{\sf improper} &=& \mbox{\sf generated-by\/}(\{\emptyset\})\\
\mbox{\sf principal}(a) &=& \mbox{\sf generated-by\/}(\{\{a\}\})\\
\mbox{\sf right}(a) &=& \mbox{\sf generated-by\/}(\{(a,a+\varepsilon) \,|\, \varepsilon\in\R_{>0}\}\\
\mbox{\sf infinity} &=& \mbox{\sf generated-by\/}(\{(1/\varepsilon,\infty) \,|\, \varepsilon\in\R_{>0}\}
\end{array}$$
All other filters that are introduced on page \pageref{specific}
can be defined in a similar way.
\begin{definition}
Let $f: X\to X$ be some (possibly partial) function with domain $\dom(f)$.
The {\em lift of $f$\/} is a function $\bar{f}: \bar{X}\to\bar{X}$, defined by:
$$\bar{f}(A) \equiv \mbox{\sf generated-by}\big(\{f[U] \,|\, U\subseteq\dom(f) \land U\in A\}\big)$$
This definition can be generalized to arbitrary arities.
The function $\bar{f}: \bar{X}\times\bar{X}\times\ldots\times\bar{X}\to\bar{X}$
is defined by:
$$\begin{array}{ll}
\bar{f}(A_1,A_2,\ldots,A_n) \equiv\\
\quad\mbox{\sf generated-by}\big(\{f[U] \,|\, U\subseteq\dom(f) \land {}&\hspace{-.72em}
U = U_1\times U_2\times\ldots\times U_n \land {}\\&\hspace{-.72em}
U_1\in A_1 \land U_2\in A_2 \land \ldots \land U_n\in A_n\}\big)
\end{array}$$
\end{definition}
Although $f$ can be a partial function, the lift of $f$ is always
total. One can get rid of the problems of partial functions in calculus
by lifting the whole theory to filters.
In some sense by going to filters
we are adding a `bottom element' $\bot$ to the values of
the theory.
Looked at in this way, we have a {\em strict\/} partial logic,
because a function applied to $\bot$ will always give $\bot$ again.
Note also that the definitions of $\bar{a}$ as a principal filter and as lift
of a 0-ary constant function coincide.
This justifies using one notation for both.
{From} now on
we will often write $f$ instead of $\bar{f}$ when one or more of the arguments of $f$
are filters.
So we will write $\sin(A)$ instead of $\overline{\sin}(A)$.
This will allow us to write things like $\sqrt{A}$,
and mean the lift of the square root function.
To state this convention more precisely: if $t[x_1,\ldots,x_n]$ is a term
that does not involve filters (so $x_1,\ldots,x_n$ are variables ranging
over the ordinary reals) then $t[A_1,\ldots,A_n]$
will mean the lift of the function
$\lambda x_1 \cdots\,x_n.\,t[x_1,\ldots,x_n]$
applied to the filters $A_1,\ldots,A_n$.
%
Note that with this convention
$1/A$ means something different from $\bar{1}/A$.
The first is the lift of the unary function $\lambda x.\,1/x$ applied to $A$.
The second is the lift of the binary function $\lambda x\,y.\,x/y$ applied to
$\bar{1}$ and $A$.
Those are not necessarily equal: $1/1^+ = 1^-$ but $\bar{1}/1^+ = \bar{1}$.
\begin{definition}
The {\em filter limit\/} of the function $f: X\to X$ when taking the limit
to the filter $A$ is defined to be:
$$\Lim_{x\to A} f(x) \equiv \bar{f}(A)$$
\end{definition}
We distinguish a filter limit from an ordinary limit
by writing `Lim' with a capital letter L.
Note that the filter limit is always defined, even for non-continuous $f$.
It might seem silly to introduce a new notation for this when we already
have defined lifting, as it is the same operation.
However, now we can write:
$$\Lim_{x\to 0^+} {x/x}$$
which is something different from
$${0^+/\,0^+}$$
The first is the lift of the unary function $\lambda x.\,x/x$ applied to
$0^+$ and has as value $\bar{1}$.
The second is the lift of the binary function $\lambda x\,y.\,x/y$
applied to the pair $(0^+,0^+)$ and has as value $\mathord{\rightarrow}$.
\begin{definition}
A filter $A$ {\em refines\/} a filter $B$, notation $A\sqsubseteq B$
when $A\supseteq B$ as collections of open sets.
When the two filters $A$ and $B$ differ we write $A\sqsubset B$.
\end{definition}
Here are some refinement relations between the filters defined on page
\pageref{specific}.
For any proper and non-empty filter $A$ we have:
$$\dagger \sqsubset A \sqsubseteq \mathord{\leftrightarrow} \sqsubset \bot$$
At any real number $a\in\R$ we have:
$$a^-,a^+ \sqsubset a^{\pm} \sqsubset \bar{a}$$
and the `infinite' filters are related by:
$$
-\infty,\infty \sqsubset \pm\infty \sqsubset \mathord{\leftrightarrow},\quad
-\infty \sqsubset \mathord{\leftarrow} \sqsubset \pm\mathord{\rightarrow} \sqsubset \mathord{\leftrightarrow},\quad
\infty \sqsubset \mathord{\rightarrow} \sqsubset \pm\mathord{\rightarrow} \sqsubset \mathord{\leftrightarrow}
$$
Note that the filters defined on page \pageref{specific} are not the only ones.
There are many `wild' filters refining $\bar{a}$ and
$\infty$.
For instance the filter generated by the sets $\{2\pi n \,|\, n > N\}$
is a filter which refines $\infty$.
It has the property that the filter limit of $\sin$ to this filter is $\bar{0}$.
We can now state the first theorem,
which lists some of the many calculation rules that one needs for
arithmetic on filters:
\begin{theorem}\label{rules}
Let $a\in\R_{>0}$ be some positive real number.
Then:
$$\begin{array}{rcl}
\infty + \bar{a} &=& \infty\\
\infty - \bar{a} &=& \infty\\
\infty + \infty &=& \infty\\
\infty - \infty &=& \mathord{\leftrightarrow}
\end{array}\quad\begin{array}{rcl}
{\bar{a}/\bar{0}} &=& \bot\\
{\bar{a}/0^+} &=& \infty\\
{\bar{a}/0^{\pm}} &=& \pm\infty\\
0^+/0^+ &=& \mathord{\rightarrow}
\end{array}\quad\begin{array}{rcl}
{\bar{a}/\infty} &=& 0^+\\
{\bar{a}/\mathord{\pm\infty}} &=& 0^{\pm}\\
{\bar{a}/\mathord{\rightarrow}} &=& \mathord{\rightarrow}\\
{\bar{a}/\mathord{\leftrightarrow}} &=& \bot\\
\end{array}\quad\begin{array}{rcl}
\bar{0}\,\infty &=& \mathord{\leftrightarrow}\\
0^+\infty &=& \mathord{\rightarrow}\\
0^{\pm}\infty &=& \pm\mathord{\rightarrow}\\
\infty\,\infty &=& \infty
\end{array}$$
\end{theorem}
\begin{proof}
We will show only the proof for the next to last calculation rule,
$0^{\pm}\infty = \pm\mathord{\rightarrow}$.
The other proofs are similar.
%
To prove this rule, we need to show that both
$0^{\pm}\infty \subseteq \pm\mathord{\rightarrow}$
and
$0^{\pm}\infty \supseteq \pm\mathord{\rightarrow}$.
So suppose that we have $V \in 0^{\pm}\infty$.
Then by the definition of lift of the multiplication function
there are $U_1\in 0^{\pm}$ and $U_2\in\infty$ such that $U_1 U_2 \subseteq V$.
By the definitions of $0^\pm$ and $\infty$ we have for some positive $\varepsilon_1$ and $\varepsilon_2$ that $(-\varepsilon_1,0)\cup(0,\varepsilon_1)\subseteq U_1$
and $(1/\varepsilon_2,\infty)\subseteq U_2$.
Now to show that $V\in\pm\mathord{\rightarrow}$, we need to show that for any
$x\ne 0$ we have that $x\in V$.
Consider some positive $\varepsilon$ smaller than $\varepsilon_1$ and $\varepsilon_2/x$.
Then $x\in V$ follows, because
we have that $\varepsilon\in U_1$, and because by $x/\varepsilon > x/(\varepsilon_2/x) = 1/\varepsilon_2$ we have that $x/\varepsilon\in U_2$.
For the other inclusion, suppose that $V\in\pm\mathord{\rightarrow}$,
which by definition means that $(-\infty,0)\cup(0,\infty)\subseteq V$.
Take for $U_1$ and $U_2$ both $(-\infty,0)\cup(0,\infty)$ too, then $U_1\in 0^{\pm}$
and $U_2\in\infty$.
Clearly $U_1 U_2 = (-\infty,0)\cup(0,\infty)$ as well,
so $U_1 U_2\subseteq V$, and therefore $V\in 0^{\pm}\infty$.
\end{proof}
Note that, although the lift of division is a total function,
`division by zero' is still not allowed in a sense,
because the result of $\bar{a}/\bar{0}$ is {\sf domain-error}.
This is essentially different from the way that Mathematica behaves.
We will come back to this in Section \ref{mathematica}
The next theorem tells us how to evaluate the lift of a continuous function in a point:
\begin{theorem}
Let $f$ be a function that is continuous and monotonically increasing
in a neighborhood of $a$. Then:
$$\bar{f}(\bar{a}) = \overline{f(a)},\quad
\bar{f}(a^{\pm}) = f(a)^{\pm},\quad
\bar{f}(a^-) = f(a)^-,\quad
\bar{f}(a^+) = f(a)^+$$
\end{theorem}
\begin{proof}
We will show only the proof of the last equality.
The other proofs are similar.
%
To prove that
$\bar{f}(a^+) = f(a)^+$
we need to show that both
$\bar{f}(a^+)\subseteq f(a)^+$
and
$\bar{f}(a^+)\supseteq f(a)^+$.
So suppose that $V\in\bar{f}(a^+)$.
Then there is a $U\in a^+$ such that $f[U]\subseteq V$,
and because $U\in a^+$ there is a positive $\varepsilon$ with
$(a,a+\varepsilon)\subseteq U$.
We may assume that $\varepsilon$ is small enough that $f$ is continuous and
monotonically increasing on $[a,a+\varepsilon]$,
and this implies $f[(a,a+\varepsilon)] = \left(f(a),f(a)+\delta\right)$
with $\delta = f(a+\varepsilon) - f(a)$.
Therefore $\left(f(a),f(a)+\delta\right)\subseteq f[U]\subseteq V$,
and hence $V\in f(a)^+$.
For the other inclusion, suppose that $V\in f(a)^+$, so for
some positive $\delta$ it holds that $\left(f(a),f(a)+\delta\right)\subseteq V$.
Because $f$ is continuous in $a$ there is a positive $\varepsilon$ such
that $f[(a-\varepsilon,a+\varepsilon)]\subseteq \left(f(a)-\delta,f(a)+\delta\right)$.
Again we may assume that $\varepsilon$ is small enough that $f$ is monotonically
increasing on $[a-\varepsilon,a+\varepsilon]$,
which gives $f[(a,a+\varepsilon)]\subseteq \left(f(a),f(a)+\delta\right)$,
and therefore $f[(a,a+\varepsilon)]\subseteq V$.
Because $(a,a+\varepsilon)\in a^+$, this implies that $V\in\bar{f}(a^+)$.
\end{proof}
Similar theorems hold for decreasing functions and functions
at a local maximum or minimum.
The next theorems show how to evaluate filter limits:
\begin{theorem} Bringing filter limits inside expressions:
$$\Lim_{x\to A} f(g_1(x),g_2(x),\ldots,g_n(x))\sqsubseteq
\bar{f}(\Lim_{x\to A} g_1(x),\Lim_{x\to A} g_2(x),\ldots,\Lim_{x\to A} g_n(x))$$
\end{theorem}
\begin{proof}
Define $h(x) = f(g_1(x),\ldots,g_n(x))$.
To prove the statement we need to show that
$\bar{h}(A) \sqsubseteq \bar{f}(\bar{g_1}(A),\ldots,\bar{g_n}(A))$,
which amounts to
$\bar{f}(\bar{g_1}(A),\ldots,\bar{g_n}(A)) \subseteq \bar{h}(A)$
So suppose $W\in\bar{f}(\bar{g_1}(A),\ldots,\bar{g_n}(A))$. That means
that there are
$V_i\in\bar{g_i}(A)$ with $V_1\times\cdots\times V_n\subseteq\dom(f)$
and $f[V_1\times\cdots\times V_n]\subseteq W$.
This implies that there are $U_i\in A$ with $U_i\subseteq\dom(g_i)$
and $g_i[U_i]\subseteq V_i$.
Now define $U = U_1\cap\cdots\cap U_n$, then $U\in A$, $U\subseteq\dom(g_i)$
and $g_i[U]\subseteq V_i$,
which then implies that $U\subseteq\dom(h)$ and $h[U]\subseteq W$.
Therefore $W\in\bar{h}(A)$.
\end{proof}
Note that this theorem also holds for non-continuous $f$.
As an example of the fact that we do not always have equality here, not even when
all functions are continuous, consider:
$$\begin{array}{c}
\Lim_{x\to\infty}(x - x) = \Lim_{x\to\infty} 0 = \bar{0}\\
(\Lim_{x\to\infty} x) - (\Lim_{x\to\infty} x) = \infty - \infty = \mathord{\leftrightarrow}
\end{array}$$
This agrees with the theorem, since
$\bar{0}\sqsubseteq\mathord{\leftrightarrow}$.
\begin{theorem} Monotonicity with respect to refinement:
$$A_1\sqsubseteq B_1, A_2\sqsubseteq B_2, \ldots, A_n\sqsubseteq B_n \Rightarrow \bar{f}(A_1,A_2,\ldots,A_n)\sqsubseteq \bar{f}(B_1,B_2,\ldots,B_n)$$
\end{theorem}
\begin{proof}
Let $V$ be given with $V\in \bar{f}(B_1,\ldots,B_n)$. Then there are $U_i\in B_i$
with $U_1\times\cdots\times U_n\subseteq\dom(f)$
and $f[U_1\times\cdots\times U_n]\subseteq W$. Because $A_i\sqsubseteq B_i$,
also $U_i\in A_i$, which implies that also $V\in \bar{f}(A_1,\ldots,A_n)$.
\end{proof}
Together these two theorems allow one to evaluate a filter limit `up to
refinement' by substituting the filter inside the expression.
Often this refinement does not hurt, because the right hand side will be
a refinement of $\bar{a}$ or $\infty$ anyway, allowing us to apply the next theorem,
which gives the relation between filter limits and the usual kind of limits:
\begin{theorem}\label{limits} Limit correspondence theorem:
\begin{eqnarray*}
\lim_{x\to a} f(x) = b &\Leftrightarrow& \Lim_{x\to a^{\pm}} f(x)\sqsubseteq \bar{b}\\
\lim_{x\to a^+} f(x) = b &\Leftrightarrow& \Lim_{x\to a^+} f(x)\sqsubseteq \bar{b}\\
\lim_{x\to \infty} f(x) = b &\Leftrightarrow& \Lim_{x\to \infty} f(x)\sqsubseteq \bar{b}
\end{eqnarray*}
\end{theorem}
\begin{proof}
We will show only the proof of the first equivalence.
The other proofs are similar.
\medskip\noindent
($\Rightarrow$)
Let be given that $\lim_{x\to a}f(x)=b$: we have to show that
$\bar{f}(a^{\pm})\sqsubseteq\bar{b}$. So suppose that $V\in\bar{b}$, which
means that for some $\epsilon>0$ we have that
$(b-\epsilon,b+\epsilon)\subseteq V$. Because of the limit,
there is a $\delta>0$ such that for all $x\in (a-\delta,a)\cup(a,a+\delta)$
(call this set $U$)
we have that $f(x)$ is defined and
$f(x)\in(b-\epsilon,b+\epsilon)$, or, in other words, $U\subseteq\dom(f)$ and
$f[U]\subseteq(b-\epsilon,b+\epsilon)$. Clearly $U$ satisfies $U\in a^{\pm}$ and
$f[U]\subseteq V$, and therefore $V\in\bar{f}(a^{\pm})$.
\medskip\noindent
($\Leftarrow$)
Now assume that $\bar{f}(a^{\pm})\sqsubseteq\bar{b}$. For a given $\epsilon>0$,
let $V = (b-\epsilon,b+\epsilon)$. Then $V\in\bar{b}$, so $V\in\bar{f}(a^{\pm})$,
and therefore there is some $U\in a^{\pm}$ with $U\subseteq\dom(f)$ and
$f[U]\subseteq V$. Because $U\in a^{\pm}$, for some $\delta>0$ we have that
$(a-\delta,a)\cup(a,a+\delta)\subseteq U$. Now this implies that if
$x\in (a-\delta,a)\cup(a,a+\delta)$ then $f(x)$ is defined and
$f(x)\in (b-\epsilon,b+\epsilon)$. Because for each $\epsilon>0$
there is a $\delta>0$ with this property,
$\lim_{x\to a}f(x)=b$.
\end{proof}
Similar theorems hold at $a^-$ and $-\infty$ and
for limits to plus or minus infinity.
In Europe $\lim_{x\to a^+}$ is sometimes written as $\lim_{x\downarrow a}$.
The $\infty$ and $a^+$ in the `ordinary' limits on the left are not filters: those
are just the customary notations for limits from the right and to infinity.
The $a^{\pm}$, $a^+$ and $\infty$ on the right {\em are\/} filters.
Together these theorems now give us a method to
rigorously evaluate ordinary limits using filters:
\begin{enumerate}
\item Replace the limit by the corresponding filter limit.
\item `Evaluate' the filter limit using filter calculations,
leading to a refinement.
\item If the right hand side of the refinement refines $\bar{a}$,
$-\infty$
or $\infty$ then we have succeeded and can use Theorem \ref{limits} (or
its analogue for infinite limits) to find
the answer to the original question.
If not, the method failed.
\end{enumerate}
As an example, we use this method to evaluate $\lim_{x\to\infty} 1/(x + 1)$:
$$\Lim_{x\to\infty} {1\over x + 1}\sqsubseteq {\bar{1}\over\Lim_{x\to\infty} (x + 1)}
\sqsubseteq {\bar{1}\over\infty + \bar{1}} = {\bar{1}\over\infty} = 0^+$$
(The refinements here are really equalities,
but the theorems
that we have do not give that, and in fact we do not need it.)
Now
$0^+\sqsubseteq\bar{0}$
and so from Theorem \ref{limits} we find that:
$$\lim_{x\to\infty} {1\over x + 1} = 0$$
\medskip\noindent
Here is another example of a limit evaluated using this method:
$$\Lim_{x\to 0^{\pm}} x \sin {1\over x} \sqsubseteq 0^{\pm} \sin {1\over 0^{\pm}} = 0^{\pm} \sin(\pm\infty) = 0^{\pm} [-1,1] = \bar{0}$$
(in this calculation `$[-1,1]$' is the filter generated by the closed interval $[-1,1]$, cf.~the
notation introduced in Section \ref{connected} below), which implies that:
$$\lim_{x\to 0} x \sin {1\over x} = 0$$
Note that we rigorously established this limit {\em by calculation}, and did not need the `squeeze
theorem' which is usually used to evaluate this limit.
\section{Interval filters and connected filters}\label{connected}
\begin{definition}
We will define a class of filters on $\R$ called the {\em interval filters}.
Consider the set:
$${\cal R} = \{-\infty^+\} \cup \{a^-\,|\, a\in\R\} \cup \{ a^+ \,|\, a\in\R\} \cup \{\infty^-\}$$
For each pair of elements $\alpha$ and $\beta$ from ${\cal R}$ for which
$\alpha\le \beta$ in the natural order on ${\cal R}$,
we will define a filter
$\mbox{\sf interval}(\alpha,\beta)$.
We map the elements of ${\cal R}$ to formulas as:
$$\begin{array}{ccccc}
\alpha &\quad& \phi_l(x,\alpha,\varepsilon) &\quad& \phi_r(x,\alpha,\varepsilon)\\
\noalign{\smallskip}
-\infty^+ && \top && x < -1/\varepsilon\\
a^- && a - \varepsilon < x && x < a\\
a^+ && a < x && x < a + \varepsilon\\
\infty^- && 1/\varepsilon < x && \top\\
\end{array}$$
and then we define:
$$\mbox{\sf interval}(\alpha,\beta) \equiv \{U\in\OR \,|\, \exists\varepsilon\in\R_{>0}.\,
\forall x\in\R.\, \phi_l(x,\alpha,\varepsilon) \land \phi_r(x,\beta,\varepsilon) \Rightarrow x\in U\}$$
\end{definition}
We will write interval filters using interval notation:
$$\begin{array}{rcl}
{[a,b)} &\equiv& \mbox{\sf interval}(a^-,b^-)\\
{[a,b]} &\equiv& \mbox{\sf interval}(a^-,b^+)
\end{array}\qquad
\begin{array}{rcl}
(a,b) &\equiv& \mbox{\sf interval}(a^+,b^-)\\
(a,b] &\equiv& \mbox{\sf interval}(a^+,b^+)
\end{array}$$
We suppose that it will be clear from the context when we mean
an interval as a set of real numbers and when we mean an interval as
an interval filter.
Generally, for finite $a$ and $b$ they are related like:
$$(a,b] = \mbox{\sf generated-by}(\{(a,b]\})$$
but not always.
If $a = b$, then the left hand side is $a^+$ but the right hand
side is {\sf improper} because the set $(a,a]$ is empty.
When we analyze a two-sided limit into two one-sided limits, and then want to
put the results back together, we need the concept of the `join' of two filters,
which we write $A \vee B$. For example, $0^- \vee 0^+ = 0^\pm$. This concept is defined as follows:
\begin{definition}\label{meet}
The operations {\em join\/} and {\em meet\/} on filters are defined by:
$$\begin{array}{rcl}
A\vee B &=& A\cap B\\
A\wedge B &=& \{U\cap V \,|\, U\in A \land V\in B\}
\end{array}$$
\end{definition}
We can now write the filters defined on page \pageref{specific}
as interval filters or as joins of interval filters:
$$\quad\begin{array}{rcl}
\bar{a} &=& [a,a]\\
{a}^- &=& [a,a)\\
{a}^+ &=& (a,a]\\
\quad{a}^{\pm} &=& [a,a)\vee(a,a]
\\\noalign{\medskip}%\end{array}\begin{array}{rcl}
\infty &=& [\infty,\infty)\\
-\infty &=& (-\infty,-\infty]\\
\pm\infty &=& (-\infty,-\infty]\vee[\infty,\infty)
\end{array}\quad\begin{array}{rcl}
\mathord{\leftrightarrow} &=& (-\infty,\infty)\\
\mathord{\rightarrow} &=& (0,\infty)\\
\mathord{\leftarrow} &=& (-\infty,0)\\
\pm\mathord{\rightarrow} &=& (-\infty,0)\vee(0,\infty)\\\noalign{\medskip}\ \\\ \\\
\end{array}$$
Now that we have the class of interval filters,
we will define the class of connected filters.
This definition is much simpler:
\begin{definition}
A filter $A$ is called connected when:
$$\forall U\in A.\, \exists U'\in A.\, U'\subseteq U \land \mbox{\it $U'$ is a connected set\/}$$
\end{definition}
Note that each of {\sf improper}, {\sf domain-error} and {\sf indeterminate}
is a connected filter.
The next three theorems give the relevant properties of the connected filters.
Together they `explain' why in practice one encounters only joins of interval
filters: the filters one starts with are of that kind, and the operations
that one applies to them conserve the property.
\begin{theorem}
The interval filters are the proper non-empty connected filters.
\end{theorem}
\begin{proof}
It is easy to verify that every interval filter is proper,
non-empty and connected.
Therefore all that is needed is to show that if a proper non-empty filter
is connected, then it is an interval filter.
Assume $A$ is a proper non-empty connected filter.
Define:
$$\begin{array}{rcl}
L &=& \big\{ l\in \{-\infty\}\cup\R \mathbin{|} \phantom{(-\infty,r)\in A \big\}}\llap{$(l,\infty)\in A \big\}$}\\
R &=& \rlap{$\big\{r\in\R\cup\{\infty\}$}\phantom{\big\{ l\in \{-\infty\}\cup\R} \mathbin{|} (-\infty,r)\in A \big\}
\end{array}$$
Both sets are non-empty, because the filter $A$ is non-empty and so $(-\infty,\infty)\in A$.
The set $L$ will be closed to the left
(if $l\in L$ and $l' < l$ then also $l'\in L$), so $L$ has to have the form
$\{-\infty\}$, $[-\infty,a)$, $[-\infty,a]$ or $[-\infty,\infty)$.
Depending on this, define $\alpha$ to be respectively $-\infty^+$, $a^-$,
$a^+$ or $\infty^-$.
Similarly $R$ will be of the
form $(-\infty,\infty]$, $[b,\infty]$, $(b,\infty]$ or $\{\infty\}$,
which gives $\beta$ being $-\infty^+$, $b^-$, $b^+$ or $\infty^-$.
We have that $L\cap R = \emptyset$ (because else $A$ would be improper), so $\alpha\le\beta$.
We are now going to show that $A = \mbox{\sf interval}(\alpha,\beta)$.
\medskip\noindent
($\subseteq$)
Suppose that $U\in A$.
The filter $A$ is proper and connected, so there is a non-empty connected $U'\in A$ with $U'\subseteq U$.
A non-empty connected open set $U'$ is always an open interval $(l,r)$,
and because $U'\in A$, we have that $l\in L$ and $r\in R$.
With the definitions of $\phi_l$ and $\phi_r$ it then follows that
$(l,r)\in\mbox{\sf interval}(\alpha,\beta)$.
Therefore also $U\in\mbox{\sf interval}(\alpha,\beta)$.
\medskip\noindent
($\supseteq$)
Suppose that $U\in\mbox{\sf interval}(\alpha,\beta)$.
Then from the definition of $\mbox{\sf interval}$ it is clear that
there is an open interval $(l,r)$ with $(l,r)\subseteq U$ and $(l,r)\in\mbox{\sf interval}(\alpha,\beta)$.
With the definitions of $\phi_l$ and $\phi_r$ it then follows that
$l\in L$ and $r\in R$.
Therefore $(l,r) = (l,\infty)\cap(-\infty,r) \in A$,
and so also $U\in A$.
\end{proof}
So all interval filters are connected, and the only connected filters
which are not an interval filter are the `error filters'
{\sf improper} and {\sf domain-error}.
\begin{theorem}
If $f$ is a function that is continuous on its domain, and $A$ is
a connected filter, then $\bar{f}(A)$ is also connected.
\end{theorem}
\begin{proof}
Suppose that $V\in\bar{f}(A)$,
so there is a $U\in A$ with $U\subseteq\dom(f)$ and $f[U]\subseteq V$.
We need to find a connected $V'\in\bar{f}(A)$ with $V'\subseteq V$.
Because $A$ is connected, there is a connected $U'\in A$ with $U'\subseteq U$.
Take $V' = f[U']$.
The image of a connected set under a continuous function is connected,
so $V'$ is connected too.
Furthermore, $V'$ has the required properties:
$U'\subseteq\dom(f)$ from which follows that $V'\in\bar{f}(A)$,
and $V' = f[U']\subseteq f[U]\subseteq V$.
\end{proof}
\begin{theorem}
$$\bar{f}(A\vee B) = \bar{f}(A)\vee\bar{f}(B)$$
\end{theorem}
\begin{proof}
($\sqsubseteq$)
Suppose $V\in\bar{f}(A)\vee\bar{f}(B)$, then both $V\in\bar{f}(A)$
and $V\in\bar{f}(B)$, so there are $U\in A$ and $U'\in B$ such that
$U,U'\subseteq\dom(f)$ and $f[U],f[U']\subseteq V$. Then
$U\cup U'\in A\vee B$, and furthermore $U\cup U'\subseteq\dom(f)$ and $f[U\cup U']\subseteq V$,
so $V\in\bar{f}(A\vee B)$.
\medskip\noindent
($\sqsupseteq$)
If $V\in\bar{f}(A\vee B)$, there is a $U\in A\vee B$ (and so $U\in A$ and
$U\in B$) with
$U\subseteq\dom(f)$ and $f[U]\subseteq V$. This same $U$ shows that
$V\in\bar{f}(A)$ and $V\in\bar{f}(A)$, which means that $V\in\bar{f}(A)\vee\bar{f}(B)$.
\end{proof}
Together, these theorems show that if one applies functions that are
continuous on their domain to finite joins of interval filters,
one always will end up with finite joins of interval filters again.
The final theorem is not needed for actual limit calculations, but it is included for completeness.
\begin{theorem}
$$\bar{f}(A\wedge B) \sqsubseteq \bar{f}(A)\wedge\bar{f}(B)$$
\end{theorem}
\begin{proof}
Let $V\in\bar{f}(A)\wedge\bar{f}(B)$, so there are $V'\in\bar{f}(A)$ and $V'\in\bar{f}(B)$
with $V = V'\cap V'$. Then there are $U'\in A$ and $U'\in B$ with
$U',U'\subseteq\dom(f)$ and $f[U']\subseteq V'$, $f[U']\subseteq V'$.
{F}rom this $U'\cap U'\in A\wedge B$, $U'\cap U'\subseteq\dom(f)$ and $f[U'\cap U']\subseteq V'\cap V'$,
and so $V'\cap V'\in\bar{f}(A\wedge B)$.
\end{proof}
Note that for $\wedge$ the reverse refinement does not hold.
If we take $f(x) = x^2$, then
$\bar{f}(\mathord{\leftarrow}\wedge\mathord{\rightarrow}) = \bar{f}(\dagger) = \dagger$,
but
$\bar{f}(\mathord{\leftarrow})\wedge\bar{f}(\mathord{\rightarrow}) = \mathord{\rightarrow}\wedge\mathord{\rightarrow} = \mathord{\rightarrow}$, and although
$\dagger\sqsubseteq\mathord{\rightarrow}$, it is not the case that $\mathord{\rightarrow}\sqsubseteq\dagger$.
\section{Mathematica revisited}\label{mathematica}
Now that we have given a calculus of filters that resembles the way
Mathematica calculates with infinity,
we will compare the behavior of our calculus and that
of Mathematica in detail.
This is what the calculations in the example Mathematica from
Section \ref{example} become when we redo them in our filter calculus:
$$\begin{array}{rcl}
{1/(\infty + 1)} &=& {0}^+\\
\sqrt{\infty} &=& \infty\\
\infty - \infty &=& \mathord{\leftrightarrow}\\
\mathord{\leftrightarrow} + \infty &=& \mathord{\leftrightarrow}\\
\sin \infty &=& [-1,1]
\end{array}\qquad
\begin{array}{rcl}
{1/[-1,1]} &=& \bot\\
{[-1,1]}\cdot[-1,1] &=& [-1,1]\\
{[-1,1]^2} &=& [0,1]\\
\bar{0}\,\sin \infty &=& \bar{0}\\
{\infty/\sin \infty} &=& {\infty/(\sin \infty)^2} = \bot
\end{array}$$
Here are some differences with Mathematica:
\begin{itemize}
\item
Mathematica does not like to give `no' for an answer.
So it prefers not to complain about undefinedness of a function.
According to Mathematica:
$${1\over[-1,1]} = (-\infty,-1]\vee[1,\infty)$$
instead of $\bot$.
Our definitions have different behavior because we want the correspondence
theorem about limits, Theorem \ref{limits}, to hold.
As an example of this difference in attitude consider the limit:
$$\lim_{x\to 0^+} x\,\arctan(\tan{1\over x})$$
The graph of $x\,\arctan(\tan({1/x}))$ looks like a `saw tooth' converging
to $0$,
and it is undefined infinitely often in each neighborhood of $0$.
Still Mathematica says%
\footnote{In version 3.0.
In version 4.1 it leaves the expression unevaluated.}:
\begin{flushleft}
\verb|In[12]:= Limit[x*ArcTan[Tan[1/x]], x->0, Direction->-1]|\\
\littleskip
\verb|Out[12]= 0|\\
\end{flushleft}
If you
ask MathXpert to evaluate this limit, you get the message: {\em This function is undefined
for certain values arbitrarily close to the limit point, so the limit is undefined.}
\medskip
\item
Mathematica does not identify as many expressions as it might.
For instance, in the example session it might have simplified:
$$\begin{array}{rcl}
\verb|Interval[{0, 0}]| &=& \verb|0|\\
\verb|Interval[{Infinity, Infinity}]| &=& \verb|Infinity|\\
\verb|Interval[{-Infinity, Infinity}]| &=& \verb|Indeterminate|
\end{array}$$
%\medskip
\item
Mathematica does not distinguish between open and closed intervals,
nor does it have the concept of {\sf left} and {\sf right} filters to
a point.
In order to add this subtlety to its \verb|Interval| calculus
all that would be needed is to mark all the endpoints of the intervals
with a $+$ or a $-$.
\medskip
\item
We have {\em two\/} kinds of `undefined' in our filter calculus:
$\mbox{\sf domain-error} = \bot$ and
$\mbox{\sf indeterminate} = \mathord{\leftrightarrow}$.
(The third filter, $\mbox{\sf improper} = \dagger$, only
occurs as the meet of two disjoint interval filters, and
never occurs in practice.)
Mathematica only has \verb|Indeterminate|,
and does not distinguish between these two kinds of undefinedness.
\medskip
\item
Mathematica issues a `warning' message like:
\begin{flushleft}
\verb|Power::infy: Infinite expression |$\displaystyle{\tt 1\over\tt 0}$\verb| encountered.|
\end{flushleft}
when it gets infinite or indeterminate results. This seems to imply that such results are
errors. However, in our theory those results are not errors at all but the
correct answers, and they should not generate such a message.
\medskip
\item We gave the details of the filter theory for the space of real numbers.
However, the expression language of Mathematica is about the complex numbers.
This is clear, for example, from the results of applying \verb|Sqrt| and \verb|Log| to
negative numbers. It is therefore strange that Mathematica gives answers involving intervals
to limit questions, since such answers are appropriate to {\em real\/} limits.
\end{itemize}
%
In any case,
our filter theory can be adapted to the complex numbers.
For example, complex infinity is
represented by the filter generated by the exteriors of disks centered at 0 (i.e., `neighborhoods of infinity').
The `one-sided' filters $a^+$ and $a^-$ are replaced by a wide variety of other filters representing
different ways in which a complex number $z$ can `approach' a limit point $a$: for example,
in complex analysis it is common to consider a limit restricted to an angular sector, such as
$\vert \theta \vert < \pi/4$. It is easy to define a `sector filter' generated by such a sector.
Our theorems that do not involve interval filters carry over to
the complex setting: pushing filter limits inside functions, the method of limit evaluation by refinement, etc.
We have not given a characterization of the connected filters in the complex case. For example,
there are more than just the sector filters: the filter generated by $\vert \theta \vert < r^2$ is not refined by any
sector filter.
\section{Conclusion and future directions}\label{conclusion}
We have presented the filter approach to evaluating limits involving
infinity. The usual way of calculating with infinities is not rigorous; indeed the
central concept {\em infinity} is never defined in calculus textbooks. The issue
is skirted by such statements as: `The symbol $\infty$ does not represent a real number and we cannot
use it in arithmetic in the usual way.' \cite{stewart}, p. 112.
Consider a student who says that $\lim_{x \to 0^+} 1/x$ is `undefined', while
the teacher says that $\infty$ is a better answer. `But', says the student,
`you said $\infty$ {\em is} undefined.' Such dialogues do occur regularly in classrooms and
teachers are unable to answer these questions on any rigorous basis. We have
now, at least in principle, provided a remedy for this situation, since our
theory of infinite limits is completely rigorous. Questions at the student level
in our theory can usually be proved or refuted.
When computer algebra systems make use of a set of calculation rules, there should
ideally be a semantics according to which these calculation rules are correct.
Even for ordinary algebra, this is not usually the case. But it is
usually the case that the rules are correct {\em except} that the system fails to check the pre-conditions.
That is, the semantics of algebra is understood -- but systems fail to implement the rules in a
semantically correct way. Up until now, the semantics of limits has not been properly
understood, and so the behavior of computer algebra systems did not even have a standard
against which implementations could be measured. In using intervals as answers to limits,
Mathematica has ventured into uncharted territory. We are now providing maps.
Our work, being completely rigorous, and based on simple set theory, is also
completely formal.%
\footnote{{\em Rigorous} implies that the concepts and theorems have a clear meaning and the theorems
can be correctly proved. {\em Formal\/} implies that the concepts can be defined and the theorems proved
in terms of set theory (or some other foundational theory of mathematics).
}
Therefore computer-checking the theory from this paper is possible,
and the resulting formalization would not only be an interesting exercise,
but also probably could be used to make the prover automatically
evaluate more limits.
In another direction, this material is suitable for inclusion in an undergraduate real-analysis course,
and the distinctions between different types of limits that it makes are suitable for inclusion in calculus books. In particular, calculus books need no longer steer away from calculations involving infinity. Simple rules for manipulating
infinity can be given and the justifications omitted, as is usually the case now when the justifications
involve epsilon-delta arguments.
\begin{thebibliography}{1}
\bibitem{beeson-mathpert}
Beeson, M.,
\newblock{{\em Mathpert Calculus Assistant}. This software program (now known as MathXpert)
was published in July, 1997 by Mathpert Systems, Santa Clara, CA,
and is commercially available from \url{}}.
\bibitem{beeson-hisc}
Beeson, M.,
\newblock{Design Principles of Mathpert: Software to support education in algebra and calculus}, in:
\newblock{Kajler, N. (ed.) {\em Computer-Human Interaction in Symbolic Computation}, Texts and Monographs in Symbolic Computation,
Springer-Verlag, Berlin/Heidelberg/New York (1998), pp. 89-115}.
\bibitem{beeson-ste}
Beeson, M.
\newblock {Beeson, M. MathXpert: un logiciel pour aider les \'el\`eves
\`a apprendre les math\'ematiques par l'action, {\em
Sciences et techniques \'educatives}, {\bf 9} (1) 37-62,
2002.}
An English translation of this article under the title
{\em MathXpert: learning mathematics in the twenty-first century} is available at\hfill\break
\url{}.
\bibitem{beeson-nsa}
Beeson, M.,
\newblock { Using nonstandard analysis to verify the correctness of computations},
\newblock{{\em International Journal of Foundations of Computer Science}, {\bf 6} (3) (1995), pp. 299-338}.
\bibitem{kur:66}
K.~Kuratowski.
\newblock {\em Topology}, volume~1.
\newblock Academic Press, New York, London, 1966.
\bibitem{mon:ged:hea:lab:vor:97}
M.~Monagan, K.~Geddes, K.~Heal, G.~Labahn, and S.~Vorkoetter.
\newblock {\em Maple V Programming Guide for Release 5}.
\newblock Springer-Verlag, Berlin/Heidelberg, 1997.
\bibitem{sim:76}
B.~Sims.
\newblock {\em Fundamentals of Topology}.
\newblock MacMillan, New York, 1976.
\bibitem{stewart}
Stewart.
\newblock{\em Calculus, 3rd edition}, Brooks-Cole, Pacific Grove, CA 1995.
\bibitem{wol:96}
S.~Wolfram.
\newblock {\em The Mathematica book}.
\newblock Cambridge University Press, Cambridge, 1996.
\end{thebibliography}
\end{document}