Provable formulas

Revision as of 16:02, 28 October 2013

This page is a stub and needs more content.

Important provable formulas are given by isomorphisms and by equivalences.

In many of the cases below the converse implication does not hold.

Distributivities

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

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

Factorizations

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

Additive structure

$\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}$

Exponential structure

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}$

Monoidality of exponential

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

Provable formulas

Revision as of 16:02, 28 October 2013

Contents

Distributivities

Factorizations

Additive structure

Exponential structure

Monoidality of exponential

Views

Personal tools

Navigation

Search

Tools

@@ Line 39: / Line 39: @@
 <math>
 \begin{array}{rclcrcl}
+  \wn(A\parr B) &\limp& \wn A\parr\wn B &\quad&
+  \wn\bot &\limp& \bot \\
   \oc A\tens\oc B &\limp& \oc(A\tens B) &\quad&
-  \one &\limp& \oc\one\\
+  \one &\limp& \oc\one \\
 \end{array}
 </math>