@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

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

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

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

Equations

• ⋯ = ⋯