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

theorem LO.Modal.PLoN.Frame.World_nonempty {α : Type u_2} (self : LO.Modal.PLoN.Frame α) : Nonempty self.World

@[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 α} (p : LO.Modal.Formula α) (x : F.World) (y : F.World) : Prop

Equations

• LO.Modal.PLoN.Frame.Rel' p x y = F.Rel p 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

theorem LO.Modal.PLoN.FiniteFrame.World_finite {α : Type u_1} (self : LO.Modal.PLoN.FiniteFrame α) : 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 (p.imp q) = (LO.Modal.Formula.PLoN.Satisfies M w p → LO.Modal.Formula.PLoN.Satisfies M w q)
• LO.Modal.Formula.PLoN.Satisfies M w p.box = ∀ {w' : M.Frame.World}, LO.Modal.PLoN.Frame.Rel' p w w' → LO.Modal.Formula.PLoN.Satisfies M w' p

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} {p : LO.Modal.Formula α} : x ⊧ p ↔ LO.Modal.Formula.PLoN.Satisfies M x p

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

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

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

Equations

• LO.Modal.Formula.PLoN.Satisfies.instNotWorld = { realize_not := ⋯ }

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

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

Equations

• LO.Modal.Formula.PLoN.Satisfies.instImpWorld = { realize_imp := ⋯ }

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

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

Equations

• LO.Modal.Formula.PLoN.Satisfies.instOrWorld = { realize_or := ⋯ }

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

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

Equations

• LO.Modal.Formula.PLoN.Satisfies.instAndWorld = { realize_and := ⋯ }

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

Equations

• LO.Modal.Formula.PLoN.Satisfies.instTarskiWorld = LO.Semantics.Tarski.mk

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

Equations

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

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 α} {p : LO.Modal.Formula α} : M ⊧ p ↔ LO.Modal.Formula.PLoN.ValidOnModel M p

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

Equations

• LO.Modal.Formula.PLoN.ValidOnModel.instBotModel = { realize_bot := ⋯ }

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

theorem LO.Modal.Formula.PLoN.ValidOnModel.imply₂ {α : Type u_1} {M : LO.Modal.PLoN.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} : M ⊧ LO.Axioms.Imply₂ p q r

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

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

Equations

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

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 α} {p : LO.Modal.Formula α} : F ⊧ p ↔ LO.Modal.Formula.PLoN.ValidOnFrame F p

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

Equations

• LO.Modal.Formula.PLoN.ValidOnFrame.instBotFrame = { realize_bot := ⋯ }

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

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

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

theorem LO.Modal.Formula.PLoN.ValidOnFrame.imply₂ {α : Type u_1} {F : LO.Modal.PLoN.Frame α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} : F ⊧ LO.Axioms.Imply₂ p q r

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

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

Equations

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

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 α} {p : LO.Modal.Formula α} : 𝔽 ⊧ p ↔ LO.Modal.Formula.PLoN.ValidOnFrameClass 𝔽 p

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

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

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

theorem LO.Modal.Formula.PLoN.ValidOnFrameClass.imply₂ {α : Type u_1} {𝔽 : LO.Modal.PLoN.FrameClass α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} : 𝔽 ⊧ LO.Axioms.Imply₂ p q r

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

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

Equations

• Λ.DefinesPLoNFrameClass 𝔽 = ∀ {F : LO.Modal.PLoN.Frame α}, F ⊧* Λ.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} : 𝐍.DefinesPLoNFrameClass (LO.Modal.PLoN.AllFrameClass α)