Power Set

ZF の続き。ある集合Aの部分集合全体の集合、冪集合ですが、普通に論理式で定義してしまうとだめ。

しばらく、まったくわからなかったんですが、冪集合の公理が置換公理抜きでできると書いてるのはコーエン先生の本だけで、他の本は全部置換公理を使ってる。さらに、構成可能集合が部分集合の集合に等しいらしい。

部分集合自体は

　 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
　 ZFSubset A x =　record { def = λ y → def A y ∧　def x y }　

と言う形で集合の and で定義してやればよい。部分集合全体は、この x を「可能な集合全部」でUnionを取る必要がある。超限帰納法かと思ったんですが、

置換公理は sup と同じなので sup (上界)で良いんじゃないか? と思いついたら、

　　Def :　{n : Level} → (A :　OD {suc n}) → OD {suc n}
　　Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )　

　　-- Constructible Set on α
　　L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
　　L {n}　record { lv = Zero ; ord = (Φ .0) } = od∅
　　L {n}　record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
　　L {n}　record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
　　　　record { def = λ y → osuc y o< (od→ord (L {n}　(record { lv = lx ; ord = Φ lx }) )) }

と言う感じで構成可能集合まで一気にできました。

冪集合の公理は「ある集合に属するとAにも属するなら、その集合はAの部分集合」

　　 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t

なんですが　t ∋ x → A ∋ x があるので、t がA 部分集合であることが言えて、 Power A が上界なことから言えるようです。

反対側の「Aの部分集合に属するならAにも属する」 の方

　　 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x

こっちは ZFSubset A ? ∋ t が見つけられれば ZFSubset A ? ∋ x → A ∋ x で言えるんですが...　

Power A に含まれるなら、部分集合のどれかに含まれるってわけなんですけどね。最小性入れてないのでできない。どれかは構成的には探せない。

最小性入れても良いのだが、入れないで置換公理と同等なようなので入れないでできる方が望ましいかな。L を使うのかも。

というわけで、まだできてません。