Provable formulas

From LLWiki
(Difference between revisions)
Jump to: navigation, search
m (→‎Monoidality of exponential: Duals added)
(Identites added)
 
(12 intermediate revisions by one user not shown)
Line 1: Line 1:
−
{{stub}}
  
−  
 
Important provable formulas are given by [[List of isomorphisms|isomorphisms]] and by [[List of equivalences|equivalences]].
  
Important provable formulas are given by [[List of isomorphisms|isomorphisms]] and by [[List of equivalences|equivalences]].
   
Line 6: Line 4:
   
 
== Distributivities ==
  
== Distributivities ==
  +
  +
=== Standard distributivities ===
   
 
<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\with C) \limp (A\tens B)\with (A\tens C)</math>
  +
  +
<math>\exists \xi . (A \with B) \limp (\exists \xi . A) \with (\exists \xi . B)</math>
  +
  +
=== Linear distributivities ===
   
 
<math>A\tens (B\parr C) \limp (A\tens B)\parr C</math>
  
<math>A\tens (B\parr C) \limp (A\tens B)\parr C</math>
  +
  +
<math>\exists \xi. (A \parr B) \limp A \parr \exists \xi.B \quad (\xi\notin A)</math>
  +
  +
<math>A \tens \forall \xi.B \limp \forall \xi. (A \tens B) \quad (\xi\notin A)</math>
   
 
== Factorizations ==
  
== Factorizations ==
   
 
<math>(A\with B)\plus (A\with C) \limp A\with (B\plus C)</math>
  
<math>(A\with B)\plus (A\with C) \limp A\with (B\plus C)</math>
  +
  +
<math>(A\parr B)\plus (A\parr C) \limp A\parr (B\plus C)</math>
  +
  +
<math>(\forall \xi . A) \plus (\forall \xi . B) \limp \forall \xi . (A \plus B)</math>
  +
  +
== Identities ==
  +
  +
<math>\one \limp A\orth\parr A</math>
  +
  +
<math>A\tens A\orth \limp\bot</math>
   
 
== Additive structure ==
  
== Additive structure ==
  +
  +
<math>
  +
\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}
  +
</math>
  +
  +
== Quantifiers ==
  +
  +
<math>
  +
\begin{array}{rcll}
  +
A &\limp& \forall \xi.A &\quad (\xi\notin A) \\
  +
\exists \xi.A &\limp& A &\quad (\xi\notin A)
  +
\end{array}
  +
</math>
  +
  +
<br />
   
 
<math>
  
<math>
 
\begin{array}{rcl}
  
\begin{array}{rcl}
−
A\with B \limp A &\quad& A\with B \limp B\\
 +
\forall \xi_1.\forall \xi_2. A &\limp& \forall \xi. A[^\xi/_{\xi_1},^\xi/_{\xi_2}] \\
−
A \limp A\plus B &\quad& B \limp A\plus B\\
 +
\exists \xi.A[^\xi/_{\xi_1},^\xi/_{\xi_2}] &\limp& \exists \xi_1. \exists \xi_2.A
 
\end{array}
  
\end{array}
 
</math>
  
</math>
Line 35: Line 73:
 
</math>
  
</math>
   
−
== Monoidality of exponential ==
 +
== Monoidality of exponentials ==
   
 
<math>
  
<math>
−
\begin{array}{rclcrcl}
 +
\begin{array}{rcl}
−
\wn(A\parr B) &\limp& \wn A\parr\wn B &\quad&
 +
\wn(A\parr B) &\limp& \wn A\parr\wn B \\
−
\wn\bot &\limp& \bot \\
 +
\oc A\tens\oc B &\limp& \oc(A\tens B) \\
−
\oc A\tens\oc B &\limp& \oc(A\tens B) &\quad&
 +
\\
−
\one &\limp& \oc\one \\
 +
\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}
  
\end{array}
 
</math>
  
</math>
  +
  +
== Promotion principles ==
  +
  +
<math>
  +
\begin{array}{rcl}
  +
\oc{A} \tens \wn{B} &\limp& \wn{(A \tens B)} \\
  +
\oc{(A \parr B)} &\limp& \wn{A} \parr \oc{B}
  +
\end{array}
  +
</math>
  +
  +
== Commutations ==
  +
  +
<math>\exists \xi . \wn A \limp \wn{\exists \xi . A}</math>
  +
  +
<math>\oc{\forall \xi . A} \limp \forall \xi . \oc A</math>
  +
  +
<math>\wn{\forall \xi . A} \limp \forall \xi . \wn A</math>
  +
  +
<math>\exists \xi . \oc A \limp \oc{\exists \xi . A}</math>

Latest revision as of 14:27, 29 October 2013

Important provable formulas are given by isomorphisms and by equivalences.

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

Contents

[edit] Distributivities

[edit] Standard distributivities

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)

\exists \xi . (A \with B) \limp (\exists \xi . A) \with (\exists \xi . B)

[edit] Linear distributivities

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

\exists \xi. (A \parr B) \limp A \parr \exists \xi.B \quad (\xi\notin A)

A \tens \forall \xi.B \limp \forall \xi. (A \tens B) \quad (\xi\notin A)

[edit] Factorizations

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

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

(\forall \xi . A) \plus (\forall \xi . B) \limp \forall \xi . (A \plus B)

[edit] Identities

\one \limp A\orth\parr A

A\tens A\orth \limp\bot

[edit] 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}

[edit] 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}

[edit] 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}

[edit] 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}

[edit] Promotion principles

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

[edit] Commutations

\exists \xi . \wn A \limp \wn{\exists \xi . A}

\oc{\forall \xi . A} \limp \forall \xi . \oc A

\wn{\forall \xi . A} \limp \forall \xi . \wn A

\exists \xi . \oc A \limp \oc{\exists \xi . A}

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