class Model.IsGLPoint3 {κ : Type u_1} [Nonempty κ] {α : Type u_2} (M : Model κ α) extends M.IsGL : Prop

LogicGLPoint3 frame class: transitive, converse well-founded, and linear (weakly connected), i.e. any two successors of a common world are comparable or equal.

• trans (a b c : M.World) : a ≺ b → b ≺ c → a ≺ c
• cwf : ConverseWellFounded Model.Rel
• linear {x y z : M.World} : x ≺ y → x ≺ z → y ≺ z ∨ y = z ∨ z ≺ y

class Model.IsFiniteGLPoint3 {κ : Type u_1} [Nonempty κ] {α : Type u_2} (M : Model κ α) extends M.IsFiniteGL : Prop

Finite LogicGLPoint3 frame class: finite, transitive, irreflexive, and linear (weakly connected), i.e. any two successors of a common world are comparable or equal.

• trans (a b c : M.World) : a ≺ b → b ≺ c → a ≺ c
• irrefl (a : M.World) : ¬a ≺ a
• finite : Finite M.World
• linear {x y z : M.World} : x ≺ y → x ≺ z → y ≺ z ∨ y = z ∨ z ≺ y

instance Model.instIsGLPoint3OfIsFiniteGLPoint3 {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [M.IsFiniteGLPoint3] : M.IsGLPoint3

theorem Model.linear {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [M.IsGLPoint3] {x y z : M.World} : x ≺ y → x ≺ z → y ≺ z ∨ y = z ∨ z ≺ y

instance Model.instIsFiniteGLPoint3ConeToRootedModel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [M.IsFiniteGLPoint3] {r : M.World} : (M.toRootedModel r).IsFiniteGLPoint3

theorem Model.World.forces_axiomWeakPoint3 {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {A B : Formula α} [M.IsGLPoint3] {x : M.World} : x ⊩[M] □(⊡A 🡒 B) ⋎ □(⊡B 🡒 A)

The weak linearity axiom .3 (WeakPoint3) holds at every world of a linear model.

theorem Model.validate_axiomWeakPoint3 {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [M.IsGLPoint3] {A B : Formula α} : M ⊧ □(⊡A 🡒 B) ⋎ □(⊡B 🡒 A)

The weak linearity axiom .3 (WeakPoint3) is valid on linear models.