Soundness

theorem LO.Modal.Kripke.Hilbert.soundness_of_FrameClass_definedBy_axiomInstances {H : Hilbert ℕ} {φ : Formula ℕ} {C : FrameClass} [defined : C.DefinedBy H.axiomInstances] : H ⊢! φ → C ⊧ φ

instance LO.Modal.Kripke.Hilbert.instDefinedByAxiomInstancesNatOfAxioms {H : Hilbert ℕ} {C : FrameClass} [defs : C.DefinedBy H.axioms] : C.DefinedBy H.axiomInstances

instance LO.Modal.Kripke.Hilbert.instSoundHilbertNatFormulaFrameClassOfDefinedByAxioms {H : Hilbert ℕ} {C : FrameClass} [C.DefinedBy H.axioms] : Sound H C

theorem LO.Modal.Kripke.Hilbert.consistent_of_FrameClass_aux {H : Hilbert ℕ} {C : FrameClass} [nonempty : C.IsNonempty] [sound : Sound H C] : H ⊬ ⊥

theorem LO.Modal.Kripke.Hilbert.consistent_of_FrameClass {H : Hilbert ℕ} (C : FrameClass) [C.IsNonempty] [Sound H C] : Entailment.Consistent H

theorem LO.Modal.Kripke.Hilbert.soundness_of_FiniteFrameClass_definedBy_axiomInstances {H : Hilbert ℕ} {φ : Formula ℕ} {C : FiniteFrameClass} [defined : C.DefinedBy H.axiomInstances] : H ⊢! φ → C ⊧ φ

instance LO.Modal.Kripke.Hilbert.instDefinedByAxiomInstancesNatOfAxioms_1 {H : Hilbert ℕ} {C : FiniteFrameClass} [defs : C.DefinedBy H.axioms] : C.DefinedBy H.axiomInstances

instance LO.Modal.Kripke.Hilbert.instSoundHilbertNatFormulaFiniteFrameClassOfDefinedByAxioms {H : Hilbert ℕ} {C : FiniteFrameClass} [C.DefinedBy H.axioms] : Sound H C

theorem LO.Modal.Kripke.Hilbert.consistent_of_FiniteFrameClass_aux {H : Hilbert ℕ} {C : FiniteFrameClass} [nonempty : C.IsNonempty] [sound : Sound H C] : H ⊬ ⊥

theorem LO.Modal.Kripke.Hilbert.consistent_of_FiniteFrameClass {H : Hilbert ℕ} (C : FiniteFrameClass) [C.IsNonempty] [Sound H C] : Entailment.Consistent H