如何证明数学命题？我们有作为起点的有效命题，通常称为“公理”；还有 “推理规则”，规定如何从公理构建其他有效命题；然后这些新命题反过来又可以用于推理规则。维特根斯坦说， “一个在证明链上最后一环的数学命题（。。。）”，一旦被证明，当它具有特别意义时，就可以被称为“定理”。Ladrière写道： “为真的陈述是公理和定理。定理是一个可以从已经证明的公理或定理中推导出来的陈述，通过一连串的中间陈述建立起一个证明。 ”

在欧几里德写下《几何原理》之前，我们当然知道如何证明一个定理，但就我们所掌握的文本而言，是欧几里德将“公理”风格引入了数学，在这里，新的命题，即定理，由公理的语料库，即由不矛盾的论题（这些是假设或简单定义）系统地生成的。所有这些术语在今天仍然以亚里士多德提出的方式发挥着作用。

我用“论题”（thèse）这个术语来指代论证的第一个直接的、无法证明的原则，在获得某些类型的知识时，对它的理解是不必要的。但是，必须获得的，我称之为另一种必须获得的知识，我称之为公理；因为有某些领域是这种类型的，然后我们习惯于更具体地使用这个术语。一个论题中，命题的一部分是假设；也就是说，推断某物存在或不存在的地方，是一个假设；一个论题中没有涉及假设的部分是一个定义。

在柏拉图的《理想国》中，有一段话揭示了首次数学被 "公理化 "时人们对公理的作用的看法："让我们假设这个原则是真实的，然后继续。让我们简单地同意，如果--在以后的阶段--我们改变了对这一原则的看法，我们由于这一原则而得出的所有结论都将失效。

在20世纪初，一些数学家，首先是希尔伯特，希望超越公理化，确保数学完全形式化，即数学完全在非直观符号的基础上发挥作用，然后，在第二阶段，分别用直观的经验现实，如时间、距离、速度、加速度等来 “解释”

这些符号。此项目的基本动机之一是要把数学从某些具有矛盾性质的悖论中解放出来，因为这些悖论在康托尔的集合论中盛行。

希尔伯特写道：“……我想把对真理不可动摇的古老主张还给数学，而这种主张似乎被集合论的悖论夺走了......。 ”(见Ladrière 1992[1957]：5)。希尔伯特自己提出了欧几里得几何学的形式化，原则上，这样就为明确区分数学的语法—只涉及无意义符号的运算—和它的语义—把数学对象作为表示经验现象或机制的模型—奠定了基础。通过推动“形式化”，希尔伯特为数学的“自动”算法的使用铺平了道路，而这将成为机器操作计算的核心，换言之，成为新兴计算机科学的中心。图灵、丘奇、克莱恩将是“可计算性”理论发展的先驱，这个新的专业被称为“可计算性”。

先是弗雷格在十九世纪末，然后，正如我所说，罗素和怀特海一起，在二十世纪初，雄心勃勃地试图为数学提供一个纯粹的逻辑基础。如果说他们的尝试并不完全成功的话，那么，在希尔伯特方面所开创的澄清任务中，还是发挥了重要的作用，尽管其意图不同。如果不是逻辑学的一般原则，还有什么能使证明理论具有一致性？

在一个数学对象中，构成它的不同符号是相互定义的，每个符号都对存在于同一语境中的其他符号能够运作的方式施加某些限制，起到强化、抑制、催化、划定其领域等作用。有些纯粹是被动的，除了反映别人强加给它们的约束外，没有其他力量。具有一定规模的数学对象阐明“原子”元素，这些元素是以一致性（非矛盾）的方式联系在一起的数学命题。

一个数学命题的形成与否合格，也就是说，组成它的符号使用得正确与否，要尊重支配有效公式表达的位置和背景规则。因此，23+13=x是一个有效的公式。就其本身而言，只要它给x分配的值是36，那么它就是真的。 “解释”，即应用，即当给代表变量的符号（如x）赋值时，其真实性取决于x的值，即x所代表的数字：如果x代替36，除了有效之外，公式也是真的。另一方面，23+x-=n不是一个有效的公式：这些符号组成了一个不符合语法的序列。

论证一个公式为真的方法是证明它。因此，公式为真的这一事实取决于它是可以证明的。然而，在(a)与(b)之间存在明显的区别：

(a) 4+5=9

和(b) “命题（a）是可证明的”。

命题(a)为真，相关的为假的命题：

4+5/=9

命题(b)是真的，相关的为假的命题：

“命题(a)是不可证明的”。

因此，产生为真的数学命题是一回事，陈述有关（真的）数学命题的可证性为真的命题是另一回事。在20世纪初，人们习惯于将这种关于数学对象属性的研究称为“元数学”。从那时起，数学家们认为我们在处理两个不同的数学活动领域：数学命题的领域和元数学命题的领域。实际上，把 “4+5=9”称为“命题（a）”这一简单的事实本身就已经是一个元数学的步骤，但数学家在此基础上建立了分界。正如我们将看到的，这里有一个危险。

就其真假而言，数学和元数学是基于不同的原则：前者有自己的验证系统，而后者的验证系统是共同的逻辑。

在数学方面，我可以这样做，比如说：

(a-b)*(a+b)=a^2-b^2

其中变量a和b表示任何实数。为什么？因为将括号内的表达式相乘，除了将产生a和b的平方，还有两个额外的表达式：a*b，正数，+号，b*a，负数，-号。但这些会相互抵消，因为实数的乘法法则是交换性的：我们乘法的顺序是无所谓的：a*b=b*a。所以a*b-b*a=a*b-a*b，a*b-a*b=0。而我们最终得到的是唯一的平方式，a^2-b^2。

公式(a-b)*(a+b)=a^2-b^2的原理，很容易理解，变量a和b代表任何实数。但哥德尔在谈及算术时，不是谈及对数字的运算：他通过罗素和怀特海在《数学原理》中赋予的“逻辑主义”来对待算术。但逻辑学处理符号表示的方式非常不同，在逻辑学中，我们有这样的说法： “（如果）有些a是b ”和 “（如果）所有b是c ”，那么 “（肯定）有些a是c ”。例如， “（如果）有些巴黎人失业了 ”， “（如果）所有失业的人都有金钱方面的烦恼”，那么 “（肯定）有些巴黎人有金钱方面的烦恼 ”。

我已经采取了预防措施，在前提前加了一个“如果”，在结论前加了一个“肯定”。这些总是隐含的，“我们知道”结论的真实性取决于前提的真实性。对于我的数学公式，没有任何类似的假设：我不必写“如果’（a-b）’” »和“如果 ‘（a+b）’ ”，那么’肯定’a^2-b^2’ ”；不：无论是“a-b”还是“a+b”都不需要满足特定的条件，以实现“a^2-b^2”，当然，除了在解释和应用公式时，数字必须介入变量a和b标记的地方这一事实。

换句话说，处理(a-b)*(a+b)=a^2-b^2类型的命题的真值，不可能像处理“有些A是B”和“所有B是C”类型的命题一样，所以“有些A是C”。这是因为，只要a和b是数字，前者就为真，而且a和b的选取值之间不需要先验的特殊关系，即命题(a-b)*(a+b)=a^2-b^2在这种形式下为真。 而像“有些A是B”和“所有B是C”这样的命题，正如我们之前所看到的，只有在A和B之间存在某种先验关系，而B和C之间存在某种先验关系的情况下才是真的。也就是说，为了“有些A是C”， “有些A是B”的事态只有在被解释后才是真实的，也就是说，一旦A和B被直观的数据、类别、表示符号所取代。 Hartmann在这方面提醒我们：(……)我们不要忘记，形式上的严谨性，就其本身而言，完全独立于结论的真实性和虚假性。它只允许我们说，如果前提是真的，结论一定是真的。 « 

也就是说，今天的逻辑学有更广泛的野心：它不再满足于像亚里士多德时代定义从含有“所有…… ”或“某些……”量词的肯定或否定中产生真实结论的条件；它还授权从综合数字和表达真或假的简单知识的中间命题中预测结论的真或假特征。从这个角度来看，逻辑学的目标是一种“元知识”的地位，判断什么是与以前和其他建立的关系中的真和假。算术命题和逻辑命题之间的区别，前者只要“形式良好”并得到证明，就断言为真，后者则从只知道是真的或假的命题集合中陈述有效的推论（而且这种真实性在其他地方已经确定）。当我们开始同时谈论（正如我们将看到在哥德尔第二定理的证明中那样）算术和证明理论时，这些区别就不再明显了，在罗素和怀特海的方法中，这只是逻辑的一个种类。