Documentation

Foundation.Modal.Hilbert.GL_K4Loeb_K4Henkin_K4Hen

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