Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 106

加算無限じゃない無限集合に関する定理を Coq とかで証明できるのか気になってる。ACL2 だとまず無理だと思う(無限集合を扱えないので……)

時間があれば全ての問題を解いて全ての証明を完全に理解したいとは思う。

とりあえず順序数は本当によく分かってなかったけど ACL2 で必要になってしまう難解概念だったんで学べてよかった。やはり学ぶ順番が重要で Wikipedia で順序数とかいきなり見ても分かるわけがない。え、順序って何……、整列集合って何……ってなって死ぬでしょ。

選択公理というものがあるのは知ってたんだけど、そもそも集合の無限分割という概念が分かってなかったんで、選択公理がどういうことか知らなかったので勉強になった。細部までは理解できていないんだけど結構コアとなる概念については学べたと思う。

あと少なくとも集合の基数についていえば 0 の 0 乗は 1 であることが分かった。理由は定義域が空集合の関数は空関数しかないから。

有理数全体の集合の濃度よりも実数全体の集合の濃度の方が大きいことは知られてると思うんだけど、実数上で有理数が稠密であることはあまり知られていないのでは？

昨日まったく同じことを言った気がするんだけど実数上で有理数が稠密なのは結構衝撃的なんだけどこれはなかなかやばいと思う。これの証明は理解できた。

それにもかかわらず、有理数と実数は対等でない(一対一対応を作れない)というのは不思議で仕方がない。

何が問題なのかというと私にはそれが F に見えなかったというのが一番大きい。なんかフォントによって大分形違うし。

でもこの二つのおかげでなんか数学耐性ができた。フラクトゥール文字が突然でてきても気にせず頑張って調べればいいだけ。

@tacumi いや、集合論の初学者だし日本語の本なんで……。

羃集合を表わすやつもフラクトゥールの P が使われて意味分からんかった。あれは power set だから P なんだろうけど、それをちゃんと暗黙の了解じゃなくてしっかりと根拠を明示的に書いて欲しい。数学書ってどれもこんな感じなの？

数学界の暗黙の了解みたいなやつ困る。集合族がなんで ???? なのか全然分かんなかったし読めなかった。これはフラクトゥールの F であり、Family of sets だから F ということは本だけ読んでても分からない。

この本、フラクトゥール文字は常識だと思っているのかフラクトゥールが出てきたときには何も説明がなかった。それにもかかわらずドイツ小文字とヘブライ文字を出したときにはちゃんと丁寧に読み方まで説明しているところが釈然としなかった。

『集合論・入門』(遊星社)はとりあえず最後まで通読した(理解したとは言ってない)。

整列集合という概念と順序数という概念を学べたのが大きい。これで ACL2 で尺度が自然数でない順序数のような超限帰納法をするときにも安心だ。

まあ、あとは選択公理を仮定すると面白いことが起きるのはよく分かった(証明を理解したとは言ってない)。選択公理からは一般連続体仮説は導けないけど、一般連続体仮説から選択公理が導けるというのには素直に感動した(証明を理解したとは言ってない)。

Spacemacs とか evil-mode とかでも EXWM できるのかはちょっと気になる。

あと、別のタイル型のウィンドウマネージャを使おうとすると、操作体系を新しく学習したり、Emacs の操作体系とちょっとづれてて混乱したりするんでやっぱ Emacs をウィンドウマネージャにするのが一番楽だと思う。

いまはメイン環境が EXWM になっているので、PC を起動しているときに Emacs が起動していない時間はほとんどない。org-capture をどこからでも発動できるのでとっても便利でいい。

Emacs を evil-mode じゃない方法で使うには実は指の長さと指の強度という身体的なパラメータが重要になってしまうんじゃないかという可能性について最近は考えるようになった。私はなんか昔バレーボールをやってたせいなのか知らないんだけど比較的に指が長くて太いみたいなんだよな。そのために Emacs の小指問題について聞いても最初はピンとこなかったところがある。

nvi はまれに使ってる。

Emacs の中で vi の操作体系にするモードが evil-mode って呼ばれてるの思い出した。私は小指が強いので使ったことがない。