穷举法

穷举法
术语名称	穷举法
英语名称	proof by exhaustion
别名	分类证明, proof by cases, 完全归纳法, complete induction, brute force method

穷举法(proof by exhaustion)/完全归纳法(complete induction)，指通过把原命题拆解成有限的情况并分别证明，来证明原命题的一种方法。

描述

有假设集 [math]\displaystyle{ \Gamma }[/math] 要证明 [math]\displaystyle{ \forall t \phi(t/x) }[/math] 时，演绎 [math]\displaystyle{ \Gamma \vdash \phi(t_1/x) \land \dots \land \phi(t_n/x) }[/math] ，其中 [math]\displaystyle{ t_1,\dots,t_n }[/math] 要覆盖全部可能取值。

由于有限集上有 [math]\displaystyle{ \forall t \phi(t/x) \Leftrightarrow \phi(t_1/x) \land \dots \land \phi(t_n/x) }[/math] ，所以相当于演绎出了 [math]\displaystyle{ \forall t \phi(t/x) }[/math] 。

注：有时不会拆解到每个取值，可以只拆解等价类。