順序数の定義を試みます。
まず準備として「推移的」を定義します。
xは推移的 :⇔ ∀u∀v((u∈v ∧ v∈x)) ⇒ u∈x)
ちょっと練習
∅は空集合とします。
主張 : ∅は推移的
主張 : {∅}は推移的
xは¬∃y(y∈x)であるような何かとします。(実はこのxは空集合だったりする^^;)
主張 : {x,{x}}は推移的
主張 : {x,{x},{x,{x}}}は推移的
主張 : {x,{x},{{x}}}は推移的
xは順序数 :⇔ (xは推移的 ∧ ∀y(y∈x ⇒ yは推移的))
順序数の定義です。ずばりと、これです。
順序数のクラスは慎重に定義しなくてはいけません。
On := { x | xは順序数 ∧ ¬(x∈x) }
On' := { x | xは順序数 }とおいてみます。
On'自身は推移的で、On'の要素も推移的なので、On'自身も順序数ということになり、
On'∈On'
という事態になってしまいます。
つまり、順序数のシンプルなクラスは再び順序数になり、止まらなくなります。
¬(x∈x)を条件に入れると、その無限上昇が止まるようです。
つまり、On∈Onにはなりません。
集合論では、クラスを定義するとき、例えば{ x | P[x] }ならば自動的に{ x | P[x] ∧ ¬(x∈x) }のように暗黙的に設定されるらしいです。
他に集合の包含関係で順序関係を与え、順序数を定義する流儀があるようです。
別の数学概念を持ち込む形になるので、定義にするにはシンプルさが失われるのではないかと思います。
話を発展させます。
和集合をとる演算子を次のように導入します。
Union := { (x,y) | x,yは集合 ∧ { u | ∃v(u∈v ∧ v∈x) }=y }
共通集合をとる演算子を次のように導入します。
Intersect := { (x,y) | x,yは集合 ∧ { u | u∈Union(x) ∧ ∀v(v∈x ⇒ u∈v) }=y }
集合の後者写像を次のように導入します。
Suc := { (x,y) | x,yは集合 ∧ Union({x,{x}})=y }
ちょっと練習
Union({x,y})=(x∪y)
Intersect({x,y})=(x∩y)
Suc(x)=(x∪{x})
イメージできるでしょうか。
無限濃度の順序数で最小のものωが次のようにして与えられます。
ω := Intersect({ x | ∅∈x ∧ ∀y(y∈x ⇒ Suc(y)∈x) })
ω := Intersect({ x | ∅∈x ∧ ∀y∀z((y∈x ∧ (y,z)∈Suc) ⇒ z∈x) }) (こういう書き方もあり)
このとき、ω∈On、つまり、ωは順序数となります。
ZFの公理に無限集合の公理があります。
その無限集合の公理の存在意義は、その公理を満たすすべての無限集合に共通に含まれる無限集合がただ一つ存在し、それがωで、同時に順序数になるということだと思います。
∃x(∅∈x ∧ ∀y(y∈x ⇒ Suc(y)∈x)) これは無限集合の公理
これから直ちに
{ x | ∅∈x ∧ ∀y(y∈x ⇒ Suc(y)∈x) }≠∅
が言えて、この非空のクラスをΩとおきます。
∀x(x∈Ω ⇒ (∅∈x ∧ ∀y(y∈x ⇒ Suc(y)∈x)))
∀x(x∈Ω ⇒ {∅,Suc(∅),Suc(Suc(∅)),...}⊂x)
これは証明とは言えませんが、うっすらと、
Intersect(Ω) = {∅,Suc(∅),Suc(Suc(∅)),...} = ω
と言うのが見えてきませんか。
ちなみに、
Intersect(Ω)∈Ω
∀x(x∈Ω ⇒ Intersect(Ω)⊂x)
が成立するはずです。
さらに、
(ω∪{ω,Suc(ω),Suc(Suc(ω)),...})∈(Ω∩On)
ω' := (ω∪{ω,Suc(ω),Suc(Suc(ω)),...})とおいて、
(ω'∪{ω',Suc(ω'),Suc(Suc(ω')),...})∈(Ω∩On)
ω'' := (ω'∪{ω',Suc(ω'),Suc(Suc(ω')),...})とおいて、
(ω''∪{ω'',Suc(ω''),Suc(Suc(ω'')),...})∈(Ω∩On)
という連鎖が成立しそうですね。
ちなみに、
∀x(x∈On ⇒ Suc(x)∈On)
標準的な集合の宇宙はωを種にして生成されます。
さらに大きい集合の宇宙はωより大きい順序数(というか基数)で生成されるという枠組みになってると思います。
α∈Onとして、Universe(α)はαを種にして生成される集合の宇宙とします。
Union({ Universe(α) | α∈On })が集合論で語りうる集合の限界なのではないかと思います。
順序数は集合論の屋台骨だと思います。