Provable formulas

Revision as of 15:55, 28 October 2013

This page is a stub and needs more content.

Important provable formulas are given by isomorphisms and by equivalences.

$A\plus (B\with C) \limp (A\plus B)\with (A\plus C)$

$A\tens (B\parr C) \limp (A\tens B)\parr C$

$(A\with B)\plus (A\with C) \limp A\with (B\plus C)$

$\begin{array}{rcl} A\with B \limp A &\quad& A\with B \limp B\\ A \limp A\plus B &\quad& B \limp A\plus B\\ \end{array}$

Provable formulas involving exponential connectives only provide us with the lattice of exponential modalities.

$\begin{array}{rclcrcl} \oc A &\limp& A &\quad& A&\limp&\wn A\\ \oc A &\limp& 1 &\quad& \bot &\limp& \wn A \end{array}$

$\begin{array}{rclcrcl} \oc A\tens\oc B &\limp& \oc(A\tens B) &\quad& \one &\limp& \oc\one\\ \end{array}$

@@ Line 1: / Line 1: @@
 {{stub}}
+Important provable formulas are given by [[List of isomorphisms|isomorphisms]] and by [[List of equivalences|equivalences]].
 In many of the cases below the [[Non provable formulas|converse implication does not hold]].
@@ Line 18: / Line 20: @@
 \begin{array}{rcl}
   A\with B \limp A &\quad& A\with B \limp B\\
-  (C\limp A)\with(C\limp B) &\limp& C\limp(A\with B)\\
-  A &\limp& A\with A\\
   A \limp A\plus B &\quad& B \limp A\plus B\\
-  (A\limp C)\with(B\limp C) &\limp& (A\plus B)\limp C\\
-  A\plus A &\limp& A\\
 \end{array}
 </math>
@@ Line 33: / Line 31: @@
 \begin{array}{rclcrcl}
   \oc A &\limp& A &\quad& A&\limp&\wn A\\
-  \oc A &\limp& 1 &\quad& \bot &\limp& \wn A\\
+  \oc A &\limp& 1 &\quad& \bot &\limp& \wn A
-  \oc A &\limp& \oc A\tens\oc A &\quad&
-  \wn A\parr\wn A &\limp& \wn A\\
-  \oc A &\limp& \oc\oc A &\quad& \wn\wn A &\limp& \wn A\\
 \end{array}
 </math>
@@ Line 45: / Line 43: @@
 \end{array}
 </math>
-Other provable formulas are given by [[List of isomorphisms|isomorphisms]].