@[reducible, inline]

abbrev LO.Modal.PLoN.CanonicalFrame {α : Type u} (Λ : LO.Modal.Hilbert α) [Nonempty (LO.Modal.MCT Λ)] : LO.Modal.PLoN.Frame α

Equations

• LO.Modal.PLoN.CanonicalFrame Λ = LO.Modal.PLoN.Frame.mk (LO.Modal.MCT Λ) fun (p : LO.Modal.Formula α) (Ω₁ Ω₂ : LO.Modal.MCT Λ) => ∼□p ∈ Ω₁.theory ∧ ∼p ∈ Ω₂.theory

@[reducible, inline]

abbrev LO.Modal.PLoN.CanonicalModel {α : Type u} (Λ : LO.Modal.Hilbert α) [Nonempty (LO.Modal.MCT Λ)] : LO.Modal.PLoN.Model α

Equations

• LO.Modal.PLoN.CanonicalModel Λ = { Frame := LO.Modal.PLoN.CanonicalFrame Λ, Valuation := fun (Ω : (LO.Modal.PLoN.CanonicalFrame Λ).World) (a : α) => LO.Modal.Formula.atom a ∈ Ω.theory }

instance LO.Modal.PLoN.CanonicalModel.instSatisfies {α : Type u} {Λ : LO.Modal.Hilbert α} [Nonempty (LO.Modal.MCT Λ)] : LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.CanonicalModel Λ).World

Equations

• LO.Modal.PLoN.CanonicalModel.instSatisfies = LO.Modal.Formula.PLoN.Satisfies.semantics (LO.Modal.PLoN.CanonicalModel Λ)

theorem LO.Modal.PLoN.truthlemma {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Nonempty (LO.Modal.MCT Λ)] [Λ.HasNecessitation] {p : LO.Modal.Formula α} {Ω : (LO.Modal.PLoN.CanonicalModel Λ).World} : Ω ⊧ p ↔ p ∈ Ω.theory

theorem LO.Modal.PLoN.complete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Nonempty (LO.Modal.MCT Λ)] [Λ.HasNecessitation] {p : LO.Modal.Formula α} {𝔽 : LO.Modal.PLoN.FrameClass α} (hFC : LO.Modal.PLoN.CanonicalFrame Λ ∈ 𝔽) : 𝔽 ⊧ p → Λ ⊢! p

theorem LO.Modal.PLoN.instComplete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Nonempty (LO.Modal.MCT Λ)] [Λ.HasNecessitation] {𝔽 : LO.Modal.PLoN.FrameClass α} (hFC : LO.Modal.PLoN.CanonicalFrame Λ ∈ 𝔽) : LO.Complete Λ 𝔽

instance LO.Modal.PLoN.instCompleteHilbertFormulaFrameClassNAllFrameClass {α : Type u} [DecidableEq α] : LO.Complete 𝐍 (LO.Modal.PLoN.AllFrameClass α)

Equations

• ⋯ = ⋯