2023.06.26
https://gyazo.com/7e46d5056471795616a6e40795cab969
前：
2023.06.25
後：
2023.06.27
#日報
やった
Lean 4
で様相論理を形式化するやつパートn
M. Maggesi, C. P. Brogi; "A Formal Proof of Modal Completeness for Provability Logic"
https://drops.dagstuhl.de/opus/volltexte/2021/13921/pdf/LIPIcs-ITP-2021-26.pdf
Bruno Bentzen; "A Henkin-style completeness proof for the modal logic S5"
https://arxiv.org/abs/1910.01697
思った
Łukasiewiczの3公理図式
しか用意していない状態での
Hilbert流演繹体系
はムズい．
というか全然証明がすごい面倒（自明）
Lean 4
の
ProofWidgets
意味不明な技術すぎてすごすぎる
メモ
定理証明支援系での論理の形式化