14/10/12 21:35:02.06 xA+0V9C8.net
素朴集合論に型を付けたらうまくいくんじゃね？
とやってみたら恐ろしく複雑で不自由になったのがフレーゲのタイプ理論。
その後100年近く塩漬け状態。
それなら集合とクラスの二つだけに分けて、後はあまり強く型付けしなければ、
カントールの楽園から追放されないんじゃね？
というのがツェルメロの公理的集合論。
集合論、集合論と言っている人は、
無限公理や正則性公理を積極的に言語で使うつもりがあるのかな?
↓必要なのはここまでなんじゃないのかな。
URLﾘﾝｸ(ja.wikipedia.org)