theorem LO.Modal.provable_S4_of_provable_efq {α : Type u} [DecidableEq α] [Inhabited α] [Encodable α] {p : LO.IntProp.Formula α} : 𝐒𝟒 ⊢! pᵍ → 𝐈𝐧𝐭 ⊢! p

theorem LO.Modal.provable_efq_iff_provable_S4 {α : Type u} [DecidableEq α] [Inhabited α] [Encodable α] {p : LO.IntProp.Formula α} : 𝐈𝐧𝐭 ⊢! p ↔ 𝐒𝟒 ⊢! pᵍ

instance LO.Modal.instModalCompanionIntuitionisticS4 {α : Type u} [DecidableEq α] [Inhabited α] [Encodable α] : LO.Modal.ModalCompanion 𝐈𝐧𝐭 𝐒𝟒

Equations

• LO.Modal.instModalCompanionIntuitionisticS4 = { companion := ⋯ }