theorem LO.Modal.Kripke.modal_equivalence_at_root_on_treeUnravelling {α : Type u_1} (M : LO.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : ⟨[r], ⋯⟩ ↭ r

@[reducible]

instance LO.Modal.Kripke.instSemanticsFormulaDep {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Kripke.FiniteTransitiveTree.Dep α)

Equations

• LO.Modal.Kripke.instSemanticsFormulaDep = { Realize := fun (T : LO.Kripke.FiniteTransitiveTree.Dep α) => LO.Modal.Formula.Kripke.ValidOnFrame T.toFrame }

@[reducible]

instance LO.Modal.Kripke.instSemanticsFormulaWorld {α : Type u_1} {M : LO.Kripke.FiniteTransitiveTreeModel α} : LO.Semantics (LO.Modal.Formula α) M.World

Equations

• LO.Modal.Kripke.instSemanticsFormulaWorld = LO.Modal.Formula.Kripke.Satisfies.semantics

theorem LO.Modal.Kripke.valid_on_FiniteTransitiveTreeClass_of_valid_on_TransitiveIrreflexiveFrameClass {α : Type u_1} {p : LO.Modal.Formula α} (h : LO.Kripke.TransitiveIrreflexiveFrameClassꟳ#α ⊧ p) (T : LO.Kripke.FiniteTransitiveTree) : T# ⊧ p

theorem LO.Modal.Kripke.satisfies_at_root_on_FiniteTransitiveTree {α : Type u} {p : LO.Modal.Formula α} (h : ∀ (F : LO.Kripke.FiniteTransitiveTree), F# ⊧ p) (M : LO.Kripke.FiniteTransitiveTreeModel α) : LO.Modal.Formula.Kripke.Satisfies M.toModel M.root p

theorem LO.Modal.Kripke.valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree {α : Type u} {p : LO.Modal.Formula α} : (∀ (M : LO.Kripke.FiniteTransitiveTreeModel α), M.root ⊧ p) → LO.Kripke.TransitiveIrreflexiveFrameClassꟳ#α ⊧ p

theorem LO.Modal.Kripke.iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : 𝐆𝐋 ⊢! p ↔ ∀ (M : LO.Kripke.FiniteTransitiveTreeModel α), M.root ⊧ p

theorem LO.Modal.Kripke.iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : 𝐆𝐋 ⊬ p ↔ ∃ (M : LO.Kripke.FiniteTransitiveTreeModel α), ¬M.root ⊧ p

def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension (F : LO.Kripke.FiniteTransitiveTree) : LO.Kripke.FiniteTransitiveTree

Equations

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

def LO.Modal.Kripke.«term_↧» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_↧» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.term_↧ 1024 1024 (Lean.ParserDescr.symbol "↧")

instance LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.instCoeWorld {F : LO.Kripke.FiniteTransitiveTree} : Coe F.World F↧.World

Equations

• LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.instCoeWorld = { coe := Sum.inr }

@[simp]

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_not_original {F : LO.Kripke.FiniteTransitiveTree} {x : F.World} : Sum.inr x ≠ F↧.root

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_eq {F : LO.Kripke.FiniteTransitiveTree} {x : Fin 1} : Sum.inl x = F↧.root

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.forth {F : LO.Kripke.FiniteTransitiveTree} {x : F.World} {y : F.World} (h : x ≺ y) : F↧.Rel (Sum.inr x) (Sum.inr y)

def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism {F : LO.Kripke.FiniteTransitiveTree} : F.toFrame →ₚ F↧.toFrame

Equations

• LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism = { toFun := fun (x : F.World) => Sum.inr x, forth := ⋯, back := ⋯ }

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.through_original_root {F : LO.Kripke.FiniteTransitiveTree} {x : F↧.World} (h : F↧.root ≺ x) : x = Sum.inr F.root ∨ Sum.inr F.root ≺ x

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension {α : Type u_1} (M : LO.Kripke.FiniteTransitiveTreeModel α) : LO.Kripke.FiniteTransitiveTreeModel α

Equations

• M↧ = { Tree := M.Tree↧, Valuation := fun (x : M.Tree↧.World) (a : α) => match x with | Sum.inl val => M.Valuation M.Tree.root a | Sum.inr x => M.Valuation x a }

def LO.Modal.Kripke.«term_↧_1» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_↧_1» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.term_↧_1 1024 1024 (Lean.ParserDescr.symbol "↧")

instance LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld {α : Type u_1} {M : LO.Kripke.FiniteTransitiveTreeModel α} : Coe M.World M↧.World

Equations

• LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld = { coe := Sum.inr }

def LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.p_morphism {α : Type u_1} {M : LO.Kripke.FiniteTransitiveTreeModel α} : M.toModel →ₚ M↧.toModel

Equations

• LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.p_morphism = LO.Kripke.Model.PseudoEpimorphism.mkAtomic LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism ⋯

theorem LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.modal_equivalence_original_world {α : Type u_1} {M : LO.Kripke.FiniteTransitiveTreeModel α} {x : M.toModel.World} : x ↭ Sum.inr x

theorem LO.Modal.GL_imply_boxdot_plain_of_imply_box_box {α : Type u_1} [DecidableEq α] [Inhabited α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : 𝐆𝐋 ⊢! □p ➝ □q → 𝐆𝐋 ⊢! ⊡p ➝ q

theorem LO.Modal.GL_unnecessitation! {α : Type u_1} [DecidableEq α] [Inhabited α] {p : LO.Modal.Formula α} : 𝐆𝐋 ⊢! □p → 𝐆𝐋 ⊢! p

noncomputable instance LO.Modal.instUnnecessitationHilbertFormulaGL {α : Type u_1} [DecidableEq α] [Inhabited α] : LO.System.Unnecessitation 𝐆𝐋

Equations

• LO.Modal.instUnnecessitationHilbertFormulaGL = { unnec := fun {p : LO.Modal.Formula α} (h : 𝐆𝐋 ⊢ □p) => Nonempty.some ⋯ }