ill.tex

\chapter{Intuitionistic linear logic}\label{intuitionistic-linear-logic}

Intuitionistic Linear Logic (\(ILL\)) is the
\wantedpage{intuitionnistic restriction} of
linear logic: the sequent calculus of \(ILL\) is obtained from the
\hyperref[sequents-and-proofs]{two-sided sequent calculus
of linear logic} by constraining sequents to have exactly one formula on
the right-hand side: \(\Gamma\vdash A\).

The connectives \(\parr\), \(\bot\) and \(\wn\) are not available
anymore, but the linear implication \(\limp\) is.

\section{Sequent Calculus}

\begin{gather*}
\LabelRule{\rulename{ax}}
\NulRule{A\vdash A}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A}
\AxRule{\Delta,A\vdash C}
\LabelRule{\rulename{cut}}
\BinRule{\Gamma,\Delta\vdash C}
\DisplayProof
\\[2ex]
\AxRule{\Gamma\vdash A}
\AxRule{\Delta\vdash B}
\LabelRule{\tens R}
\BinRule{\Gamma,\Delta\vdash A\tens B}
\DisplayProof
\qquad
\AxRule{\Gamma,A,B\vdash C}
\LabelRule{\tens L}
\UnaRule{\Gamma,A\tens B\vdash C}
\DisplayProof
\qquad
\LabelRule{\one R}
\NulRule{{}\vdash\one}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash C}
\LabelRule{\one L}
\UnaRule{\Gamma,\one\vdash C}
\DisplayProof
\\[2ex]
\AxRule{\Gamma,A\vdash B}
\LabelRule{\limp R}
\UnaRule{\Gamma\vdash A\limp B}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A}
\AxRule{\Delta,B\vdash C}
\LabelRule{\limp L}
\BinRule{\Gamma,\Delta,A\limp B\vdash C}
\DisplayProof
\\[2ex]
\AxRule{\Gamma\vdash A}
\AxRule{\Gamma\vdash B}
\LabelRule{\with R}
\BinRule{\Gamma\vdash A\with B}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\with_1 L}
\UnaRule{\Gamma,A\with B\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma,B\vdash C}
\LabelRule{\with_2 L}
\UnaRule{\Gamma,A\with B\vdash C}
\DisplayProof
\qquad
\LabelRule{\top R}
\NulRule{\Gamma\vdash\top}
\DisplayProof
\\[2ex]
\AxRule{\Gamma\vdash A}
\LabelRule{\plus_1 R}
\UnaRule{\Gamma\vdash A\plus B}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash B}
\LabelRule{\plus_2 R}
\UnaRule{\Gamma\vdash A\plus B}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\AxRule{\Gamma,B\vdash C}
\LabelRule{\plus L}
\BinRule{\Gamma,A\plus B\vdash C}
\DisplayProof
\qquad
\LabelRule{\zero L}
\NulRule{\Gamma,\zero\vdash C}
\DisplayProof
\\[2ex]
\AxRule{\oc{\Gamma}\vdash A}
\LabelRule{\oc R}
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\oc d L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma,\oc{A},\oc{A}\vdash C}
\LabelRule{\oc c L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash C}
\LabelRule{\oc w L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\\[2ex]
\AxRule{\Gamma\vdash A}
\LabelRule{\forall R}
\UnaRule{\Gamma\vdash \forall\xi A}
\DisplayProof
\qquad
\AxRule{\Gamma,A[\tau/\xi]\vdash C}
\LabelRule{\forall L}
\UnaRule{\Gamma,\forall\xi A\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A[\tau/\xi]}
\LabelRule{\exists R}
\UnaRule{\Gamma\vdash\exists\xi A}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\exists L}
\UnaRule{\Gamma,\exists\xi A\vdash C}
\DisplayProof
\end{gather*}
with \(\xi\) not free in \(\Gamma,C\) in the rules \(\forall R\) and \(\exists L\).

By restricting to connectives $\tens$, $\one$ and $\limp$, one gets Intuitionistic Multiplicative Linear Logic (\(IMLL\)).\label{imll}

\section{The intuitionistic fragment of linear logic}\label{the-intuitionistic-fragment-of-linear-logic}

In order to characterize intuitionistic linear logic inside linear
logic, we define the intuitionistic restriction of linear formulas:
\begin{equation*}
J ::= X \mid J\tens J \mid \one \mid J\limp J \mid J\with J \mid \top \mid J\plus J \mid \zero \mid \oc{J} \mid \forall\xi J \mid \exists\xi J
\end{equation*}
\(JLL\) is the \hyperref[fragment]{fragment} of linear logic obtained by restriction to
intuitionistic formulas.

\begin{proposition}[From $ILL$ to $JLL$]
If $\Gamma\vdash A$ is provable in $ILL_{012}$, it is provable in $JLL_{012}$.
\end{proposition}

\begin{proof}
$ILL_{012}$ is included in $JLL_{012}$.
\end{proof}

\begin{theorem}[From $JLL$ to $ILL$]
If $\Gamma\vdash\Delta$ is provable in $JLL_{12}$, it is provable in $ILL_{12}$.
\end{theorem}

\begin{proof}
We only prove the first order case, a proof of the full result is given in the PhD thesis of Harold Schellinx~\cite{phdschellinx}.

Consider a cut-free proof of $\Gamma\vdash\Delta$ in $JLL_{12}$, we can prove by induction on the length of such a proof that it belongs to $ILL_{12}$.
\end{proof}

\begin{corollary}[Unique conclusion in $JLL$]\label{uconcljll}
If $\Gamma\vdash\Delta$ is provable in $JLL_{12}$ then $\Delta$ is a singleton.
\end{corollary}

The theorem is also valid for formulas containing \(\one\) or \(\top\)
but not anymore with \(\zero\).
\({}\vdash((X\limp Y)\limp\zero)\limp(X\tens(\zero\limp Z))\) is
provable in \(JLL_0\):
\begin{prooftree}
\LabelRule{\rulename{ax}}
\NulRule{X\vdash X}
\LabelRule{\zero L}
\NulRule{\zero\vdash Y,Z}
\LabelRule{\limp R}
\UnaRule{{}\vdash Y,\zero\limp Z}
\LabelRule{\tens R}
\BinRule{X\vdash Y,X\tens(\zero\limp Z)}
\LabelRule{\limp R}
\UnaRule{{}\vdash X\limp Y,X\tens(\zero\limp Z)}
\LabelRule{\zero L}
\NulRule{\zero\vdash {}}
\LabelRule{\limp L}
\BinRule{(X\limp Y)\limp\zero\vdash X\tens(\zero\limp Z)}
\LabelRule{\limp R}
\UnaRule{{}\vdash((X\limp Y)\limp\zero)\limp(X\tens(\zero\limp Z))}
\end{prooftree}
but not in \(ILL_0\).

\section{Input / output polarities}\label{input-output-polarities}

In order to go to \(LL\) without \(\limp\), we consider two classes of
formulas: \emph{input formulas} (\(I\)) and \emph{output formulas}
(\(O\)).
\begin{align*}
I &::= X\orth \mid I\parr I \mid \bot \mid I\tens O \mid O\tens I \mid I\plus I \mid \zero \mid I\with I \mid \top \mid \wn{I} \mid \exists\xi I \mid \forall\xi I \\
O &::= X \mid O\tens O \mid \one \mid O\parr I \mid I\parr O \mid O\with O \mid \top \mid O\plus O \mid \zero \mid \oc{O} \mid \forall\xi O \mid \exists\xi O
\end{align*}

By applying the definition of the linear implication
\(A\limp B = A\orth\parr B\), any formula of \(JLL\) is mapped to an
output formula (and the dual of a \(JLL\) formula to an input formula).
Conversely, any output formula is coming from a \(JLL\) formula in this
way (up to commutativity of \(\parr\): \(O\parr I = I\parr O\)).

The \hyperref[fragment]{fragment} of linear logic obtained by restriction to
input/output formulas is thus equivalent to \(JLL\), but the closure of
the set of input/output formulas under orthogonal allows for a one-sided
presentation.
\begin{gather*}
\LabelRule{\rulename{ax}}
\NulRule{\vdash O\orth,O}
\DisplayProof
\qquad
\AxRule{{}\vdash \Gamma,O}
\AxRule{{}\vdash\Delta,O\orth}
\LabelRule{\rulename{cut}}
\BinRule{{}\vdash\Gamma,\Delta}
\DisplayProof
\\[2ex]
\AxRule{{}\vdash\Gamma,A}
\AxRule{{}\vdash\Delta,B}
\LabelRule{\tens}
\BinRule{{}\vdash\Gamma,\Delta,A\tens B}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,A,B}
\LabelRule{\parr}
\UnaRule{{}\vdash\Gamma,A\parr B}
\DisplayProof
\qquad
\LabelRule{\one}
\NulRule{{}\vdash\one}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma}
\LabelRule{\bot}
\UnaRule{{}\vdash\Gamma,\bot}
\DisplayProof
\\[2ex]
\AxRule{{}\vdash\Gamma,A}
\AxRule{{}\vdash\Gamma,B}
\LabelRule{\with}
\BinRule{{}\vdash\Gamma,A\with B}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,A}
\LabelRule{\plus_1}
\UnaRule{{}\vdash\Gamma,A\plus B}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,B}
\LabelRule{\plus_2}
\UnaRule{{}\vdash\Gamma,A\plus B}
\DisplayProof
\qquad
\LabelRule{\top}
\NulRule{{}\vdash\Gamma,\top}
\DisplayProof
\\[2ex]
\AxRule{{}\vdash\wn{\Gamma},O}
\LabelRule{\oc}
\UnaRule{{}\vdash\wn{\Gamma},\oc{O}}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,I}
\LabelRule{\wn d}
\UnaRule{{}\vdash\Gamma,\wn{I}}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,\wn{I},\wn{I}}
\LabelRule{\wn c}
\UnaRule{{}\vdash\Gamma,\wn{I}}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma}
\LabelRule{\wn w}
\UnaRule{{}\vdash\Gamma,\wn{I}}
\DisplayProof
\\[2ex]
\AxRule{{}\vdash\Gamma,A}
\LabelRule{\forall}
\UnaRule{{}\vdash\Gamma,\forall\xi A}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,A[\tau/\xi]}
\LabelRule{\exists}
\UnaRule{{}\vdash\Gamma,\exists\xi A}
\DisplayProof
\end{gather*}
with \(A\) and \(B\) arbitrary input or output formulas (under the
condition that the composite formulas containing them are input or
output formulas) and \(\xi\) not free in \(\Gamma\) in the rule
\(\forall\).

\begin{lemma}[Output formula]
If ${}\vdash\Gamma$ is provable in $LL_{12}$ and contains only input and output formulas, then $\Gamma$ contains exactly one output formula.
\end{lemma}

\begin{proof}
Assume $\Gamma_O$ is obtained by turning the output formulas of $\Gamma$ into $JLL$ formulas and $\Gamma_I$ is obtained by turning the dual of the input formulas of $\Gamma$ into $JLL$ formulas, $\Gamma_I\vdash\Gamma_O$ is provable in $LL_{12}$ thus in $JLL_{12}$. By \cref{uconcljll} (Unique conclusion in $JLL$), $\Gamma_O$ is a singleton, thus $\Gamma$ contains exactly one output formula.
\end{proof}


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