feat(Modal): Deduction System based on Inference Rules Set

[SnO2WMaN]

#90 (comment) の指摘を受けて．

• maxmを前提が空のRuleとすれば良いというのはそうだが，実際やってみると全てがRulesに入ってしまい（集合操作としては自明であっても）微妙に操作がし辛いため一旦maxmは残している．
• antecendentsがSetだと上段が無限個並んだ推論規則みたいなものを考えることが出来てしまうためListにした．が別におそらくどちらでも実際上は構わないと思う．

今回はとりあえずModalLogicのDeductionを控えめに修正したが，今後Deductionを共通化してLogic以下に移動させようと思う．が軽く試した感じではあまりにも煩雑になりすぎるし，帰納法自体を別途用意しなければまともに証明を書き下すのも困難なので長期的な話になると思う．

[iehality]

前提をSetにしたのはomega-ruleのような規則を排除しないためだった．様相論理の場合はそのような規則はなさそうなのでListでも良いとは思う．maxmについては，代わりに次のような補題を使えば無くてもほとんど同様に操作できると思う．

def Rules.Axiom (𝓡 : Rules α) : Set (Formula α) := {p | ⟨∅, p⟩ ∈ 𝓡}

def Deduction.maxm {p} (hp : p ∈ 𝓡.Axiom) : 𝓡 ⊢ p := ...

[SnO2WMaN]

まだちゃんと確かめていないのだが，例えばNecOnly（推論規則をネセシテーションしか持たない）とそれに関する帰納法はかなり有用なのだが（正規様相論理はそうなので），公理規則を入れると微妙にNecOnlyであることのチェックが面倒になりかつその帰納法が使えなくなってしまいそう．（MPを別立てで考える場合ではMP + Nec = ?とすればよいが，公理を入れることができると自由になってしまう）

実用を考えても上段が0の推論規則は特別視しても良いような気もする．アドホックな解決ではあると思うが

[SnO2WMaN]

FYI: 試しで全てを共通化してLogic/Logic以下に置こうとした残骸が下記ブランチにあるが，毎回このような帰納法をRule集合に応じて定義する必要が発生して壊滅的になってしまった．（上手くやればどうにかなるかもしれないが…）

5d84b5f#diff-bfdfb53a91bc05494494cb5f665c9567201e9582a8694002bd17f89d391e1a2aR147-R179

それはそれとして，Logic以下に置くとLO.Deductionは名前が被るので良い名前を考えたい．ProofSystemやFregeSystemとかだろうか？（後者の用法が正しいかはわからない）

[iehality]

FYI: 試しで全てを共通化してLogic/Logic以下に置こうとした残骸が下記ブランチにあるが，毎回このような帰納法をRule集合に応じて定義する必要が発生して壊滅的になってしまった．（上手くやればどうにかなるかもしれないが…）

5d84b5f#diff-bfdfb53a91bc05494494cb5f665c9567201e9582a8694002bd17f89d391e1a2aR147-R179

それはそれとして，Logic以下に置くとLO.Deductionは名前が被るので良い名前を考えたい．ProofSystemやFregeSystemとかだろうか？（後者の用法が正しいかはわからない）

Logic/Logic下への一般化はあまり利益がない気がしてきた．利用方法としては，個別に定義した証明体系との同型性を示して，証明論に関する結果を一般的に述べるとかだと思うが，これらは帰結に一つの論理式しか現れない証明体系とは相性が悪い気がする（シークエント計算などに関して似たようなことを示せば便利かもしれないが）．名前については，推論規則から生成される証明ということでRules.GeneratedProofとかどうだろう．

[SnO2WMaN]

今後どういう形で上手く纏めるかなどは実際に形式化を進める中で実践的に修正していくことにして， #90 (comment) の問題自体は解消されたので一旦これでマージする予定で．