@[reducible, inline]

abbrev LO.Modal.PLoN.CanonicalFrame {α : Type u} (H : Hilbert α) [Nonempty (MCT H)] : 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 : Hilbert α) [Nonempty (MCT H)] : 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 : Hilbert α} [Nonempty (MCT H)] : Semantics (Formula α) (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 : Hilbert α} [Nonempty (MCT H)] [H.HasNecessitation] {φ : Formula α} {Ω : (CanonicalModel H).World} : Ω ⊧ φ ↔ φ ∈ Ω.theory

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

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

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