Lattice of exponential modalities

$\xymatrix{ & & {\wn} \\ & & & & {\wn\oc\wn}\ar[ull] \\ \varepsilon\ar[uurr] & & & {\oc\wn} \ar[ur] & & {\wn\oc} \ar[ul] \\ & & & & {\oc\wn\oc} \ar[ul]\ar[ur] \\ & & {\oc} \ar[uull]\ar[urr] }$

An exponential modality is an arbitrary (possibly empty) sequence of the two exponential connectives $\oc$ and $\wn$. It can be considered itself as a unary connective. This leads to the notation μA for applying an exponential modality μ to a formula A.

There is a preorder relation on exponential modalities defined by $\mu\lesssim\nu$ if and only if for any formula A we have $\mu A\vdash \nu A$. It induces an equivalence relation on exponential modalities by μ˜ν if and only if $\mu\lesssim\nu$ and $\nu\lesssim\mu$.

Lemma

For any formula A, $\oc{A}\vdash A$ and $A\vdash\wn{A}$.

Lemma (Functoriality)

If A and B are two formulas such that $A\vdash B$ then, for any exponential modality μ, $\mu A\vdash \mu B$.

Lemma

For any formula A, $\oc{A}\vdash \oc{\oc{A}}$ and $\wn{\wn{A}}\vdash\wn{A}$.

Lemma

For any formula A, $\oc{A}\vdash \oc{\wn{\oc{A}}}$ and $\wn{\oc{\wn{A}}}\vdash\wn{A}$.

This allows to prove that any exponential modality is equivalent to one of the following seven modalities: $\varepsilon$ (the empty modality), $\oc$, $\wn$, $\oc\wn$, $\wn\oc$, $\oc\wn\oc$ or $\wn\oc\wn$. Indeed any sequence of consecutive $\oc$ or $\wn$ in a modality can be simplified into only one occurrence, and then any alternating sequence of length at least four can be simplified into a smaller one.

The order relation induced on equivalence classes of exponential modalities with respect to ˜ can be proved to be the one represented on the picture in the top of this page. All the represented relations are valid and moreover we can prove that no other relation between classes is true (by relying on the following lemma).

Lemma

If α is an atom, $\wn{\alpha}\not\vdash\alpha$ and $\wn{\alpha}\not\vdash\wn{\oc{\wn{\alpha}}}$.

The order relation on equivalence classes of exponential modalities is a lattice.