Just $ A sandbox

プログラミングと計算機科学とかわいさ

Agdaで集合論をやろうとして上手く行かなかった

この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した.

写像の定義を

_⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B

としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる.
x ∈ A を像の方に押し込めて

_⟶_ A B = ∀ x → ∃ \y → x ∈ A → y ∈ B

のように定義すると, 今度は x ∈ A に依って決まる写像が定義できなくなる.

最初の方法ではZFCから排中律を示すところで引っかかり(本来異なる集合 A,B に対して A ≡ B を言おうとするので型エラーになって上手く行かない), あとの方法では置換公理を使う場面でひっかかる(函数の像を扱うとき).
よっていずれにせよ上手く行かない.

この前の記事のコメントではAgdaの型を用いて を定義する方法も教えてもらった.

data _∈_ {l} {A : Set l} (x : A) (B : Set l) : Set (suc l) where
  in-eq : A ≡ B → x ∈ B

この方法だと, の定義がもろにAgdaの型システムに依存しているので, 方針はガラッと変わるはず.
多分これで今やっていることの模倣はできると思うけれど, そもそも何を公理として仮定して良いのかが分からないし, もともとAgdaの型システムではどういうことができるのかもよく分からないのでなんとも言えない.

Agdaの方に上手く寄れば, 多分普通の数学の模倣はできるような気がするけれど, 少なくとも数学のやり方をそのまま持ってくるだけでは上手く行かないのかなぁと思った.
こういうことをするなら, Agdaよりもっと向いている言語を他に探したほうがいいのかもとも思った.
でもAgdaはHaskellerの自分にとっては学びやすかったし, 気に入ったところも多かったので少し残念.

供養

https://github.com/myuon/agda-cate

(圏論はそれなりに上手く行っているので, 圏論方面はもう少し開発を続けるかもしれない)

矛盾の証明

矛盾を示すときに使える方法としては主に以下の2つだと思う

  • 命題 ¬PP をぶつける
  • 矛盾 の特徴付けを使う

矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから,
空集合の公理がそのまま矛盾の特徴付けになる.
∃ \(A : Set) → (∀ x → ¬ (x ∈ A))

否定命題にPをぶつけるというのは口で言うほど簡単ではなくて, まずどの否定命題を選んでくるかからよく考えないといけない.

一体何の話かというと, Agdaで「ZFC ⇒ 排中律 (P ∨ (¬ P))」を示すときに,

https://myuon.github.io/agda-cate/Sets.Sets.NonDatur.html#660

A = ⟦ x ∈ [0,1] ∣ x ≡ 0 ∨ P ⟧ -- A := {x ∈ {0,1} ∣ x = 0 ∨ P}
B = ⟦ x ∈ [0,1] ∣ x ≡ 1 ∨ P ⟧ -- B := {x ∈ {0,1} ∣ x = 1 ∨ P}
X = [ A , B ] -- X := {A,B}

みたいにするんだけど, 以下の議論では, ここにさらっとでてくる自然数0と1が異なることが仮定されている.

0と1は上のように非順序対を作って使うので適当なsetでないといけないんだけど, 当然AgdaのData.Natで定義されているNatの元は(inductive data typesで定義されているから)setではない.
そこで 0 = ∅, 1 = ∅ ∪ {∅} に戻って0と1が異なることを示さないといけなかったけれど, これには空集合の公理や対の公理や和集合の公理が必要で, しかもそんなに明らかなことでもない.
https://myuon.github.io/agda-cate/Sets.Sets.Natural.html#793

Natの世界でもSetの世界でも0と1が異なることを示すには, 0=1を仮定して矛盾を導かなければいけないので, それがいつも自明なことではないなと実感した.

というかむしろ, Agdaの場合は同値なものがrewriteによって書き換えるだけで証明が済んでしまうことが多いので, 等しさが特別扱いやすいだけなのかもしれないけど.

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