Documentation

Logic.Modal.Standard.PLoN.Soundness

source
theorem LO.Modal.Standard.PLoN.sound {α : Type u_1} {p : LO.Modal.Standard.Formula α} {Λ : LO.Modal.Standard.DeductionParameter α} {𝔽 : LO.Modal.Standard.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) (d : Λ ⊢! p) :
𝔽 ⊧ p
source
theorem LO.Modal.Standard.PLoN.sound_of_defines {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {𝔽 : LO.Modal.Standard.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) :
LO.Sound Λ 𝔽
source
theorem LO.Modal.Standard.PLoN.unprovable_bot_of_nonempty_frameclass {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {𝔽 : LO.Modal.Standard.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
Λ ⊬! ⊥
source
theorem LO.Modal.Standard.PLoN.consistent_of_defines {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {𝔽 : LO.Modal.Standard.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
LO.System.Consistent Λ
source
instance LO.Modal.Standard.PLoN.instSoundDeductionParameterFormulaFrameClassNAllFrameClass {α : Type u_1} :
LO.Sound 𝐍 (LO.Modal.Standard.PLoN.AllFrameClass α)
Equations
  • ⋯ = ⋯
source
instance LO.Modal.Standard.PLoN.instConsistentFormulaDeductionParameterN {α : Type u_1} :
LO.System.Consistent 𝐍
Equations
  • ⋯ = ⋯