$ \def\dash{\unicode{8212}} \def\trov{\triangleright} \def\ttrov{\triangleright_t} \def\xtrov{\triangleright_x} \def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\ups{{\uparrow}} \def\preq{\dashv\vdash} \def\sh{\#} \def\lol{\multimap} \def\lto{\rightarrowtail} \def\rto{\twoheadrightarrow} \def\tensor{\otimes} \def\wat#1{\mathrel{@_{#1}}} \def\ast#1{\mathrel{*_{#1}}} \def\bull#1{\mathrel{\bullet_{#1}}} \def\rle{=} $
$P / N$$P\ast t q / N\ast t f$
$P \lto N$ $\exists \alpha. (P \ast t \alpha) \land \exists \phi . (N \ast t \phi) \land (\alpha \lto \phi \rle f)$
$P \rto N$ $\exists \alpha. (P \ast t \alpha) \land \exists \phi . (N \ast t \phi) \land (\alpha \rto \phi \rle f)$
$P_1 \tensor P_2$ $\exists \alpha_1. (P_1 \ast t \alpha_1) \land \exists \alpha_2 . (P_2 \ast t \alpha_2) \land (\alpha_1 * \alpha_2 \rle q)$
$1$ $1 \rle q$
$N_1 \land N_2$ $N_1 \ast t f \lor N_2 \ast t f$
$P_1 \lor P_2$ $P_1 \ast t q \lor P_2 \ast t q$
$\top$ $\bot$
$0$ $\bot$
$a^-$ $\star_n(a^-, f, t)$
$a^+$ $\star_p(a^+,q, t)$
$\ups P$ $\dns (P \bull t f)$
$\dns N$ $\dns (N \bull t q)$
$\Diamond P$ $ f \sqsubseteq t \land \dns \forall x \ge t . P \bull x f$
$\square N$ $q \sqsubseteq t \land \dns \forall x \ge t . N \bull x q$
We translate positive propositions $P$ at `resource descriptors' $q$, and negatives $N$ at `frame descriptors' $f$. Both translations are also parametrized by a kripke world $t$. These are characterized by:
Frames $f$$::=$$q \lto f \celse q \rto f \celse \phi $
Resources $q$$::=$$q \tensor q \celse 1 \celse \alpha$
Kripke Worlds $t$$::=$$x$
This definition uses the following abbreviations: $$ P \bull t f = \forall \alpha. P \ast t \alpha \imp \alpha \ttrov f$$ $$ N \bull t q = \forall \phi. N \ast t \phi \imp q \ttrov \phi$$ A resource is really just a collection of resource variables, which describes the shape of a context, also known as a sequent minus its conclusion. A frame is just a frame variable, with some resource variables glommed onto it, which describes the shape of a sequent minus a hypothesis. We bake in some equalities on worlds and frames to capture the context equivalences of linear logic.

The atomic propositions I'm positing to exist in the destination language are: Equality on atoms $q \ttrov f$ must at least have the adjunctions $$(q_1 \ttrov q_2 \rto f) = (q_1 \tensor q_2 \ttrov f) = (q_2 \ttrov q_1 \lto f)$$ but we can impose additional axioms to get ordered ($q_1 \tensor (q_2 \tensor q_3) = (q_1 \tensor q_2) \tensor q_3$) or linear ($q_1 \tensor q_2 = q_2 \tensor q_1$) or intuitionistic ($q = 1$) logic.

We also always want the compatibility axioms $$ \frac {q \sqsubseteq t \qquad f \sqsubseteq t } {q \lto f \sqsubseteq t} \qquad \frac {q \sqsubseteq t \qquad f \sqsubseteq t } {q \rto f \sqsubseteq t} \qquad \frac {q_1 \sqsubseteq t \qquad q_2 \sqsubseteq t } {q_1 \tensor q_2 \sqsubseteq t} \qquad \frac {} {1 \sqsubseteq t} $$

If you want the modal logic K, don't add any more axioms for $\sqsubseteq$ or $\ge$.

If you want the modal logic T, add reflexivity for $\ge$.

If you want the modal logic K4, add transitivity for $\ge$ and "transitivity" for $\sqsubseteq$: $$ \frac {f \sqsubseteq t \qquad t \le t'} {f \sqsubseteq t'} \qquad \frac {q \sqsubseteq t \qquad t \le t'} {q \sqsubseteq t'} $$

If you want the modal logic S4, take the union of the axioms in T and K4.