@[reducible, inline]

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

Equations

• LO.Modal.PLoN.canonicalFrame 𝓢 = LO.Modal.PLoN.Frame.mk (LO.Modal.MaximalConsistentSet 𝓢) fun (φ : LO.Modal.Formula ℕ) (Ω₁ Ω₂ : LO.Modal.MaximalConsistentSet 𝓢) => ∼□φ ∈ Ω₁ ∧ ∼φ ∈ Ω₂

@[reducible, inline]

abbrev LO.Modal.PLoN.canonicalModel {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : 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 ∈ Ω }

@[reducible]

instance LO.Modal.PLoN.instSemanticsFormulaNatWorldCanonicalModel {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] : Semantics (Formula ℕ) (canonicalModel 𝓢).World

Equations

• LO.Modal.PLoN.instSemanticsFormulaNatWorldCanonicalModel = LO.Modal.Formula.PLoN.Satisfies.semantics (LO.Modal.PLoN.canonicalModel 𝓢)

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

class LO.Modal.PLoN.Canonical {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] (C : FrameClass) : Prop

• canonical : canonicalFrame 𝓢 ∈ C

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