- site
- https://sno2wman.net
- Scrapbox
- https://scrapbox.io/sno2wman
- https://twitter.com/SnO2WMaN
- GitHub
- https://github.com/SnO2WMaN
嘘つきのパラドクス
2022年 11月 に登録
このアカウントでは
- 論理学に関する様々な話題
- 命題論理あるいは様相論理の諸々の結果のLean4による形式化の進捗
- 開発中の音MADのデータベースOtoMADB(https://www.otomadb.com)の進捗
- 日報
などが放送される予定です。よろしくおねがいします。
証明可能性論理の参考文献の「どこかに不動点を扱うので近い」みたいな理由で様相μ計算の話がチラッと出ていたという記憶の一点で最近触れてみたがどう考えても人間が取り扱えるものではなさすぎる
名は体を表すので名字をFalsemannにしたい
第一線の人でもSahlqvist論理式のSahlqvistの読み方が何なのかははっきりしていないらしくてそんな…と思った
近況: 「容易に示せる」→ 容易に示せるのか〜 → シッチャカメッチャカに…
#日報メモ 調べてないからわからないが国会図書館って本の帯はともかくとしてカバーも廃棄して記録してないのか？
ドキュメントを流し読みしているのが一番悪いとはいえMathlib4の証明を読んで「こんなtacticsあるんだ」みたいな発見をすることが多々あり、さておきLean4のドキュメントは利用例も含めて少なすぎるので、日本語圏での普及を目的として何かしらのWikiとかを作って啓蒙/連帯したすぎる
長らく1100回ぐらい手動で行っていた日報のツイートはここでは自動で投稿するようにしたい
近況は標準様相論理の完全性定理をLean4で形式化しており、無事に命題論理の段階で失敗している
ここは静かで、寂しい
- site
- https://sno2wman.net
- Scrapbox
- https://scrapbox.io/sno2wman
- https://twitter.com/SnO2WMaN
- GitHub
- https://github.com/SnO2WMaN
嘘つきのパラドクス
2022年 11月 に登録
