Documentation
Foundation
.
Modal
.
Hilbert
.
GL_K4Loeb_K4Henkin_K4Hen
Search
return to top
source
Imports
Init
Foundation.Modal.Hilbert.Normal.Basic
Foundation.Modal.Hilbert.WithHenkin.Basic
Foundation.Modal.Hilbert.WithLoeb.Basic
Imported by
LO
.
Modal
.
provable_GL_TFAE
LO
.
Modal
.
instEquivFormulaNatLogicGLK4Loeb
LO
.
Modal
.
instEquivFormulaNatLogicGLK4Henkin
LO
.
Modal
.
instEquivFormulaNatLogicGLK4Hen
source
theorem
LO
.
Modal
.
provable_GL_TFAE
{
φ
:
Formula
ℕ
}
:
[
Modal.GL
⊢
φ
,
Modal.K4Loeb
⊢
φ
,
Modal.K4Henkin
⊢
φ
,
Modal.K4Hen
⊢
φ
]
.
TFAE
source
instance
LO
.
Modal
.
instEquivFormulaNatLogicGLK4Loeb
:
Modal.GL
≊
Modal.K4Loeb
source
instance
LO
.
Modal
.
instEquivFormulaNatLogicGLK4Henkin
:
Modal.GL
≊
Modal.K4Henkin
source
instance
LO
.
Modal
.
instEquivFormulaNatLogicGLK4Hen
:
Modal.GL
≊
Modal.K4Hen