$
\def\imp{\Rightarrow}
\def\celse{\ \ }
\def\prov{\vdash}
\def\dns{{\downarrow}}
\def\ups{{\uparrow}}
\def\preq{\dashv\vdash}
\def\sh{\#}
\def\tensor{\land^+}
\def\altdiamond{\blacklozenge}
\def\altsquare{\blacksquare}
$
For some time I've been trying to find a nice reductionistic answer to the question of what is the deal with
PfenningDavies style modalities, anyway?
Ideally something that smells like a Kripke semantics. This is the best I've got so far.
The game is to take a modal language and translate it away into firstorder logic. This is done in such a way as to preserve the intended focusing proof search behavior of the source language.
The source language is a polarized modal language. Polarized means that propositions are divide into positive and negative propositions.
Its syntax goes like this:
Negative $N$  $::=$  $P \imp N \celse N \land N \celse \top \celse a^ \celse \ups P \celse \Diamond P \celse \altsquare P \celse{\bigcirc N}$ 
Positive $P$  $::=$  $P \tensor P \celse P \lor P \celse 1 \celse 0 \celse a^+ \celse \dns N \celse \square N \celse \altdiamond N $ 
The distinction between negative $\land$ and positive $\tensor$ isn't
super important, since the two are effectively the same in a
nonsubstructural logic, but I like to keep the distinction since we're considering focusing.
There's a big zoo of various connectives here. $\square$ is PfenningDavies box. PfenningDavies $\Diamond$ decomposes
as $\bigcirc \Diamond$ in this language here. The usual lax logic connective is $\bigcirc \ups$. The modalities $\altsquare$ and
$\altdiamond$ are unfamiliar to me  they were backformed from throwing in an existential quantifier over worlds at certain points
in the translation where it wasn't already being used.
The target language is focused first order intuitionistic logic.
$$P^{t\phi} = P^t \imp h(t\phi)$$
$$N^t = \forall \phi. N^{t\phi} \imp h(t \phi)$$
For any proposition $X$, let $\bar X$ be $X$ with all pairs of double shifts removed.
Then
$\bar P^{t\phi} \preq P^{t\phi}$

$\bar N^{t} \preq N^{t}$

For any proposition $X$, let $X^*$ be $X$ with every $\Diamond$ replaced by $\bigcirc \Diamond$.
Then provability of $\prov N$ in PfenningDavies coincides
with provability of $\prov \forall \phi . ( N^*)^{t\phi} \to h(t\phi)$ in focused firstorder logic.