\documentstyle[fullpage,11pt]{article}

\input{macros}
\newcommand{\defeq}{\buildrel \mbox{\small def} \over =}

 % zero-width inference rule markers
 % (if they have width, they throw off centering)
\newcommand{\zwb}[1]{\makebox[0cm][l]{{\scriptsize $#1$}}}

\newcommand{\mall}{\mbox{{\sc mall}}}
\newcommand{\imall}{\mbox{{\sc imall}}}
\newcommand{\mll}{\mbox{{\sc mll}}}
\newcommand{\cll}{\mbox{{\sc cll}}}
\newcommand{\imll}{\mbox{{\sc imll}}}
\newcommand{\ill}{\mbox{{\sc ill}}}
\newcommand{\cmll}{\mbox{{\sc cmll}}}

\newcommand{\la}{\mbox{$-\!\circ$}}     % Linear Arrow
\newcommand{\bla}{\mbox{$\circ\!-$}}    % Backwards Linear Arrow
%\newcommand{\Par}{\,{\parfont P}\,}    % Par (font)
\newcommand{\Par}{{\mbox{\raisebox{.4ex}{$\wp$}}}} % Par (gross)
\newcommand{\with}{\mbox{\,{\&}\,}}     % With (Additive And) (&)
\newcommand{\lplus}{\mbox{$\oplus$}}    % oplus
\newcommand{\tensor}{\mbox{$\otimes$}}  % Tensor (Multiplicative And) o*
\newcommand{\one}{\mbox{$1$}}           % 1
\newcommand{\zero}{\mbox{$0$}}          % 0
\renewcommand{\bottom}{\mbox{$\bot$}}     % bottom
\newcommand{\ltop}{\mbox{$\top$}}       % top

\newcommand{\as}{{\sc seq{}}{}} %%% Abramsky's System
\newcommand{\lm}{{\sc nat}}     %%% Our System

 % Definition
\newcommand{\define}{\mbox{${\stackrel{\Delta}{=}}$}}

\newcommand{\additives}[1]{#1}  % show additives
\newcommand{\emptyrhs}[1]{} % get rid of emptyrhs rules in int logic

\begin{document}

\title{\bf Sequent Calculus for Linear Logic}
\author{Notes for CS 358, Spring 1995}
\date{April 19 Lecture}
\maketitle


\section{Intuitive Explanation of Connectives}

The central concept of linear logic is illustrated by 
linear implication, written $A \la B$.
Negation is written as a post-fix operation, $A^\perp$.
The four remaining propositional connectives 
are two forms of conjunction, $\otimes$ and $\with$,
and two forms of disjunction, $\Par$ and $\oplus$.

\begin{quote}\noindent
\begin{tabular}{ll}
$A \la B$ & Using $A$ exactly once, we can obtain $B$: \\
&  A process that consumes one $A$, 
  then produces one $B$ then halts.\\[2ex]

$A^\perp$ & A negative resource (or debt) that cancels $A$:\\
&  A process that can consume exactly one $A$ and then halt.\\[2ex]

$A \otimes B$ & Presence of resources $A$ and $B$:\\
&  A process that can produce exactly one $A$ and one $B$ and then halt.\\[2ex]

$A \with  B$ & Choice between resources $A$ and $B$:\\
& A process with two push-buttons, one labeled $A$, the other $B$.\\
& If we push $A$, exactly one $A$ will be produced before halting,
 similarly for $B$\\[2ex]

$A \oplus B$ & One of $A$ and $B$\\
& A process that will produce $A$ or $B$ and then halt.\\
&  (A black box that might contain either a process \\
& that produces an $A$ or a process that produces a $B$.)\\[2ex]

$A \Par B$ & Resources $A$ or $B$, in the situation that if not one then the other:\\
& A process that outputs $A$ if the negation of $B$ is given,
otherwise $B$ if the negation of $A$.
\end{tabular}
\end{quote}

Using this process intuition, we can anticipate the
provability or non-provability of various sequents:
\begin{quote}\noindent
$(A \otimes (A \la B)) \la B$.
If we are given $A \otimes (A \la B)$, then we can wire 
the $A$ process so that it's output goes into the $A \la B$,
resulting in the consumption of $A$ and final output of $B$. 
 
$(A \otimes (A \la B)\otimes (A \la C)) \la B\otimes C$ 
should not be provable, by conservation of resources.
If we are given $A$, $A \la B$ and $A \la C$ processes, 
then we can either feed the output of 
the $A$ process into $A \la B$ or into $A \la C$, but not both.

$(A \otimes A \otimes A \otimes(A \la B)\otimes (A \la C)) \la B\otimes C$ 
also fails. We can convert one $A$ to $B$, one $A$ to $C$,
but this leaves one extra $A$ left over.
$(A \otimes (A \la B)) \la B$.


$A^\perp \Par A$. This specifies a process
that is able to output $A$ or $A^\perp$, but need not
decide which until it interacts with its environment.
If presented with $A$, which is the negation of $A^\perp$,
then the possibility of outputing  $A^\perp$is disabled
and the output must be $A$.
Conversely, if presented with $A^\perp$, the output 
must be $A^\perp$.
We can easily construct such a process as simply a \q{wire}
or \q{channel} that outputs its input.
\end{quote}

According to standard terminology, the forms of conjunction and disjunction
can be divided into two categories, as shown in this table.
\begin{center}
\begin{tabular}{|c|c|c|}
\hline
 & Multiplicative &  Additive \\
\hline 
Conjunction & $\otimes$ & $\with$ \\
\hline 
Disjunction  &  $\Par$ & $\oplus$\\
\hline 
\end{tabular}
\end{center}
Intuitively, \q{multiplicative} connectives have the flavor of
\q{partitioning of resources,} \ie, both conjuncts or
disjuncts may be obtained, by a process that divides available
resources into those needed for each result.
On the other hand, 
\q{additive} connectives intuitively involve some \q{choice between resources,}
so that either or both results may be obtained, by some process
that chooses which to produce.
This informal explanation is probably very hard to make sense
of in the abstract; it is best to look carefully at each
of the rules and form your own intuition from the
definition of the logic itself.

We may treat implication as a derived form
\[
A \la B  \ \ \defeq \ \ A^{\perp} \Par B
\]
and restrict negation as discussed below.

The remaining propositional operators are modalities $!$ and $?$,
with the following intuitive explanations.
\begin{quote}\noindent
\begin{tabular}{ll}
$!A $ & As much $A$ as we want: \\
&  A process that will produce $A$ as many times as required\\
& to satisfy other processes that take $A$ as input.\\[2ex]

$?A$ & dual to $!A$:\\
&  A process that will input $A^\perp$ as many times as required\\
& to satisfy other processes that output $A^\perp$.\\[2ex]
\end{tabular}
\end{quote}


\section{Negation}

Some analysis of the proof system will be simpler if we
treat negation as a derived form, allowing negation 
only on propositional symbols or, in the first-order case, atomic formulas.
This approach makes termination of the cut-elimination
procedure easier to establish by restricting the use of the
negation rule.

\[\begin{array}{rclcrcl}
 (p_i)^{\perp} & \define & p_i^{\perp} & \hspace{2cm} & 
 (p_i^{\perp})^{\perp} & \define & p_i \\
 (A \otimes B)^{\perp} & \define & B^{\perp} \Par A^{\perp} & &
 (A \Par B)^{\perp} & \define & B^{\perp} \otimes A^{\perp} \\
% (A \la B)^{\perp} & \define & B^{\perp} \otimes A & & \\
 (A \oplus B)^{\perp} & \define & A^{\perp} \with B^{\perp} & & 
 (A \with B)^{\perp} & \define & A^{\perp} \oplus B^{\perp} \\
 (!A)^{\perp} & \define & ?A^{\perp} & &
 (?A)^{\perp} & \define & !A^{\perp} \\
 (1)^{\perp} & \define & \bot & &
 (\bot)^{\perp} & \define & 1 \\
 (0)^{\perp} & \define & \top & &
 (\top)^{\perp} & \define & 0 \\
\end{array}\]


With implication treated as an abbreviation, $A \la B  = A^{\perp} \Par B$,
we have this derived property of implication:
\[
(A \la B)^\perp = (A^{\perp} \Par B)^\perp = A \otimes B^\perp
\]

\section{Sequent rules (two-sided)}
\noindent
\begin{center}
\begin{tabular}{rccl}
{\bf Identity} &   $\begin{array}{c}
	            \hline
		    A \vdash A
		    \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
            \Gamma_2, A \vdash \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash \Sigma_1, \Sigma_2
            \end{array}$ & {\bf Cut} \\[.5cm]
{\bf Exch. Left} &  $\begin{array}{c}
	    \Gamma_1, A, B, \Gamma_2 \vdash \Sigma \\
            \hline
            \Gamma_1, B, A, \Gamma_2 \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash \Sigma_1, A, B, \Sigma_2 \\
            \hline
            \Gamma \vdash \Sigma_1, B, A, \Sigma_2
            \end{array}$ & {\bf Exch. Right} \\[.5cm]
{\bf $\otimes$ Left} &  $\begin{array}{c}
	    \Gamma, A, B \vdash \Sigma \\
            \hline
            \Gamma, (A \otimes B) \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
            \Gamma_2 \vdash B, \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash (A \otimes B), \Sigma_1, \Sigma_2
            \end{array}$ & {\bf $\otimes$ Right} \\[.5cm]
%\comment{
	{\bf $\la$ Left} &  $\begin{array}{c}
		    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
	            \Gamma_2, B \vdash \Sigma_2\\
        	    \hline
	            \Gamma_1, \Gamma_2, (A \la B) \vdash \Sigma_1, \Sigma_2
        	    \end{array}$ 
	         &  $\begin{array}{c}
		    \Gamma, A \vdash B, \Sigma \\
	            \hline
	            \Gamma \vdash (A \la B), \Sigma
        	    \end{array}$ & {\bf $\la$ Right} \\[.5cm]
%  } % end comment (la)
{\bf $\Par$ Left} &  $\begin{array}{c}
	    \Gamma_1, A \vdash \Sigma_1 \hspace{1cm}
            \Gamma_2, B \vdash \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2, (A \Par B) \vdash \Sigma_1, \Sigma_2
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash A, B, \Sigma \\
            \hline
            \Gamma \vdash (A \Par B), \Sigma
            \end{array}$ & {\bf $\Par$ Right} \\[.5cm]
{\bf $\&$ Left} &  $\begin{array}{ccc}
	    \Gamma, A \vdash \Sigma & \hspace*{.1cm} &
	    \Gamma, B \vdash \Sigma \\
            \cline{1-1} \cline{3-3}
            \Gamma, (A \& B) \vdash \Sigma & &
            \Gamma, (A \& B) \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash A, \Sigma \hspace{1cm}
            \Gamma \vdash B, \Sigma\\
            \hline
            \Gamma \vdash (A \& B), \Sigma
            \end{array}$ & {\bf $\&$ Right} \\[.5cm]
{\bf $\oplus$ Left} &  $\begin{array}{c}
	    \Gamma, A \vdash \Sigma \hspace{1cm}
            \Gamma, B \vdash \Sigma\\
            \hline
            \Gamma, (A \oplus B) \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{ccc}
	    \Gamma \vdash A, \Sigma & \hspace*{.1cm} &
	    \Gamma \vdash B, \Sigma \\
            \cline{1-1} \cline{3-3}
            \Gamma \vdash (A \oplus B), \Sigma & &
            \Gamma \vdash (A \oplus B), \Sigma
            \end{array}$ & {\bf $\oplus$ Right} \\[.5cm]
{\bf ! W} &  $\begin{array}{c}
	    \Gamma \vdash \Sigma \\
            \hline
            \Gamma, !A \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma, !A, !A \vdash \Sigma \\
            \hline
            \Gamma, !A \vdash \Sigma
            \end{array}$ & {\bf ! C} \\[.5cm]
{\bf ! D} & $\begin{array}{c}
	     \Gamma, A \vdash \Sigma\\
             \hline
             \Gamma, !A \vdash \Sigma
             \end{array}$
           & $\begin{array}{c}
	     !\Gamma \vdash A, ?\Sigma\\
             \hline
             !\Gamma \vdash !A, ?\Sigma
             \end{array}$ & {\bf ! S} \\[.5cm]
{\bf ? W} &  $\begin{array}{c}
	    \Gamma \vdash \Sigma \\
            \hline
            \Gamma \vdash ?A, \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash ?A, ?A, \Sigma \\
            \hline
            \Gamma \vdash ?A, \Sigma
            \end{array}$ & {\bf ? C} \\[.5cm]
{\bf ? D} & $\begin{array}{c}
	     \Gamma \vdash A, \Sigma\\
             \hline
             \Gamma \vdash ?A, \Sigma
             \end{array}$
           & $\begin{array}{c}
	     !\Gamma, A \vdash ?\Sigma \\
             \hline
             !\Gamma, ?A \vdash ?\Sigma
             \end{array}$ & {\bf ? S} \\[.5cm]
{\bf $^{\perp}$ Left} & $\begin{array}{c}
	     \Gamma \vdash A, \Sigma \\
             \hline
	     \Gamma, A^{\perp} \vdash \Sigma \\
             \end{array}$
           & $\begin{array}{c}
	     \Gamma, A \vdash \Sigma \\
             \hline
	     \Gamma \vdash A^{\perp}, \Sigma \\
             \end{array}$ & {\bf $^{\perp}$ Right} \\[.5cm]
{\bf $0$ Left} & $\Gamma, 0 \vdash \Sigma$
           & $\Gamma \vdash \top, \Sigma$ & {\bf $\top$ Right} \\[.5cm]
{\bf $\bot$ Left} & $\bot \vdash$
           & $\begin{array}{c}
	     \Gamma \vdash \Sigma \\
             \hline
	     \Gamma \vdash \bot, \Sigma \\
             \end{array}$ & {\bf $\bot$ Right} \\[.5cm]
{\bf $1$ Left} & $\begin{array}{c}
	     \Gamma \vdash \Sigma \\
             \hline
	     \Gamma, 1 \vdash \Sigma \\
             \end{array}$
           & $\vdash 1$ & {\bf $1$ Right} \\[.5cm]
\comment{ 
{\bf $\forall$ Left} & $\begin{array}{c}
	     \Gamma,A\{t/x\} \vdash \Sigma \\
             \hline
	     \Gamma,\forall x . A \vdash \Sigma \\
             \end{array}$
           & $\begin{array}{c}
	     \Gamma  \vdash A\{y/x\}, \Sigma \\
             \hline
	     \Gamma  \vdash \forall x . A, \Sigma \\
             \end{array}$ & {\bf $\forall$ Right} \\[.5cm]
{\bf $\exists$ Left} & $\begin{array}{c}
	     \Gamma,A\{y/x\} \vdash \Sigma \\
             \hline
	     \Gamma,\exists x . A \vdash \Sigma \\
             \end{array}$
           & $\begin{array}{c}
	     \Gamma \vdash A\{t/x\}, \Sigma \\
             \hline
	     \Gamma \vdash \exists x . A, \Sigma \\
             \end{array}$ & {\bf $\exists$ Right} \\[.5cm]
} % end quantifier comment 
\end{tabular}
\end{center}

\comment{The {\bf $\forall$ Right} and {\bf $\exists$ Left} rules only
apply if $y$ is not free in $\Gamma,\Sigma$, and any nonlogical
theory axioms.
} % end quantifier comment

\section{Discussion of selected rules}

In is interesting to compare the two forms of conjunction in linear
logic with classical conjunction. 
\begin{center}
\begin{tabular}{rccl}
{\bf $\land$ Left} &  $\begin{array}{c}
	    \Gamma, A \vdash \Sigma \\
            \hline
            \Gamma, A \land B \vdash \Sigma
            \end{array}$ 
            $\begin{array}{c}
	    \Gamma, B \vdash \Sigma \\
            \hline
            \Gamma, A \land B \vdash \Sigma
            \end{array}$
         &  $\begin{array}{c}
	    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
            \Gamma_2 \vdash B, \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash (A \land B), \Sigma_1, \Sigma_2
            \end{array}$ & {\bf $\land$ Right} \\[.5cm]
{\bf $\otimes$ Left} &  $\begin{array}{c}
	    \Gamma, A, B \vdash \Sigma \\
            \hline
            \Gamma, (A \otimes B) \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
            \Gamma_2 \vdash B, \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash (A \otimes B), \Sigma_1, \Sigma_2
            \end{array}$ & {\bf $\otimes$ Right} \\[.5cm]
{\bf $\&$ Left} &  $\begin{array}{ccc}
	    \Gamma, A \vdash \Sigma & \hspace*{.1cm} &
	    \Gamma, B \vdash \Sigma \\
            \cline{1-1} \cline{3-3}
            \Gamma, (A \& B) \vdash \Sigma & &
            \Gamma, (A \& B) \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash A, \Sigma \hspace{1cm}
            \Gamma \vdash B, \Sigma\\
            \hline
            \Gamma \vdash (A \& B), \Sigma
            \end{array}$ & {\bf $\&$ Right} \\[.5cm]
\end{tabular}
\end{center}
Two apparent points are:\hfil\\
1. Each form of linear conjunction has one of the classical rules, but no the other.
\hfil\\
2. If we look at \q{intuitionistic} form of the right rules
for $\otimes$ and $\&$, we can see that $\otimes$ uses independent
resources to produce both conjuncts independently, while
$\&$ allows the same resources to produce one conjunct or the
other, but due to linearity (conservation of resources) not both.

A similar comparison may be made for linear and classical disjunction.
The negation rules are the same for classical and linear logic.

\section{Simplified presentation}

Using the negation rule, we can push all formulas of a
sequent $A_1,\ldots,A_k \ts B_1,\ldots, B_\ell$ to the right
of the turnstile, giving us the equivalent sequent
$\ts A_1^\perp,\ldots,A_k^\perp, B_1,\ldots, B_\ell$.
We can write all of the proof rules in one-sided form
as follows, dropping the $\la$ and negation rules
since $\la$ is considered a derived connective
and negation is not needed if we keep all formulas
on the right and negation only occurs on atomic formulas.

\begin{center}
\begin{tabular}{rccl}
{\bf Identity} &   $\begin{array}{c}
	            \hline
		     \vdash A^\perp, A
		    \end{array}$ 
         &  $\begin{array}{c}
	    \vdash \Gamma, A \hspace{1cm}
            \vdash A^\perp,\Sigma\\
            \hline
            \vdash \Gamma, \Sigma
            \end{array}$ & {\bf Cut} \\[.5cm]
{\bf Exchange} &  $\begin{array}{c}
	    \vdash \Gamma, A, B, \Sigma \\
            \hline
            \vdash \Gamma, B, A, \Sigma \\
            \end{array}$ 
         &  $\begin{array}{c}
	    \vdash \Gamma, A, B \\
            \hline
            \vdash \Gamma, A \Par B
            \end{array}$ & {\bf \Par} \\[.5cm]
{\bf $\otimes$} &  $\begin{array}{c}
	    \vdash \Gamma, A \quad\quad \vdash \Sigma, B\\
            \hline
            \vdash \Gamma, \Sigma, A\otimes B
            \end{array}$ 
         &  $\begin{array}{c}
	    \vdash \Gamma, A \quad\quad \vdash \Gamma, B\\
            \hline
            \vdash \Gamma, A\with B
            \end{array}$ & {\bf $\with$} \\[.5cm]
{\bf $\oplus$} &  $\begin{array}{c}
	    \vdash \Gamma, A\\
            \hline
            \vdash \Gamma, A\oplus B
            \end{array}$ 
         &  $\begin{array}{c}
	    \vdash \Gamma, B\\
            \hline
            \vdash \Gamma, A\oplus B
            \end{array}$ & {  } \\[.5cm]
{\bf ? W} &  $\begin{array}{c}
	    \vdash \Sigma \\
            \hline
            \vdash ?A, \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \vdash ?A, ?A, \Sigma \\
            \hline
            \vdash ?A, \Sigma
            \end{array}$ & {\bf ? C} \\[.5cm]
{\bf ? D} & $\begin{array}{c}
	     \vdash A, \Sigma\\
             \hline
             \vdash ?A, \Sigma
             \end{array}$
           & $\begin{array}{c}
	     \vdash ?\Sigma, A \\
             \hline
             \vdash ?\Sigma, !A
             \end{array}$ & {\bf ? S} \\[.5cm]
{\bf $\bot$ } 
           & $\begin{array}{c}
	     \vdash \Sigma \\
             \hline
	     \vdash \bot, \Sigma \\
             \end{array}$ \\[.5cm]
{\bf $\top$} & $\vdash \Sigma, \top$ 
           & $\vdash 1$ & {\bf $1$} 
\end{tabular}
\end{center}

\paragraph{Exercises}\hfil\\

1. Prove the formulas 
$(A \otimes (A \la B)) \la B$ and $A^\perp \Par A$.
Use the fact that {\bf Cut} is eliminable to show that
$(A \otimes (A \la B)\otimes (A \la C)) \la B\otimes C$ 
and
$(A \otimes A \otimes A \otimes(A \la B)\otimes (A \la C)) \la B\otimes C$ 
are not provable. Use either one-sided or two-sided sequents,
as you prefer.

2. Consider the informal \q{process interpretation} for
the sequent $A \otimes B, A^\perp \otimes B, A \otimes B^\perp, A^\perp \otimes B^\perp$.
Explain how you might create a process that satisfies this specification.
Then show that this sequent is not derivable.
\end{document}
