structure LO.Modal.PLoN.Frame (α : Type u_2) : Type (max (u_1 + 1) u_2)

• World : Type u_1
• World_nonempty : Nonempty self.World
• Rel : LO.Modal.Formula α → self.World → self.World → Prop

@[reducible, inline]

noncomputable abbrev LO.Modal.PLoN.Frame.default {α : Type u_1} {F : LO.Modal.PLoN.Frame α} : F.World

Equations

• LO.Modal.PLoN.Frame.default = ⋯.some

def LO.Modal.PLoN.«term﹫» : Lean.ParserDescr

Equations

• LO.Modal.PLoN.«term﹫» = Lean.ParserDescr.node `LO.Modal.PLoN.«term﹫» 1024 (Lean.ParserDescr.symbol "﹫")

instance LO.Modal.PLoN.instCoeFunFrameForallFormulaForallWorldForallProp {α : Type u_1} : CoeFun (LO.Modal.PLoN.Frame α) fun (F : LO.Modal.PLoN.Frame α) => LO.Modal.Formula α → F.World → F.World → Prop

Equations

• LO.Modal.PLoN.instCoeFunFrameForallFormulaForallWorldForallProp = { coe := LO.Modal.PLoN.Frame.Rel }

@[reducible, inline]

abbrev LO.Modal.PLoN.Frame.Rel' {α : Type u_1} {F : LO.Modal.PLoN.Frame α} (φ : LO.Modal.Formula α) (x y : F.World) : Prop

Equations

• LO.Modal.PLoN.Frame.Rel' φ x y = F.Rel φ x y

def LO.Modal.PLoN.«term_≺[_]_» : Lean.TrailingParserDescr

Equations

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

structure LO.Modal.PLoN.FiniteFrame (α : Type u_1) extends LO.Modal.PLoN.Frame α : Type (max u_1 (u_2 + 1))

• World : Type u_2
• World_nonempty : Nonempty self.World
• Rel : LO.Modal.Formula α → self.World → self.World → Prop
• World_finite : Finite self.World

instance LO.Modal.PLoN.instCoeFiniteFrameFrame {α : Type u_1} : Coe (LO.Modal.PLoN.FiniteFrame α) (LO.Modal.PLoN.Frame α)

Equations

• LO.Modal.PLoN.instCoeFiniteFrameFrame = { coe := fun (F : LO.Modal.PLoN.FiniteFrame α) => F.toFrame }

@[reducible, inline]

abbrev LO.Modal.PLoN.terminalFrame (α : Type u_1) : LO.Modal.PLoN.FiniteFrame α

Equations

• LO.Modal.PLoN.terminalFrame α = LO.Modal.PLoN.FiniteFrame.mk (LO.Modal.PLoN.Frame.mk Unit fun (x : LO.Modal.Formula α) (x x : Unit) => True)

@[reducible, inline]

abbrev LO.Modal.PLoN.FrameClass (α : Type u_1) : Type (max u_1 (u_2 + 1))

Equations

• LO.Modal.PLoN.FrameClass α = Set (LO.Modal.PLoN.Frame α)

@[reducible, inline]

abbrev LO.Modal.PLoN.Valuation {α : Type u_2} (F : LO.Modal.PLoN.Frame α) : Type u_1 → Type (max u_1 u_3)

Equations

• LO.Modal.PLoN.Valuation F α = (F.World → α → Prop)

structure LO.Modal.PLoN.Model (α : Type u_1) : Type (max u_1 (u_2 + 1))

• Frame : LO.Modal.PLoN.Frame α
• Valuation : LO.Modal.PLoN.Valuation self.Frame α

@[reducible, inline]

abbrev LO.Modal.PLoN.Model.World {α : Type u_1} (M : LO.Modal.PLoN.Model α) : Type u_2

Equations

• M.World = M.Frame.World

instance LO.Modal.PLoN.instCoeSortModelType {α : Type u_1} : CoeSort (LO.Modal.PLoN.Model α) (Type u_2)

Equations

• LO.Modal.PLoN.instCoeSortModelType = { coe := LO.Modal.PLoN.Model.World }

def LO.Modal.Formula.PLoN.Satisfies {α : Type u_1} (M : LO.Modal.PLoN.Model α) (w : M.World) : LO.Modal.Formula α → Prop

Equations

• LO.Modal.Formula.PLoN.Satisfies M w (LO.Modal.Formula.atom a) = M.Valuation w a
• LO.Modal.Formula.PLoN.Satisfies M w LO.Modal.Formula.falsum = False
• LO.Modal.Formula.PLoN.Satisfies M w (φ.imp ψ) = (LO.Modal.Formula.PLoN.Satisfies M w φ → LO.Modal.Formula.PLoN.Satisfies M w ψ)
• LO.Modal.Formula.PLoN.Satisfies M w φ.box = ∀ {w' : M.Frame.World}, LO.Modal.PLoN.Frame.Rel' φ w w' → LO.Modal.Formula.PLoN.Satisfies M w' φ

instance LO.Modal.Formula.PLoN.Satisfies.semantics {α : Type u_1} (M : LO.Modal.PLoN.Model α) : LO.Semantics (LO.Modal.Formula α) M.World

Equations

• LO.Modal.Formula.PLoN.Satisfies.semantics M = { Realize := fun (w : M.World) => LO.Modal.Formula.PLoN.Satisfies M w }

@[simp]

theorem LO.Modal.Formula.PLoN.Satisfies.iff_models {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {φ : LO.Modal.Formula α} : x ⊧ φ ↔ LO.Modal.Formula.PLoN.Satisfies M x φ

theorem LO.Modal.Formula.PLoN.Satisfies.box_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {φ : LO.Modal.Formula α} : x ⊧ □φ ↔ ∀ (y : M.Frame.World), LO.Modal.PLoN.Frame.Rel' φ x y → y ⊧ φ

theorem LO.Modal.Formula.PLoN.Satisfies.not_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {φ : LO.Modal.Formula α} : x ⊧ ∼φ ↔ ¬x ⊧ φ

instance LO.Modal.Formula.PLoN.Satisfies.instNotWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} : LO.Semantics.Not M.World

Equations

• ⋯ = ⋯

theorem LO.Modal.Formula.PLoN.Satisfies.imp_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {φ ψ : LO.Modal.Formula α} : x ⊧ φ ➝ ψ ↔ x ⊧ φ → x ⊧ ψ

instance LO.Modal.Formula.PLoN.Satisfies.instImpWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} : LO.Semantics.Imp M.World

Equations

• ⋯ = ⋯

theorem LO.Modal.Formula.PLoN.Satisfies.or_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {φ ψ : LO.Modal.Formula α} : x ⊧ φ ⋎ ψ ↔ x ⊧ φ ∨ x ⊧ ψ

instance LO.Modal.Formula.PLoN.Satisfies.instOrWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} : LO.Semantics.Or M.World

Equations

• ⋯ = ⋯

theorem LO.Modal.Formula.PLoN.Satisfies.and_def {α : Type u_1} {M : LO.Modal.PLoN.Model α} {x : M.World} {φ ψ : LO.Modal.Formula α} : x ⊧ φ ⋏ ψ ↔ x ⊧ φ ∧ x ⊧ ψ

instance LO.Modal.Formula.PLoN.Satisfies.instAndWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} : LO.Semantics.And M.World

Equations

• ⋯ = ⋯

instance LO.Modal.Formula.PLoN.Satisfies.instTarskiWorld {α : Type u_1} {M : LO.Modal.PLoN.Model α} : LO.Semantics.Tarski M.World

Equations

• ⋯ = ⋯

def LO.Modal.Formula.PLoN.ValidOnModel {α : Type u_1} (M : LO.Modal.PLoN.Model α) (φ : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.PLoN.ValidOnModel M φ = ∀ (w : M.World), w ⊧ φ

instance LO.Modal.Formula.PLoN.ValidOnModel.instSemanticsModel {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.Model α)

Equations

• LO.Modal.Formula.PLoN.ValidOnModel.instSemanticsModel = { Realize := fun (M : LO.Modal.PLoN.Model α) => LO.Modal.Formula.PLoN.ValidOnModel M }

@[simp]

theorem LO.Modal.Formula.PLoN.ValidOnModel.iff_models {α : Type u_1} {M : LO.Modal.PLoN.Model α} {φ : LO.Modal.Formula α} : M ⊧ φ ↔ LO.Modal.Formula.PLoN.ValidOnModel M φ

instance LO.Modal.Formula.PLoN.ValidOnModel.instBotModel {α : Type u_1} : LO.Semantics.Bot (LO.Modal.PLoN.Model α)

Equations

• ⋯ = ⋯

theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₁ {α : Type u_1} {M : LO.Modal.PLoN.Model α} {φ ψ : LO.Modal.Formula α} : M ⊧ LO.Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₂ {α : Type u_1} {M : LO.Modal.PLoN.Model α} {φ ψ χ : LO.Modal.Formula α} : M ⊧ LO.Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.PLoN.ValidOnModel.elim_contra {α : Type u_1} {M : LO.Modal.PLoN.Model α} {φ ψ : LO.Modal.Formula α} : M ⊧ LO.Axioms.ElimContra φ ψ

def LO.Modal.Formula.PLoN.ValidOnFrame {α : Type u_1} (F : LO.Modal.PLoN.Frame α) (φ : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.PLoN.ValidOnFrame F φ = ∀ (V : LO.Modal.PLoN.Valuation F α), { Frame := F, Valuation := V } ⊧ φ

instance LO.Modal.Formula.PLoN.ValidOnFrame.instSemanticsFrame {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.Frame α)

Equations

• LO.Modal.Formula.PLoN.ValidOnFrame.instSemanticsFrame = { Realize := fun (F : LO.Modal.PLoN.Frame α) => LO.Modal.Formula.PLoN.ValidOnFrame F }

@[simp]

theorem LO.Modal.Formula.PLoN.ValidOnFrame.iff_models {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {φ : LO.Modal.Formula α} : F ⊧ φ ↔ LO.Modal.Formula.PLoN.ValidOnFrame F φ

instance LO.Modal.Formula.PLoN.ValidOnFrame.instBotFrame {α : Type u_1} : LO.Semantics.Bot (LO.Modal.PLoN.Frame α)

Equations

• ⋯ = ⋯

theorem LO.Modal.Formula.PLoN.ValidOnFrame.nec {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {φ : LO.Modal.Formula α} (h : F ⊧ φ) : F ⊧ □φ

theorem LO.Modal.Formula.PLoN.ValidOnFrame.mdp {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {φ ψ : LO.Modal.Formula α} (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) : F ⊧ ψ

theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₁ {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {φ ψ : LO.Modal.Formula α} : F ⊧ LO.Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₂ {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {φ ψ χ : LO.Modal.Formula α} : F ⊧ LO.Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.PLoN.ValidOnFrame.elim_contra {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {φ ψ : LO.Modal.Formula α} : F ⊧ LO.Axioms.ElimContra φ ψ

def LO.Modal.Formula.PLoN.ValidOnFrameClass {α : Type u_1} (𝔽 : LO.Modal.PLoN.FrameClass α) (φ : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.PLoN.ValidOnFrameClass 𝔽 φ = ∀ {F : LO.Modal.PLoN.Frame α}, F ∈ 𝔽 → F ⊧ φ

instance LO.Modal.Formula.PLoN.ValidOnFrameClass.instSemanticsFrameClass {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Modal.PLoN.FrameClass α)

Equations

• LO.Modal.Formula.PLoN.ValidOnFrameClass.instSemanticsFrameClass = { Realize := fun (𝔽 : LO.Modal.PLoN.FrameClass α) => LO.Modal.Formula.PLoN.ValidOnFrameClass 𝔽 }

@[simp]

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.iff_models {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {φ : LO.Modal.Formula α} : 𝔽 ⊧ φ ↔ LO.Modal.Formula.PLoN.ValidOnFrameClass 𝔽 φ

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.nec {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {φ : LO.Modal.Formula α} (h : 𝔽 ⊧ φ) : 𝔽 ⊧ □φ

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.mdp {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {φ ψ : LO.Modal.Formula α} (hpq : 𝔽 ⊧ φ ➝ ψ) (hp : 𝔽 ⊧ φ) : 𝔽 ⊧ ψ

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₁ {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {φ ψ : LO.Modal.Formula α} : 𝔽 ⊧ LO.Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₂ {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {φ ψ χ : LO.Modal.Formula α} : 𝔽 ⊧ LO.Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.elim_contra {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {φ ψ : LO.Modal.Formula α} : 𝔽 ⊧ LO.Axioms.ElimContra φ ψ

def LO.Modal.Hilbert.DefinesPLoNFrameClass {α : Type u_1} (H : LO.Modal.Hilbert α) (𝔽 : LO.Modal.PLoN.FrameClass α) : Prop

Equations

• H.DefinesPLoNFrameClass 𝔽 = ∀ {F : LO.Modal.PLoN.Frame α}, F ⊧* H.theorems ↔ F ∈ 𝔽

@[reducible, inline]

abbrev LO.Modal.PLoN.AllFrameClass (α : Type u_2) : LO.Modal.PLoN.FrameClass α

Equations

• LO.Modal.PLoN.AllFrameClass α = Set.univ

theorem LO.Modal.PLoN.AllFrameClass.nonempty {α : Type u_1} : Set.Nonempty (LO.Modal.PLoN.AllFrameClass α)

theorem LO.Modal.PLoN.N_defines {α : Type u_1} : (LO.Modal.Hilbert.N α).DefinesPLoNFrameClass (LO.Modal.PLoN.AllFrameClass α)