notations.tex

\chapter{Notations}\label{notations}

\section{Logical systems}\label{logical-systems}

For a given logical system such as $MLL$ (for
multiplicative linear logic), we consider the following variations:
\begin{center}
\begin{tabular}{lll}
\hline
Notation & Meaning & Connectives\\
\hline
$MLL$ &
propositional without units &
$X,{\tens},{\parr}$\\
$MLL_u$ &
propositional with units only &
$\one,\bot,{\tens},{\parr}$\\
$MLL_0$ &
propositional with units and variables &
$X,\one,\bot,{\tens},{\parr}$\\
$MLL_1$ &
first-order without units &
$X\vec{t},{\tens},{\parr},\forall x,\exists x$\\
$MLL_{01}$ &
first-order with units &
$X\vec{t},\one,\bot,{\tens},{\parr},\forall x,\exists x$\\
$MLL_2$ &
second-order propositional without units &
$X,{\tens},{\parr},\forall X,\exists X$\\
$MLL_{02}$ &
second-order propositional with units &
$X,\one,\bot,{\tens},{\parr},\forall X,\exists X$\\
$MLL_{12}$ &
first-order and second-order without units &
$X\vec{t},{\tens},{\parr},\forall x,\exists x,\forall X,\exists X$\\
$MLL_{012}$
& first-order and second-order with units &
$X\vec{t},\one,\bot,{\tens},{\parr},\forall x,\exists x,\forall X,\exists X$\\
\hline
\end{tabular}
\end{center}

\section{Formulas and proof trees}\label{formulas-and-proof-trees}

\subsection{Formulas}

\begin{itemize}
\item
  First order quantification:
  $\forall x
  A$ with substitution
  $A[t/x]$
\item
  Second order quantification:
  $\forall X
  A$ with substitution
  $A[B/X]$
\item
  Quantification of arbitrary order (mainly first or second):
  $\forall\xi
  A$ with substitution
  $A[\tau/\xi]$
\end{itemize}

\subsection{Rule names}\label{rule-names}

Name of the connective, followed by some additional information if
required, followed by ``L'' for a left rule or ``R'' for a right rule. This
is for a two-sided system, ``R'' is implicit for one-sided systems. For
example: $\wedge_1
\text{add} L$.

\section{Semantics}

\subsection{\texorpdfstring{\hyperref[coherent-semantics]{Coherent spaces}}{Coherent spaces}}\label{notations-coherent-spaces}

\begin{itemize}
\item Web of the space $X$: $\web X$
\item Coherence relation of the space $X$: large $\coh_X$ and strict $\scoh_X$
\end{itemize}

\subsection{\texorpdfstring{\hyperref[finiteness-semantics]{Finiteness spaces}}{Finiteness spaces}}\label{notations-finiteness-spaces}

\begin{itemize}
\item
  Web of the finiteness space
  $\mathcal
  A$:
  $\web{\mathcal
  A}$
\item
  Finiteness structure of the space
  $\mathcal
  A$:
  $\mathfrak
  F(\mathcal A)$ (which is consistent with the fact that
  $\finpowerset{\web{\mathcal
  A}}\subseteq \mathfrak
  F(\mathcal A)
  \subseteq\powerset{\web{\mathcal
  A}}$).
\end{itemize}

\section{\texorpdfstring{\hyperref[nets]{Nets}}{Nets}}

\begin{itemize}
\item The free ports of a net $R$:~$\mathrm{fp}(R)$.
\item The result of the connection of two nets
  $R$ and
  $R'$, given
  the partial bijection
  $f:\mathrm{fp}(R)\pinj
  \mathrm{fp}(R')$:
  $R\bowtie_f
  R'$.
\item The number of loops in the resulting net:
  $\Inner{R}{R'}_f$
  (includes the loops already present in
  $R$ and
  $R'$).
\end{itemize}

\section{Miscellaneous}\label{notations-miscellaneous}

\begin{itemize}
\item \hyperref[isomorphism]{Isomorphism}: $A\cong B$
\item injection: $A\hookrightarrow B$
\item partial injection: $A\pinj B$
\end{itemize}

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