集合論のめんどくさいところは、扱いを間違えると、あっさり矛盾が出て来るので、いろいろ気を付けないといけない。公理の数は少ないんだけど、そんなこんなで微妙に工夫されている。
{ x | ¬ x ∈ x }
で、もう矛盾しちゃう(ラッセル)ので、こういうのは「集合じゃなくて、クラス」とか言っちゃう。集合だと、
{ x∈u | ψ(x) }
とか書くらしい。で、正則性の公理ってのがあって、
¬x=φ →∃a∈x a ∩ x = φ
「空集合でなければ、自分の要素で自分とdisjointな要素が必ずある」を要求すると、
x ∋ x
とか
x_0 ∋ x_1 ∋ ...
で無限に続くようなのがなくなるらしいです。まどろっこしいです。 x ∋ x を仮定すると、{x} が正則性の公理を満たさなくなるらしいんだが、y ∈ {x} で、y は x 以外にありえないってのが定義から出るらしいんだが、{x} ってどこで定義した? ってな感じです。たぶん、{x} に対応する論理式があるんだよな。そこまで戻れば実は自明。証明図書いて欲しいよ。
いやだから「なんかの集まり」から始めるから、そうなるんじゃないか? 普通、その「なんか」を指定してから始めるだろ? とか言うと、数学の範囲がかなり狭くなってしまうらしい。いや、それでもかなり広いんだけど。
特に、最小上界の存在、つまり、有理数列から実数を導くあたりが、実数が良くわかってないのに、それに言及する形になるので気まずいらしい。非述語的とか言うらしい。非構成的とは言わんのか。
いや、物理学なら別にそれは当り前で誰も気にしてない。時間と時刻が両方とも未定義とか、ある意味当り前だし。
で、数学が実数を実験で確認するものだと諦めれば割と簡単なんですが、そうはいかないらしい。数学は数学で閉じて議論できる「理想的な」実数が欲しいわけ。でも、それは、まだ無矛盾と証明されたとは見なされてないようです。
ま、それは、ともかく、集合論にはブール代数とうモデルがあるので、それを理解するのが今回の復習の目的なはずです。はずなんだが、集合論の公理が、ブール代数とどう関係するのかが既に良くわからん。
たぶん、この当たりを Isabel HOL で証明したものもあるはずなんだけど。
いや、いま、そんなことをしているのはよろしくないんだけど。
