查看“︁穷举法”︁的源代码

[[分类:证明方法]]
{{InfoBox
|name=穷举法
|eng_name=proof by exhaustion
|aliases=分类证明,proof by cases,完全归纳法,complete induction,brute force method
}}
'''穷举法'''('''proof by exhaustion''')/'''完全归纳法'''('''complete induction''')，指通过把原命题拆解成有限的情况并分别证明，来[[证明]]原命题的一种方法。

== 描述 ==

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

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

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