Documentation

Logic.Modal.Kripke.GL.Tree

source
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
source
@[reducible]
instance LO.Modal.Kripke.instSemanticsFormulaDep {α : Type u_1} :
LO.Semantics (LO.Modal.Formula α) (LO.Kripke.FiniteTransitiveTree.Dep α)
Equations
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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.
Instances For
    source
    def LO.Modal.Kripke.«term_↧» :
    Lean.TrailingParserDescr
    Equations
    Instances For
      source
      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 }
      source
      @[simp]
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_not_original {F : LO.Kripke.FiniteTransitiveTree} {x : F.World} :
      Sum.inr x ≠ F↧.root
      source
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_eq {F : LO.Kripke.FiniteTransitiveTree} {x : Fin 1} :
      Sum.inl x = F↧.root
      source
      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)
      source
      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 := ⋯ }
      Instances For
        source
        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
        source
        @[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 }
        Instances For
          source
          def LO.Modal.Kripke.«term_↧_1» :
          Lean.TrailingParserDescr
          Equations
          Instances For
            source
            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 }
            source
            def LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.p_morphism {α : Type u_1} {M : LO.Kripke.FiniteTransitiveTreeModel α} :
            M.toModel →ₚ M↧.toModel
            Equations
            Instances For
              source
              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
              source
              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
              source
              theorem LO.Modal.GL_unnecessitation! {α : Type u_1} [DecidableEq α] [Inhabited α] {p : LO.Modal.Formula α} :
              𝐆𝐋 ⊢! □p → 𝐆𝐋 ⊢! p
              source
              noncomputable instance LO.Modal.instUnnecessitationHilbertFormulaGL {α : Type u_1} [DecidableEq α] [Inhabited α] :
              LO.System.Unnecessitation 𝐆𝐋
              Equations