Provable formulas

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(→‎Factorizations: Link to the lattice of exponential modalities added.)
(Added formules from Semantics page)
Line 1: Line 1:
 
{{stub}}
  
{{stub}}
  +
  +
In many of the cases below the [[Non provable formulas|converse implication does not hold]].
   
 
== Distributivities ==
  
== Distributivities ==
Line 11: Line 13:
 
<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>
   
−
In many of the above cases the [[Non provable formulas|converse implication does not hold]].
 +
== Additive structure ==
   
−
== Exponentials ==
 +
<math>
  +
\begin{array}{rcl}
  +
A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\
  +
(C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\
  +
A &\longrightarrow& A\with A\\
  +
A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\
  +
(A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\
  +
A\plus A &\longrightarrow& A\\
  +
\end{array}
  +
</math>
  +
  +
== Exponential structure ==
   
 
Provable formulas involving exponential connectives only provide us with the [[lattice of exponential modalities]].
  
Provable formulas involving exponential connectives only provide us with the [[lattice of exponential modalities]].
  +
  +
<math>
  +
\begin{array}{rclcrcl}
  +
\oc A &\longrightarrow& A &\quad& A&\longrightarrow&\wn A\\
  +
\oc A &\longrightarrow& 1 &\quad& \bot &\longrightarrow& \wn A\\
  +
\oc A &\longrightarrow& \oc A\tens\oc A &\quad&
  +
\wn A\parr\wn A &\longrightarrow& \wn A\\
  +
\oc A &\longrightarrow& \oc\oc A &\quad& \wn\wn A &\longrightarrow& \wn A\\
  +
\end{array}
  +
</math>
  +
  +
== Monoidality of exponential ==
  +
  +
<math>
  +
\begin{array}{rclcrcl}
  +
\oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&
  +
\one &\longrightarrow& \oc\one\\
  +
\end{array}
  +
</math>

Revision as of 21:56, 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 \longrightarrow A &\quad& A\with B \longrightarrow B\\ (C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\ A &\longrightarrow& A\with A\\ A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\ (A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\ A\plus A &\longrightarrow& A\\ \end{array}

Exponential structure

Provable formulas involving exponential connectives only provide us with the lattice of exponential modalities.

\begin{array}{rclcrcl} \oc A &\longrightarrow& A &\quad& A&\longrightarrow&\wn A\\ \oc A &\longrightarrow& 1 &\quad& \bot &\longrightarrow& \wn A\\ \oc A &\longrightarrow& \oc A\tens\oc A &\quad& \wn A\parr\wn A &\longrightarrow& \wn A\\ \oc A &\longrightarrow& \oc\oc A &\quad& \wn\wn A &\longrightarrow& \wn A\\ \end{array}

Monoidality of exponential

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

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