Documentation

Foundation.Modal.Kripke.GL.Tree

source
theorem LO.Modal.Hilbert.GL.Kripke.valid_on_FiniteTransitiveTreeClass_of_valid_on_TransitiveIrreflexiveFrameClass {φ : LO.Modal.Formula ℕ} (h : LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass ⊧ φ) (T : LO.Modal.Kripke.FiniteTransitiveTree) :
T.toFrame ⊧ φ
source
theorem LO.Modal.Hilbert.GL.Kripke.satisfies_at_root_on_FiniteTransitiveTree {φ : LO.Modal.Formula ℕ} (h : ∀ (T : LO.Modal.Kripke.FiniteTransitiveTree), T.toFrame ⊧ φ) (M : LO.Modal.Kripke.FiniteTransitiveTreeModel) :
LO.Modal.Formula.Kripke.Satisfies M.toModel M.root φ
source
theorem LO.Modal.Hilbert.GL.Kripke.valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree {φ : LO.Modal.Formula ℕ} :
(∀ (M : LO.Modal.Kripke.FiniteTransitiveTreeModel), LO.Modal.Formula.Kripke.Satisfies M.toModel M.root φ) → LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass ⊧ φ
source
theorem LO.Modal.Hilbert.GL.Kripke.provable_iff_satisfies_at_root_on_FiniteTransitiveTree {φ : LO.Modal.Formula ℕ} :
LO.Modal.Hilbert.GL ℕ ⊢! φ ↔ ∀ (M : LO.Modal.Kripke.FiniteTransitiveTreeModel), LO.Modal.Formula.Kripke.Satisfies M.toModel M.root φ
source
theorem LO.Modal.Hilbert.GL.Kripke.unprovable_iff_exists_unsatisfies_at_root_on_FiniteTransitiveTree {φ : LO.Modal.Formula ℕ} :
LO.Modal.Hilbert.GL ℕ ⊬ φ ↔ ∃ (M : LO.Modal.Kripke.FiniteTransitiveTreeModel), ¬LO.Modal.Formula.Kripke.Satisfies M.toModel M.root φ
source
def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension (F : LO.Modal.Kripke.FiniteTransitiveTree) :
LO.Modal.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 {T : LO.Modal.Kripke.FiniteTransitiveTree} :
      Coe T.World T↧.World
      Equations
      • LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.instCoeWorld = { coe := Sum.inr }
      source
      @[simp]
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_not_original {T : LO.Modal.Kripke.FiniteTransitiveTree} {x : T.World} :
      Sum.inr x ≠ T↧.root
      source
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_eq {T : LO.Modal.Kripke.FiniteTransitiveTree} :
      Sum.inl () = T↧.root
      source
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.forth {T : LO.Modal.Kripke.FiniteTransitiveTree} {x y : T.World} (h : x ≺ y) :
      T↧.Rel (Sum.inr x) (Sum.inr y)
      source
      def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism {T : LO.Modal.Kripke.FiniteTransitiveTree} :
      T.toFrame →ₚ T↧.toFrame
      Equations
      • LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism = { toFun := fun (x : T.World) => Sum.inr x, forth := ⋯, back := ⋯ }
      Instances For
        source
        theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.through_original_root {T : LO.Modal.Kripke.FiniteTransitiveTree} {x : T↧.World} (h : T↧.root ≺ x) :
        x = Sum.inr T.root ∨ Sum.inr T.root ≺ x
        source
        @[reducible, inline]
        abbrev LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension (M : LO.Modal.Kripke.FiniteTransitiveTreeModel) :
        LO.Modal.Kripke.FiniteTransitiveTreeModel
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def LO.Modal.Kripke.«term_↧_1» :
          Lean.TrailingParserDescr
          Equations
          Instances For
            source
            instance LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld {M : LO.Modal.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 {M : LO.Modal.Kripke.FiniteTransitiveTreeModel} :
            M.toModel →ₚ M↧.toModel
            Equations
            Instances For
              source
              theorem LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.modal_equivalence_original_world {M : LO.Modal.Kripke.FiniteTransitiveTreeModel} {x : M.toModel.World} :
              x ↭ Sum.inr x