iehality
Rename and Move HilbertStyle to Propositional Logic
そろそろ改修したいこととして，
-
HilbertStyleという名前はそろそろ古く，ちゃんとEntailmentに書き直すべきだと思う． - そもそもあるべき場所としては
Logic以下ではなくPropositionalに置かれているべきな気もする（Modalはそうなっているので）． - いくつか古典論理を仮定する部分とそうでないものがごちゃごちゃになっておりそのたびに
variableの操作がめちゃくちゃになっているのでClassicalとIntuitionisticなどにファイルを分離する．
やるとしたら #288 と並行してやるべきかもしれない．
Łukasiewicz流の命名だが，N(∼)とE(⭤)は良いのだが，他の論理記号の略称は自然ではないように思える．普通の略称として次のように改めたらどうだろうか．
-
➝:C->I(Imply) -
⋏:K->A(And) -
⋎:A→O(Or)
これらの記法は Łukasiewicz のオリジナルの記法を真似たものだった （cf. https://plato.stanford.edu/entries/lukasiewicz/polish-notation.html ）．独自に記法を作るよりすでによく知られているものを使ったほうが良いと思うのだが，どうだろうか．
私の慣れの問題な気もするので改めるのはなかったことにしてください．
それとは別の問題として，命題変数無しでŁukasiewicz記法を使う場合には論理式の形は一意に決まらないような気もするがどうだろうか．（例えばCCはp➝q➝rでもp➝(q➝r)の両方の解釈が有り得る）．命題変数自体の選び方や順番には依存してしまうがこれは書かなければならない情報であると思う．改修前のClでは書いていた． https://github.com/FormalizedFormalLogic/Foundation/blob/1301a4f129f6cf8288308f2df3d0bca3865edc41/Foundation/Logic/HilbertStyle/Cl.lean
実用性を考えると，定理名はそれを検索しやすいものにしたいので主張から一意に定まるものにしたい．メタ変数記号を書いてしまうと変数名の分だけ自由があるので避けたい（ mathlib の naming convention でも複数の解釈ができたとしてもメタ変数記号は書かない）．どうしても被る場合は _right, _left ' などを後置すべきだと思う．加えて経験的に（少なくとも現行の HilbertStyle/Supplimental.lean 下のものは）被ることは少ない．