$ \def\dash{\unicode{8212}} \def\trov{\triangleright} \def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\ddns{{\Downarrow}} \def\ups{{\uparrow}} \def\preq{\dashv\vdash} \def\sh{\#} \def\lol{\multimap} \def\tensor{\otimes} \def\wat#1{\mathrel{@_{#1}}} \def\bull#1{\mathrel{\bullet_{#1}}} \def\hole{\unicode{9728}} \def\cn{{:}} \def\here{\dns} \def\dia{{\large\unicode{9671}}} $

Language A

Negative $N$	$::=$	$P \lol N \celse N \land N \celse \top \celse \dia P \celse a^- \celse \ups P$
Positive $P$	$::=$	$P \tensor P \celse P \lor P \celse 1 \celse 0 \celse \square N \celse a^+ \celse \dns N$

Translation from A to B

We postulate three sorts of first-order terms, frames ($\phi, f, \ldots$) resources ($\alpha, p, \ldots$) and Kripke worlds ($s, t, \ldots$). We overload the symbols $\lol$ and $\tensor$ as example frame and resource constructors.

The expressions $p\trov f$ and $\star(f)$ are negative atoms. Every Language-A atom (regardless of polarity) is mapped to a Language-B positive atom. The expression $s \ge t$ is a positive atom. The expression $\forall s \ge t . N$ abbreviates $\forall s . (s \ge t) \imp N$. $$P^\bullet_t(\phi) = \forall\alpha \cn P^t . (\alpha\trov \phi)$$ $$N^\bullet_t(\alpha) = \forall\phi \cn N^t . (\alpha\trov \phi)$$

$N$ $N^t$

$P \lol N$ $\exists \alpha \cn P^t . \exists \phi \cn N^t . [\alpha \lol \phi]$

$N_1 \land N_2$ $N_1^t \lor N_2^t$

$\top$ $0$

$\dia P$ $\eta \phi . \star(\phi) \tensor \dns \forall s \ge t . P^\bullet_s(\phi)$

$a^-$ $ \eta\phi . a^+(\phi, t)$

$\ups P$ $\eta \phi . \dns P^\bullet_t(\phi)$

$P$ $P^t$

$P_1 \tensor P_2$ $ \exists \alpha_1 \cn P_1^ t. \exists \alpha_2 \cn P_2^ t . [\alpha_1 \tensor \alpha_2]$

$P_1 \lor P_2$ $P_1 ^t \lor P_2 ^ t $

$1$ $[\epsilon]$

$0$ $0$

$\square N$ $\eta \alpha . \dns \forall s \ge t . N^\bullet_s(\alpha)$

$a^+$ $\eta\alpha . a^+(\alpha, t)$

$\dns N$ $\eta \alpha .\dns N^\bullet_t(\alpha)$

Language B

Prenegative $M$	$::=$	$\dns N \celse a^+(t)\celse M \tensor M$
Negative $N$	$::=$	$\forall x\cn P.N \celse M\imp N \celse N \land N \celse \top \celse a^-(t)$
Positive $P$	$::=$	$\exists x \cn P.P \celse P \lor P \celse 0 \celse [t]\celse \eta x . M$
Contexts $\Gamma$	$::=$	$\cdot \celse \Gamma, M \celse \Gamma, x:P$
Conclusions $K$	$::=$	$t:P \celse N \celse M$

Sequents are either $\Gamma\prov K$. Contex class="right"ts are dependent and therefore ordered. Context variables can appear in the propositions attached to variable bindings to their right, although $x$ may not occur in the $P$ of $x:P$ itself. The metavariable $J$ stands for an arbitrary $\Gamma' \prov K$. When we say $\Gamma \prov J$, we mean $\Gamma, \Gamma' \prov K$. $$ {\Gamma\prov N \over \Gamma\prov \dns N} \qquad {\Gamma, \dns N \prov J \over \Gamma, N \prov J} $$ $$ { \Gamma\prov M_1 \qquad \Gamma\prov M_2\over \Gamma \prov M_1\tensor M_2} \qquad {\Gamma, M_1, M_2 \prov J \over M_1\tensor M_2\prov J} $$ $$ {\over\Gamma, a^+(t), \Gamma' \prov a^+(t)} \qquad {\over\Gamma, a^-(t), \Gamma' \prov a^-(t)} $$ $$ {\Gamma, x:P \prov N \over\Gamma \prov \forall x\cn P . N} \qquad {\Gamma\prov t : P \qquad \Gamma, [t/x] N\prov J \over\Gamma, \forall x \cn P . N \prov J} $$ $$ {\Gamma, M \prov N \over\Gamma \prov M\imp N} \qquad {\Gamma\prov M \qquad \Gamma, N\prov J \over\Gamma, M \imp N \prov J} $$ $$ {\Gamma, N_i\prov J \over\Gamma,N_1 \land N_2\prov J}\qquad {\Gamma\prov N_1\qquad\Gamma\prov N_2 \over \Gamma \prov N_1 \land N_2 } $$ $$ {\over \Gamma \prov \top} \qquad{\over \Gamma,0,\Gamma' \prov J} \qquad{\over \Gamma \prov t : 1} \qquad{\over \Gamma \prov t : [t]} $$ $$ {\Gamma\prov[t/x]J \over\Gamma, x:[t] \prov J}\qquad {\Gamma\prov t : P\qquad \Gamma \prov s : [t/x]P' \over\Gamma \prov s : \exists x\cn P . P'} \qquad {\Gamma, x :P, y : P' \prov J \over\Gamma, y : \exists x \cn P . P' \prov J} $$ $$ {\Gamma \prov t: P_i\over\Gamma\prov t:P_1 \lor P_2}\qquad {\Gamma, x:P_1\prov J\qquad\Gamma, x:P_2\prov J \over \Gamma, x:P_1 \lor P_2 \prov J} $$ $$ { \Gamma\prov [t/x]M \over\Gamma \prov t : \eta x . M }\qquad {\Gamma, y, [y/x]M \prov J \over\Gamma, y : \eta x . M\prov J} $$

Translation from B to C

Translate sequents like this: For all $N$ we have $$\Gamma\prov t : P \qquad\Longleftrightarrow\qquad \forall \Gamma . ((\forall x\cn P^* .N) \imp [t/x]N)$$ And furthermore $$\Gamma\prov N \qquad\Longleftrightarrow\qquad \forall \Gamma . N^*$$ $$\Gamma\prov M \qquad\Longleftrightarrow\qquad \forall \Gamma . M^*$$ Quantify over contexts like this: $$\forall(\Gamma, x :P).N = \forall\Gamma.\forall x\cn P^* . N$$ $$\forall(\Gamma, M).N = \forall\Gamma.M^*\imp N$$ $$\forall(\cdot).N = N$$ What $X^*$ means is a recursive elimination of every $\forall x \cn P.N$ according to this function:

$P$	$\forall x \cn P . N $
$\exists y \cn P_1 . P_2$	$ \forall y \cn P_1 . \forall x \cn P_2.N$
$P_1 \lor P_2$	$ \forall x \cn P_1 . N \land \forall x \cn P_2 . N$
$0$	$ \top$
$1$	$ \forall x . N$
$[t]$	$ [t/x]N$
$\eta x \cn P . M$	$ \forall x \cn P. (M\imp N)$

Language C

Prenegative $M$	$::=$	$\dns N \celse a^+(t)$
Negative $N$	$::=$	$\forall x .N \celse M\imp N \celse a^-(t) \celse N \land N \celse \top$
Contexts $\Gamma$	$::=$	$\cdot \celse \Gamma, M $