theorem LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.soundness_frameclass {Ax : Axiom ℕ} {φ : Formula ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) : Hilbert.Minimal Ax ⊢ φ → C ⊧ φ

instance LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.instFrameClassSound {Ax : Axiom ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) : Sound (Hilbert.Minimal Ax) C

theorem LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.consistent_of_sound_frameclass {Ax : Axiom ℕ} (C : Veltman.FrameClass) (C_nonempty : Set.Nonempty C) [sound : Sound (Hilbert.Minimal Ax) C] : Entailment.Consistent (Hilbert.Minimal Ax)

theorem LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.soundness_frame {Ax : Axiom ℕ} {φ : Formula ℕ} {F : Veltman.Frame} (hV : F ⊧* Ax) : Hilbert.Minimal Ax ⊢ φ → F ⊧ φ

theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.soundness_frameclass {Ax : Axiom ℕ} {φ : Formula ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) : Basic Ax ⊢ φ → C ⊧ φ

instance LO.InterpretabilityLogic.Hilbert.Basic.Veltman.instFrameClassSound {Ax : Axiom ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) : Sound (Basic Ax) C

theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.consistent_of_sound_frameclass {Ax : Axiom ℕ} (C : Veltman.FrameClass) (C_nonempty : Set.Nonempty C) [sound : Sound (Basic Ax) C] : Entailment.Consistent (Basic Ax)

theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.soundness_frame {Ax : Axiom ℕ} {φ : Formula ℕ} {F : Veltman.Frame} [F.IsGL] (hV : F ⊧* Ax) : Basic Ax ⊢ φ → F ⊧ φ

instance LO.InterpretabilityLogic.Hilbert.Basic.Veltman.instFrameSound {Ax : Axiom ℕ} {F : Veltman.Frame} [F.IsGL] (hV : F ⊧* Ax) : Sound (Basic Ax) F

theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.consistent_of_sound_frame {Ax : Axiom ℕ} (F : Veltman.Frame) [sound : Sound (Basic Ax) F] : Entailment.Consistent (Basic Ax)

theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.weakerThan_of_subset_frameClass {Ax₁ Ax₂ : Axiom ℕ} (C₁ C₂ : Veltman.FrameClass) (hC : C₂ ⊆ C₁) [Sound (Basic Ax₁) C₁] [Complete (Basic Ax₂) C₂] : Basic Ax₁ ⪯ Basic Ax₂