There are some attempts to introduce modalities in substructural logics. But, the selection of axioms for modalities looks sometimes ad hoc, as non-modal logical connectives in substructural logics are not related to each other like those in classical logic.

We propose a way — a proper way we hope — of introducing modalities over full Lambek logic FL. In algebraic terms, our modal operators are

“conuclei” on residuated lattices.

Using these modalities, Goedel translation can be naturally extended to one from substructural logics over FL to modal substructural logics over our FLS4. Moreover, Girard’s translation of intuitionistic logic into intuitionistic linear logic with exponential can be obtained as a particular case of our result.