SnO₂WMaN @sno2wman@fedibird.com

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

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

#Lean4

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

#OtoMADB

まあいいんじゃないでしょうか

#OtoMADB

どうにかかろうじてマトモな見かけにはしたが、まだ不自然に縦長になってしまっている感はある

終わっている

https://github.com/Ziphil/ZenmlZotica/blob/136a91d9f58438e13666e3dbce3a4f2907f3e35a/test/file/sample.zml#L584-L600

Ziphil氏がメンテナンスしているZenML及びZotica、下のような証明図が比較的?簡潔かつ直感的に記述出来るのいいなと思う

https://ziphil.github.io/ZenmlZoticaDemo/

Girardの論文でフとヲを使っているのをチラ見したことがあるがこれらが何を指しているものなのか及びなぜこの記号で導入したのかはよくわかっていない

https://girard.perso.math.cnrs.fr/trsy4.pdf

究極的にはLemmon/Fitch/Jaśkowski流の自然演繹の書き方っぽいものを普通に自然言語の証明でもやればいいのにと思うし，自分はこれがそもそもScrapboxでの記述にフィットしていたという側面もある

https://plato.stanford.edu/entries/natural-deduction/figdesc.html#figjaskowskiex

G.Boolos, "The Logic of Provability"の表紙はいくらなんでもダサすぎると本当に個人的に思う

皆がこの問題にどのように対応しているのか不明すぎる