FOM: Length of formalizations

[Randy Pollack]

The discussion on "Length of formalizations" misses a crucial point.

Mizar supports a complicated linguistic superstructure on top of its
foundational logic.  The mathematics that is formalized in Mizar is
expressed in terms of this superstructure.  Although the logic may be
formally laid out, this linguistic superstructure is almost completely
unspecified.  One learns about it by example and personal
transmission.  Thus, it seems misleading to think that Mizar books are
fully formalized.

I'm not saying Mizar is smoke.  On the contrary, since our favorite
logics clearly cannot support actual formalization, it is essential to
have a linguistic superstructure, or perhaps a more expressive
foundational logic.  But a long-term goal of the enterprise must be a
formal explanation of this linguistic layer.

The situation with Isabelle is a bit different than Mizar.  Isabelle
also has a linguistic superstructure for parsing, pretty printing,
etc.  But Isabelle also has a formal metalevel in which the particular
object logics (eg FOL+ZF) are formalized.  This metalevel (which is an
impredicative HOL with type classes and equality; much stronger than
the FO object logic) supports many of the linguistic tools necessary
for mathematics.  E.g. equality at the metalevel supports definitions
at the object level.  (There is much more to say about metalevel
approaches.)  The formalization of ZF in Isabelle is truly impressive.
To my reading it uses the formal metalanguage in surprisingly subtle
ways.  

I don't think Isabelle, or any other existing proof tool, is yet
competent to deal with everyday mathematical practice.  Among the
outstanding problems are the packaging of mathematical structures and
abstract use of such structures.

BTW, I agree with Andrej Bauer that it is "when" not "if" mainstream
maths will be presented formally.

-- 
Randy Pollack
Phone: +44 131 650 5145                      URL: www.dcs.ed.ac.uk/~rap/
Computer Science, Edinburgh Univ. Kings Buildings, Edinburgh EH9 3JZ, UK