かじもとにっき

ゆるふわなおはなしをかきます

数学的帰納法

定義 well-founded set

\left\langle {A, \prec } \right\rangleは、Aの任意の空でない部分集合が極小元を持つ時、すなわち、Aの任意の部分集合Bに対し、
B \ne \emptyset  \equiv \mathop {\exists x}\limits_{x \in B} .\mathop {\forall y}\limits_{y \prec x} .y \notin B
が成り立つ時well-founded。

定理 数学的帰納法

\left\langle {A, \prec } \right\rangleがwell-foundedであるとき、またその時に限り、
(\forall x.Px) \equiv (\forall x.(\mathop {\forall y}\limits_{y \prec x} .Py) \Rightarrow Px)
が成り立つ。
これを\left\langle {A, \prec } \right\rangle上の数学的帰納法と言う。

証明

Aの任意の部分集合Bに対して論理式Px \equiv x \notin Bを作ることが出来、また、任意の論理式Pxに対して集合B = \left\{ {x;\neg Px} \right\}を作ることが出来ることによる:

\begin{array}{l}B \ne \emptyset  \equiv \mathop {\exists x}\limits_{x \in B} .\mathop {\forall y}\limits_{y \prec x} .y \notin B\\ \equiv B = \emptyset  \equiv \mathop {\forall x}\limits_{x \in B} .\mathop {\neg \forall y}\limits_{y \prec x} .y \notin B\\ \equiv B = \emptyset  \equiv \forall x.x \notin B \vee \mathop {\neg \forall y}\limits_{y \prec x} .y \notin B\\ \equiv (\forall x.Px) \equiv (\forall x.Px \vee \mathop {\neg \forall y}\limits_{y \prec x} .Py)\\ \equiv (\forall x.Px) \equiv (\mathop {(\forall y}\limits_{y \prec x} .Py) \Rightarrow \forall x.Px)\end{array}

定義

\left\langle {A, \prec } \right\rangleがnoetherian*1 iff 任意のx \in Aに対し、xから始まる全てのdecreasing chainが有限。

定理

\left\langle {A, \prec } \right\rangleがnoetherian iff \left\langle {A, \prec } \right\rangleがwell-founded。

*1:Emmy Noetherに因む