Gödelの不完全性定理についてのきちんとした証明(可証性述語を与えるところまでの膨大な構成),Chaitinの不完全性定理,Quineからの流れによるGrzegorczykの算術を介さない不完全性証明,その他のパラドックスの形式化,証明可能性論理などの諸々の話題をTypstでメモ書きすることにした
このアカウントでは
- 論理学に関する様々な話題
- 命題論理あるいは様相論理の諸々の結果のLean4による形式化の進捗
- 開発中の音MADのデータベースOtoMADB(https://www.otomadb.com)の進捗
- 日報
などが放送される予定です。よろしくおねがいします。
標準様相論理の強完全性定理のコミットがマージされた.今後は有限モデル性などを示す予定.
https://github.com/iehality/lean4-logic/commit/678d96629bf0b1ffab87563c1066e63cdb11acb3
アドベントカレンダーつくった!何でも良いので書いてください
この前の様相論理の記事の続きを書きました
様相論理: 可能世界意味論(1階述語論理) - liewecmays
https://liewecmays.net/articles/modal-logic_possible-world-semantics_first-order
Gödel-Mckinsey-Tarskiの定理を直観主義命題論理=S4だけでなく古典命題論理=S5などにも一般化できる事実を知らなかった
https://liewecmays.net/articles/modal-logic_possible-world-semantics_propositional#直観主義論理との関係
証明可能性論理の形式化のために最近少しずつやっているが,可証性述語が存在する算術が不動点補題を満たし導出可能性条件/形式化された完全性定理などを満たすならば,不完全性定理やLöbの定理などが証明できるという事実をLean4で形式化していた(どうやって可証性述語をとったりそのような条件を満たすかを示すかは一切触れていない)
https://link.springer.com/book/10.1007/978-94-010-0411-4
> M. Fitting; "Types, Tableaus, and Gödel’s God"
Gödel Godが何かは知ってはいるけど、それにしても並べられると字面が物騒すぎる
多分これなのだろうけどJaparidzeがDzhaparidzeともスペリングされるのでわけがわからないことになっている
日報(2023.09.20)
日報(2023.09.19)
日報(2023.09.18)
日報(2023.09.17)
嘘つきのパラドクス