Machine Logic

Hao Wang on the formalisation of mathematics

26 Jul 2023

Since I have already devoted a blog post to a wildly overrated philosopher who barely understood logic, it’s time to pay tribute to an underrated philosopher who wrote thoughtfully and presciently on the formalisation of mathematics: Hao Wang. Wang must be seen primarily as a philosopher in the traditional sense, who wrote essays and books, but he also wrote code. He is the creator of the first truly powerful automatic theorem prover, using what we now know as a tableau method. Indeed, most of today’s technology for automated deduction has its origins in the work of philosophers — we can add Hilary Putnam and J Alan Robinson – who decided to write more than just words.

Wang on formalisation

Here is Hao Wang, writing in 1955 (!):¹

We are led to believe that there is a fairly simple axiom system from which it is possible to derive almost all mathematical theorems and truths mechanically. This is at present merely a theoretical possibility, for no serious attempts seem to have been made to prove, for instance, all the theorems, of an elementary textbook of calculus.

Of course, we are now well past that stage.

Nevertheless, we seem to get a feeling of grandeur from the realization that a simple axiom system which we can quite easily memorize by heart embodies, in a sense, practically all the mathematical truths. It is not very hard to get to know the axiom system so well that people would say you understood the system.

He was doubtless thinking of Zermelo Fraenkel set theory. Modern type theories are possibly a little too difficult for most people to memorise.

Unfortunately just to be able thus to understand the system neither gives you very deep insight into the nature of mathematics nor makes you a very good mathematician.

Very true. But we find ourselves asking again, how was he thinking about this back in 1955? And his points are absolutely topical today. He considers what level of formality is best for communication: an intuitive abstract, a more detailed exposition, and so on leading ultimately to a formalisation in the style of Russell and Whitehead. It’s clear that the increasing precision is not always beneficial! But he continues

To put thoughts on physics into mathematical symbols is one way of formalization. Through accumulation and tradition this way of formalization has also become a powerful way of communication: for those who understand the language, a short formula may express more precisely thought which could only be explained by many pages of ordinary words, and much less satisfactorily.

The use of symbolism can be powerful and effective, but it needs to be done right.

Of course, he wrote much more. He described formalisation as a continuing process dating back to Euclid, whose famous axiomatic system provided a common framework for many schools of ancient Greek mathematics. It continued with the 19th-century “arithmetisation of analysis”:

There is the long story of how Lagrange, Cauchy, Weierstrass, and others strove to formalize exactly the basic notions of limits, continuity, derivatives, etc., providing thereby rigorous (though not necessarily reliable) foundations for mathematical analysis.

And this continued into the 20th century with the origins of set theory, the paradoxes and the promulgation of the seemingly consistent Zermelo-Fraenkel axioms.

Wang’s paper continues with insightful and relatively informal observations on many aspects of formalisation and precision that are still relevant today. He’s written a more technical paper:² covering similar themes, but which goes on to sketch an actual axiomatic framework specifically designed for formalisation.

It begins in his usual lively style:

Zest for both system and objectivity is the formal logician’s original sin. He pays for it by constant frustrations and by living ofttimes the life of an intellectual outcaste. The task of squeezing a large body of stubborn facts into a more or less rigid system can be a painful one, especially since the facts of mathematics are among the most stubborn of all facts. Moreover, the more general and abstract we get, the farther removed we are from the raw mathematical experience. As intuition ceases to operate effectively, we fall into many unexpected traps.

And continues with remarks that are historically informed while at the same time intriguing:

A field has often to be developed very thoroughly before it is ripe for a systematic and rigorous organization. The history of the calculus illustrates this point clearly: founded in the seventeenth century, rapidly expanded in the eighteenth, the calculus got acceptable foundations only in the nineteenth century and even today logicians generally have misgivings on the matter.

This foundational development, Wang argues, also required a coherent treatment of set theory. He notes how claims about “arbitrary curves” or “arbitrary functions” required elucidation.

The problem is that of representing functions by trigonometric series which interested many a mathematician when Cantor began his research career around 1870. In trying to extend the uniqueness of representation to certain functions with infinitely many singular points, he was led to the notion of a derived set which not only marked the beginning of his study of the theory of point sets but led him later on to the construction of transfinite ordinal numbers. Such historical facts ought to help combat the erroneous impression that Cantor invented, by one stroke of genius, a whole theory of sets which was entirely isolated from the main stream of mathematics at his time.

The article goes on to discuss various aspects of Cantor’s set theory and then start to speculate on how the formalisation of mathematics might be undertaken. From today’s perspective, his focus looks excessively set-theoretic, with only hints of a phenomenon that might have influenced today’s type theories:

There are… numerous attempts to construct artificial systems which are both demonstrably consistent and also adequate to the development of the “principal” (or “useful”) parts of mathematics. Most of these systems modify our basic logical principles such as the law of excluded middle and the principle of extensionality (for sets), and it is not easy to become familiar with them. So far as I know, none of these has been accepted widely.

Wang then embarks on the development of a system he calls Σ, which he advocates as a basis for formalising mathematics. He calls it “constructive” but this appears to be in the sense of avoiding impredicative definitions rather than banishing the law of excluded middle. So it is a ramified type theory in the sense of Principia Mathematica. I confess to having skipped the sequel at this point; such a formalism is not attractive today.

Nevertheless, I am amazed at how Wang could see so far ahead, writing in the 1950s. He wrote with fluency, clarity and wit, although his native language was Chinese. Such a contrast with that other person, whose gnomic writings on logic offer no insights and don’t appear to be informed by any sort of reflection, knowledge, or even familiarity with the basic concepts of logic.

Wang writing actual code

Wang appears to have been a true polymath, with his knowledge of the history and philosophy of mathematics, technical details of set theory (on which he has written at length) while being at the same time a coder. Programming an IBM 704 could not have been easy. Fortran had been invented by 1960, but Wang does not mention it.³ He almost certainly wrote in assembly language.

Because I have mentioned this work in previous posts (this one and that one), I will resist the temptation to repeat myself and instead refer you to Martin Davis’s chapter in the Handbook of Automated Reasoning entitled “The Early History of Automated Deduction”, which is dedicated to Hao Wang. There you will find many more technical details about Wang’s implementation of Gentzen-style proof calculi and decision procedures for fragments of first-order logic.

In this post, I’ve only been able to touch on a few of Wang’s many contributions. I can’t go into his discussions with Gödel and his communication of Gödel’s philosophical views, for example. Fortunately, much can be found on-line and elsewhere.