Documentation

Foundation.Modal.Boxdot.GL_Grz

source
noncomputable def LO.System.lem₁_boxdot_Grz_of_L {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.GL 𝓢] {φ : F} :
𝓢 ⊢ ⊡(⊡(φ ➝ ⊡φ) ➝ φ) ➝ □(φ ➝ ⊡φ) ➝ φ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LO.System.boxdot_Grz_of_L {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.GL 𝓢] {φ : F} :
    𝓢 ⊢ ⊡(⊡(φ ➝ ⊡φ) ➝ φ) ➝ φ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem LO.System.boxdot_Grz_of_L! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.GL 𝓢] {φ : F} :
      𝓢 ⊢! ⊡(⊡(φ ➝ ⊡φ) ➝ φ) ➝ φ
      source
      theorem LO.Modal.Kripke.mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass {F : LO.Modal.Kripke.FiniteFrame} (hF : F ∈ LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass) :
      LO.Modal.Kripke.FiniteFrame.mk (F.toFrame^=) ∈ LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass
      source
      theorem LO.Modal.Kripke.mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass {F : LO.Modal.Kripke.FiniteFrame} (hF : F ∈ LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass) :
      LO.Modal.Kripke.FiniteFrame.mk (F.toFrame^≠) ∈ LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass
      source
      theorem LO.Modal.Kripke.iff_boxdot_reflexive_closure {φ : LO.Modal.Formula ℕ} {F : LO.Modal.Kripke.Frame} {V : LO.Modal.Kripke.Valuation F} {x : { toFrame := F, Val := V }.World} :
      LO.Modal.Formula.Kripke.Satisfies { toFrame := F, Val := V } x (φᵇ) ↔ LO.Modal.Formula.Kripke.Satisfies { toFrame := F^=, Val := V } x φ
      source
      theorem LO.Modal.Kripke.iff_frame_boxdot_reflexive_closure {φ : LO.Modal.Formula ℕ} {F : LO.Modal.Kripke.Frame} :
      F ⊧ φᵇ ↔ F^= ⊧ φ
      source
      theorem LO.Modal.Kripke.iff_reflexivize_irreflexivize {φ : LO.Modal.Formula ℕ} {F : LO.Modal.Kripke.Frame} (F_Refl : Reflexive F.Rel) {x : F.World} {V : LO.Modal.Kripke.Valuation F} :
      LO.Modal.Formula.Kripke.Satisfies { toFrame := F, Val := V } x φ ↔ LO.Modal.Formula.Kripke.Satisfies { toFrame := F^≠^=, Val := V } x φ
      source
      theorem LO.Modal.Hilbert.boxdotTranslatedGL_of_Grz {φ : LO.Modal.Formula ℕ} :
      LO.Modal.Hilbert.Grz ℕ ⊢! φ → LO.Modal.Hilbert.GL ℕ ⊢! φᵇ
      source
      theorem LO.Modal.Hilbert.Grz_of_boxdotTranslatedGL {φ : LO.Modal.Formula ℕ} :
      LO.Modal.Hilbert.GL ℕ ⊢! φᵇ → LO.Modal.Hilbert.Grz ℕ ⊢! φ
      source
      theorem LO.Modal.Hilbert.iff_Grz_boxdotTranslatedGL {φ : LO.Modal.Formula ℕ} :
      LO.Modal.Hilbert.GL ℕ ⊢! φᵇ ↔ LO.Modal.Hilbert.Grz ℕ ⊢! φ
      source
      instance LO.Modal.Hilbert.instBoxdotPropertyNatGLGrz :
      LO.Modal.BoxdotProperty (LO.Modal.Hilbert.GL ℕ) (LO.Modal.Hilbert.Grz ℕ)
      Equations