这个学派是由德国数学家大卫-希尔伯特（1862-1943）于1910年左右创立的。诚然，人们可以说在十九世纪已经有了形式主义，因为弗雷格在他的《算术原理》（Grundegesetze）第二卷中反对形式主义；《算术原理》第一卷于1893年出版，第二卷于1903年出版。然而，现代形式主义的概念，包括有限推理，必须归功于希尔伯特。由于现代数理逻辑的书籍和课程通常都涉及形式主义，这个学派今天比逻辑主义或直觉主义都要有名。因此，我们将只讨论形式主义的重点，并从以下问题开始： “当我们进行形式化时，我们所形式化的是什么？ ” 

答案是，我们对给定的公理化理论进行形式化。我们应该防止混淆公理化和形式化。欧几里德在公元前300年将几何学公理化，但形式化是在2200年后的逻辑主义者和形式主义者才开始的。公理化理论的例子是，欧几里得公理的平面几何，皮亚若公理的算术，具有九条公理的ZF，等等。下一个问题是: “我们如何将一个给定的公理化理论形式化？ ”

假设给出了某种公理化的理论T，我们考虑一阶逻辑， “把T形式化”意味着为T选择一种适当的一阶语言。一阶语言的词汇由五项组成，其中四项总是相同的，并且不依赖于给定的理论T。这四项是：（1）无数个变量的列表—谁能在谈论数学时不使用变量？(2) 日常语言的连接词，如“非”、“和”、“或”、 “如果，那么”、“当且仅当” --谁能不使用连接词来谈论任何事情？(3) 等价符号=；同样，没有人可以在谈论数学时不使用这个符号。(4) 两个量词，“所有”量词和“存在”量词；第一个量词被用来说诸如“所有复数都有平方根”的事情，第二个量词被用来说诸如“存在无理数”的事情。 人们可以不用上述一些符号，但不必讨论这个问题。相反，我们转向第五项。

由于T是一个公理化的理论，它有所谓的“未定义项”。我们必须为T的每个未定义项选择一个合适的符号，这些符号构成了第五项。例如，在平面欧几里得几何的未定义术语中，出现了“点”、 “线”和“入射”，对于其中的每一个，都必须在一阶语言的词汇表中引入一个适当的符号。在未定义的术语中，出现了“零”、 “加法”和“乘法”，我们为它们选择的符号当然是0、+和*。最容易形式化的理论是ZF，因为这个理论只有一个未定义的术语，即成员关系。当然，我们为这种关系选择了通常的符号。这些符号，在公理化的理论T中每一个未定义项都有一个，通常被称为一阶语言的“参数”，因此参数构成了第五项。

由于参数是一阶语言词汇中唯一取决于给定公理化理论T的符号，人们只需选择这些参数就可以把T形式化。一旦做出这个选择，整个理论T就被完全形式化了。现在，我们不仅可以在所产生的一阶语言L中表达T的所有公理、定义和定理，而且还可以表达更多的东西! 我们还可以在L中表达所有经典逻辑的公理，因此也可以表达所有用来证明T的定理的证明。

但现在第三个问题出现了： “为什么会有人想把一个给定的公理化理论形式化？ ” 毕竟，欧几里德从来不认为有必要把他的公理化的几何学形式化。提出这个问题很重要，因为即使是伟大的皮亚诺也对形式化的真正目的有错误的想法，他用一种形式化的语言（非常类似于一阶语言）发表了他在微分方程方面最重要的发现之一，其结果是没有人读它，直到一些慈善家把文章翻译成普通德语。

现在让我们试着回答第三个问题。如果数学家在某个数学分支做技术研究，比如说欧几里得平面几何，他们感兴趣的是发现和证明这个数学分支的重要定理。对于这种技术性工作，形式化通常不仅没有帮助，反而是一种明显的阻碍。然而，如果人们提出这样的基础性问题，例如：“为什么这个数学分支没有矛盾？ ”，那么形式化就不仅仅是一种帮助，而是一种绝对的必要。

希尔伯特明白形式化是解决这种基础性问题的适当技术，这确实是他的天才之举。他教给我们的东西可以粗略地描述如下。假设T是一个公理化的理论，它被形式化为一阶语言L。这个语言有如此精确的语法，它本身可以作为一个数学对象来研究。例如，我们可以问：“如果我们完全在L的形式上进行，只使用T的公理和经典逻辑的公理，所有这些都在L中表达，我们可能遇到矛盾吗？ ”如果我们能用数学方法证明这个问题的答案是 “no”，那么我们就有了一个数学证明，证明T理论是没有矛盾的!

这基本上就是著名的“希尔伯特计划”的全部内容。其目的是将数学的各个分支形式化，然后从数学上证明其中每一个分支都没有矛盾。事实上，如果通过这种技术，形式主义者能够证明ZF是没有矛盾的，那么他们就已经证明了所有的经典数学都是没有矛盾的，因为经典数学可以用ZF的九个公理来重新进行公理化。简而言之，形式主义者试图创造一种数学技术，通过这种技术可以证明数学是没有矛盾的。这就是形式主义的最初目的。

值得注意的是，逻辑主义和形式主义都将数学的各个分支形式化，但原因完全不同。逻辑主义者想用这种形式化来证明有关的数学分支属于逻辑学；形式主义者则想从数学上证明该分支不存在矛盾。由于这两个学派都“形式化”，他们有时会被混淆。

形式主义者成功地完成了他们的计划吗？没有! 1931年，Kurt Godel在[6]中表明，形式化不能被视为一种数学技术，通过这种技术可以证明数学没有矛盾。那篇论文中的定理为希尔伯特计划敲响了丧钟，它涉及的公理化理论不存在矛盾，其公理足够强大，以至于可以用它们来进行算术。当然，其公理如此强大的理论的例子是Peano算术和ZF。假设T是这样一个理论，并且T已经通过一阶语言L被形式化了。那么哥德尔定理用非技术性语言说： “L中没有任何句子可以被解释为断言T是没有矛盾的，可以在语言L中被正式证明”。尽管对这一定理的解释有些争议，但大多数数学家从中得出的结论是，希尔伯特计划是无法进行的，数学无法证明其自身的无矛盾性。那么，这里就是数学的第三个危机。

当然，形式主义学派对当今数学的巨大重要性是众所周知的。正是在这一学派中，现代数理逻辑及其各种分支，如模型理论、递归理论等，真正进入了盛世。

形式主义和逻辑主义、直觉主义一样，都是建立在哲学上的，但形式主义的哲学根源比其他两个学派的哲学根源要隐蔽一些。不过，人们通过对希尔伯特计划稍作思考就可以找到。

再让T成为一个公理化的理论，该理论已经在一阶语言L中被形式化了。在执行希尔伯特计划时，人们必须谈论L语言中的一个对象，而在这样做的时候，人们并不是在那个安全的语言L本身中说话。相反，人们是在用普通的、日常的语言谈论L，不管是英语、法语还是什么。在使用我们的自然语言而不是正式语言L的时候，当然会有各种危险，即矛盾，事实上，任何种类的错误，都可能溜进去。希尔伯特说，避免这种危险的方法是，当一个人用他的自然语言谈论L的时候，他只使用绝对安全的、没有任何怀疑的推理。他把这样的推理称为“有限推理”，当然，他还必须给它们下一个定义。笔者所知的有限推理的最明确的定义是由法国形式主义者Herbrand给出的，如果我们用“有限推理”代替“直觉的”：

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

请注意，这个定义使用的是哲学语言而不是数学语言，即便如此，如果不了解有限推理的内容，就没有人能够声称理解希尔伯特计划。当形式主义定义有限推理时，形式主义的哲学根源就会暴露无遗。

我们已经把逻辑主义和现实主义，以及直觉主义和概念主义进行了比较。与形式主义相联系的哲学是“唯名主义”，这是一种声称抽象实体不存在的哲学，既不像现实主义所坚持的那样存在于人的头脑之外，也不像概念主义所坚持的那样存在于人的头脑中的精神构造。对于唯名论来说，抽象实体只是发声的话语或书写的线条，仅仅是名字。这就是“唯名论”这个词的由来，因为在拉丁语中，唯名论的意思是“属于一个名字”。同样，当形式主义者试图证明某个公理化的理论T是没有矛盾的，他们并不研究T中出现的抽象实体，而是研究用来形式化T的一阶语言L。也就是说，他们研究如何通过正确使用L的词汇来形成L的句子；如何通过正确使用L的那些被挑出来作为公理的特殊句子来证明其中的某些句子；特别是，他们试图证明L的任何句子都不能同时被证明和反证，因为他们会因此确立原始理论T是没有矛盾的。重要的一点是，对L的整个研究是一种严格的句法研究，因为意义抽象实体与L的句子相关联。对这种语言的研究是通过考虑L的句子是无意义的表达，它们根据明确的句法规则被操纵，就像国际象棋的棋子是无意义的数字，根据游戏规则被推来推去。对严格形式主义者来说， “做数学”就是“根据明确的句法规则来操纵一阶语言的无意义符号”。因此，严格的形式主义者不处理抽象的实体，如无限数列或序数，而只处理它们的无意义的名字，即一阶语言中的适当表达。形式主义和唯名论都避免直接使用抽象实体，这就是为什么形式主义应该与唯名论进行比较的原因。

逻辑主义、直觉主义和形式主义分别对应于现实主义、概念主义和唯名论，这一事实在奎因的文章《论存在的东西》中得到了揭示。

后记

数学中的这三个危机把我们带到了何处？它们没有给我们一个坚实的数学基础。哥德尔的论文于1931年发表后，数学家们集体沮丧地举起了手，转而远离了数学哲学。然而，本文所讨论的三个学派的影响仍然很大，因为它们给我们带来了许多新的和美丽的数学，主要涉及集合论、直觉主义和各种构造主义的修改，以及数理逻辑及其许多分支。然而，尽管这种数学常常被称为“数学基础”，但人们不能因为在这些领域工作就说自己在推动数学哲学的发展。现代数理逻辑、集合论和直觉主义及其修改，如今都是数学的技术分支，就像代数或分析一样，除非我们直接回到数学哲学，否则我们不能指望为我们的科学找到一个坚实的基础。显然，这样的基础对于技术性的数学研究是不需要的，但我们中间仍有一些人渴望得到这样的基础。作者认为，数学基础的关键隐藏在逻辑主义、直觉主义和形式主义的哲学根源中，这就是为什么三次揭开了这些根源。

*****

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 [6] 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 [3].

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.