计算机领域中的许多问题往往需要用数学模型和方法来解决，而数学的独特的证明方式在其中起着核心的作用。
简单来说，证明是一种建立事实的方法。然而，就像“美丽”这个词一样，“事实”有时候也是因人而异的：在法官眼中，事实得由证据来决定；在商界，事实可能由一个可信赖的人或是组织或仅仅是你的 boss 指定；在物理或是生物领域，事实由实验来确定；在哲学中，事实如“我思故我在”这句名言般缥缈。
当然，数学有它自己对于证明的定义。
数学意义上的证明
数学上证明是从一组基本的公理出发，通过一系列逻辑推理最终得到待证明的命题。
这个定义由三个核心组成，分别是命题、逻辑推理和公理。本文先介绍命题。其余两个后续文章会继续介绍。
命题
生活中我们也常常会提到命题这个词，命题实际上就是一个陈述语句，只不过命题这个陈述语句要么是对的，要么是错的。如果一个陈述语句无法判断对错，那么就不是命题。比如，“你喜欢数学吗？”这句话就不是命题。
下面是两个命题：
命题1： 2 + 3 = 5
命题2： 1 + 1 = 3
复合命题
单个命题比较简单，如果把多个命题通过“非”， “与”， “或”， “如果-那么”等词连接起来就成了复合命题。下面的命题就是由三个命题P、Q和R组合而成的：
如果 P 与 Q， 那么 R
如果已知单个命题的真假、根据不同的连接词就可以得出复合命题的真假。下面用真值表来表达。
“非”, “与”, 和“或”
| P | 非 P |
|---|---|
| T | F |
| F | T |
| P | Q | P 与 Q |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | F |
| F | F | F |
从上表可以看出，命题 “P 与 Q” 仅当 P 和 Q 都是真时才为真。
| P | Q | P 或 Q |
|---|---|---|
| T | T | T |
| T | F | T |
| F | T | T |
| F | F | F |
命题 “P 或 Q” 只要 P 和 Q 有一个为真就为真。而如果想排除掉 P 和 Q 共同为真的情况，可以使用 异或 连接词：
| P | Q | P 异或 Q |
|---|---|---|
| T | T | T |
| T | F | T |
| F | T | T |
| F | F | F |
“如果-那么”
前面三个连接词比较容易理解，而“如果-那么”则不太容易理解。先看真值表
| P | Q | 如果 P 那么 Q |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
我们用一个具体点的命题来验证上面的结论：
如果黎曼猜想是对的，那么对于每个实数 $x$，都有 $x^2 \geq 0$
黎曼猜想是一个著名的未解问题，因此命题 P 的真假未知，但是这并不妨碍我们判定上面这个命题是真的。也就是说，无论 P 是真的还是假的，上述命题都是真的。
有点不可思议？那我们再来看一个更极端的例子：
如果猪可以飞，那么你可以理解切比雪夫不等式
实际上，你可不可以理解切比雪夫不等式和猪可不可以飞没有半毛钱关系！不管猪可不可以飞，这个命题都是真的。
总之，命题“如果 P 那么 Q”是真的情况有两种，要么Q是真的，要么P是假的。
当且仅当
这个比较容易理解，“P 当且仅当 Q” 即意味着P和Q是等价的。
下面是一个例子：
$$x^2 - 4 \geq 0 \quad 当且仅当\quad |x| \geq 2$$
| P | Q | P 当且仅当 Q |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | F |
| F | F | T |
数学符号
在数学中，往往用符号替换英语，上述的几种连接词可以用下面的符号表示：
| 英语 | 符号 |
|---|---|
| 非 P | $\lnot{P}$ |
| P 与 Q | $P\land{Q}$ |
| P 或 Q | $P\lor{Q}$ |
| 如果 P 那么 Q | $P\implies{Q}$ |
| P 当且仅当 Q | $P\iff{Q}$ |
逻辑上相等的命题
实际上，与命题 “如果 P 那么 Q” 相等的命题是“如果非 P 那么非 Q”。这两个命题有着相同的真值表。
注意 “如果 P 那么 Q” 与 “如果 Q 那么 P” 并不相等。只有当 “P 当且仅当 Q” 为真时二者才相等。
计算机程序中的命题逻辑
了解了上述的复合命题的判定方法，很容易知道下面这两行程序表述的命题是相等的，而有时候我们可能会写成第一行的样子，导致程序运行时间和程序代码变长。
if (x > 0 || (x <= 0 && y > 100)) |
if (x > 0 || y > 100) |
断言和量词
之前我们谈到的命题都是直观上很容易判断真假的命题，然而，有些命题可能会涉及无穷的数导致要判断真假得检查无穷的情况。比如下面这个命题：
对于每个非负整数 n，$n^2 + n + 41$是质数
实际上，上述的涉及无穷的数的命题在数学上十分常见，以至于有特定的符号来描述，上面的命题也可以写成下面的形式：
$$\forall n \in N. n^2 + n + 41 是质数$$
下面是另一个例子：
$$\forall a,b,c,d \in Z^+. a^4 + b^ 4 + c^4 \neq d^4.$$
这种真假依赖于检查多个变量的命题称为断言。断言常常和一些量词一起出现，比如描述这个断言是针所有情况都为真还是针对某些情况为真。比如，下面这个断言：
$$x^2 \geq 0$$
对任何实数x都为真。而下面这个断言：
$$5x^2 - 7 = 0$$
则仅当$x = \pm\sqrt{7/5}$才成立
用数学符号来描述某些情况成立的例子如下：
$$\exists x \in D \quad P(x)$$
表示在集合 D 中存在 x，满足 P(x)
证明的模式
证明的方法包括：
- 公理法
- 穷举法
- 反证法
- 数学归纳法