The discovery by Babbage of the principles underlying the general purpose digital computer, long before the technology became available to build these computers, has become part of the popular culture.
It is now a hundred years since the beginnings of modern mathematical logic. Early in that development the power of the new logic was demonstrated by Whitehead and Russell in their epic mathematical tome Principia Mathematica. In this work Whitehead and Russell demonstrated that the main body of mathematics then known could be derived within a simple formal logical system.
This might have been the beginning of a new era in mathematics, but it was not. At least probably not in the way that the authors might have hoped. Like Babbage, Whitehead and Russell had ideas which were before their time.
Russell's theory of types may have been the first significant advance in mathematical rigour not to have been taken into the practice of mathematics. For Russell and Whitehead `the theory of types' was a way of doing ultimately rigorous mathematical proofs, a tool for mathematicians to be used in the development of mathematics. In practice it marked an unexpected watershed in the development of mathematical logic. The point at which formal logical systems ceased to be regarded, even by the developers of these systems, as tools for practical use in the development of mathematics. Henceforth formal systems became the objects of study in a new discipline called metamathematics. Mathematics was henceforth, though in principle derivable in these formal systems, in practice developed as informally as ever.
The purposes of Russell and Whitehead were not entirely (or even primarily) concerned with the pragmatics of rigorous proof. A central aim of their work was to demonstrate the philosophical conjecture that mathematics is reducible to pure logic. In this purpose also they are widely held to have failed.
The main purpose of this essay is to discuss `the mechanisation of mathematics'. The discussion is partly speculation about the future, intended to motivate the reader's interest in the topic. This speculation will be underpinned by anecdotal evidence from current developments, which I hope will help to give some credence to the speculations. The discussion will take place in the context of the substantial technical advances which have taken place in mathematical logic over the past century.
I hope that historians in the twenty second century will come to view the twentieth as the century of the development of mathematical logic, and the twenty first that of its effective exploitation.
However, during this century, while formal logical systems have been sidelined as practical approaches to ordinary mathematical proof, they have also been undermined philosophically. They have been undermined, for example, by philosophers such as Quine and Lakatos, who, each in his own way, appear to doubt that there is any fundamental distinction between the mathematical and the physical sciences. The importance of logical truth is undermined by conventionalists who see no more than arbitrary conventions, and perhaps even by Wittgenstein who appeared to regard indubitability as incompatible with truth, though this doctrine may be too extreme to do much damage.
It is my main purpose in this essay, to discuss why the mechanisation of mathematics, in the sense here intended, is possible. It is clear in the practical use of computers for proving mathematical theorems and developing mathematical systems, that the criteria by which the truth of a conjecture is judged, and the means whereby it is established, differ between mathematics (pure or applied) and most other sciences. The ground of this distinction is that mathematics is essentially abstract. Mathematics deals entirely with abstract entities; a mathematical conjecture says nothing about the material world. Our understanding of such conjectures is such that we do not consider that a physical experiment will suffice to establish them. For a conjecture in one of the physical sciences to be a substantive hypothesis it must say something about the physical world. For such a hypothesis to say something substantive, it must say something which could possibly be false (which is not quite to say that it need be falsifiable).