Documentation

Foundation.Modal.PLoN.Soundness

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