SnO₂WMaN
SnO₂WMaN
可証性述語の本質的性質を捉えるために入れておいたが，確かに形式化の上でそうである必要は特になかった．修正します．
書き直しを試してみたが，却ってベース理論が適切に推論されずに冗長に引数を指定する必要が生じて煩雑になってしまう気がする．困るなら修正するが，そうでないならこのままでも良いとも思う．
とりあえず連絡しておくと，CIで"Check dependencies consistency"がエラーになっているとき，`docbuild`の中のMathlibなどの依存関係とFoundationの（つまりrootの）依存関係のバージョンが食い違っている．これがズレているとCI上のキャッシュが上手く効かずビルドに凄まじい時間がかかってしまい各ジョブの実行可能時間を超えてエラーになることがある．まずはそれを修正してみてはどうだろうか．
docbuildのlake updateは現状手動で適当にやる方針です
1. 現状のこのブランチの修正を #308 に取り込んだ． 2. おそらく唯一の問題点`FixedPoint`の`diagonal`でメモリリークする原因だが全くわからない．Zulipなどで情報を募ったほうがよいかもしれない．
Łukasiewicz流の命名だが，`N`(`∼`)と`E`(`⭤`)は良いのだが，他の論理記号の略称は自然ではないように思える．普通の略称として次のように改めたらどうだろうか． - `➝`: `C` -> `I` (Imply) - `⋏`: `K` -> `A` (And) - `⋎`: `A` → `O` (Or)
私の慣れの問題な気もするので改めるのはなかったことにしてください． それとは別の問題として，命題変数無しでŁukasiewicz記法を使う場合には論理式の形は一意に決まらないような気もするがどうだろうか．（例えば`CC`は`p➝q➝r`でも`p➝(q➝r)`の両方の解釈が有り得る）．命題変数自体の選び方や順番には依存してしまうがこれは書かなければならない情報であると思う．改修前のClでは書いていた． https://github.com/FormalizedFormalLogic/Foundation/blob/1301a4f129f6cf8288308f2df3d0bca3865edc41/Foundation/Logic/HilbertStyle/Cl.lean
~~TODO: 名前が良くないのでK4M, S4Mに変更する．~~
健全性を示すことは完全性を示すことより難しい（超限帰納法を使うのと，そもそも証明がかなりテクニカルでその証明の細部を紛失した）．このPRではとりあえず完全性だけを形式化することを目標とする．
勘違いしていたが本質的に難しい部分はフレーム定義性だった．