FOM: Length of formalizations
rap at dcs.ed.ac.uk
Fri Jan 14 10:00:30 EST 2000
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
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
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.
Phone: +44 131 650 5145 URL: www.dcs.ed.ac.uk/~rap/
Computer Science, Edinburgh Univ. Kings Buildings, Edinburgh EH9 3JZ, UK
More information about the FOM