Negative $N$ | $::=$ | $P \imp N \celse N \land N \celse \top \celse \Diamond 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$ |
$N$ | $N^w$ |
$P \imp N$ | $P^w \imp N^w$ |
$N_1 \land N_2$ | $N_1^w \land N_2^w$ |
$\top$ | $\top$ |
$\Diamond P$ | $\forall \phi . \dns (\forall v \ge w . P^v \to h(v \phi \star)) \to h(w \phi \star)$ |
$a^-$ | $\forall \phi m . a^+(w\phi) \to h(w \phi m)$ |
$\ups P$ | $\forall \phi m . \dns (P^w \to h(w \phi m)) \to h(w \phi m)$ |
$P$ | $P^w$ |
$P_1 \tensor P_2$ | $P_1^w \tensor P_2^w$ |
$P_1 \lor P_2$ | $P_1^w \lor P_2^w$ |
$1$ | $1$ |
$0$ | $0$ |
$\square N$ | $\dns \forall v \ge w . N^v$ |
$a^+$ | $a^+(w)$ |
$\dns N$ | $\dns N^w$ |