Provable formulas

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(→‎Monoidality of exponentials: monoidality laws for additives)
(→‎Distributivities: tens/with added)
Line 6: Line 6:
   
 
== Distributivities ==
  
== Distributivities ==
  +
  +
<math>A\tens (B\parr C) \limp (A\tens B)\parr C</math>
   
 
<math>A\plus (B\with C) \limp (A\plus B)\with (A\plus C)</math>
  
<math>A\plus (B\with C) \limp (A\plus B)\with (A\plus C)</math>
   
−
<math>A\tens (B\parr C) \limp (A\tens B)\parr C</math>
 +
<math>A\tens (B\with C) \limp (A\tens B)\with (A\tens C)</math>
   
 
== Factorizations ==
  
== Factorizations ==

Revision as of 19:21, 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

Distributivities

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

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

A\tens (B\with C) \limp (A\tens B)\with (A\tens 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}

Quantifiers

\begin{array}{rcll} A &\limp& \forall \xi.A &\quad (\xi\notin A) \\ \exists \xi.A &\limp& A &\quad (\xi\notin A) \end{array}


\begin{array}{rcl} \forall \xi_1.\forall \xi_2. A &\limp& \forall \xi. A[^\xi/_{\xi_1},^\xi/_{\xi_2}] \\ \exists \xi.A[^\xi/_{\xi_1},^\xi/_{\xi_2}] &\limp& \exists \xi_1. \exists \xi_2.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) \\ \\ \oc{(A \with B)} &\limp& \oc{A} \with \oc{B} \\ \wn{A} \plus \wn{B} &\limp& \wn{(A \plus B)} \\ \\ \wn{(A \with B)} &\limp& \wn{A} \with \wn{B} \\ \oc{A} \plus \oc{B} &\limp& \oc{(A \plus B)} \end{array}

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