2024.11.11
https://gyazo.com/f7593ff0dcf3f10ae22904c7e83ba319
前：
2024.11.10
後：
2024.11.12
#日報
メモ
FormalizedFormalLogicで形式化してある地味だけどちゃんとした証明を見たことがない事実：Łukasiewiczの3公理で古典命題論理(= 最小論理 + 爆発律 + 排中律)がちゃんと実現出来ることのHilbert流での証明
https://github.com/FormalizedFormalLogic/Foundation/blob/master/Foundation/Logic/HilbertStyle/Lukasiewicz.lean
メモ
カップ麺うまいなと思いながら一日１回食べてる
食事が一日１回だから毎日カップ麺食ってることになりますね
照
死のう