公理的集合論における自然数の存在(その 1)

まぁ、公理的集合論などと言わずとも、自然数は確かに存在しているのですが、それを公理的集合論の中で扱えるように、公理的集合論の中に「埋め込む」作業を、今回はやってみようと思います。
まず
$M(y)\equiv(\emptyset\in y\wedge\forall x(x\in y\to x^+\in y))$
という論理式を用意しておきます*1。無限公理により、 $M(a)$ が真となる集合 $a$ は少なくとも一つ存在します。 $M(a)$ が真となる集合 $a$ を無限系譜と言うことにします。また
$\forall x(x\in a\to M(x))$
を満たす $a\neq\emptyset$ を無限樹と言うことにします。このとき、次の補題が成り立ちます。

補題

$a,b$ を無限樹とするとき、次が成り立つ。

$\cap a$ は無限系譜。

$a\subseteq b\to\cap a\supseteq\cap b$

(証明)
1. $c\in a$ を一つとって
$\cap a=\{x\in c|\forall y\in a(x\in y)\}$
と表す。 $a$ は無限樹であるから
$\forall y(y\in a\to M(y))$
なので $\forall y\in a(\emptyset\in y)$ が成り立つ。よって $\emptyset\in\cap a$ . また $z\in\cap a$ ならば、定義により $\forall y\in a(z\in y)$ であり、 $\forall y\in a$ が無限系譜であることにより $\forall y\in a(z^+\in y)$ となるから $z^+\in\cap a$ となる。よって $\cap a$ は無限系譜。
2. $c\in a$ を一つ取る。 $a\subseteq b$ 故 $c\in b$ であるから
$\cap a=\{x\in c|\forall y\in a(x\in y)\}$
$\cap b=\{x\in c|\forall y\in b(x\in y)\}$
である。 $a\subseteq b$ 故
$\forall y\in b(x\in y)\to\forall y\in a(x\in y)$
であるから $\cap a\supseteq\cap b$ .
さて、 $a$ を無限系譜として
$\tilde{a}=\{x\in\mathcal{P}(a)|M(x)\}$
とおくと、ベキ集合公理と分出公理図式により、これは集合です。また $a\in\tilde{a}$ なので $\tilde{a}\neq\emptyset$ でもあります。このことから $\tilde{a}$ は無限樹となるので、上の補題により $\cap\tilde{a}$ は無限系譜となります。これは $a$ によって一意に定まります。これを $\omega_a$ と書いておくことにしましょう。(続く)

*1: $x^+=x\cup\{x\}$ です。