前言

“逻辑”就是用形式系统来定义语言。自然语言是模糊的，充满二义性的，充满表达上的省略的。逻辑系统是形式化的，有明确的对象和规则的。通过建立自然语言和逻辑系统之间的关系，我们就可以用逻辑来代替自然语言，也即用清晰明确地对象和规则来表达“意义”。

前言

数学的公理化最早可以追溯到欧几里得的《几何原本》，人们认识到很大一部分真理（知识）的发现并不应当是经验的，而是建立在更有限的一小部分经验上的。人们可以规定一小部分“显然为真”的命题称为“公理(axioms)”，并规定一组由命题推导出命题的规则称为“演绎规则(deduction rules)”。这样以后，每个数学断言都会落入这一公理系统当中，要验证其正确性只需找到一个从公理出发的推导过程，称为一个“证明(proof)”。

长久以来，对数学命题的叙述是建立在自然语言之上的。自然语言的模糊性导致了一系列悖论。例如，如果把集合用自然语言定义为“一系列对象的组合”，就会导致罗素悖论：“由全体不属于自身的集合构成的集合是否属于自身？如果它属于自身，那么它不属于自身；如果它不属于自身，那么它属于自身。所以原问题又不为真又不为假”。这里的关键在于集合的定义——由全体不属于自身的集合的组合是否仍能被称为一个集合？又比如，“任何一个自然数都可以用20个中文字描述”，这显然不可能，因为中文字是有限的而自然数是无限的。但是我们可以“证明”确实如此：假设存在不能用20个中文字描述的自然数，那么取其中最小的一个，这个数就是“不能用20个中文字描述的最小自然数”，但是我们已经用17个中文字描述了这个数，矛盾。所以任何一个自然数都可以用20个中文字描述。这里的关键在于，“能用20个中文字描述”是否是一个有意义的数学描述？

关于演绎规则也存在争论。人们当然承认诸如“如果$A$为真，且$A\to B$为真，那么$B$为真”这样的三段论演绎法。但对于一些其它演绎法意见就不那么一致了。例如，当我们要证明某一对象存在时，是否必须举出一个具体的例子，还是只需证明其不存在是不可能的？例如当我们要证明无理数的无理数次方可能是有理数（$\exists z \in \Q,x,y\in \R\setminus \Q,z=x^y$）时，可以给出这样的一个证明：假设\sqrt{2}^\sqrt{2}\in\Q，那么取$x=\sqrt{2},y=\sqrt{2}$，命题得证；假设\sqrt{2}^\sqrt{2}\not\in\Q，那么取x=\sqrt{2}^\sqrt{2},y=\sqrt{2}，有$x^y=\sqrt{2}^{\sqrt{2}\cdot \sqrt{2}}=(\sqrt{2})^2=2$，命题得证；证毕。在以上证明中，我们只是证明了存在这样的$z$，但并不能通过以上证明知道这个$z$具体应当取什么值。该证明能够成立，是因为我们假设了排中律成立：一个命题要么为真要么为假，所以\sqrt{2}^\sqrt{2}\in\Q与\sqrt{2}^\sqrt{2}\not\in\Q中至少有一个为真。有的人觉得排中律不应当被承认，这样的人被称为直觉主义者。

鉴于自然语言的模糊性以及演绎规则的纷争，人们希望能够建立清晰可靠的系统，能够明确定义一切“断言”，明确定义一切“演绎规则”。这样的系统必须建立在一个严格的符号系统上。符号系统又称为“形式系统”或“逻辑系统”。该系统中命题的“语法(syntax)”以及命题到命题的“演绎规则”都要有清晰明确的定义。形式系统只接受特定符号的一些特定的排列，除此之外的符号排列都是“不符合语法的”。

注意，自然语言也是一个符号系统，但是它没有确定的语法。一个看似严重的问题是，对“语法”以及“演绎规则”的描述也只能是基于自然语言的。但实际上，这并没有让我们陷入因果循环，因为形式系统中的语法与演绎规则只是由自然语言得到描述，而并不依赖于自然语言。就好比围棋的规则可以用自然语言描述，但规则本身却是客观的对棋子的操作。任何一个形式系统的语法都需要通过另一种语言描述，这种描述形式系统语法的语言称为“元语言(meta-language)”。所以，形式化的数学系统（数理逻辑系统）其实就是以自然语言为元语言的符号系统。

形式系统的语法与演绎规则只是对符号的客观操作。所以，形式命题或形式证明除了符号的排列本身并不具有通常理解的“意义”。形式符号的意义产生于阅读它的人，也即只有在阅读时形式语言才产生“语义(semantics)”。就好像棋盘上摆放的棋子本身并没有意义，只有我们把它们当作一个游戏时才产生意义。形式语言（一串符号）产生的语义必须由对这串符号的解释(interpret)来确定，这种“解释”所传达的信息和用自然语言书写的数学所传达的信息是一致的。一个好的形式系统应该满足，如果一个推理关系在形式系统中成立，那么该推理经过解释以后在元语言中也是成立的。形式系统这样的性质称为“可靠性(soundness)”。

反之，把数学从自然语言转化到形式语言的过程称为形式化(formalization)。在选取形式系统时，我们必须保证我们有足够能力表达自然语言中出现的命题，表达自然语言中的推导过程。我们应当恰当选择演绎规则，使得形式系统能够把自然语言中“合乎逻辑”的推导都形式化为系统中的演绎规则。这样的性质称为形式系统的“完全性(completeness)”。我们将会看到，人们已经发现一种称为“一阶逻辑”的形式系统，原则上能形式化所有基于集合论的数学。

除了建立形式系统，建立公理系统本身也是困难的。长久以来，对公理的挑选只能是“经验的”。例如，很长一段时间人们无法确定欧几里得的平行公设是否能由其余的公设推出，也即把平行公设从公理中剔除是否会影响我们所能得到的结论。在为集合论建立公理体系时，人们也遇到了类似的问题（是否承认选择公理）。

公理化的发展让人们日益坚信这样一个没有经过仔细检验的假定：在一个精心的设计的公理系统中，任何一个数学命题都可以通过证明或证伪来判定其真假。这符合人的直觉，因为科学的发展使理性主义相较于经验主义获得了巨大成功，对于不显然的断言人们习惯了追问“为什么”而不是简单的接受。其实我们已经意识到，数学的形式系统所需要的语法规则和演绎规则是相当有限的，也即本质不同的规则其实寥寥无几，但我们依旧相信这寥寥无几的规则所形成的庞大系统能够判定一切数学断言。直到哥德尔证明了真理性是比可证性更广的概念，这就是哥德尔不完备性定理。例如，我们能找到一个满足自然数算数的皮亚诺公理的形式系统，却又同时找到了一个关于自然数算数的数学命题，我们可以证明该命题不能被形式系统推出，又可以证明该命题的否定也不能被形式系统推出。这就是“不完备性”（关于这个命题具体是什么，它大概描述的是“该公理系统本身是一致的”，这一描述本身可以被写为该算术系统内部的一个命题）。一个更直观的例子是集合论的ZFC公理体系，人们证明了ZFC公理系统下“连续统假设”既不能证真也不能证伪（我们知道自然数的幂集与实数等势，并且实数的势大于自然数的势。连系统假设的内容是，不存在势的大小介于自然数与实数之间的集合）。直观上，连续统假设是否为真应当是一个客观的事实，所以其不可证应当归因于ZFC系统本身的不完备性——我们是否漏掉了某个显然的事实作为ZFC的公理，或者我们漏掉了某个演绎规则在一阶逻辑的定义中。又或许，既然能够证明连续统假设独立于ZFC公理，它本身就应当作为集合论的一个公理……