Modal Companion

Gödel-McKensey-Tarski Theorem

Through a translation called Gödel Translation from propositional logic formula to modal logic formula, intuitionistic logic $\mathbf{Int}$ can be embedded into $S4$. (This theorem is known as Gödel-McKensey-Tarski Theorem.)

def GoedelTranslation : Superintuitionistic.Formula α → Formula α

postfix:75 "ᵍ" => GoedelTranslation

theorem provable_efq_iff_provable_S4
  {p : Superintuitionistic.Formula α}
  : 𝐈𝐧𝐭 ⊢! p ↔ 𝐒𝟒 ⊢! pᵍ

• LO.Modal.Standard.provable_efq_iff_provable_S4

Modal Companion

The generalized version of this relationship is called Modal Companion. $(\mathbf{Int},S4)$ has modal companion.

class ModalCompanion (i𝓓 : Superintuitionistic.DeductionParameter α) (m𝓓 : Modal.Standard.DeductionParameter α) where
  companion : ∀ {p : Superintuitionistic.Formula α}, i𝓓 ⊢! p ↔ m𝓓 ⊢! pᵍ

instance : ModalCompanion 𝐈𝐧𝐭 𝐒𝟒

• LO.Modal.Standard.instModalCompanionIntuitionisticS4