@[reducible, inline]

abbrev LO.Modal.Standard.PLoN.CanonicalFrame {α : Type u} (Λ : LO.Modal.Standard.DeductionParameter α) [Inhabited (Λ)-MCT] : LO.Modal.Standard.PLoN.Frame α

Equations

• LO.Modal.Standard.PLoN.CanonicalFrame Λ = LO.Modal.Standard.PLoN.Frame.mk (Λ)-MCT fun (p : LO.Modal.Standard.Formula α) (Ω₁ Ω₂ : (Λ)-MCT) => ~□p ∈ Ω₁.theory ∧ ~p ∈ Ω₂.theory

@[reducible, inline]

abbrev LO.Modal.Standard.PLoN.CanonicalModel {α : Type u} (Λ : LO.Modal.Standard.DeductionParameter α) [Inhabited (Λ)-MCT] : LO.Modal.Standard.PLoN.Model α

Equations

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

instance LO.Modal.Standard.PLoN.CanonicalModel.instSatisfies {α : Type u} {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] : LO.Semantics (LO.Modal.Standard.Formula α) (LO.Modal.Standard.PLoN.CanonicalModel Λ).World

Equations

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

theorem LO.Modal.Standard.PLoN.truthlemma {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] [Λ.HasNecessitation] {p : LO.Modal.Standard.Formula α} {Ω : (LO.Modal.Standard.PLoN.CanonicalModel Λ).World} : Ω ⊧ p ↔ p ∈ Ω.theory

theorem LO.Modal.Standard.PLoN.complete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] [Λ.HasNecessitation] {p : LO.Modal.Standard.Formula α} {𝔽 : LO.Modal.Standard.PLoN.FrameClass α} (hFC : LO.Modal.Standard.PLoN.CanonicalFrame Λ ∈ 𝔽) : 𝔽 ⊧ p → Λ ⊢! p

theorem LO.Modal.Standard.PLoN.instComplete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] [Λ.HasNecessitation] {𝔽 : LO.Modal.Standard.PLoN.FrameClass α} (hFC : LO.Modal.Standard.PLoN.CanonicalFrame Λ ∈ 𝔽) : LO.Complete Λ 𝔽

instance LO.Modal.Standard.PLoN.instCompleteDeductionParameterFormulaFrameClassNAllFrameClass {α : Type u} [DecidableEq α] : LO.Complete 𝐍 (LO.Modal.Standard.PLoN.AllFrameClass α)

Equations

• ⋯ = ⋯