surreal numbers

Surreal Numbers in Coq(slides,pdf) - yoriyukiの日記

読んでみました。面白そうな概念なんですが、ここで紹介されているスライドだと「Coqで表現するには」ってところに比重がおかれていて、これを使ってどういう議論をするかってことはほとんどないのが残念。まあそれに、区間がproper classになっちゃうのはやっぱりなんか気持ち悪いような。
でも、連続体っぽいものを全ての順序数を含む形で定義できるって言うのはやっぱりちょっといいかも。

あ、確かに実数の超準モデルになっています。とはいえ、恐ろしくレベルの高い超準ですが。