VI.—ON FORMALIZATION
Hao Wang · Mind · 1955
THE most striking results of formalization occur in logic and mathematics. Here formalization provides at least one kind of systematization. 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. 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. 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. To say that physics uses the experimental method is not to say much about physics. To say that all theorems of mathematics can be proved from certain axioms by chains of syllogism (or modus ponens) is to say just as little about mathematics. Merely knowing the experimental method is not knowing the whole of physics; merely knowing an axiom system adequate for developing mathematics is not knowing the whole of mathematics. There is another kind of systematization which is less superficial than learning the axiom system. It is an intuitive grasp of the whole field, a vivid picture of the whole structure in your mind such as a good chess player would have of the game of chess. This second kind of systematization is something that formalization (or at least formalization alone) would not provide us. If we had never used logistic systems at all, the many interesting results about logistic systems (such as those of Skolem, Herbrand, and G6del') would, of course, never have been expressed in the specific form in which they are now being expressed. But it is not certain that essentially the same