Formalized Formal Logic

3.1. Kripke Semantics

3.1.1. Soundness

🔗theorem
LO.Modal.Kripke.instSound_of_validates_axioms {Ax : Axiom ℕ}
  {C : Kripke.FrameClass} (hV : C ⊧* Ax) : Sound (Hilbert.Normal Ax) C
LO.Modal.Kripke.instSound_of_validates_axioms
  {Ax : Axiom ℕ} {C : Kripke.FrameClass}
  (hV : C ⊧* Ax) :
  Sound (Hilbert.Normal Ax) C

3.1.2. For Modal.K

🔗theorem
LO.Modal.K.Kripke.sound : Sound Modal.K Kripke.FrameClass.K
LO.Modal.K.Kripke.sound :
  Sound Modal.K Kripke.FrameClass.K
🔗theorem
LO.Modal.K.Kripke.complete : Complete Modal.K Kripke.FrameClass.K
LO.Modal.K.Kripke.complete :
  Complete Modal.K Kripke.FrameClass.K