反证法

反证法
术语名称	反证法
英语名称	proof by contradiction

反证法(proof by contradiction)，指通过引入命题反面假设并演绎出矛盾，来证明原命题的一种方法。

对应于自然演绎法中的否定消去( [math]\displaystyle{ \lnot }[/math] -elim)，对应的重言式是双重否定式。

描述

有假设集 [math]\displaystyle{ \Gamma }[/math] 要证明 [math]\displaystyle{ \phi }[/math] 时，引入新假设 [math]\displaystyle{ \lnot\phi }[/math] ，并对某个 [math]\displaystyle{ \psi }[/math] 演绎 [math]\displaystyle{ \Gamma, \lnot\phi \vdash \psi \land \lnot \psi }[/math] 。

根据矛盾律得到右边是假，即 [math]\displaystyle{ \Gamma, \lnot\phi \vdash \bot }[/math] ，这实际上证明了两者不相容，因此有 [math]\displaystyle{ \Gamma \vdash \lnot\lnot\phi }[/math] ，结合双重否定式有 [math]\displaystyle{ \Gamma\vdash \phi }[/math] ，因此原命题得证。