Provable formulas

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(→‎Additive structure: Units added)
m (→‎Monoidality of exponential: typo)
Line 35: Line 35:
 
</math>
  
</math>
   
−
== Monoidality of exponential ==
 +
== Monoidality of exponentials ==
   
 
<math>
  
<math>

Revision as of 20:11, 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.

Contents

 [hide] 

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}{rclcrclcrcl} A\with B &\limp& A &\quad& A\with B &\limp& B &\quad& A &\limp& \top\\ A &\limp& A\plus B &\quad& B &\limp& A\plus B &\quad& \zero &\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 \end{array}

Monoidality of exponentials

\begin{array}{rcl} \wn(A\parr B) &\limp& \wn A\parr\wn B \\ \oc A\tens\oc B &\limp& \oc(A\tens B) \end{array}

Retrieved from "http://140.77.166.78/mediawiki/index.php?title=Provable_formulas&oldid=602"
Personal tools