A modal companion of a superintuitionistic logic is a modal logic above that “simulates” . The strict conditional of such a modal logic, when restricted to boxed atoms, behaves in the exact same way as the Heyting implication connective behaves in . In fact, there is a natural full and faithful translation of into any of its modal companions, called the Gödel translation.
Definition
The Gödel translation is a map from intuitionistic formulae to monomodal formulae defined recursively as follows.
A modal companion of a a superintuitionistic logic is a modal logic above such that is a full and faithful translation of into . That is:
The Gödel translation can be extended to rules by putting . We can then define a modal companion of a superintuitionistic rule system the same way.
Modal companion mappings
The theory of modal companions revolves mostly around studying the properties of three (families of) mappings: and . These mappings can be thought of as mappings on logics, on algebras or on spaces.
Mappings on logics
We have effectively already introduced the mapping on logics (and rule systems). If is a modal logic above , we put
This is always a superintuitionistic logic.
In the other direction: if is a superintuitionistic logic, we put
It turns out that and are respectively the weakest and strongest modal companions of .