llwikibook/prov.tex at master · ComputerAidedLL/llwikibook · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
\section{Provable formulas}\label{provable-formulas}

Important provable formulas are given by
\hyperref[list-of-isomorphisms]{isomorphisms} and by
\hyperref[list-of-equivalences]{equivalences}.

In many of the cases below the \hyperref[non-provable-formulas]{converse implication does not hold}.

\subsection{Distributivities}\label{distributivities}

\subsubsection{Standard distributivities}\label{standard-distributivities}
\begin{align*}
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)
\end{align*}

\subsubsection{Linear distributivities}\label{linear-distributivities}
\begin{align*}
A\tens (B\parr C) &\limp (A\tens B)\parr C \\
\exists \xi. (A \parr B) &\limp A \parr \exists \xi.B  & (\xi\notin A) \\
A \tens \forall \xi.B &\limp \forall \xi. (A \tens B) &  (\xi\notin A) \\
\end{align*}

\subsection{Factorizations}\label{factorizations}
\begin{align*}
(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)
\end{align*}

\subsection{Identities}\label{identities}
\begin{align*}
\one &\limp A\orth\parr A \\
A\tens A\orth &\limp\bot
\end{align*}

\subsection{Additive structure}\label{additive-structure}

\begin{equation*}
\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}
\end{equation*}

\subsection{Quantifiers}\label{quantifiers-2}

\begin{equation*}
\begin{array}{rcll}
  A & \limp&  \forall \xi.A  & \quad  (\xi\notin A) \\
  \exists \xi.A & \limp&  A  & \quad  (\xi\notin A) \\[2ex]
  \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}
\end{equation*}

\subsection{Exponential structure}\label{exponential-structure}

Provable formulas involving exponential connectives only provide us with
the \hyperref[lattice-of-exponential-modalities]{lattice of exponential modalities}.

\begin{equation*}
\begin{array}{rclcrcl}
  \oc A & \limp&  A & \quad&  A& \limp& \wn A\\
  \oc A & \limp&  1 & \quad&  \bot & \limp&  \wn A
\end{array}
\end{equation*}

\subsection{Monoidality of exponentials}\label{monoidality-of-exponentials}

\begin{equation*}
\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}
\end{equation*}

\subsection{Promotion principles}\label{promotion-principles}

\begin{equation*}
\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}
\end{equation*}

\subsection{Commutations}\label{commutations}
\begin{align*}
\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}
\end{align*}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: