2023.11.15
https://www.youtube.com/watch?v=50R1_i6MhOo
怖すぎる
ウィングスーツ
前：2023.11.14
後：2023.11.16
#日報
メモ
FormalizedFormalLogic/Foundationをフォークして導出可能性条件を用いた不完全性定理の形式化をしようとしていた
https://github.com/SnO2WMaN/lean4-logic/blob/10e517d64972677fb2319a151ec6a74068e52e4f/Logic/Predicate/FirstOrder/Incompleteness/Provability.lean
SnO2WMaN/lean4-modal-logicでは
例えば$ T \vdash \sigma \land \piなら$ T \vdash \sigma，$ T \vdash σ \lrarr πなら$ T \vdash σ \rarr πみたいに，$ T \vdashに関して少なくとも直観主義命題論理が成り立てばOKだった記憶がある
その他$ \mathrm{Pr}_T(x)に関していくつかの事実
これは行けるだろうと思って全部証明を後回しにしているが，普通にどうやればいいのか，そもそも形式化があってるのかはよくわかってない
T ⊢ σとT ⊢! σがあり，自分はT ⊢! σで証明しているが，違うのかもしれない．