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の自分にとっては学びやすかったし, 気に入ったところも多かったので少し残念.
