ZF集合論の続き

集合論の本だと、

　　ZF集合論の公理 → 順序数 → 構成可能集合 → ZF集合論のモデル

ってな手順です。今回は、

　　ZFの公理の Agda の record を作る
　　順序数(Ordinal)を data で構築する
　　集合を順序数定義可能集合(順序数上の方程式)として定義する
　　集合と順序数の対応を仮定する (ゲーデル数/ゲーデル集合)
　　上界(Sup)を仮定する
　　集合論のモデルを順序数を使って構築する

ってな手順です。公理は

　　 pair : ( A B : ZFSet　) →　( (A , B)　∋ A ) ∧ ( (A , B)　∋ B　)
　　 union-u : ( X z : ZFSet　) → Union X ∋ z → ZFSet
　　 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
　　 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z)　∧ (union-u X z X∋z ∋ z )
　　 _⊆_ A B {x} = A ∋ x →　B ∋ x
　　 A ∩ B = Select A (　λ x → ( A ∋ x ) ∧ ( B ∋ x )　)
　　 empty :　∀( x : ZFSet　) → ¬ ( ∅ ∋ x )
　　 power→ : ∀( A t : ZFSet　) → Power A ∋ t → ∀ {x}　→　_⊆_ t A {x}
　　 power← : ∀( A t : ZFSet　) → ( ∀ {x}　→　_⊆_ t A {x})　→ Power A ∋ t
　　 extensionality :　{ A B : ZFSet　} → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)　) → A ≈ B
　　 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
　　 regularity : ∀( x : ZFSet　) → (not : ¬ (x ≈ ∅)) → (　minimul x not　∈ x ∧　(　minimul x not　∩ x　≈ ∅ ) )
　　 infinity∅ :　∅ ∈ infinite
　　 infinity :　∀( X x : ZFSet　) → x ∈ infinite →　( x ∪ Select X (　λ y → x ≈ y )) ∈ infinite
　　 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet　} →　( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈　Select X ψ )
　　 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet　) →　( ψ x ∈　Replace X ψ )　

ってな感じ。Agda は高階関数型だから一階述語論理と違ってAxiom Schemeとか関係なく、任意の関数を含む公理を記述可能。

これをモデルが満たすかどうかをチェックにいきます。

順序数定義可能集合ODは単なる述語なので、こんな感じ。

　　record OD {n : Level}　: Set (suc n) where
　　　field
　　　　def : (x : Ordinal {n} ) → Set n

Agda で証明できない仮定の方は、o< が順序数の順序で、c< が集合の順序∈で、

　　postulate　　　
　　　od→ord : {n : Level} → OD {n} → Ordinal {n}
　　　ord→od : {n : Level} → Ordinal {n} → OD {n}
　　postulate　　　
　　　c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
　　　o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
　　　oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
　　　diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
　　　sup-od : {n : Level } → ( OD {n} → OD {n}) →　OD {n}
　　　sup-c< : {n : Level } → ( ψ : OD {n} →　OD {n}) → ∀ {x : OD {n}} → ψ x　c< sup-od ψ

これくらいです。Ordinal の方は泣くほど複雑になって、結構苦労したんですが、なんとか動いているみたい。

これで、pair/empty から始めて、regurarity, selection, union, extensionality　までできました。思ったより順調かな。
selection は分出公理とか subset とか呼ばれるものです。

Ordinal が複雑なのが残念すぎる。Union 公理の証明で順序数の osuc つまり、x ∪ {x} で

　　 y o< osuc x　→ x o< y → ⊥

を証明するのが Ordinal が正しくできているかにかかっていて厳しかったです。作り直しかと思ったよ。

残りは power set , infinity, replacement ですが、できるかな〜

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/ZF-in-agda/