theorem LO.Modal.provable_S4_of_provable_efq {φ : LO.IntProp.Formula ℕ} : LO.Modal.Hilbert.S4 ℕ ⊢! φᵍ → LO.IntProp.Hilbert.Int ℕ ⊢! φ

theorem LO.Modal.provable_efq_iff_provable_S4 {φ : LO.IntProp.Formula ℕ} : LO.IntProp.Hilbert.Int ℕ ⊢! φ ↔ LO.Modal.Hilbert.S4 ℕ ⊢! φᵍ

instance LO.Modal.instModalCompanionNatIntS4 : LO.Modal.ModalCompanion (LO.IntProp.Hilbert.Int ℕ) (LO.Modal.Hilbert.S4 ℕ)

Equations

• LO.Modal.instModalCompanionNatIntS4 = ⋯