Documentation

Foundation.InterpretabilityLogic.Veltman.Hilbert

source
theorem LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.soundness_frameclass {Ax : Axiom ℕ} {φ : Formula ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) :
Hilbert.Minimal Ax ⊢ φ → C ⊧ φ
source
def LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.instFrameClassSound {Ax : Axiom ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) :
Sound (Hilbert.Minimal Ax) C
Equations
  • ⋯ = ⋯
Instances For
    source
    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)
    source
    theorem LO.InterpretabilityLogic.Hilbert.Minimal.Veltman.soundness_frame {Ax : Axiom ℕ} {φ : Formula ℕ} {F : Veltman.Frame} (hV : F ⊧* Ax) :
    Hilbert.Minimal Ax ⊢ φ → F ⊧ φ
    source
    theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.soundness_frameclass {Ax : Axiom ℕ} {φ : Formula ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) :
    Basic Ax ⊢ φ → C ⊧ φ
    source
    def LO.InterpretabilityLogic.Hilbert.Basic.Veltman.instFrameClassSound {Ax : Axiom ℕ} {C : Veltman.FrameClass} (hV : C ⊧* Ax) :
    Sound (Basic Ax) C
    Equations
    • ⋯ = ⋯
    Instances For
      source
      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)
      source
      theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.soundness_frame {Ax : Axiom ℕ} {φ : Formula ℕ} {F : Veltman.Frame} [F.IsGL] (hV : F ⊧* Ax) :
      Basic Ax ⊢ φ → F ⊧ φ
      source
      def LO.InterpretabilityLogic.Hilbert.Basic.Veltman.instFrameSound {Ax : Axiom ℕ} {F : Veltman.Frame} [F.IsGL] (hV : F ⊧* Ax) :
      Sound (Basic Ax) F
      Equations
      • ⋯ = ⋯
      Instances For
        source
        theorem LO.InterpretabilityLogic.Hilbert.Basic.Veltman.consistent_of_sound_frame {Ax : Axiom ℕ} (F : Veltman.Frame) [sound : Sound (Basic Ax) F] :
        Entailment.Consistent (Basic Ax)
        source
        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₂