翻译：《计算机科学与数学》 前言

本文阐述如何使用数学模型和方法分析在计算机科学中产生的问题。证明在本文中扮演了核心角色，因为作者们和大多数学家共享一个信念，即证明对于真正的理解是最重要的。证明也在计算机科学中扮演了一个不断成长的角色；证明被用来验证软硬件的正确运行，这是再多的测试也无法做到的事情。

简而言之，证明是一种建立真相的方法。就像美貌一样，“真相”取决于旁观者的眼睛，并且不会令人惊讶的是在不同领域证明的构成不同。在司法系统中，法律真相是由陪审团基于在审判中允许呈现的证据决定的。在商业世界中，权威的真相是由值得信赖的个人或者组织定义的，或者可能就是你的老板。在物理学或者生物学领域，科学的真相是通过实验确认的(1)。在统计学领域，可能性的真相建立在对样本数据的统计分析上。

哲学的证明涉及到一丝不苟的阐述和典型地基于一系列细微的、模棱两可的观点的说服。最好的例子是“我思故我在”，一个拉丁句子被翻译成“我思考，因此我存在”。该短语源自于数学家、哲学家笛卡尔17世纪的一篇文章，它是世界上最著名的引用之一：在网上搜索一下，你会被搜索结果淹没。

从自己正在思考自己的存在的事实推断自己的存在是非常酷和有说服力的想法。然而，只要沿着这种思路多讨论一下，笛卡尔就得出了存在无限仁慈上帝的结论。无论你是否相信无限仁慈的上帝，你也可能赞同任何关于上帝无限仁慈的简短证明都是遥不可及的。因此，就算经由大师之手，这种结论也是不可信的。

定义

一个命题的数学证明是一系列由一组基本的公理引出的逻辑推论。

三个关键点在该定义中被强调：命题、逻辑推论、公理。第一章通过一些组织证明的基本方式检验这三点。第二章介绍了良序原理，一种基本的证明方法。第五章介绍了与归纳法密切相关的证明方法。

如果你要证明一个命题，那么最好精准地理解命题的意思。为了避免日常用语的歧义和不准确的定义，数学家们非常精确地使用语言，他们通常使用逻辑表达式表达命题；逻辑表达式是第三章的主题。

前三章假定读者熟悉一些类似集合、函数的数学概念。第四章和第八章更详细地介绍与数学相关的数据类型，检验无穷集证明事物的特殊性质和方法。第7章继续研究递归定义的数据类型。

(1)事实上，只有科学的失败才可以被实验解释——当实验和预期的表现不一样。但是再多的实验也无法保证下个实验不会失败。因此，科学家们几乎不讨论真理，而是可以精准预测过去的理论、可预测的未来、实验。

阅读原文