\documentstyle[11pt]{article}
 
\title{Can we Resolve the Tension between Constructive Type Theorists
and Classical Mathematicians?}
\author{Paul B. Jackson \\
\tt pbj@dcs.ed.ac.uk}
 
\begin{document}
\date{}
\maketitle
 
\section{Introduction}
Constructive type theories (CTTs) are advocated as a foundation for
mathematics which replaces classical logic and set theory.
Significant work has gone into building interactive theorem-proving
systems based on
CTTs~\cite{Bruijn80,Constable&86,Jackson94,alf95,Luo&92,Coq95}
and it seems desirable to involve the projects currently around such
systems in any future QED venture.  However, mathematics based on CTTs
is rather different from the usual classical mathematics taught in
schools and universities.  QED must support this classical mathematics
if it is to have any success.  How then is cooperation possible?
 
 
 
 
\section{CTT-based mathematics}
All CTT-based mathematics has a computational reading. For example, a
theorem of form:
\[
\forall x \in A. \exists y \in B. P_{x,y}
\]
can be read as saying that given any $x$ in set $A$, there is a method of
{\em computing} a $y$ in set $B$ satisfying the predicate $P_{x,y}$.
Further, a CTT proof of such a theorem precisely specifies one such method.
In general, theorems in CTT-based mathematics can be considered as
specifications for programs and proofs as guides for the automatic
construction of programs.
This program synthesis paradigm has been one of the major factors
stimulating recent interest in CTTs.
 
CTT-based mathematics so far has been largely modelled on the school
of constructive mathematics first developed by
Bishop~\cite{Bishop&85,Mines&88}.
A feature of the Bishop school that increases its acceptability to
classical mathematicians is that every theorem also has a reading
as a classical theorem.  This is not the case with other schools of
constructive mathematics.
 
CTT-based mathematics has a finer grain than classical mathematics.
Many distinctions are made that offer alternative computational readings.
These distinctions are at a very basic level: for example, different
readings are frequently be given for equivalence and subtype relations.
It is a challenge to decide which alternatives to adopt and to
keep the number of alternatives considered to a reasonable size.
 
Formalization forces definite choices to be made on alternatives where
in the texts the need for a decision is glossed over or delayed.  It
also frequently turns out that functions need extra arguments that
provide computational information.  A formal development must include
these arguments, though they also are often glossed over in the texts.
 
Current CTTs are somewhat awkward. In nearly all, the notion of {\em
type} is not nearly as versatile as that of {\em set} in set
theories. For example, equality of types is usually not extensional
and a principle of comprehension is usually lacking.  Also, many CTTs
are regarded as being too complex to be acceptable as foundational
theories.
 
Examples of formalization of mathematics in CTTs include the intermediate
value theorem and some basic abstract algebra~\cite{Forester93,Jackson94}.
 
For the above reasons, formalizing Bishop-style mathematics in CTTs
seems to be a significantly slower and more uncertain process than
formalizing classical mathematics.
 
\section{Opportunities for Cooperation}
 
\subsection{Libraries}
Sharing of libraries on elementary concrete topics such as integers
and finite sequences (lists) might be possible since there CTT-based
and classical mathematics are similar. However, sharing of
libraries on more abstract topics would be much more problematic.
 
Importing of classical developments into a CTT setting would be all
but impossible because all the essential distinctions would be
missing.
 
Importing a CTT-based development into a classical setting is
possible, though the classical mathematician is likely to consider all
the extra distinctions as irrelevant clutter. More pragmatically, the
need to import might not be there, since the quantity and sophistication
of formalized classical mathematics is likely to be much greater than
that of CTT-based mathematics, both for reasons given in the previous
section and simply because the corpus of formalizable classical
mathematics is far far larger.
 
 
\subsection{Systems Development}
Opportunities are brightest here.  There are many engineering
challenges common to any system intended for helping to develop
mathematics. For example, in the areas of user interfaces,
mathematical databases, and automated reasoning.
 
\subsection{Classical Mathematicians using CTT-based Systems}
 
It has been shown consistent to extend CTTs with oracles
in order to create classical type theories~\cite{Howe91}. A CTT-based
system with such an extended CTT could be used by a classical
mathematician to develop classical mathematics, though work is still
needed to demonstrate that the extended type theory would have a
versatility approaching that of set theory.
 
\subsection{Constructive Type Theorists using Classical Systems}
 
It might be possible to persuade the architects of CTT-based systems
to consider seeking in a classical system some of the advantages they
attribute to CTTs.
 
For example, type theories are claimed to provide a more structured
language than set theory for mathematics, closer to that used in
normal mathematical practice. However the Mizar
project~\cite{Rudnicki92&} has demonstrated how such advantages can be
gained by layering a type system on top of a classical set theoretic
foundation.
 
Another advantage claimed is that CTTs provide a natural environment
for program verification and synthesis, since CTTs have a built-in
programming language and a program synthesis paradigm.  However, the
built-in languages are rather simple purely-functional languages. CTTs
have no advantages when it comes to dealing with more sophisticated
languages with imperative, concurrent or parallel features.  Analogous
synthesis paradigms can be explored in a classical setting if for
example programs are represented syntactically and logic variables are
used to stand in for program sections that remain to be synthesized.
With such an approach both the programming language and the synthesis
mechanism would be more open to exploration since neither would be be
hard wired.
 
\section{Conclusions}
\begin{itemize}
 
\item {\em No},
the fundamental tension between constructive type theorists and
classical mathematicians is not resolvable:
the mathematics that each are interested in is just too different.
 
\item {\em Yes}, many aspects of the tension between constructive type
theorists and classical mathematicians are resolvable: in particular,
there do seem to be a number of opportunities for productive
collaboration, especially in the engineering of interactive
theorem-proving systems.
 
\end{itemize}
 
 
\section{Discussion}
Here I've reconstituted a few of the comments made at the end of the
talk from some rather sketchy notes that I took down.  Hopefully no one's
views are misrepresented. The comments are being checked with their
ascribed authors at the moment.
 
\begin{itemize}
\item ({\em Holmes}) ``One of the major features of CTTs is the role of proof
objects''.  In proof theory, these proof objects can be more compact and
convenient to work with than proof trees.
 
\item ({\em Kapur})
``Present day constructivist often cite 19th century mathematics as being
in their tradition, but this mathematics also fits in perfectly well with
classical mathematics''.
Kapur also emphasized the size of the CTT community and
expressed the need to have them involved in any QED venture.
 
\item ({\em Trybulec}) ``Too much of the QED manifesto was devoted to
constructive concerns. There {\em is} a koine on which nearly all
mathematicians agree.  The QED project should try to take the simplest
possible approach. The problems are hard enough as it is''.
 
\item ({\em McCarthy})
``Hilbert complained about being driven out of Cantor's paradise. Well, set
theories like ZF allow us to be driven out the minimal amount''.
 
\item ({\em Trybulec}) ``A development of Heyting Algebras
was carried out in the classical system Mizar''. Trybulec showed this
to a colleague who thought the development contained a new result.
\end{itemize}
 
\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{AGNvS94}
 
\bibitem[AGNvS94]{alf95}
Thorsten Altenkirch, Veronica Gaspes, Bengt Nordstr{\"o}m, and Bj{\"o}rn von
  Sydow.
\newblock {\em A User's Guide to {ALF}}.
\newblock Chalmers University of Technology, Sweden, May 1994.
\newblock Available on the WWW {\tt
  file://ftp.cs.chalmers.se/pub/users/alti/alf.ps.Z}.
 
\bibitem[BB85]{Bishop&85}
Errett Bishop and Douglas Bridges.
\newblock {\em Constructive Analysis}.
\newblock Springer-Verlag, 1985.
 
\bibitem[C{\etalchar{+}}86]{Constable&86}
Robert Constable et~al.
\newblock {\em Implementing Mathematics with The Nuprl Development System}.
\newblock Prentice-Hall, NJ, 1986.
 
\bibitem[CCF{\etalchar{+}}95]{Coq95}
C.~Cornes, J.~Courant, J.~Filliatre, G.~Huet, P.~Manoury, C.~Munoz, C.~Murthy,
  C.~Parent, C.~Paulin-Mohring, A.~Saibi, and B.~Werner.
\newblock The {Coq} proof assistant reference manual: Version {5.10}.
\newblock Technical Report 0177, {INRIA}, July 1995.
\newblock Available from {\tt ftp.inria.fr}.
 
\bibitem[dB80]{Bruijn80}
N.~G. de~Bruijn.
\newblock A survey of the project {AUTOMATH}.
\newblock In J.~P. Seldin and J.~R. Hindley, editors, {\em Essays in
  Combinatory Logic, Lambda Calculus, and Formalism}, pages 589--606. Academic
  Press, 1980.
 
\bibitem[For93]{Forester93}
Max~B. Forester.
\newblock Formalizing constructive real analysis.
\newblock Technical Report TR93-1382, Computer Science Dept., Cornell
  University, Ithaca, NY, 1993.
 
\bibitem[How91]{Howe91}
Douglas~J. Howe.
\newblock On computational open-endedness in {M}artin-{L}{\"{o}}f's type
  theory.
\newblock In {\em Proceedings of Sixth Symposium on Logic in Computer Science},
  pages 162--172. IEEE Computer Society, 1991.
 
\bibitem[Jac95]{Jackson94}
Paul~B. Jackson.
\newblock {\em Enhancing the Nuprl Proof Development System and Applying it to
  Computational Abstract Algebra}.
\newblock PhD thesis, Cornell University, January 1995.
\newblock Available as Cornell Computer Science Technical Report {TR95-1509}
  from {\tt http://cs-tr.cs.cornell.edu}.
 
\bibitem[LP92]{Luo&92}
Zhaohui Luo and Robert Pollack.
\newblock Lego proof development system: User's manual.
\newblock Technical Report ECS-LFCS-92-211, LFCS, University of Edinburgh, May
  1992.
\newblock Available from {\tt http://www.dcs.ed.ac.uk/lfcsreps/}.
 
\bibitem[MRR88]{Mines&88}
Ray Mines, Fred Richman, and Wim Ruitenburg.
\newblock {\em A Course in constructive Algebra}.
\newblock Universitext. Springer-Verlag, 1988.
 
\bibitem[Rud92]{Rudnicki92&}
P.~Rudnicki.
\newblock An overview of the {Mizar} project.
\newblock In {\em 1992 Workshop on Types for Proofs and Programs}, Bastad,
  1992. Chalmers University of Technology.
 
\end{thebibliography}
 
\end{document}