For some time I've been trying to find a nice reductionistic answer to the question of what is the deal with Pfenning-Davies 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 first-order 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 Pfenning-Davies box. Pfenning-Davies $\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)$$

$N$ $N^{t\phi}$ $P \imp N$ $P^t \tensor N^{t\phi}$ $N_1 \land N_2$ $N_1^{t\phi} \lor N_2^{t\phi}$ $\bot$ $1$ $\top$ $0$ $a^-$ $ a^+(t\phi)$ $\ups P$ $\dns P^{t\phi}$ $\Diamond P$ $ \dns \forall s \ge t . P^{s\phi}$ $\altsquare P$ $ \exists s \ge t . \dns P^{s\phi}$ $\bigcirc N$ $\star(\phi) \tensor N^{t\phi}$

$P$ $P^t$ $P_1 \tensor P_2$ $P_1^t \tensor P_2^t$ $P_1 \lor P_2$ $P_1^t \lor P_2^t$ $1$ $1$ $0$ $0$ $a^+$ $a^+(t)$ $\dns N$ $\dns N^t$ $\square N$ $\dns \forall s \ge t . N^s$ $\altdiamond N$ $ \exists s \ge t . \dns N^s$

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 Pfenning-Davies coincides with provability of $\prov \forall \phi . ( N^*)^{t\phi} \to h(t\phi)$ in focused first-order logic.