@[reducible, inline]

abbrev LO.Modal.PLoN.canonicalFrame {S : Type u_1} [Entailment S (Formula ℕ)] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] : Frame

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LO.Modal.PLoN.canonicalModel {S : Type u_1} [Entailment S (Formula ℕ)] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] : Model

Equations

• LO.Modal.PLoN.canonicalModel 𝓢 = { toFrame := LO.Modal.PLoN.canonicalFrame 𝓢, Valuation := fun (Ω : (LO.Modal.PLoN.canonicalFrame 𝓢).World) (a : ℕ) => LO.Modal.Formula.atom a ∈ Ω }

theorem LO.Modal.PLoN.truthlemma {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] [Entailment.Necessitation 𝓢] {φ : Formula ℕ} {X : (canonicalModel 𝓢).World} : X ⊩ φ ↔ φ ∈ X

instance LO.Modal.PLoN.instComplete_of_mem_canonicalFrame {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] [Entailment.Necessitation 𝓢] {C : FrameClass} (h : canonicalFrame 𝓢 ∈ C) : Complete 𝓢 C