Soundness

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

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

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

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

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