add(Modal/Kripke): Rewriting to only Model based semantics

[SnO2WMaN]

close #789

[SnO2WMaN]

LO.Modal.K.iff_provable_valid_all_kripkeModel.{u} {α : Type u} {φ : Formula α} [DecidableEq α] [Encodable α] [Entailment.K (Modal.K α)] : Modal.K α ⊢ φ ↔ ∀ {κ : Type u} [_ : Nonempty κ] (M : KripkeModel κ α), M ⊧ φ

[SnO2WMaN]

universeに関してより自由なKripke意味論にはなっているが，こんなに細かいことを気にしたいかというと実用上は…

[iehality]

実際に取り組むことがあるかわからないが，強制様相論理みたいなものを考えるなら集合論のモデル（in Type 1）をWorld にとる Kripke モデルなどを考えることが自然にあると思うので，できるなら universe は固定しないほうが良いと思う．

[SnO2WMaN]

思ったのでメモ書き．

今回に関しては特に気にする必要は無いのだが，より一般に考えるとフレームは論理式の情報に依存してはいる，という気がしてきた．例えば多様相の様相論理を考えると各様相毎に関係が生えているはずで，この様相たちの個数やアリティなどは論理式の定義に依拠していると考えられる．monomodalである n = 1 の場合は特殊例として充足関係などがfix出来ていると見ることが出来ると思う．

実装上の問題として，フレームレベルの充足性でSemanticsに関する諸々の議論を再利用したいが，以下は定義出来ない（随分前にも同様に困ったが）から，Fにαを何らか依存させる正当化が欲しい．
実際 NのフレームがKripkeフレームの一般化であって，これは論理式に依存している．

def Validates (F : KripkeFrame κ) (φ : Formula α) := ∀ (M : KripkeModel F α), M ⊧ φ

instance {κ : Type u} [Inhabited κ] {α : Type v} : Semantics (KripkeFrame κ) (Formula α) where
  Models := Validates

[SnO2WMaN]

ForcingRelation.AllForces.falsum の仮定が Nonempty ではなく Inhabited なのは何かしら意図があるのだろうか？現状のKripke意味論のWorldの仮定はNonemptyにしているので微妙に合ってない（といっても1行ぐらいの差だが）

[iehality]

ForcingRelation.AllForces.falsum の仮定が Nonempty ではなく Inhabited なのは何かしら意図があるのだろうか？現状のKripke意味論のWorldの仮定はNonemptyにしているので微妙に合ってない（といっても1行ぐらいの差だが）

とくに意図はなかった．Nonempty に変えるべきだと思う．