feat(Normal Modal): Strength of Logics Part.1

[SnO2WMaN]

TODO

• Strong Soundness: Γ ⊢ᴹ[Λ]! p → Γ ⊨ᴹ[(𝔽(Λ) : FrameClass β)] p
• Consequence Weakening: (h : Λ₁ ⪯ᴸ Λ₂): Γ ⊨ᴹ[(𝔽(Λ₂) : FrameClass α)] p → Γ ⊨ᴹ[(𝔽(Λ₁) : FrameClass α)] p
• Property on strict logic stronger

Optional

CompletenessとLogic.FrameClassDefinabilityの証明はAxiomSetに依らずほとんど同じなのでマクロなどを駆使して再利用できるようにしたい（さもなければmodal cubeの残りの論理に対して全く同じ証明を10個ほど書かなければならないため，コード量がただただかさむ）

[SnO2WMaN]

あまりにもコミットが積み上がったので一旦これでPRとしては完了したものとしてreadyにする．示したものは以下．

• 𝐒𝟒 <ᴸ 𝐒𝟓: 𝐒𝟓は𝐒𝟒より真に強い
• 𝐒𝟓 =ᴸ 𝐊𝐓𝟒𝐁: 𝐒𝟓は𝐊𝐓𝟒𝐁と同程度の強さ
• 強健全性定理: Γ ⊢ᴹ[Λ]! p → Γ ⊨ᴹ[(𝔽(Λ) : FrameClass β)] p

[SnO2WMaN]

rebaseして現行の修正分に合わせた．

[iehality]

Logic/HilbertStyle.leanを削除しLogic/HilbertStyle2.leanはLogic/Deduction.leanに改名しました。また命題直感主義論理の証明体系をSystemのインスタンスとして定義し直していますが、Systemの根幹部分をDeductionと融合させたので本質的な問題はないはずです（突然大規模な変更を加えてしまってすみません）。これは問題はなさそうなのでマージします。