http://www.cl.cam.ac.uk/users/jrh/papers/form-math2.html
ABSTRACT:
It is generally accepted that in principle it's possible to formalize
completely almost all of present-day mathematics. The practicability
of *actually* doing so is widely doubted, as is the value of the
result. But in the computer age we believe that such formalization is
possible and desirable. In contrast to the QED Manifesto (Anonymous
1994) however, we do not offer polemics in support of such a project.
We merely try to place the formalization of mathematics in its
historical perspective, as well as looking at existing praxis and
identifying what we regard as the most interesting issues, theoretical
and practical.
TABLE OF CONTENTS:
History and Philosophy
Rigour and the axiomatic method
The History of Formal Logic
Hilbert's Programme
The Bourbaki view
Enter the computer
Formalizing mathematics
Formalization
Criticism and reconstruction
The choice of a foundational system
Definitions and locutions
Partial functions and undefined terms
Practical issues
Feasibility
Extensibility and LCF
Metatheory and reflection
How much automation do we want?
User interaction
Experience of formalized mathematics
The Future
Cheers,
John.
=========================================================================
John Harrison | email: jharriso@abo.fi
Abo Akademi University | web: http://www.abo.fi/~jharriso/
Department of Computer Science | phone: +358 (9)21 265-4049
Lemminkaisenkatu 14a | fax: +358 (9)21 265-4732
20520 Turku | home: +358 (9)21 2316132
FINLAND | time: UTC+2:00
=========================================================================