lean4-logic
lean4-logic copied to clipboard
iehality
Lean4 Logic Formalization
ローカル環境で更新を試すとそれなりに重く時間のかかる作業になってしまうため，定期的にまたは手動で`lake update`をCI上で行い，ビルドが成功するならPRを自動で立てるようなActionがあっても良いかもしれない．
認識論理のように複数（可算無限個）の様相演算子を持つ体系や証明可能性述語などのことを考えると、特定の`box`および`dia`ではなく、`System`上の1項様相演算子が公理Kや公理4の性質を満たす、と定義したほうが汎用的な気がする。 例えば認識論理では`[∀ i, Axiom.K (boxes i)]`のようにしたり、現在のDerivabilityConditionで行われているD1,D2,D3上の実質的な様相論理の計算を使いまわせたりする気がする。
Add framework for sequent calculi. ```lean class SequentCalc₁ {F : outParam Type*} (R : outParam Type*) [Precollection F R] (S : Type*) where Sqt : S → R → Type*...
- `variable`周りの挙動が変わっているが、どう変わったのかがRelease noteに見当たらなかったのでそれなりに大変な書き換えが必要な可能性がある close #116
そろそろ改修したいこととして， 1. `HilbertStyle`という名前はそろそろ古く，ちゃんと`Entailment`に書き直すべきだと思う． 2. そもそもあるべき場所としては`Logic`以下ではなく`Propositional`に置かれているべきな気もする（`Modal`はそうなっているので）． 3. いくつか古典論理を仮定する部分とそうでないものがごちゃごちゃになっておりそのたびに`variable`の操作がめちゃくちゃになっているので`Classical`と`Intuitionistic`などにファイルを分離する． やるとしたら #288 と並行してやるべきかもしれない．