数学归纳法

数学归纳法把自然数的良基结构转化为证明原则：基例把证明接到数轴上，归纳步保证一旦到达某处就能继续前进，两者合起来便排除了最小反例。它不是从有限多个例子猜测普遍规律，而是一条覆盖所有自然数的逻辑规则。起始值必须与命题范围一致，归纳假设也只能按当前归纳步声明的索引使用。

例如，证明对所有 $n\ge 0$，

基例 $n=0$ 时两侧都为 $1$；若结论对 $n$ 成立，则加上 $2^{n+1}$ 得

完成 $n+1$ 情形。同样的方法可证明 $1+\cdots +n=n(n+1)/2$。若基例从 $n=1$ 开始却声称覆盖 $n=0$，结论便有缺口；若归纳步只能从 $P(n)$ 推到 $P(n+2)$，一个基例也只能覆盖一个奇偶类，必须再补另一个起点。错误归纳还常在从 $n$ 到 $n+1$ 时暗中改变不可保持的条件。归纳不是“检查很多样本”，而是要证明覆盖机制没有断点。

自然数公理库自然数模型Natural numbers · Peano system由零元、后继和二阶归纳原则范畴性刻画的离散数系模型。的后继与良基性质支撑普通归纳；强归纳公理库强归纳法Strong induction · Complete induction归纳步可假设所有较小自然数情形成立。、良基归纳和结构归纳是同一机制在不同索引结构上的表达。它们用于递推恒等式、递归算法正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。、语法树性质和有限组合结构。状态系统上的对应形式是归纳不变式公理库不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。：基例覆盖全部初始状态，归纳步覆盖每一条转移，而性质对所有可达状态成立是由这两项推出的结论。模型检查可以搜索反例或辅助发现不变式，却不能用若干已枚举状态替代归纳闭包证明。无论采用哪种形式，基例范围都必须覆盖归纳步能够到达的所有同余类、语法分支或初始状态。