0926
お昼から仕事。エフェクトをごにょごにょ。説得力あるアニメイションの作りかたみたいなの、ちょっとずつ道具が集まってきたけど、まださっぱりわからない。こういうのの専門家に弟子入りしたい思いがある。
あと結局CollectionViewのself-sizing cellsは壊れているのでしょうか。なんかAutoLayout絡みの警告がガンガン出るのはいいとしても、estimatedSizeの分しかセルが配置されてない？っぽいし、配置されたセルも位置が変だし、だめっぽい。はー、TableViewのほうはそんなことないのかしら。がっかりです。
クリプキは17歳の高校生で様相論理の意味論を完成したそうです。高校生って。プラネタリウムじゃないんだから。（高校生くらいが部活動で作りそうだな～という意図です）
導入する公理の種類が適用可能なフレームの構造と対応するなんて、なんてステキなんでしょう、と思いました。でも、このフレームって概念、直感的な「可能世界」みたいな概念をあんまり反映はしていない気がする。これは僕の知っているものじゃない。じゃあいったい何なんだ。
まあ、古典命題論理がそうであった（たとえば「→」とか）ように、これもそういう模型でしかない、のではあるけれど。公理系がいろいろあるのもそういう事情を反映していそう。たまたま用語が日常語に由来しているというだけで、これはまったく別の記述力を持っていると考えるべき。「◇□Ｐ→□Ｐ」とかちょっと戸惑うし。「（Ｐは必然的である）可能性がある ならば Ｐは必然的である」？？そんなことあるめえよ。僕が勘違いしているのか？
論理学って、要するにある構文の持つ構造を調べたり、それがどういう意味論とぴったり重なるかを調べたりする、みたいな学問なのかしらね、と思いました。たとえば時相論理というやつがあって、これはシステムの検証なんかで依存関係を記述する方法として利用されているらしいのだけど、つまり、ある文法で書ける文字列全体の構造、曖昧さや矛盾が生じないこと、そしてそれに対して適切な意味をつねに与えることができること、なんかを論理学がきちんと調べて保証する、みたいな話なのかな、みたいな。ぜんぜん調べないで言ってますけど。