整礎帰納法と構造的帰納法
構造的帰納法は整礎帰納法の一種。
整礎帰納法: $ Rが$ X上の整礎関係であるとき以下が成り立つ。
$ \forall{x} \in{X}. P(x)と$ \forall{x} \in{X}.((\forall{y} \in{X}. yRx \Rightarrow P(y)) \Rightarrow P(x))は同値
算術式の集合$ Aexpで考えると、$ x, y \in{Aexp}について「$ xは$ yの直接の部分式である」という関係は整礎関係である。
$ \forall{x} \in{X}.((\forall{y} \in{X}. yRx \Rightarrow P(y)) \Rightarrow P(x))が成り立つことを示すには、$ x \in Aexpが数字か変数か足し算か掛け算のどれかで場合分けすればよい。