分类讨论证明

分类讨论先把复杂论域拆成若干结构较统一的情形，再在每个分支使用最合适的论证并推出同一结论。正确性取决于“覆盖全部可能”与“每个分支论证有效”，不取决于分类是否看起来自然。分支可以重叠，无需互斥，但互斥通常更清楚；分类标准也应真正降低各分支难度。

证明任意整数 $n$ 的 $n(n+1)$ 为偶数，可分 $n$ 偶与 $n$ 奇两种情形。再证明对任意整数 $n$，$3\mid n^3-n$：按模 $3$ 的余数分为 $n\equiv 0,1,2$ 三种情形，分别有

三个分支穷尽所有整数，因此结论成立。分类可以重叠，只要每个对象至少落入一个已证明分支；但分类过细会制造重复，分类不穷尽则直接使证明失效。例如，只讨论正数与负数会漏掉零，按模 $m$ 分类时也必须覆盖 $0,1,\dots ,m-1$ 的每个余数类。

命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。中的析取消去，就是 自然演绎公理库自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。里的分类讨论规则。绝对值、奇偶性、符号、图的局部结构和算法正确性，都常按输入形状或分支条件分类；反证法公理库反证法Proof by contradiction · Reductio ad absurdum假设目标命题为假并推出矛盾，从而证明目标。和归纳法内部也经常嵌套有限情形分析。复杂证明可以先给出分类引理，集中处理边界条件并避免复述。