型付ラムダ計算 それと型がつけられるかということがどうも正則性公理と関わっている気がして、この公理ってないほうが楽しくないかな。 と書いたら くるるさんから正則性公理 にお返事をもらった。 むしろ言及したいのは「この公理ってないほうが」の部分でありまして。正則性公理がある意味adhocな公理であることは間違いないです。そして、そのことを攻撃するのは論理的には全く正しいし、ない方が楽しいかもねと言われればおき得ることの範囲が広がるんだから確かにそうかもしれないとしか言いようがありません。 ですが、正則性公理が現代集合論ではとても強力に使われていることだけは主張しておいたほうが良いかと思います。 それは確かに分かるのですが、「ZF のモデルが標準モデルと同型になる条件が無限降下列の非存在」とか、いかにも正則性公理が adhoc であることを示しているように見えませんかね。あ、正則性公理なかった