SnO₂WMaN @sno2wman@fedibird.com

標準様相論理の強完全性定理のコミットがマージされた．今後は有限モデル性などを示す予定．

https://github.com/iehality/lean4-logic/commit/678d96629bf0b1ffab87563c1066e63cdb11acb3

#Lean4

@palalansouki

おめでとう！

Gödel-Mckinsey-Tarskiの定理を直観主義命題論理=S4だけでなく古典命題論理=S5などにも一般化できる事実を知らなかった

https://liewecmays.net/articles/modal-logic_possible-world-semantics_propositional#直観主義論理との関係

証明可能性論理の形式化のために最近少しずつやっているが，可証性述語が存在する算術が不動点補題を満たし導出可能性条件/形式化された完全性定理などを満たすならば，不完全性定理やLöbの定理などが証明できるという事実をLean4で形式化していた（どうやって可証性述語をとったりそのような条件を満たすかを示すかは一切触れていない）

https://github.com/SnO2WMaN/lean4-modallogic/blob/896246058108e612671e5f0eae4da6d9cc1fad86/ModalLogic/Arithmetic/IT1.lean#L38-L44

松本『復刊　数理論理学』には様相論理の入門編があったが古すぎてLewisのS1~S5ベースで議論しておりKripke意味論とかについて一切触れていなくてすごかった

（Taitの？）片側シーケント計算が結局の所どういう点で証明論的な分析や形式化において良い点があるのかをいまいち把握出来ていないのと、様相論理のシーケント計算におけるそれの文献は遥かに無さそうという点で迷っている（GLのTait計算は見たことがあるが論文は結局読めていない）

https://link.springer.com/book/10.1007/978-94-010-0411-4

> M. Fitting; "Types, Tableaus, and Gödel’s God"

Gödel Godが何かは知ってはいるけど、それにしても並べられると字面が物騒すぎる

Boolosによると「第2不完全性定理を用いたLöbの定理の証明」は1966年のKripkeに帰するらしくKripke何でもやりすぎと思った

多分これなのだろうけどJaparidzeがDzhaparidzeともスペリングされるのでわけがわからないことになっている

https://scrapbox.io/sno2wman/可証性論理D

冬はG.Boolos; "The Provability of Logic"をチビチビと読んでいこう

OtoMADBの開発をしたい一方で、算術的完全性定理の証明（いまだにわかっていない）や証明可能性論理の発展的な話題にも触れたいというジレンマに挟まれて大変なことになっている
少なくともOtoMADBがクローンしてdocker compose up -dなどを済ませればローカルでも動かせるような環境であれば他の開発者（いるのか？）もコントリビュートしやすいとは思うが、現状そうなっていない、主にAuth0周りが原因で…

日報(2023.09.20)

https://scrapbox.io/sno2wman/2023.09.20

日報(2023.09.19)

https://scrapbox.io/sno2wman/2023.09.19

このように登録できるように

https://www.otomadb.com/mads/1803

Youtubeの音MADをWeb側からも登録できるようになった　これも皆さんには関係のないことではありますが…

#OtoMADB

日報(2023.09.18)

https://scrapbox.io/sno2wman/2023.09.18