いつのまにか、私は様相述語論理の専門家ということになってしまった。内容は面白い。っていうか Kripke frame が役に立たない。だから証明論的な体系をコンピューター上の定理証明支援系(Agda)に実装することになる。・・・これって、「意味論」と呼んでい…

朝から雨、昼にかけて強くなる。起床は9時、日ごとに時間が遅くなる。出勤して雑用と論文読み、20時半まで。帰る頃には雨があがっていた。 画像がぼけていてわかりにくいが、Oxford Textbooks of Logic は、通称 OTL らしく、背表紙に OTL と銘打ってあるの…