反证法 · aiwiki.page

反证法是一种数学证明方法：暂时假定待证命题的否定成立，并证明这一假设会导致矛盾。在经典逻辑中，这就确立了原命题。该方法广泛用于数学和形式逻辑学，也常被称为“归谬法”（reductio ad absurdum）或“间接证明法”。不过，这些名称也可以指更广泛的推理形式，即通过不可能的后果来否定某个假设。(forallx.openlogicproject.org)

逻辑结构

设 $P$ 为待证命题， $\Gamma$ 表示已接受的前提，例如公理、定义和此前已确立的结果。论证具有以下结构：

暂时假定 $\neg P$ 。
对 $\Gamma$ 和这一假设应用有效的推理规则。
推导出矛盾，以 $\bot$ 表示。
撤销假设 $\neg P$ ，得出 $P$ 。

在自然演绎中，这一经典逻辑规则可以表示为

\frac{\Gamma,\neg P\vdash\bot}{\Gamma\vdash P}.

这里， $\vdash$ 表示“可由左侧推导出右侧”。撤销一个假设，意味着最终结论不再依赖该临时假设，但仍可能依赖 $\Gamma$ 中的前提。(forallx.openlogicproject.org)

矛盾可以是某个命题 $Q$ 与其否定 $\neg Q$ 同时成立，也可以是在通常的算术假设下出现 $0=1$ 这样的不可能情形。矛盾不必直接涉及 $P$ ：只要在论证中推导出真正的矛盾即可。仅仅得到出乎意料或看似不可信的后果，并不构成逻辑矛盾。(forallx.openlogicproject.org)

否定与相关证明方法

正确地否定待证命题至关重要。对于条件形式的定理 $A\rightarrow B$ ，其在经典逻辑中的否定是 $A\land\neg B$ 。因此，反证法同时假定条件成立而结论不成立。对于全称量化命题 $\forall x\,R(x)$ ，其否定是 $\exists x\,\neg R(x)$ ，即存在一个反例。存在性命题的否定为 $\neg\exists x\,R(x)$ ，等价于 $\forall x\,\neg R(x)$ 。这些区别将反证法与一阶逻辑联系起来。(web.stanford.edu)

利用逆否命题进行证明的方法与反证法有关，但两者并不相同。要证明 $A\rightarrow B$ ，逆否证明法会证明 $\neg B\rightarrow\neg A$ ；反证法则假定 $A\land\neg B$ ，并推导出不可能的情形。有些论证可以用这两种方式中的任一种来表述，但它们所陈述的目标和采用的临时假设不同。直接证明则从条件出发推导结论，而不假定结论的否定。(web.stanford.edu)

二的平方根的无理性

一个经典例子是证明 $\sqrt2$ 为无理数。反过来，假定它是有理数。那么

\sqrt2=\frac{a}{b},

其中 $a,b$ 是没有大于一的公因子的正整数。两边平方可得

a^2=2b^2.

因此， $a^2$ 为偶数，故 $a$ 也是偶数，因为奇数的平方仍是奇数。令 $a=2k$ ，代入得

4k^2=2b^2,\qquad b^2=2k^2,

所以 $b$ 也是偶数。于是， $a$ 和 $b$ 有公因子二，这与所选分数为最简分数相矛盾。因此，有理数这一假设不成立。对于这一具体证明，最简分数的条件不可或缺：仅仅找到一个未约分的分数，并不会构成矛盾。(web.stanford.edu)

素数有无穷多个

另一个常见例子来自数论。假定素数只有有限多个，列为 $p_1,\ldots,p_n$ ，并构造

N=p_1p_2\cdots p_n+1.

由于 $N>1$ ，它有一个素因子 $q$ 。所列出的素数没有一个能整除 $N$ ，因为 $N$ 除以任意 $p_i$ 的余数都是一。因此， $q$ 不在这份本应完整的列表中，产生矛盾。需要注意的是，这一论证并不要求 $N$ 本身是素数。(euclids-elements.org)

这是以反证法形式呈现的一个与欧几里得相关的结论。几何原本第九卷命题20证明：对于任意给定的有限个素数，都存在不在其中的素数。其论证也可以从构造性的角度理解，即构造出一个给定集合之外的素数，而不是一开始就假定所有素数都已列出。(euclids-elements.org)

经典逻辑与直觉主义逻辑的基础

一般的经典反证法涉及双重否定消去。从 $\neg P$ 推导出 $\bot$ ，首先确立的是 $\neg\neg P$ ；经典逻辑随后允许由此推得 $P$ 。以直觉主义逻辑为基础时，不受限制的双重否定消去与排中律 $P\lor\neg P$ ，作为适用于所有命题的原则，是等价的。(plato.stanford.edu)

直觉主义逻辑并不无条件地接受上述最后一步推理。不过，它仍然接受通过假定 $P$ 并推导出矛盾来证明否定命题，从而确立 $\neg P$ 。因此，构造性推理并不禁止一切涉及矛盾的论证。上面的无理性证明确立的是“不存在有理数表示”这一否定性断言，并不需要不受限制的双重否定消去。(plato.stanford.edu)

形式化使用与局限

在形式证明中，假设的作用域十分重要：在临时子证明内部得到的结论，不能在没有适当推理规则的情况下直接用于该子证明之外。反证规则明确规定了这些假设依赖关系，从而区分合法的归谬论证与暗中继续依赖已被否定假设的论证。(forallx.openlogicproject.org)

矛盾也涉及前提的整体。如果背景前提本身就能推出不可能的情形，那么在加入 $\neg P$ 后推导出矛盾，并不能单独证明背景理论是可靠的。经典逻辑允许从相互矛盾的前提推出任意结论。次协调逻辑拒绝这一不受限制的原则，因此，不能将经典逻辑的反证规则原封不动地套用于所有逻辑系统。(plato.stanford.edu)