View source for Lattice of exponential modalities

<math>
\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]
}
</math>

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

There is a preorder relation on exponential modalities defined by <math>\mu\lesssim\nu</math> if and only if for any formula <math>A</math> we have <math>\mu A\vdash \nu A</math>. It induces an [[List of equivalences|equivalence]] relation on exponential modalities by <math>\mu \sim \nu</math> if and only if <math>\mu\lesssim\nu</math> and <math>\nu\lesssim\mu</math>.

{{Lemma|
For any formula <math>A</math>, <math>\oc{A}\vdash A</math> and <math>A\vdash\wn{A}</math>.
}}

{{Lemma|title=Functoriality|
If <math>A</math> and <math>B</math> are two formulas such that <math>A\vdash B</math> then, for any exponential modality <math>\mu</math>, <math>\mu A\vdash \mu B</math>.
}}

{{Lemma|
For any formula <math>A</math>, <math>\oc{A}\vdash \oc{\oc{A}}</math> and <math>\wn{\wn{A}}\vdash\wn{A}</math>.
}}

{{Lemma|
For any formula <math>A</math>, <math>\oc{A}\vdash \oc{\wn{\oc{A}}}</math> and <math>\wn{\oc{\wn{A}}}\vdash\wn{A}</math>.
}}

This allows to prove that any exponential modality is equivalent to one of the following seven modalities: <math>\varepsilon</math> (the empty modality), <math>\oc</math>, <math>\wn</math>, <math>\oc\wn</math>, <math>\wn\oc</math>, <math>\oc\wn\oc</math> or <math>\wn\oc\wn</math>.
Indeed any sequence of consecutive <math>\oc</math> or <math>\wn</math> 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.

{{Proof|
We obtain <math>\oc{\oc{A}}\vdash\oc{A}</math> by functoriality from <math>\oc{A}\vdash A</math> (and similarly for <math>\wn{A}\vdash\wn{\wn{A}}</math>).
From <math>\oc{A}\vdash \oc{\wn{\oc{A}}}</math>, we deduce <math>\wn{\oc{A}}\vdash \wn{\oc{\wn{\oc{A}}}}</math> by functoriality and <math>\oc{\wn{B}}\vdash \oc{\wn{\oc{\wn{B}}}}</math> (with <math>A=\wn{B}</math>). In a similar way we have <math>\oc{\wn{\oc{\wn{A}}}}\vdash \oc{\wn{A}}</math> and <math>\wn{\oc{\wn{\oc{A}}}}\vdash \wn{\oc{A}}</math>.
}}

The order relation induced on equivalence classes of exponential modalities with respect to <math>\sim</math> can be proved to be the one represented on the picture in the top of this page. All the represented relations are valid.

{{Proof|
We have already seen <math>\oc{A}\vdash A</math> and <math>\oc{A}\vdash \oc{\wn{\oc{A}}}</math>. By functoriality we deduce <math>\oc{\wn{\oc{A}}}\vdash \oc{\wn{A}}</math> and by <math>A=\wn{\oc{B}}</math> we deduce <math>\oc{\wn{\oc{B}}}\vdash \wn{\oc{B}}</math>.

The others are obtained from these ones by duality: <math>A\vdash B</math> entails <math>B\orth\vdash A\orth</math>.
}}

{{Lemma|
If <math>\alpha</math> is an atom, <math>\wn{\alpha}\not\vdash\alpha</math> and 
<math>\alpha\not\vdash\wn{\oc{\wn{\alpha}}}</math>.
}}

We can prove that no other relation between classes is true (by relying on the previous lemma).

{{Proof|
From the lemma and <math>A\vdash\wn{A}</math>, we have <math>\wn{\alpha}\not\vdash\wn{\oc{\wn{\alpha}}}</math>.

Then <math>\wn</math> cannot be smaller than any other of the seven modalities (since they are all smaller than <math>\varepsilon</math> or <math>\wn\oc\wn</math>). For the same reason, <math>\varepsilon</math> cannot be smaller than <math>\oc</math>, <math>\oc\wn</math>, <math>\wn\oc</math> or <math>\oc\wn\oc</math>. This entails that <math>\wn\oc\wn</math> is only smaller than <math>\wn</math> since it is not smaller than <math>\varepsilon</math> (by duality from <math>\varepsilon</math> not smaller than <math>\oc\wn\oc</math>).

From these, <math>\wn{\oc{\alpha}}\not\vdash\oc{\wn{\alpha}}</math> and <math>\oc{\wn{\alpha}}\not\vdash\wn{\oc{\alpha}}</math>, we deduce that no other relation is possible.
}}

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