2024.11.30

https://gyazo.com/7bfa60087b21f1a841444bb35ed2f207

思った

部分構造論理で交換規則を棄却する：「φ∧ψとψ∧φは同値ではない」が量子論理に対応するみたいな話を聞いたときに「おもしろいがなぜそんなことを…」とは思ったのだけど、量子論などに精通していればなるほど！となる内容だったのだろうかと今でも思う

これ交換則だからLambek計算とかの話かもしれん（分配則だったかも）

メモ

仮にMathlibに移管したとして、Leanのアップデート対応や定理の追加/リファクタリングなどのメンテナンスを今後ずっと私(達)がやるなり論理学とLeanに詳しいメンテナを捕まえてくる必要があり、それなりに忙殺されそうであまり前向きではないというのもある

知った