\documentstyle[11pt]{article}
\title{Development of Analysis in the QED Project}
\author{F. Javier Thayer\thanks{e-mail: \tt jt@linus.mitre.org}}
\date{} 
\begin{document}
 
\maketitle
\section{Introduction}
 
The QED project is a cooperative effort in the area of automated
mathematical reasoning. Many goals have been suggested for this common
effort.  A common element in most of the suggested goals is the
construction of a rigorous mathematics database. By rigorous I mean
that each entry in the database is a valid theorem stated in some
formal theory.
 
Following is a summary of my presentation on Formalized Analysis at
the 2nd QED workshop held in Warsaw, Poland July 20 to 22.  My focus
in the discussion is the styles of mathematical development
appropriate for formalizing analysis in the QED project. I believe the
answer to this question is time dependent.
 
\section{Time Scales}
 
In discussing the QED project and its goals, I suggest we establish
some time scales. My subjective values for these time horizons are
short term (6 months to 2 years), medium term (2 to 5 years), long
term (5 to 15) years and the distant future 15 years or more.  Though
QED is clearly a project for the long term or maybe even the distant
future, setting achievable short and medium term goals is crucial for
the project for a number of reasons. Shorter-term goals provide:
\begin{itemize}
 \item Feedback for testing ideas.
 \item Motivation for developers.
 \item Reassurance for funders.
 \item Useful applications, in education, symbolic mathematics and formal
 methods.
 
   \end{itemize}
 
\section{Approaches to Analysis}
 
The terms ``Big Theory'' and ``Little Theory'' have been coined by
Farmer, Guttman and Thayer to describe certain styles of mathematical
development. I will only mention here some characteristics of each of
these styles. For the Big Theory style there is usually a well
understood formalism in which all reasoning is imbedded.  Moreover, no
special logical artifices (such as theory interpretations) are needed
to apply theorems about structures since structures are first-class
objects. I am using structure here in the sense of a structure such as
a vector space, or topological space.  For the Little Theories style
one considers a large number of ``small'' axiomatic theories
interrelated by theory interpretations. Structures such as vector
spaces and so on are dealt with as axiomatic theories. One considers
one instance or at best a small number of instances of such
structures.
 
\section{ Big Theory: Advantages and Disadvantages}
 
I would expect any development style using the Big Theory approach to
be based on some form of set theory. This is an advantage, since
foundational prerequisites for the working mathematician are almost
zero. Regarding the Bourbaki approach as the prototypical ``big
theory'' style, its is clear that the Big Theory style is conceptually
elegant, extremely refined, general and highly traditional.
 
The biggest advantage of the Big Theory approach, is that
quantification over theories is straightforward.  This provides a
whole range of ideas and techniques not easily available in the little
theories style. For instance, topological methods can be applied to
families of structures, to build and study structures such as fibre
bundles, sheaves, and deformations.  These ideas are an essential part
of the analyst's toolkit.
 
Though the Big Theory approach allows for enormous flexibility, and
the application of a whole range of techniques (as seen above), it has
various drawbacks. One minor drawback, is that ``big theory'' has to
be developed to the point where one can begin to define structures
either as tuples or by some other artifice. Another drawback, is that
the mathematical universe is too homogeneous. This makes pattern
matching, and consequently application of results considerably more
difficult. One way of dealing with this is to superimpose a sorting
structure on the universe to facilitate pattern matching.
 
 
\section{Little Theories: Advantages and Disadvantages}
 
 Little Theories provide pedagogically compact, often insightful
approaches to various areas in mathematics. Basically, write down the
axioms and you're in business. This makes short or medium term goals
attainable. Similarly, much of analysis that only involves reasoning
with inequalities, fits nicely into little theories since we are not
using more difficult topological properties of mappings.  Finally, the
Little Theories approach fits in nicely with Type Theory. This
provides syntactic cues for matching and theorem application.
 
 
On the negative side, Type Theory is inflexible. For instance,
completions (algebraic and completions in particular) and other
extensions (such as adjunction of points at infinity to a topological
space) are very hard to deal with. Another difficulty of Little
Theories is the need for special artifices to compensate for lack of
machinery. For instance, functorial concepts cannot be easily
accommodated within the little theories approach, so that topological
arguments based on homology cannot be used.
 
\section{Discussion}
 
The presentation was followed by a discussion that focused on a number
of issues including the suitability of Type Theory for mechanized
mathematics. Though my presentation was not directly focused on types,
there was some concern that by favoring the Big Theory approach, I
argued against types. Although I do not consider types (or sorts) to
be useful in the long term, I believe there use is an extremely
helpful adjunct to the Little Theories style which in the shorter term
is extremely valuable.
 
\section{Summary}
 
The Little Theories approach is pedagogically extremely useful, and in
the short and medium term is capable of providing a framework for
development of automated mathematics. It can work well with existing
symbolic mathematics systems providing payoff in education and
possibly other areas. As a long term goal, however, I believe that QED
must include in its mathematical database, general theorems on
topology and geometry, theorems about families of structures,
theorems about functors such as enveloping algebras and so on. This is
a powerful argument that some big theory approach to QED is required.
 
\end{document}