反证法

在经典命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。中，反证法为证明 $P$，临时假设 $\mathrm{\neg }P$，再从该假设与已知事实合法地推出矛盾，从而排除所有反例。它适合否定性结论、不可存在性，以及目标对象难以直接构造的论证；但矛盾必须真正依赖 $\mathrm{\neg }P$，不能只是说明假设“看起来不合理”。经典逻辑中最后一步依赖双重否定消去；在直觉主义逻辑里，从 $\mathrm{\neg }\mathrm{\neg }P$ 一般不能直接得到 $P$。

证明 $\sqrt{2}$ 无理：假设存在既约分数 $p/q$ 表示它，推出 $p,q$ 同为偶数，矛盾。若推出的只是“令人意外”而非形式矛盾，反证没有完成。

证明素数有无穷多个。假设全部素数为 $p_1,\dots ,p_k$，令

$N>1$ 必有素因子 $q$，但每个 $p_i$ 除 $N$ 都余 $1$，所以 $q$ 不在原列表中，产生矛盾。这里矛盾必须来自“素数只有有限多个”这一否定目标与已经证明的整除事实；若矛盾实际源于另一个未经证明的辅助假设，反证形式本身不能修补漏洞。

反证法常用于无理性、无穷性、唯一性、不可数性和不可判定性问题公理库可判定语言Decidability · Recursive language · Decidable language存在对所有输入都停机并正确回答成员资格的图灵机语言类。。正文应明确矛盾来自哪两个互斥陈述，并避免把待证结论悄悄作为中间假设。它与逆否证明公理库逆否证明法Proof by contrapositive通过证明 ¬Q→¬P 来证明 P→Q。不同：逆否证明直接建立一个等价蕴涵，不必导出 $\mathrm{\perp }$。构造性逻辑会区分 $\mathrm{\neg }\mathrm{\neg }P$ 与 $P$，因此使用范围必须随逻辑背景调整。