Classical set theory in Agda

Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。

標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているように見えるだけであんまり使い物にならない。
具体的に言うと和集合の公理がないので(binary cupとindexed bigcupはある)任意個のUnionがとれない。
他にも、そもそも∈の定義が函数適用なので X ∈ B と書いときにXとBでは型が違うのがすごくキモいとか。キモいというかこれのせいでZFの一部の公理は型があわなくて表現できなかったりもする。

そういうわけでまずは集合を使えるようにするというだけ。
コードは一番下に載っけました。

コードについて

二重否定除去

Relation.Nullary.Negation

elem

属するの演算と2つの公理。
elem-∈は(x : A)と(x ∈ A)がcompatibleになるように。
≡-∈は示せなさそうで必要になったから入れたけど本当に必要なんだろうか。よく分からない。

postulate
  _∈_ : Set → Set → Set₁
  elem-∈ : {A : Set} → ∀ x → x ∈ A → A
  ≡-∈ : {A X Y : Set} → X ≡ Y → X ∈ A → Y ∈ A

公理

仮定したのは以下。

• 外延性の公理
• 対の公理
• 和集合の公理
• 無限公理
• 分出公理
• 冪集合の公理

postulate
  extensionality : {A B : Set} → A ≡ B ⇔ Lift {_} {zero} (∀ x → (x ∈ A ⇔ x ∈ B))
  ∃-paring : ∀(A B : Set) → ∃ \(P : Set) → ∀ x → x ∈ P ⇔ (x ≡ A) ∨ (x ≡ B)
  ∃-union : (A : Set) → ∃ \(B : Set) → ∀ X → X ∈ B ⇔ (∃ \C → (C ∈ A) ∧ (X ∈ C))
  infinite : ∃ \A → (∅ ∈ A) ∧ (∀ X → X ∈ A → X ⁺ ∈ A)
  replacement : (A : Set) → (P : Set → Set₁) → ∃ \B → ∀ x → x ∈ B ⇔ (x ∈ A) ∧ P x
  powerset : (A : Set) → ∃ \B → ∀ X → X ∈ B ⇔ X ⊆ A

空集合の存在だけは(Data.Empty.⊥を使って)示せるので示した。

あとは命題の表現に便利そうな函数とか部分集合とか共通部分とか適当な補題を示したりした。
本に載っているままのやり方だけど

-- ``Russellのparadoxを回避"する命題。
cor-1-4 : (A : Set) → ∃ \B → B ∉ A

も示せた。

コメント

これだけのことが検索しても全くヒットしなくてつらかった。誰もAgdaで数学しないのかなって思った。

あと、仮定した公理が適切なものかどうかもよく分からない。なんか変なことしてたら教えてください。
選択公理とかも入れてもう少し綺麗にしてから自分のライブラリに入れて使おうと思います。

参考にした本

たまたま手元にあった。

集合と位相 (岩波基礎数学選書)

コード

https://gist.github.com/myuon/ea11f62f9a9a9fed02b0