@[reducible, inline]

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

Instances

• LO.Modal.Hilbert.N.instCanonicalNatAllFrameClass

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