超準解析反省会場

dif_engine @dif_engine

普通の数学、とかいうと怒られそうだけど、微積分だとか代数幾何とか、そういう数学の初歩的な部分はいわゆる「数学の基礎」よりずっと早く興隆した。だから大昔は実数とは何かとか気にせずに、まあこう言うとまた言い過ぎだろうけど、数学をやってた。

dif_engine @dif_engine

で、解析学周辺の話から（たとえば三角級数の収束の問題）、段々数学をきちんと形式化しようねって話になって、その頃はまだ数学者たちも形式化によるエンライトメントを信じてたと思うんですよ。

dif_engine @dif_engine

でも結局、頑張って覚えた集合論も、素朴に期待されたような「数学の絶対性の担保」足り得ないことがわかってしまった。しかも、一悶着あった末に受け入れた選択公理からバナッハ・タルスキーのパラドックスなんかが出てきたでしょ。

dif_engine @dif_engine

こういう不幸（？）が重なって、なんか「もう形式化ええねん」という厭戦気分というか、もう「あなたと形式化、いますぐダウンロード」ってボタンを押したくない、そんな感じになってたところにA.Robinsonが華々しく「基礎論フル活用して無限小合理化したｗｗｗ」とやったでしょ。

dif_engine @dif_engine

しかも、A.Robinson の本を見ると高階タイプ理論でしょ。多くの数学者は「集合論こそ至高」と洗脳されてきたので「はい、一緒に高階タイプ理論をインストールします」というチェックボックスをみて多くの人が引き返したんですよ。

dif_engine @dif_engine

もう少し経つと色々整理されてきて、要するに標準宇宙と超準宇宙の間に初等埋め込みがあるというのが本当に大事なことで、べつに高階タイプ理論をインストールしなくていいことが周知されてきたわけですね。

dif_engine @dif_engine

でも、Davis とか読むと、「個体を持つ集合論でやります（キリッ）」とか書いてあって、実際そういう風になってないと超準宇宙の構成は難しいということがわかってくるわけです。（正則性公理の扱いで、微妙に口ごもったり開き直る本もある）。

dif_engine @dif_engine

竹内外史とかになると、初等埋め込みはモデル論の初歩的な話題だからtrivialに易しいだろ、とそういうノリなので清々しいし、さすが俺達の外史という芸風です。

dif_engine @dif_engine

で、初等埋め込みがtrivialに易しいかどうかはともかく、誰かに初等埋め込みについて説明しようとすると「言語」が出てきてこれを見てインストールを諦める人が多いわけです。

dif_engine @dif_engine

公理的集合論の授業を受けた人は、「言語」で諦めたりしないはずだと信じたい気もしますね。でも、学部で授業を受けたから100％わかってるはず、とも言い切れないのは、大抵の人が自分の経験から知ってることではある。

dif_engine @dif_engine

大学によって違うだろうけど、一年生に公理的集合論を教えるというのは色々厳しくて、多少自然言語を交えて、たとえば松村の集合論みたいに教えたりするだろう。そうすると、数学科出ていてもあまり集合論しっかりと習ってないということもあり得る…のかな。

dif_engine @dif_engine

超準解析とか関係なくても、集合論きちんとやると論理式、推論規則ぐらいは触れてるはず！　←という暴力

dif_engine @dif_engine

話はずれますが、バナタルから読み取るべきなのは「選択公理めっちゃ怪しいｗっｗ」ではなくて「実数と物理世界を同一視するな」だと思うんですよ。

dif_engine @dif_engine

話を戻すと、公理的集合論を「ちゃんと」やってたら言語とか推論規則だとかに馴染みがあるはずなので、E.Nelsonの internal set theory は学びやすいと思うんですよ（いつもの結論に到達した）。

dif_engine @dif_engine

そんなに素晴らしいならなんで解説書とか増えないのかって気もしますけど、Nelsonは天才だから14ページくらいにぎっしり書いてあって、あれを薄く伸ばしたような本を書くのは気が引ける、そういうことかもしれない（てきとう）。

dif_engine @dif_engine

A.Robertによる教科書もありますが、エスプリの効いた一コマ漫画がところどころにあって、ああいうのにイラッと来る人はいるだろうな～と思いました。