2024.04.01
https://gyazo.com/004a235be21ba26b14072b1a205b9d4f
前:
2024.03.31
後:
2024.04.02
#日報
思った
2年前からずっとキーボードのテンキーの
/
と
-
の位置が逆であったことにたった今気づいた
思った
入社式たのしーなーたのしーなー
やった
Geach論理
の
フレーム定義性
/
Geach合流性
について
Lean 4
で形式化した
https://github.com/SnO2WMaN/lean4-logic/commit/25c5b6f096ec38fed0584f6fccd859b03a0b049b
あとは
カノニカルモデル
が
Geach合流性
に対応すれば行けます
Geach合流性
って便利すぎる みんなは最初からこれで証明したほうがいい