Documentation

Foundation.Modal.PLoN.Soundness

source
theorem LO.Modal.PLoN.sound {α : Type u_1} {φ : LO.Modal.Formula α} {H : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : H.DefinesPLoNFrameClass 𝔽) (d : H ⊢! φ) :
𝔽 ⊧ φ
source
theorem LO.Modal.PLoN.sound_of_defines {α : Type u_1} {H : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : H.DefinesPLoNFrameClass 𝔽) :
LO.Sound H 𝔽
source
theorem LO.Modal.PLoN.unprovable_bot_of_nonempty_frameclass {α : Type u_1} {H : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : H.DefinesPLoNFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
H ⊬ ⊥
source
theorem LO.Modal.PLoN.consistent_of_defines {α : Type u_1} {H : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : H.DefinesPLoNFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) :
LO.System.Consistent H
source
instance LO.Modal.PLoN.instSoundHilbertFormulaFrameClassNAllFrameClass {α : Type u_1} :
LO.Sound (LO.Modal.Hilbert.N α) (LO.Modal.PLoN.AllFrameClass α)
Equations
  • ⋯ = ⋯
source
instance LO.Modal.PLoN.instConsistentFormulaHilbertN {α : Type u_1} :
LO.System.Consistent (LO.Modal.Hilbert.N α)
Equations
  • ⋯ = ⋯