Documentation

Logic.Modal.Standard.Kripke.Soundness

source
theorem LO.Modal.Standard.Kripke.sound {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} {p : LO.Modal.Standard.Formula α} (defines : Ax.DefinesKripkeFrameClass 𝔽) (d : 𝝂Ax ⊢! p) :
𝔽.alt ⊧ p
source
theorem LO.Modal.Standard.Kripke.sound_of_defines {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (defines : Ax.DefinesKripkeFrameClass 𝔽) :
LO.Sound (𝝂Ax) 𝔽.alt
source
theorem LO.Modal.Standard.Kripke.unprovable_bot_of_nonempty_frameClass {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (defines : Ax.DefinesKripkeFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
𝝂Ax ⊬! ⊥
source
theorem LO.Modal.Standard.Kripke.consistent_of_defines {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (defines : Ax.DefinesKripkeFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
LO.System.Consistent 𝝂Ax
source
instance LO.Modal.Standard.Kripke.K_sound {α : Type u_1} :
LO.Sound 𝐊 LO.Modal.Standard.Kripke.AllFrameClass.alt
Equations
  • ⋯ = ⋯
source
instance LO.Modal.Standard.Kripke.K_consistent' {α : Type u_1} :
LO.System.Consistent 𝝂𝗞
Equations
  • ⋯ = ⋯
source
instance LO.Modal.Standard.Kripke.K_consistent {α : Type u_1} :
LO.System.Consistent 𝐊
Equations
  • ⋯ = ⋯
source
theorem LO.Modal.Standard.Kripke.finite_sound {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FiniteFrameClass} {p : LO.Modal.Standard.Formula α} (defines : Ax.FinitelyDefinesKripkeFrameClass 𝔽) (d : 𝝂Ax ⊢! p) :
𝔽.toFrameClass.alt ⊧ p
source
theorem LO.Modal.Standard.Kripke.sound_of_finitely_defines {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FiniteFrameClass} (defines : Ax.FinitelyDefinesKripkeFrameClass 𝔽) :
LO.Sound (𝝂Ax) 𝔽.toFrameClass.alt
source
theorem LO.Modal.Standard.Kripke.unprovable_bot_of_nonempty_finite_frameClass {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FiniteFrameClass} (defines : Ax.FinitelyDefinesKripkeFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
𝝂Ax ⊬! ⊥
source
theorem LO.Modal.Standard.Kripke.consistent_of_finitely_defines {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FiniteFrameClass} (defines : Ax.FinitelyDefinesKripkeFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
LO.System.Consistent 𝝂Ax
source
theorem LO.Modal.Standard.Kripke.restrict_finite {𝔽 : LO.Modal.Standard.Kripke.FrameClass} :
∀ {α : Type u_1} {p : LO.Modal.Standard.Formula α}, 𝔽.alt ⊧ p → 𝔽ꟳ.alt ⊧ p
source
instance LO.Modal.Standard.Kripke.instFiniteSound {α : Type u_1} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [sound : LO.Sound Λ 𝔽.alt] :
LO.Sound Λ 𝔽ꟳ.alt
Equations
  • ⋯ = ⋯
source
instance LO.Modal.Standard.Kripke.K_fin_sound {α : Type u_1} :
LO.Sound 𝐊 LO.Modal.Standard.Kripke.AllFrameClassꟳ.alt
Equations
  • ⋯ = ⋯
source
theorem LO.Modal.Standard.K_strictlyWeakerThan_KD {α : Type u_1} [Inhabited α] [DecidableEq α] :
𝐊 <ₛ 𝐊𝐃
source
theorem LO.Modal.Standard.K_strictlyWeakerThan_K4 {α : Type u_1} [Inhabited α] [DecidableEq α] :
𝐊 <ₛ 𝐊𝟒
source
theorem LO.Modal.Standard.K_strictlyWeakerThan_KB {α : Type u_1} [Inhabited α] [DecidableEq α] :
𝐊 <ₛ 𝐊𝐁
source
theorem LO.Modal.Standard.K_strictlyWeakerThan_K5 {α : Type u_1} [Inhabited α] [DecidableEq α] :
𝐊 <ₛ 𝐊𝟓