theorem LO.Modal.PLoN.sound {α : Type u_1} {p : LO.Modal.Formula α} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) (d : Λ ⊢! p) : 𝔽 ⊧ p

theorem LO.Modal.PLoN.sound_of_defines {α : Type u_1} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) : LO.Sound Λ 𝔽

theorem LO.Modal.PLoN.unprovable_bot_of_nonempty_frameclass {α : Type u_1} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) : Λ ⊬ ⊥

theorem LO.Modal.PLoN.consistent_of_defines {α : Type u_1} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Modal.PLoN.FrameClass α} (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty : Set.Nonempty 𝔽) : LO.System.Consistent Λ

instance LO.Modal.PLoN.instSoundHilbertFormulaFrameClassNAllFrameClass {α : Type u_1} : LO.Sound 𝐍 (LO.Modal.PLoN.AllFrameClass α)

Equations

• ⋯ = ⋯

instance LO.Modal.PLoN.instConsistentFormulaHilbertN {α : Type u_1} : LO.System.Consistent 𝐍

Equations

• ⋯ = ⋯