# 数学中的三个危机 ：逻辑主义、直觉主义和形式主义 - 译文（3）：形式主义

- 我们所理解的有限论证是指满足以下条件的论证：在这个论证中，我们只考虑给定的有限数量的对象和函数；这些函数是定义明确的，它们的定义允许以一种单一的方式计算它们的值；我们从不说明一个对象的存在而不给出构建它的方法；我们从不考虑无限集合的所有对象x的全体；当我们说一个论证（或一个定理）对所有这些x都是真实的，我们的意思是，对于每个x本身，有可能重复有关的一般论证，这应该被视为只是这些特殊论证的原型。

*****

Formalism

This school was created in about 1910 by the German mathematician David Hilbert (1862-1943). True, one might say that there were already formalists in the nineteenth century since Frege argued against them in the second volume of his Grundegesetze der Arithmetic; the first volume of Grundegesetze appeared in 1893 and the second one in 1903. Nevertheless, the modern concept of formalism, which includes finitary reasoning, must be credited to Hilbert. Since modern books and courses in mathematical logic usually deal with formalism, this school is much better known today than either logicism or intuitionism. We will hence discuss only the highlights of formalism and begin by asking, what is it that we formalize when we formalize something ? »

The answer is that we formalize some given axiomatized theory. One should guard against confusing axiomatization and formalization. Euclid axiomatized geometry in about 300 B.C., but formalization started only about 2200 years later with the logicists and formalists. Examples of axiomatized theories are Euclidean plane geometry with the usual Euclidean axioms, arithmetic with the Peano axioms, ZF with its nine axioms, etc. The next question is : « How do we formalize a given axiomatized theory ? »

Suppose then that some axiomatized theory T is given. Restricting ourselves to first order logic, « to formalize T » means to choose an appropriate first order language for T. The vocabulary of a first order language consists of five items, four of which are always the same and are not dependent on the given theory T. These four items are the following : (1) A list of denumerably many variables - who can talk about mathematics without using variables ? (2) Symbols for the connectives of everyday speech, say for « not », for « and », for the inclusive « or », for « if then », and for « if and only if » - who can talk about anything at all without using connectives ? (3) The equality sign =; again, no one can talk about mathematics without using this sign. (4) The two quantifiers, the « for all » quantified and the « there exist » quantifier ; the first one is used to say such things as « all complex numbers have a square root », the second one to say things like « there exist irrational numbers » One can do without some of the above symbols, but there is no reason to go into that. Instead, we turn to the fifth item.

Since T is an axiomatized theory, it has so called « undefined terms ». One has to choose an appropriate symbol for every undefined term of T and these symbols make up the fifth item. For instance, among the undefined terms of plane Euclidean geometry, occur « point », « line », and « incidence », and for each one of them an appropriate symbol must be entered into the vocabulary of the first order language. Among the undefined terms od arithmetic occur « zero », « addition », and « multiplication », and the symbols one chooses for them are of course 0, +, and *, respectively. The easiest theory of all to formalize is ZF since this theory has only one undefined term, namely, the membership relation. One chooses, of course, the usual symbol for that relation. These symbols, one for each undefined term of the axiomatized theory T, are often called the »parameters » of the first order language and hence the parameters make up the fifth item.

Since the parameters are the only symbols in the vocabulary of a first order language which depend on the given axiomatized theory T, one formalizes T simply by choosing these parameters. Once this choice has been made, the whole theory T has been completely formalized. One can now express in the resulting first order language L not only all axioms, definition, and theorems of T, but more ! One can also express in L all axioms of classical logic and, consequently, also all proofs one uses to prove theorems of T. In short, one can now proceed entirely within L, that is, entirely « formally ».

But now a third question presents itself : « Why in the world would anyone want to formalize a given axiomatized theory ? » After all, Euclid never saw a need to formalize his axiomatized geometry. It is important to ask this question, since even the great Peano has mistaken ideas about the real purpose of formalization. He published one of his most important discoveries in differential equations in a formalized language (very similar to a first order language) with the result that nobody read it until some charitable soul translated the article into common German.

Let us now try to answer the third question. If mathematicians do technical research in a certain branch of mathematics, says plane Euclidean geometry, they are interested in discovering and proving the important theorems of the branch of mathematics. For that kind of technical work, formalization is usually not only no help but a definite hindrance. If, however, one asks such foundational questions was, for instance, « Why is this branch of mathematics free of contradictions ? » , then formalization is not just a help but an absolute necessity.

It was really Hilbert’s stroke of genius to understand that formalization is the proper technique to tackle such foundational questions. What he taught us can be put roughly as follows. Suppose that T is an axiomatized theory which has been formalized in terms of the first order language L. This language has such a precise syntax that it itself can be studied as a mathematical object. One can ask for instance : « Can one possibly run into contradictions if one proceeds entirely formally within L, using only the axioms of T and those of classical logic, all of which have been expressed in L? » If one can prove mathematically that the answer to this question is « no »n one has there a mathematical proof that the theory T is free of contradictions !

This is basically what the famous « Hilbert program » was all about. The idea was to formalize the various branches of mathematics and then to prove mathematically that each one of them is free of contradictions. In fact if, by means of this technique, the formalists could have just shown that ZF is free of contradictions, they would thereby already have shown that all of classical mathematics is free of contradictions, since classical mathematics can redone axiomatically in terms of the nine axioms of ZF. In short, the formalists tried to create a mathematical technique by means of which one could prove that mathematics is free of contradictions. This was the original purpose of formalism.

It is interesting to observe that both logicists and formalists formalized the various branches of mathematics, but for entirely different reasons. The logistics wanted to use such a formalization to show that the branch of mathematics in question belongs to logic; the formalists wanted to use it to prove mathematically that the branch is free of contradictions. Since both schools « formalized », they are sometimes confused.

Did the formalists complete their program successfully ? No! In 1931, Kurt Godel showed in  that formalization cannot be considered as a mathematical technique by means of which one can prove that mathematics id free of contradictions. The theorem in that paper which rang the death bell for the Hilbert program concerns axiomatized theories which are feee of contradictions and whose axioms are strong enough so that arithmetic can be done in terms of them. Examples of theories whose axioms are that strong are, of course, Peano arithmetic and ZF. Suppose now that T is such a theory and that T has been formalized by means of the first order language L. Then Godel’s theorem says, in nontechnical language, « No sentence of L which can be interpreted as asserting that T is free of contradictions can be proven formally within the language L ». Although the interpretation of this theorem is somewhat controversial, most mathematicians have concluded from it that the Hilbert program cannot be carried out : Mathematics is not able to prove its own freedom of contradictions. Here, then, is the third crisis in mathematics.

Of course, the tremendous importance of the formalist school for present-day mathematics is well known. It was in this school that modern mathematical logic and its various offshoots, such as model theory, recursive ruction theory, etc., really came into bloom.

Formalism, as logicism and intuitionism, is founded in philosophy, but the philosophical roots of formalism are somewhat more hidden than those of the other two schools. One can find then, though, by reflecting a little on the Hilbert program.

Let again T be an axiomatized theory which had been formalized in terms of the first order language L. In carrying out Hilbert’s program, one has to talk about there language L as one object, and while doing this, one is not talking within that safe language L itself. On the contrary, one is talking about L in ordinary, everyday language, be it English or French or what have you. While using our natural language and not formal language L, there is of course every danger that contradictions, in fact, any kind of error, may slip in. Hilbert said that the way to avoid this danger is by making absolutely certain that, while one is talking in one’s natural language about L, one uses only reasonings which are absolutely safe and beyond and kind of suspicion. He called such reasonings « finitely reasonings », but had, of course, to give a definition of them. The most explicit definition of finitely reasoning known to the author was given by the French formalist Herbrand. It says, if we replace « intuitionistic » by « finitary » :

By a finitary argument we understand an argument satisfying the following condition : In it we never consider anything but a given finite number of objects and of functions; these functions are well defined, their definition allowing the computation of their values in a univocal way; we never state that an object exists without giving the means of constructing it; we never consider the totality of all the objects x odd an infinite collection; and when we say that an argument (or a theorem) is true for all these x, we mean that, for each x taken by itself, it is possible to repeat the general argument in question, which should be considered to be merely the prototype of these particular arguments.

Observe that this definition uses philosophical and not mathematical language. Even so, no one can claim to understand the Hilbert program without an understanding of what finitely reasoning amounts to. The philosophical roots of formalism come out into the open when the formalism define what they mean by finitely reasoning.

We have already compared logicism with realism, and intuitionism with conceptualism. The philosophy which is closed to formalism is « nominalism ». This is the philosophy which claims that abstract entities have no existence of any kind, neither outside the human mind as maintained by realism, nor as mental constructions within the human mind as maintained by conceptualism. For nominalism, abstract entities are mere vocal utterances or written lines, mere names. This is where the word « nominalism » comes from, since in Latin nominals means « belonging to a name ». Similarly, when formalists try to prove that a certain axiomatized theory T is free of contradictions, they do not study the abstract entities which occur in T but, instead, study that first order language L which was used to formalize T. That is, they study how one can form sentences in L by the proper use of the vocabulary of L; how certain of these sentences can be proven by the proper use of those special sentences of L which were singled out as axioms; and, in particular, they try to show that no sentence of L cane proven and disprove at the same time, since they would thereby have established that the original theory T is free of contradictions. The important point is that this whole study of L isa strictly syntactical study, since meanings abstract entities are associated with the sentence of L. This language is investigated by considering the sentences of L was meaningless expressions which are manipulated according to explicit, syntactical rules, just as the pieces of a chess game are meaningless figures which are pushed around according to the rules if the game. For the strict formalist « to do mathematics » is « to manipulate the meaningless symbols of a first order language according to explicit, syntactical rules » . Hence, the strict formalist does not work with abstract entities, such as infinite series or cardinals, but only with their meaningless names which are the appropriate expressions in a first order language. Both formalists and nominalists avoid the direct use of abstract entities, and this why formalism should be compared with nominalism.

The fact that logicism, intuitionism and formalism correspond to realism, conceptualism and nominalism, respectively, was brought to light in Quine’s article, « On what There Is ». Formalisme can be learned from any modern book in mathematical logic, for instance .

Epilogue

Where do the three crisis in mathematics leave us ? They leave us without a firm foundation for mathematics. After Godel’s paper appeared in 1931, mathematicians on the whole threw up their hands in frustration and turned away from the philosophy of mathematics. Nevertheless, the influence of the three schools discussed in this article has remained strong, since they have given us much new and beautiful mathematics. This mathematics concerns mainly set theory, intuitionism and its various constructivist modifications, and mathematical logic with its many offshoots. However, although this kind of mathematics often referred to as « foundations of mathematics », one cannot claim to be advancing the philosophy of mathematics just because one is working in one of these areas. Modern mathematical logic, set theory, and intuitionism with its modifications are nowadays technical branches of mathematics, just as algebra or analysis, and unless we return directly to the philosophy of mathematics, we cannot expect to find a firm foundation for our science. It is evident that such a foundation is not necessary for technical mathematical research, but there are still those among us who yearn for it. The author believes that the key to the foundations of mathematics lies hidden somewhere among the philosophical roots of logicism, intuitionism and formalism and this is why has his uncovered these roots, three times over.

https://m.sciencenet.cn/blog-2322490-1292240.html

## 全部精选博文导读

GMT+8, 2023-6-7 14:42