Lattice of exponential modalities - Revision history

Olivier Laurent: Pointer to list of equivalences

2014-11-21T10:26:12Z

Pointer to list of equivalences

Olivier Laurent: Proof sketches

2011-02-21T15:03:21Z

Proof sketches

Olivier Laurent: typo

2011-02-21T14:19:42Z

typo

Olivier Laurent: Typo: same lemma twice

2011-02-21T11:41:40Z

Typo: same lemma twice

Olivier Laurent: First complete description of this lattice (and can ingredients for the proof)

2011-02-21T11:39:09Z

First complete description of this lattice (and can ingredients for the proof)

Olivier Laurent: declared as stub

2009-10-16T21:28:10Z

declared as stub

Olivier Laurent: lattice drawing only

2009-10-05T21:37:13Z

lattice drawing only

New page

<math>
\xymatrix{
& & {\wn} \\
& & & & {\wn\oc\wn}\ar[ull] \\
\emptyset\ar[uurr] & & & {\oc\wn} \ar[ur] & & {\wn\oc} \ar[ul] \\
& & & & {\oc\wn\oc} \ar[ul]\ar[ur] \\
& & {\oc} \ar[uull]\ar[urr]
}
</math>

@@ Line 11: / Line 11: @@
 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 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>.
+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|

@@ Line 32: / Line 32: @@
 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.
-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 and moreover we can prove that no other relation between classes is true (by relying on the following lemma).
+{{Proof|
 {{Lemma|
 If <math>\alpha</math> is an atom, <math>\wn{\alpha}\not\vdash\alpha</math> and
-<math>\wn{\alpha}\not\vdash\wn{\oc{\wn{\alpha}}}</math>.
+<math>\alpha\not\vdash\wn{\oc{\wn{\alpha}}}</math>.
 }}

@@ Line 19: / Line 19: @@
 {{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>.
 }}

@@ Line 1: / Line 1: @@
 <math>
 \xymatrix{
@@ Line 10: / Line 8: @@
+}
 </math>

← Older revision		Revision as of 21:28, 16 October 2009
Line 1:		Line 1:
		+	{{stub}}
		+
	<math>		<math>
	\xymatrix{		\xymatrix{

@@ Line 3: / Line 3: @@
  & & {\wn} \\
  & & & & {\wn\oc\wn}\ar[ull] \\
-\emptyset\ar[uurr] & & & {\oc\wn} \ar[ur] & & {\wn\oc} \ar[ul] \\
+\varepsilon\ar[uurr] & & & {\oc\wn} \ar[ur] & & {\wn\oc} \ar[ul] \\
  & & & & {\oc\wn\oc} \ar[ul]\ar[ur] \\
  & & {\oc} \ar[uull]\ar[urr]