Google 翻译生成的粗略草稿，质量较低。术语依照术语表，但句子可能有误；之后会由仔细的译文取代。
简介
自希腊时代起，数学就涉及证明；有些人甚至怀疑，按照希腊人赋予字的精确而严格的意义，证明是否可以在数学之外找到。我们可以公平地说，这并没有改变，因为构成欧几里得的证明对我们来说仍然是证明；当这个概念面临被遗忘的危险，数学本身也受到威胁时，人们又转向希腊人寻求证明的模型。但在过去的一百年中，通过重要的收购，这一古老的遗产不断扩大。
通过在适当选择的数学文本中证明机制的数学分析，可以辨别词汇和语法背后的结构。这个数学分析得出的结论是，足够明确的数学文本可以用传统语言包含表达，只需一小部分数固定的“字”，根据一小部分数不可打破规则的语法由……组成组装：这样的文本被称为“形式化”。国际象棋游戏的描述，通常的对数记号和表，是形式化文本的例。如果括号的使用规则被完全编纂并严格遵守，普通代数计算的公式将是另一个例；实际上，其中一些规则从未明确规定，并且允许对它们进行某些减损。
形式化文本的验证或多或少是一个机械过程，唯一可能的错误原因是长度或文本的复杂性：这就是为什么数学家通常会充满信心地接受另一个执行的代数计算的结果，只要他知道计算不会太长并且已经小心完成。另一方面，在非形式化的文本中，人们会面临因例错误使用直觉或类比论证而产生错误推理的危险。在实践中，希望满足自己拥有证明或理论的完美正确性或“严谨性”的数学家几乎不会求助于当今可用的完整形式化中的一个或另一个，甚至通常也不会求助于代数和其他微积分提供的不完整和部分形式化。总的来说，他很乐意将阐述带到点，他的经验和数学天赋告诉他，翻译成正式语言最多需要习题的耐心（虽然无疑是一个非常乏味的耐心）。如果，正如一次又一次发生的那样，对所考虑的文本的正确性产生怀疑，他们最终关心的是将其明确地翻译成这样一种形式化语言的可能性：要么因为根据上下文不同的含义使用了相同的字，要么因为无意识地使用了他们没有明确授权的论证模式而违反了句法规则，或者再次因为犯了重大错误。除了最后一种可能性之外，纠正的过程迟早总是包含在构造越来越接近形式化文本的文本中，直到数学家普遍认为朝这个方向走得更远是多余的。在其他字中，数学文本的正确性是通过或多或少明确地与形式化语言的规则进行比较来验证的。
严格来说，公理化的方法只不过是一种起草文本的艺术，其形式化在原理中是简单明了的。因此，它并不是一项新发明。但它作为发现工具的系统使用是当代数学的原始特征之一。就阅读或书写形式化文本而言，字或文本中的符号是否具有这种或那种含义，或者实际上它们是否具有任何含义，都无关紧要；唯一重要的点是正确遵守语法规则。因此，众所周知，相同的代数计算可用于求解关于磅权或英镑的问题，关于抛物线或重力下的运动。同样的优势也适用于根据公理方法编写的每一篇文本，并且出于同样的原因：一旦建立了一般拓扑的定理，它们就可以随意应用于普通空间、希尔伯特空间等。这种能够赋予字或理论的主要概念不同含义的能力确实是丰富数学家直觉的重要来源，这种直觉不一定是空间或感官的，如有时所相信的那样，而是对数学对象的行为的某种感觉，经常得到来自各种来源的像的帮助，但首先是建立在日常经验的基础上。因此，人们经常被引导去有益地研究理论的那些部分，这些理论传统上在该理论中被忽略，但在一般公理化背景下系统地研究，给定的理论是其中的一个特例（对于例，其历史起源于一般理论的另一个专业化）。此外，这正是我们在这卷级数中最关心的问题 – 当我们关心复杂的数学对象时，公理化方法允许我们分离它们的属性，并围绕一小部分概念数重新组合它们：也就是说，使用字稍后将收到精确的定义，根据定义对它们进行分类到*结构*，他们属于。 （当然，相同的结构可以与各种不同的数学对象联系起来。）对于例，球体的一些属性是拓扑的，其他属性是代数的，其他属性又可以被视为微分几何或李群理论的属于。尽管当应用于紧密交织的结构时，这个原理有时可能会变得有些人为，但它是这个级数主题的书籍划分的基。
¶ 正如正确地说语言的艺术先于语法的发明一样，公理化的方法在形式化语言的发明之前就已经被实践了很长时间之前；但它的有意识的实践只能依赖于控制这些语言的一般知识原理及其与当前数学文本的关系。在本书中，我们的第一个目标是描述这样一种语言，并阐述可应用于许多其他类似语言的一般原理；然而，这些语言中的一种总是足以满足我们的目的。因为在过去，人们认为数学的每个分支都依赖于其自身特定的直觉，这些直觉提供了其概念和基本真理，而如今，从逻辑上讲，人们知道实际上可以从单一来源集合论推导出整个已知数学。因此，对于我们的目的来说，描述单一形式化语言的原理，指示如何用这种语言编写集合论，然后展示我们在这个级数中关注的数学的各个分支如何适应这个框架就足够了。我们这样做并不是声称要永远立法。未来的某个日期，数学家可能会同意使用推理的模式，其中不能在此描述的语言中形式化：那么，即使不是完全变换语言，至少也有必要扩大其语法规则。但这是由未来决定的。
形式化语言的描述不需要说，它是用普通语言制定的，就像国际象棋的规则一样。 我们不建议讨论心理和形而上学的问题，它是在这种情况下使用普通语言的基础（对于例，认识到字母表中的字母在页面上的两个不同位置是“相同”的可能性，等等）。 此外，不使用计数几乎不可能完成这样的描述。 有人反对说，在这种情况下使用数是可疑的，甚至等同于*petitio principii*。 然而，很明显，事实上我们只是使用数作为标记（并且我们可以通过其他符号来替换它们，例如颜色或字母），并且当我们数出现在明确书写的公式中的符号时，我们没有使用任何数学推理。 我们不会讨论向智力发展尚未达到能够读、写、算的阶段的人教授形式化语言原理的问题。
如果形式化数学像国际象棋一样简单，那么一旦我们选择的形式化语言被描述，剩下的任务就只剩下用这种语言写出我们的证明的任务了，就像国际象棋手册的作者在他的记号中写下他打算教授的游戏，并在必要时附上评论一样。但事情远没有那么简单，不需要任何丰富的经验就可以看出这样一个项目是绝对不可能实现的：集合论开头的最小的证明已经需要数百个符号才能完全形式化。因此，从级数的第I开始，必须通过引入相当大的数新字（称为*缩写符号*）和附加语法规则（称为*演绎判据*）来压缩形式化文本。通过这样做，我们获得了比严格意义上的形式化语言更易于管理的语言。任何数学家都会同意，这些压缩语言可以被视为仅仅是原始形式化语言的速记转录。但我们不再确定从这些语言中的一种到另一个可以纯粹机械的方式进行：因为为了实现这种确定性，有必要将控制新规则使用的语法规则复杂化到点，以至于它们的用处变得虚幻；正如在代数计算以及数学家常用的几乎所有形式或记号中一样，可用的工具比理论上更完美但实际上更麻烦的工具更可取。
正如读者将看到的，这种压缩语言的引入伴随着特定型的“论证”，其中属于就是所谓的*元数学*。该学科完全忽略了最初可能归因于字或形式化数学文本短语的任何含义，并将这些文本视为特别简单的对象，即先前给出的对象的组合，其中只有指定的序是重要的。此外，正如化学教科书提前宣布在给定条件下进行的实验结果一样，例一样，元数学“论证”通常断言，当对给定型的文本执行一系列运算时，最终文本将是给定型的另一个。在最简单的情况下，断言确实是最纯粹的真理（对于例来说，可与以下内容相比：“如果一袋计数器包含黑色计数器和白色计数器，并且如果我们将替换所有黑色计数器都放在白色计数器上，那么袋子中将只有白色计数器”）。但很快我们就遇到了例，其中论证发生了典型的数学转向，其中任意整数和数学归纳的使用占主导地位。尽管我们已经反驳了之前在形式化语言的描述中使用计数的反对意见，但在这个点不再可能否认回避问题的危险，因为从一开始我们似乎就在利用算术的所有资源，我们稍后建议为这些资源（除其他外）奠定基础。对于这个反对意见，回答是有时，这个型的论点仅仅描述了可以实际执行和验证的运算，因此从可以被赋予数学本身的东西中得出另一个序的信念。但似乎更简单地说，如果明确写出形式化文本，我们“可以”避免所有这些元数学论证：我们不应该使用“演绎判据”，而应该每次重新开始运算的序列，而判据的目的是通过预测其结果来缩写。但形式化数学不能在实践中被完整地写下来，因此我们必须对所谓的数学家的公共的感抱有信心：类似于计算器或工程师对公式或数字表的信心，而无需意识到皮亚诺公理的存在，并且最终基于其从未被矛盾的知识事实证明。
因此，我们很快就会放弃形式化数学，但不会之前，我们已经仔细地追踪了回到它的路径。由此引入的第一个“语言滥用”将使我们能够以与所有数学文本在实践中编写相同的方式来编写级数的其余部分（特别是本书I的结果摘要），也就是说部分用普通语言，部分用公式构成部分，特殊和不完整的形式化，其中最著名的例是公式代数计算。 有时我们将更加宽松地使用普通语言，通过自愿滥用语言，通过纯粹而简单的省略段落（读者可以放心地认为自己能够轻松地恢复），以及通过将不能翻译成形式化语言并旨在帮助读者重建完整文本的指示。其他同样无法翻译成形式化语言的段落在序中被引入，以澄清所涉及的想法，如有必要，可以诉诸读者的直觉；只要文本正式化的可能性保持不变，这种修辞资源的使用是完全合法的。其中第一个例将出现在本书的章III中，描述了整数和基数数的理论。
因而，根据公理方法编写，并始终考虑到完全形式化的可能性，我们的级数声称具有完美的严谨性：这一主张与前面的考虑一点也不相矛盾，也与纠正不时滑入文本中的错误的需要相矛盾。
¶ 我们对一致性（或不矛盾）问题采取同样现实的态度。这个问题一直是现代逻辑学家关注的主要问题之一，并且在一定程度上促成了形式化语言的创建（cf.历史注记）。如果定理及其否定都在理论中得到证明，则称该数学理论是矛盾的；从推理的通常规则（即形式化语言语法规则的基）可以看出，每个定理在理论中既是真又是假，因此该理论毫无意义。因而，如果我们不由自主地陷入矛盾，我们不能允许它继续存在，而不会使它发生的理论变得徒劳。
我们能确定这永远不会发生吗？ Without entering into a discussion — which is outside our competence — of the very notion of certainty, we may observe that metamathematics can set itself the task of examining the problems of consistency by its own methods. 说一个理论是矛盾的，实际上意味着它包含是正确的形式化证明，从而得出结论。 现在元数学可以尝试借用数学中的推理的方法来研究这样一个形式化文本的结构，希望“证明”这样一个文本不能存在。 事实上，某些部分形式化语言已经给出了这样的“证明”，这些语言不如我们建议引入的语言丰富，但足以表达经典数学的良好部分。 我们当然可以合理地问，实际上已经以这种方式“证明”了什么：因为，如果数学是矛盾的，那么它对材料对象，特别是形式化文本的某些应用将面临虚幻的危险。 为了摆脱这种困境，形式化语言的一致性必须通过论证来“证明”，而这些论证可以用一种不那么丰富、因此更值得信任的语言来形式化；但是，哥德尔的著名元数学定理断言，这对于我们将要描述的型语言来说是不可能的，它的公理足够丰富，可以表述经典算术的结果。
另一方面，在“相对”一致性的证明中（也就是说，在假设其他一些理论（对于例集合理论来说，是不矛盾的）的假设下建立理论的一致性），论证的元数学部分（cf.章I, § 2, no. 4）非常简单，似乎很难在不放弃对我们智力的所有合理运用的情况下否认这一点。由于各种数学理论现在在逻辑上都依附于集合论，因而，这些理论中的一个或另一个遇到的任何矛盾必然会引起集合论本身的矛盾。当然，这并不是我们可以推断集合论一致性的论点。然而，自该理论的公理首次精确表述以来的半个世纪中，这些公理已被应用于数学最多样化的分支中得出结论，而没有导致矛盾，因此我们有理由希望永远不会出现矛盾。
如果结果相反，则观察到的矛盾是集合论的基本原理所固有的；因而，如果可能的话，在不影响我们最希望保留的那些数学的部分的情况下，需要对这些原理进行修改，并且很明显，通过使用公理方法和形式化语言，修改任务将变得更容易，这使我们能够更精确地制定这些原理，并更清楚地分离出它们的推论。事实上，这或多或少是最近发生的事情，当集合论的“悖论”通过采用基本上等同于我们将在这里描述的形式化语言而消除时；如果这种语言本身被证明是矛盾的，则必须进行类似的修改。
至和向上，我们相信数学注定要生存下去，这座宏伟大厦的本质部分永远不会因为矛盾的突然出现而倒塌；但我们不能假装这个观点不仅仅基于经验。有人会说，这只是小小的安慰；但两千五百年来，数学家一直在纠正他们的错误，从而丰富而不是削弱了他们的科学。这让他们有权利平静地面对未来。