$
\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 \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:
- $t_1 \ge t_2$ is a positive atom on two Kripke worlds,
- $f \sqsubseteq t$ is a positive atom on a frame and a world.
- $q \sqsubseteq t$ is a positive atom on a resource and a world.
- $q \ttrov f$ is a negative atom taking a resource, a world, and a frame.
- $\star_n(a^-, f, t)$ is a positive atom taking a negative source-language atom, a frame, and a world.
- $\star_p(a^+, q, t)$ is a positive atom taking a positive source-language atom, a resource, and a world.
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.