五十嵐淳『プログラミング言語の基礎概念』を読んでいます。
整礎順序集合
集合とその上の順序が整礎であるとは、（真の）無限降下列が存在しないことをいいます。 厳密な定義は以下です。
整礎順序集合(well-founded ordered set)とは、集合 $X$ とその上の二項関係 $\prec \subseteq X \times X$ の組 $(X, \prec)$ で、 $X$ の任意の空でない部分集合 $S$ が、順序 $\prec$ について極小元をもつこと。
ちなみに、$x \in X$ が $\prec$ に関して $X$ の極小元であるとは、 $\forall y \in X . y \nprec x$ であることを言います。
整礎帰納法
整礎順序集合について、次のような帰納法を考えることが出来ます。
整礎帰納法の原理とは、整礎順序集合 $(X, \prec)$ と $X$ の元に関する述語 $P$ が与えられたとき、
$$ \forall x \in X . P(x) \Leftrightarrow \forall x \in X . (\forall y \in X . y \prec x \Rightarrow P(y)) \Rightarrow P(x) $$
整礎順序集合について、
- すべての元がある述語をみたすこと
- すべての元について、「その元より小さいすべての元が述語をみたすならば、その元についても述語が成り立つ」
が同値だということです。無限降下列がないということが、この原理の正当性に重要な要素となっています。
整礎帰納法の特殊ケース
よく知られる数学的帰納法などは、この整礎帰納法の特別なケースとなっています。
数学的帰納法
整礎帰納法の原理において、
- $X$ として自然数の集合（0を含む）
- $\prec$ として $n \prec m \Leftrightarrow m = n + 1$
とすれば、
- $P(0)$ と、
- $P(k)$ を仮定した上での $P(k + 1)$
を示すことで、任意の自然数について $P$ が成り立つことを証明する数学的帰納法となります。 $(\mathbb{N}, \prec)$ が整礎順序集合となっていることが重要です。
- $\prec$ として自然数上の通常の大小関係
をとれば、
- $P(0), P(1), \ldots , P(k)$ を仮定した上での $P(k + 1)$
を示すことによる数学的帰納法となります。
構造に関する帰納法
ペアノ自然数
$$ n \in \mathrm{Nat} ::= Z\ |\ S(n) $$
の構造に関して、
- $X$ として $\mathrm{Nat}$
- $\prec$ として $n \prec m \Leftrightarrow m \equiv S(n)$
をとれば、ペアノ自然数の構造に関する帰納法となります。