Provable formulas

From LLWiki
(Difference between revisions)
Jump to: navigation, search
m (\limp instead of \longrightarrow)
(Added link to list of isomorphisms.)
Line 48: Line 48:
 
\end{array}
  
\end{array}
 
</math>
  
</math>
  +
  +
  +
Other provable formules are given by [[List of isomorphisms|isomorphisms]].

Revision as of 21:09, 25 April 2013

This page is a stub and needs more content.

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

Contents

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

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

Monoidality of exponential

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


Other provable formules are given by isomorphisms.

Retrieved from "http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Provable_formulas&oldid=584"