SnO₂WMaN
SnO₂WMaN
`Finset.box`が重複しており致命的な問題になっているので時間がかかるかもしれない．そもそも `Finset.box` という純粋に論理学的な演算をトップレベルで定義するのもあまり良くないと思っていて `Finset.Logic.box` みたいな名前にするべきだとは思っていたが．ただしこの場合 `s.box` (`s : Finset`) のような記述は出来ず，すごく煩雑になってしまう可能性はある．
> > `Finset.box`が重複しており致命的な問題になっているので時間がかかるかもしれない．そもそも `Finset.box` という純粋に論理学的な演算をトップレベルで定義するのもあまり良くないと思っていて `Finset.Logic.box` みたいな名前にするべきだとは思っていたが．ただしこの場合 `s.box` (`s : Finset`) のような記述は出来ず，すごく煩雑になってしまう可能性はある． > > `instance [LO.Box α] : LO.Box (Finset α)` を定義するのはどうだろうか． そもそも `Finset.box` や `List.box` をなぜか帰納的に定義していてよくわからなかったので別個立てて書き換えておく．
GLでの証明と同じようにカノニカルモデルを濾過法で使う同値類で割ったモデルを考えたがおそらくこれは出来ない気がする．
#123 で必要な道具立て(`complement`など)を用意するのでそれが終わり次第再開．
部分論理式周りのコードはそのうちリファクタリングしたほうが良い気がしてきた。
Part1: #514 Part2: ?
分類定理から出す．おそらく分類定理自体はこの事実と独立．
> 2項関係が木を成している，という定義の形式的な記述をどうすればよいか... Boolosに書いてあった: transな $\prec$ が木であるとは $x \prec z$ かつ $y \prec z$ のとき $x \prec y$, $x = y$, $y \prec x$ のいずれかが成立． ただしこの定義もアドホックで大分違う気がする．
いくつかコメントをつけておいた．表現可能性や対角線補題に関しては大掛かりな変更がいるような気もするので早急に取り掛かるかは任せる．