[FOM] Adventures in Formalization

[Larry Paulson]

I am always glad when a serious mathematician takes an interest in the work that
I and my colleagues have been doing over the past several decades. Your posts
raise a great many issues, and I can only comment on a few of them. Of course, I
am speaking for myself only, and other researchers are bound to take their own
point of view.

To answer one of your questions plainly:

> Can absolute rigor actually have an actual physical existence?

No. In our community, we do everything we can to build rigorous systems. We use
safe programming languages such as ML. We work in axiomatic formalisms, which in
many cases are chosen to be quite conservative. We impose on our users the
discipline of developing everything purely by making definitions rather than by
introducing new axioms. We impose on ourselves, in many cases, the discipline of
a system architecture (the LCF approach) that gives only a small kernel of code
the capability to declare that a certain piece of syntax designates a theorem.

Some of us go further still, verifying critical parts of a proof assistant right
through the stages of compilation from ML to machine language, and this verified
machine code could, in principle, run under a verified operating system (such
things exist) and on verified hardware. Nevertheless, using an untrusted
technology to verify itself is ultimately begging the question. Incidentally,
there are some among us who have read Lakatos and don't believe in absolute
rigour, even in principle.

Our aim is to achieve very high reliability along with the capability of coping
with expressions, proofs and formal developments that are far too large to cope
with any other way.

> I envision a large system and various important weaker subsystems. Since too
> much math can be done in systems much weaker than ZFC, this should be
> reflected in the choice of Gold Standards. There should be a few major Gold
> Standards ranging from Finite Set Theory to full blown ZFC.

A great many formalisms are used at present. Higher-order logic (used in HOL
Light and HOL4) is of course much weaker than ZFC, but seems to be good enough
for large chunks of analysis. A great many constructive type theories are used,
above all in Coq; unfortunately I have no clear idea how the strength of such
formalisms compares with that of ZFC.

I cannot help but remark that I've created a quite good proof assistant for ZFC,
namely Isabelle/ZF. It is really for doing set theory itself, and it provides no
notational concessions for people whose interest is, say, complex analysis.

ZFC will not suffice for those domains of mathematics that casually step right
outside of set theory by imagining such things as the category of all sets and
functions.

> Take a look at the statements of theorems in http://www.cs.ru.nl/~freek/100/
> They are all unconscionably ugly to read and digest for a typical person
> outside the Theorem Proving community. In the Theorem Proving community, they
> are probably looked at as breathtaking works of art.

I will try to ignore the tone of this passage and merely comment on some of the
reasons why the syntax of these systems has so little in common with standard
mathematical notation. Most of these systems were not designed for doing
mathematics: they were experiments in mechanised logic with applications to the
verification of hardware and software. Two noteworthy systems, namely AUTOMATH
and Mizar, did have the objective of doing mathematics. Both of them are great
achievements, the former in demonstrating the power of type theory to express
mathematics, the latter in its language of algebraic properties and its soft
type system, mapping down to Tarski–Grothendieck set theory and already meeting
many of your objectives, though its syntax isn't beautiful. The syntax of
AUTOMATH is particularly unreadable, but de Bruijn was working in the era of
punched cards, and was trying to solve problems more fundamental than surface
syntax.

The question of zero may be instructive. In HOL Light, the complex number zero
is written Cx(&0). Here, 0 denotes a natural number; the & is the injection from
natural numbers into the reals; Cx is the injection from the reals into the
complex numbers. One half, written as a complex number, is Cx(&1 / &2). I agree
that that looks horrible. I will take the liberty of answering for John Harrison
as to why he and his users put up with it: because it allows him to have a
simple type system and a small proof kernel (his system isn't called HOL Light
for nothing).

Isabelle/HOL uses the concept of axiomatic type classes to overload the constant
0 quite elegantly, along with the properties typically relating + and other
symbols. And so 0 can denote a natural number, an integer, a real number, a
complex number, the null polynomial, etc. One can do similar things with the
constant 1. The price of this is a more complicated type system, and yet its
limitations become apparent quite quickly. Mathematicians who use Isabelle are
sometimes annoyed at the necessity to write Suc(n) rather than n+1; they are
equal of course, but almost everything works better if the former expression is
used, and it is even worse that sometimes an expression such as n+3 needs to be
rewritten as Suc(n+2) in order to get something done. And while Suc(0) and 1 are
equal, they are syntactically different, despite our best efforts to make the
differences invisible.

As for the prospects of supporting standard mathematical notation, commercial
computer algebra systems such as Mathematica probably represent the best we can
expect. Mathematica has a lot of money behind it, and of course it was built
from the start to support mathematics and nothing else. A lot of mathematical
conventions will have to go. Consider how many different operations are
expressed by nothing: the expression xy could denote the product of x and y, or
string concatenation, or function composition (in either order), or it could
denote the pointwise product of two functions and probably a dozen other things.
And that is only the start of our difficulties.

Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
Cambridge CB3 0FD, England
Tel: +44(0)1223 334623