Documentation

Foundation.Modal.Boxdot.GL_Grz

source
instance LO.Modal.Kripke.instIsFiniteGrzReflGenOfIsFiniteGL {F : Frame} [F.IsFiniteGL] :
F^=.IsFiniteGrz
source
instance LO.Modal.Kripke.instIsFiniteGLIrreflGenOfIsFiniteGrz {F : Frame} [F.IsFiniteGrz] :
F^≠.IsFiniteGL
source
theorem LO.Modal.provable_boxdot_GL_of_provable_Grz {φ : Formula ℕ} :
Hilbert.Grz ⊢! φ → Hilbert.GL ⊢! φᵇ
source
theorem LO.Modal.provable_Grz_of_provable_boxdot_GL {φ : Formula ℕ} :
Hilbert.GL ⊢! φᵇ → Hilbert.Grz ⊢! φ
source
theorem LO.Modal.iff_provable_boxdot_GL_provable_Grz {φ : Formula ℕ} :
Hilbert.GL ⊢! φᵇ ↔ Hilbert.Grz ⊢! φ
source
theorem LO.Modal.iff_boxdot_GL_Grz {φ : Formula ℕ} :
Modal.GL ⊢! φᵇ ↔ Modal.Grz ⊢! φ