Cantor

Bernstein までできたので、Cantor までやるのが礼儀かなと。

S と Power S の Bijection はないってやつですが、

集合論でないのは

　　diagonal : { S : Set } → ¬ Bijection　( S → Bool ) S

と割と普通に対角線論法で証明できてる。

　　_c<_ : ( A B : HOD ) → Set n
　　A c< B = ¬ ( Injection (& B)　(& A) )

で順序を定義してやって、Powers S から S への injection がないこと示せば良い。

　　Cantor1 : ( S : HOD ) → S c< Power S

つまり

　　 f2 : Injection (& (Power S)) (& S)

から矛盾を示せば良いわけですが、

　　 f1 : Injection (& S) (& (Power S))

は簡単に作れる。Sの要素 x を {x} にすれば良い。なので、Bernstein から Bijection を作れる。

　　 b : HODBijection (Power S) S
　　 b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)　

あとは、対角線論法を実行すれば良いわけですが、割と迷走。結論的には

　　 diag : {x : Ordinal} → (sx : odef S x) → Bool

で対角線の要素が部分集合に入っているかを調べて、

　　 Diag : HOD
　　 Diag = record { od = record { def = λ x → odef S x ∧ ((sx : odef S x) → diag sx ≡ false) }
　　　　 ; odmax = & S ; <odmax = odef∧< }

みたいな形で HOD を作れば良いらしい。Diag は Power S の要素なので、S の要素に戻せるわけですが、

　　 odef S n → ¬ (fun→ b (& Diag) diag3 ≡ n)

を示せるので、Sの要素どれとも等しくない。なので矛盾。

なのだが、

　　Berstein の証明の check に 30秒
　　対角線論法 の証明の check に1分

かかる。さらに、Bijection から Injection は容易に導出できるので、Bijection がないとも示せるんですが、

　　Cantor2 : (u : HOD) → ¬ ( HODBijection u (Power u) )

には、50分。どういうことなのかなぁ。Bernstein を切り離すと数秒でいけるんですが。

ただ、切り離すと、少し条件を甘くしても check が通ってしまう。つまり、切り離して証明してもつなげると通らない。

まぁ、一応、通ったから良いんだが、あまりよろしくないな。証明の信頼性に問題があるってことでしょ。

集合論の難しさでもあるな。