2024.01.25
https://gyazo.com/ba1f97691f57e6631ef8a8fdce98cc1f
前:
2024.01.24
後:
2024.01.26
#日報
やった(か?)
正規様相論理の完全性定理
の形式化
https://github.com/iehality/lean4-logic/pull/15
終わったーーー!!!!!!!!!!!!!!!!!!
メモ
演繹定理
は計算不能
noncomputable
としたが,そういうものなのだろうか?
実質的に
カット除去
と同じことが起きている.のか?