2025.08.02
https://gyazo.com/bd85fd1a5509c5ce3a387be8062cc722
メモ
様相論理GLのシークエント計算のカット除去は1980年ぐらいから様々な方法が提案されて40年ぐらい結局合ってるのか片が付かず（特に論理式の「集まり」に関する議論の細部が），Coqで形式化して多分合ってるでしょうということになっているらしいのだけど，そういう感じのこともしたい やった
https://gyazo.com/96f8e674d7d6af95127b7dc0e4feb4f4
メモ
やろうと思っている事実の形式化．ここまではできそう．これ以上に面白く初等的な事実があれば教えてほしい．
$ \sf PA^-は$ \sf Qより真に強い．
$ \sf Qで何が証明できないのかはよくわからない．
$ \forall x.(0 + x = x)とかかができないのでそれを証明すれば良さそう．
これやりかた完全に忘れてて$ \sf Qの公理を全部連結すればいいということしか覚えてなくて，定理の集合が再帰的にならない，みたいな事実を使うことを忘れていた．
実はやってないんじゃないかという気がする定理
メモ
音MADのDJをするにあたって音MADではない音源もあるため映像をどうするかという問題があり，自分のPCでRekordboxの映像機能を使うとスペックの問題で破滅的になるのは目に見えているので簡単なソフトを自作してその場でシャカシャカ動いて音声と映像を同時に流すことを画策している
そんな時間あるんですか？