Documentation
Foundation
.
Modal
.
Boxdot
.
GL_Grz
Search
return to top
source
Imports
Init
Foundation.Modal.Boxdot.Basic
Foundation.Modal.Kripke.Logic.GL.Completeness
Foundation.Modal.Kripke.Logic.Grz.Completeness
Imported by
LO
.
Modal
.
Kripke
.
instIsFiniteGrzReflGenOfIsFiniteGL
LO
.
Modal
.
Kripke
.
instIsFiniteGLIrreflGenOfIsFiniteGrz
LO
.
Modal
.
provable_boxdot_GL_of_provable_Grz
LO
.
Modal
.
provable_Grz_of_provable_boxdot_GL
LO
.
Modal
.
iff_provable_boxdot_GL_provable_Grz
LO
.
Modal
.
iff_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
⊢!
φ