Documentation

Foundation.Modal.Kripke.GL.MDP

source
@[reducible, inline]
abbrev LO.Modal.GL.Kripke.MDPCounterexampleFrame (F₁ 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
    instance LO.Modal.GL.Kripke.MDPCounterexampleFrame.instCoeWorld {F₁ F₂ : LO.Modal.Kripke.FiniteTransitiveTree} :
    Coe F₁.World (LO.Modal.GL.Kripke.MDPCounterexampleFrame F₁ F₂).World
    Equations
    • LO.Modal.GL.Kripke.MDPCounterexampleFrame.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }
    source
    instance LO.Modal.GL.Kripke.MDPCounterexampleFrame.instCoeWorld_1 {F₁ F₂ : LO.Modal.Kripke.FiniteTransitiveTree} :
    Coe F₂.World (LO.Modal.GL.Kripke.MDPCounterexampleFrame F₁ F₂).World
    Equations
    • LO.Modal.GL.Kripke.MDPCounterexampleFrame.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }
    source
    def LO.Modal.GL.Kripke.MDPCounterexampleFrame.p_morphism₁ {F₁ F₂ : LO.Modal.Kripke.FiniteTransitiveTree} :
    F₁.toFrame →ₚ (LO.Modal.GL.Kripke.MDPCounterexampleFrame F₁ F₂).toFrame
    Equations
    • LO.Modal.GL.Kripke.MDPCounterexampleFrame.p_morphism₁ = { toFun := fun (x : F₁.World) => Sum.inr (Sum.inl x), forth := ⋯, back := ⋯ }
    Instances For
      source
      def LO.Modal.GL.Kripke.MDPCounterexampleFrame.p_morphism₂ {F₁ F₂ : LO.Modal.Kripke.FiniteTransitiveTree} :
      F₂.toFrame →ₚ (LO.Modal.GL.Kripke.MDPCounterexampleFrame F₁ F₂).toFrame
      Equations
      • LO.Modal.GL.Kripke.MDPCounterexampleFrame.p_morphism₂ = { toFun := fun (x : F₂.World) => Sum.inr (Sum.inr x), forth := ⋯, back := ⋯ }
      Instances For
        source
        theorem LO.Modal.GL.Kripke.MDPCounterexampleFrame.through_original_root {F₁ F₂ : LO.Modal.Kripke.FiniteTransitiveTree} {x : (LO.Modal.GL.Kripke.MDPCounterexampleFrame F₁ F₂).World} (h : (LO.Modal.GL.Kripke.MDPCounterexampleFrame F₁ F₂).root ≺ x) :
        (x = (Sum.inr ∘ Sum.inl) F₁.root ∨ Sum.inr (Sum.inl F₁.root) ≺ x) ∨ x = (Sum.inr ∘ Sum.inr) F₂.root ∨ Sum.inr (Sum.inr F₂.root) ≺ x
        source
        @[reducible, inline]
        abbrev LO.Modal.GL.Kripke.MDPCounterexampleModel (M₁ 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
          instance LO.Modal.GL.Kripke.MDPCounterexampleModel.instCoeWorld {M₁ M₂ : LO.Modal.Kripke.FiniteTransitiveTreeModel} :
          Coe M₁.World (LO.Modal.GL.Kripke.MDPCounterexampleModel M₁ M₂).World
          Equations
          • LO.Modal.GL.Kripke.MDPCounterexampleModel.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }
          source
          instance LO.Modal.GL.Kripke.MDPCounterexampleModel.instCoeWorld_1 {M₁ M₂ : LO.Modal.Kripke.FiniteTransitiveTreeModel} :
          Coe M₂.World (LO.Modal.GL.Kripke.MDPCounterexampleModel M₁ M₂).World
          Equations
          • LO.Modal.GL.Kripke.MDPCounterexampleModel.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }
          source
          def LO.Modal.GL.Kripke.MDPCounterexampleModel.p_morphism₁ {M₁ M₂ : LO.Modal.Kripke.FiniteTransitiveTreeModel} :
          M₁.toModel →ₚ (LO.Modal.GL.Kripke.MDPCounterexampleModel M₁ M₂).toModel
          Equations
          Instances For
            source
            theorem LO.Modal.GL.Kripke.MDPCounterexampleModel.modal_equivalence_original_world₁ {M₁ M₂ : LO.Modal.Kripke.FiniteTransitiveTreeModel} {x : M₁.toModel.World} :
            x ↭ (Sum.inr ∘ Sum.inl) x
            source
            def LO.Modal.GL.Kripke.MDPCounterexampleModel.p_morphism₂ {M₁ M₂ : LO.Modal.Kripke.FiniteTransitiveTreeModel} :
            M₂.toModel →ₚ (LO.Modal.GL.Kripke.MDPCounterexampleModel M₁ M₂).toModel
            Equations
            Instances For
              source
              theorem LO.Modal.GL.Kripke.MDPCounterexampleModel.modal_equivalence_original_world₂ {M₁ M₂ : LO.Modal.Kripke.FiniteTransitiveTreeModel} {x : M₂.toModel.World} :
              x ↭ (Sum.inr ∘ Sum.inr) x
              source
              theorem LO.Modal.GL.MDP_Aux {X : LO.Modal.Theory ℕ} {φ₁ φ₂ : LO.Modal.Formula ℕ} (h : (□''X) *⊢[LO.Modal.Hilbert.GL ℕ]! □φ₁ ⋎ □φ₂) :
              (□''X) *⊢[LO.Modal.Hilbert.GL ℕ]! □φ₁ ∨ (□''X) *⊢[LO.Modal.Hilbert.GL ℕ]! □φ₂
              source
              theorem LO.Modal.GL.modal_disjunctive {φ₁ φ₂ : LO.Modal.Formula ℕ} (h : LO.Modal.Hilbert.GL ℕ ⊢! □φ₁ ⋎ □φ₂) :
              LO.Modal.Hilbert.GL ℕ ⊢! φ₁ ∨ LO.Modal.Hilbert.GL ℕ ⊢! φ₂
              source
              instance LO.Modal.GL.instModalDisjunctiveHilbertNatFormulaGL :
              LO.System.ModalDisjunctive (LO.Modal.Hilbert.GL ℕ)
              Equations