Suc-帰納法と累積帰納法

Suc-帰納法:\[(P(0)\wedge \forall k[P(k)\rightarrow P(k+1)])\rightarrow\forall n[P(n)]\tag{1}\]
累積帰納法:\[\forall n[\forall m< n[P(m)]\rightarrow P(n)]\rightarrow\forall n[P(n)]\tag{2}\]

(1)⇒(2):図式(1)のもと、$\forall n[\forall m< n[P(m)]\rightarrow P(n)]$なる任意の述語$P$をとり、$\forall n[P(n)]$を導く。$Q(n)\equiv\forall m< n[P(m)]$とおくと、$Q(0)$が成り立つ。また上の仮定は$\forall n[Q(n)\rightarrow P(n)]$と書けるから、$Q(k)$なる任意の$k$について$P(k)$も成立し、$Q(k)\wedge P(k)$すなわち$Q(k+1)$が成り立つ。すると図式(1)から$\forall n[Q(n)]$が成り立ち、これは$\forall n[P(n)]$を含意する。

(2)⇒(1):図式(2)のもと、(ア)$P(0)$および(イ)$\forall k[P(k)\rightarrow P(k+1)]$を満たす任意の述語$P$をとり、$\forall n[P(n)]$を導く。そのために(ウ)$\forall m< n[P(m)]$なる任意の$n$をとり、$P(n)$を導くことで図式(2)の前件の成立を言う。$n=0$のときは(ア)から直ちに$P(n)$が従う。$n\neq0$のとき、$n=m+1$なる$m$がとれて、(ウ)から$P(m)$が成立するが、(イ)により$P(m+1)$すなわち$P(n)$も成立する。