Provable formulas

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Added link to list of isomorphisms.)
m (→‎Monoidality of exponential: typo)
Line 50: Line 50:
   
   
−
Other provable formules are given by [[List of isomorphisms|isomorphisms]].
 +
Other provable formulas are given by [[List of isomorphisms|isomorphisms]].

Revision as of 22: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 formulas are given by isomorphisms.

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