seqcalc.tex

\chapter{Sequent calculus}\label{sequent-calculus}

This article presents the language and sequent calculus of second-order
linear logic and the basic properties of this sequent calculus. The core
of the article uses the two-sided system with negation as a proper
connective; the \hyperref[one-sided-sequent-calculus]{one-sided
system}, often used as the definition of linear logic, is presented at
the end of \cref{one-sided-sequent-calculus}.

\section{Formulas}\label{formulas}

Atomic formulas, written \(\alpha,\beta,\gamma\), are predicates of the
form \(p(t_1,\ldots,t_n)\), where the \(t_i\) are terms from some
first-order language. The predicate symbol \(p\) may be either a
predicate constant or a second-order variable. By convention we will
write first-order variables as \(x,y,z\), second-order variables as
\(X,Y,Z\), and \(\xi\) for a variable of arbitrary order (see~\cref{notations}).

Formulas, represented by capital letters \(A\), \(B\), \(C\), are built
using the following connectives:
\begin{center}
\begin{tabular}{llll}
\hline
\(\alpha\) & atom & \(A\orth\) & negation\\
\(A \tens B\) & tensor & \(A \parr B\) & par\\
\(\one\) & one & \(\bot\) & bottom\\
\(A \plus B\) & plus & \(A \with B\) & with\\
\(\zero\) & zero & \(\top\) & top\\
\(\oc A\) & of course & \(\wn A\) & why not\\
\(\exists \xi.A\) & there exists & \(\forall \xi.A\) & for
all\\
\hline
\end{tabular}
\end{center}

Each line (except the first one) corresponds to a particular class of
connectives, and each class consists in a pair of connectives. Those in
the left column are called \hyperref[positive-formula]{positive} and those
in the right column are called \hyperref[negative-formula]{negative}. The
\emph{tensor} and \emph{with} connectives are conjunctions while
\emph{par} and \emph{plus} are disjunctions. The exponential connectives
are called \emph{modalities}, and traditionally read \emph{of course
\(A\)} for \(\oc A\) and \emph{why not \(A\)} for \(\wn A\). Quantifiers
may apply to first- or second-order variables.

There is no connective for implication in the syntax of standard linear
logic. Instead, a \emph{linear implication} is defined similarly to the
decomposition \(A\imp B=\neg A\vee B\) in classical logic, as
\(A\limp B:=A\orth\parr B\).

Free and bound variables and first-order substitution are defined in the
standard way. Formulas are always considered up to renaming of bound
names. If \(A\) is a formula, \(X\) is a second-order variable and
\(B[x_1,\ldots,x_n]\) is a formula with variables \(x_i\), then the
formula \(A[B/X]\) is \(A\) where every atom \(X(t_1,\ldots,t_n)\) is
replaced by \(B[t_1,\ldots,t_n]\).

\section{Sequents and proofs}\label{sequents-and-proofs}

A sequent is an expression \(\Gamma\vdash\Delta\) where \(\Gamma\) and
\(\Delta\) are finite multisets of formulas. For a multiset
\(\Gamma=A_1,\ldots,A_n\), the notation \(\wn\Gamma\) represents the
multiset \(\wn A_1,\ldots,\wn A_n\). Proofs are labelled trees of
sequents, built using the following inference rules:

\begin{itemize}
\item
  Identity group: 
  \begin{equation*}
  \LabelRule{\rulename{axiom}}
  \NulRule{ A \vdash A }
  \DisplayProof
  \qquad\qquad
  \AxRule{ \Gamma \vdash A, \Delta }
  \AxRule{ \Gamma', A \vdash \Delta' }
  \LabelRule{\rulename{cut}}
  \BinRule{ \Gamma, \Gamma' \vdash \Delta, \Delta' }
  \DisplayProof  
  \end{equation*}
\item
  Negation: 
  \begin{equation*}
    \AxRule{ \Gamma \vdash A,\Delta }
    \LabelRule{n_L}
    \UnaRule{\Gamma, A\orth \vdash \Delta }
    \DisplayProof
    \qquad\qquad
    \AxRule{ \Gamma, A \vdash \Delta }
    \LabelRule{n_R}
    \UnaRule{ \Gamma \vdash A\orth, \Delta }
    \DisplayProof
  \end{equation*}
\item
  Multiplicative group:
  \begin{itemize}
  \item
    tensor: 
    \begin{equation*}
      \AxRule{ \Gamma, A, B \vdash \Delta }
      \LabelRule{ \tens_L }
      \UnaRule{ \Gamma, A \tens B \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash A, \Delta }
      \AxRule{ \Gamma' \vdash B, \Delta' }
      \LabelRule{ \tens_R }
      \BinRule{ \Gamma, \Gamma' \vdash A \tens B, \Delta, \Delta' }
      \DisplayProof      
    \end{equation*}
  \item
    par: 
    \begin{equation*}
      \AxRule{ \Gamma, A \vdash \Delta }
      \AxRule{ \Gamma', B \vdash \Delta' }
      \LabelRule{ \parr_L }
      \BinRule{ \Gamma, \Gamma', A \parr B \vdash \Delta, \Delta' }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash A, B, \Delta }
      \LabelRule{ \parr_R }
      \UnaRule{ \Gamma \vdash A \parr B, \Delta }
      \DisplayProof    
    \end{equation*}
  \item
    one:
    \begin{equation*}
       \AxRule{ \Gamma \vdash \Delta }
       \LabelRule{\one_L }
       \UnaRule{ \Gamma, \one \vdash \Delta }
       \DisplayProof
       \qquad\qquad
       \LabelRule{ \one_R }
       \NulRule{ \vdash \one }
       \DisplayProof   
    \end{equation*}
  \item
    bottom: 
    \begin{equation*}
       \LabelRule{ \bot_L }
       \NulRule{ \bot \vdash }
       \DisplayProof
       \qquad\qquad
       \AxRule{ \Gamma \vdash \Delta }
       \LabelRule{ \bot_R }
       \UnaRule{ \Gamma \vdash \bot, \Delta }
       \DisplayProof      
    \end{equation*}
  \end{itemize}
\item
  Additive group:
  \begin{itemize}
  \item
    plus: 
    \begin{equation*}
      \AxRule{ \Gamma, A \vdash \Delta }
      \AxRule{ \Gamma, B \vdash \Delta }
      \LabelRule{ \plus_L }
      \BinRule{ \Gamma, A \plus B \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash A, \Delta }
      \LabelRule{ \plus_{R1} }
      \UnaRule{ \Gamma \vdash A \plus B, \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash B, \Delta }
      \LabelRule{ \plus_{R2} }
      \UnaRule{ \Gamma \vdash A \plus B, \Delta }
      \DisplayProof
    \end{equation*}
  \item
    with: 
    \begin{equation*}
      \AxRule{ \Gamma, A \vdash \Delta }
      \LabelRule{ \with_{L1} }
      \UnaRule{ \Gamma, A \with B \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma, B \vdash \Delta }
      \LabelRule{ \with_{L2} }
      \UnaRule{ \Gamma, A \with B \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash A, \Delta }
      \AxRule{ \Gamma \vdash B, \Delta }
      \LabelRule{ \with_R }
      \BinRule{ \Gamma \vdash A \with B, \Delta }
      \DisplayProof      
    \end{equation*}
  \item
    zero: 
    \begin{equation*}
       \LabelRule{ \zero_L }
       \NulRule{ \Gamma, \zero \vdash \Delta }
       \DisplayProof
    \end{equation*}
  \item
    top: 
    \begin{equation*}
       \LabelRule{ \top_R }
       \NulRule{ \Gamma \vdash \top, \Delta }
       \DisplayProof    
    \end{equation*}
  \end{itemize}
\item
  Exponential group:
  \begin{itemize}
  \item
    of course: 
    \begin{gather*}
       \AxRule{ \Gamma, A \vdash \Delta }
       \LabelRule{ d_L }
       \UnaRule{ \Gamma, \oc A \vdash \Delta }
       \DisplayProof
       \qquad\qquad
       \AxRule{ \Gamma \vdash \Delta }
       \LabelRule{ w_L }
       \UnaRule{ \Gamma, \oc A \vdash \Delta }
       \DisplayProof
       \qquad\qquad
       \AxRule{ \Gamma, \oc A, \oc A \vdash \Delta }
       \LabelRule{ c_L }
       \UnaRule{ \Gamma, \oc A \vdash \Delta }
       \DisplayProof
       \\[2ex]
       \AxRule{ \oc A_1, \ldots, \oc A_n \vdash B ,\wn B_1, \ldots, \wn B_m }
       \LabelRule{ \oc_R }
       \UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B ,\wn B_1, \ldots, \wn B_m }
       \DisplayProof      
    \end{gather*}
  \item
    why not:
    \begin{gather*}
      \AxRule{ \Gamma \vdash A, \Delta }
      \LabelRule{ d_R }
      \UnaRule{ \Gamma \vdash \wn A, \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash \Delta }
      \LabelRule{ w_R }
      \UnaRule{ \Gamma \vdash \wn A, \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash \wn A, \wn A, \Delta }
      \LabelRule{ c_R }
      \UnaRule{ \Gamma \vdash \wn A, \Delta }
      \DisplayProof
      \\[2ex]
      \AxRule{ \oc A_1, \ldots, \oc A_n, A \vdash \wn B_1, \ldots, \wn B_m }
      \LabelRule{ \wn_L }
      \UnaRule{ \oc A_1, \ldots, \oc A_n, \wn A \vdash \wn B_1, \ldots, \wn B_m }
      \DisplayProof      
    \end{gather*}
  \end{itemize}
\item
  Quantifier group (in the \(\exists_L\) and \(\forall_R\) rules,
  \(\xi\) must not occur free in \(\Gamma\) or \(\Delta\)):
  \begin{itemize}
  \item
    there exists: 
    \begin{equation*}
      \AxRule{ \Gamma , A \vdash \Delta }
      \LabelRule{ \exists_L }
      \UnaRule{\Gamma, \exists\xi.A \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash \Delta, A[t/x] }
      \LabelRule{ \exists^1_R }
      \UnaRule{ \Gamma \vdash \Delta, \exists x.A }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash \Delta, A[B/X] }
      \LabelRule{ \exists^2_R }
      \UnaRule{ \Gamma \vdash \Delta, \exists X.A }
      \DisplayProof
    \end{equation*}
  \item
    for all: 
    \begin{equation*}
      \AxRule{ \Gamma, A[t/x] \vdash \Delta }
      \LabelRule{ \forall^1_L }
      \UnaRule{ \Gamma, \forall x.A \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma, A[B/X] \vdash \Delta }
      \LabelRule{ \forall^2_L }
      \UnaRule{ \Gamma, \forall X.A \vdash \Delta }
      \DisplayProof
      \qquad\qquad
      \AxRule{ \Gamma \vdash \Delta, A }
      \LabelRule{ \forall_R }
      \UnaRule{ \Gamma \vdash \Delta, \forall\xi.A }
      \DisplayProof
    \end{equation*}
  \end{itemize}
\end{itemize}


The left rules for \emph{of course} and right rules for \emph{why not}
are called \emph{dereliction}, \emph{weakening} and \emph{contraction}
rules. The right rule for \emph{of course} and the left rule for
\emph{why not} are called \emph{promotion} rules. Note the fundamental
fact that there are no contraction and weakening rules for arbitrary
formulas, but only for the formulas starting with the \(\wn\) modality.
This is what distinguishes linear logic from classical logic: if
weakening and contraction were allowed for arbitrary formulas, then
\(\tens\) and \(\with\) would be identified, as well as \(\plus\) and
\(\parr\), \(\one\) and \(\top\), \(\zero\) and \(\bot\). By
\emph{identified}, we mean here that replacing a \(\tens\) with a
\(\with\) or vice versa would preserve provability.

Sequents are considered as multisets, in other words as sequences up to
permutation. An alternative presentation would be to define a sequent as
a finite sequence of formulas and to add the exchange rules:

\begin{equation*}
  \AxRule{ \Gamma_1, A, B, \Gamma_2 \vdash \Delta }
  \LabelRule{\rulename{exchange}_L}
  \UnaRule{ \Gamma_1, B, A, \Gamma_2 \vdash \Delta }
  \DisplayProof
  \qquad\qquad
  \AxRule{ \Gamma \vdash \Delta_1, A, B, \Delta_2 }
  \LabelRule{\rulename{exchange}_R}
  \UnaRule{ \Gamma \vdash \Delta_1, B, A, \Delta_2 }
  \DisplayProof
\end{equation*}


\section{Equivalences}\label{equivalences}

Two formulas \(A\) and \(B\) are (linearly) equivalent, written
\(A\linequiv B\), if both implications \(A\limp B\) and \(B\limp A\) are
provable. Equivalently, \(A\linequiv B\) if both \(A\vdash B\) and
\(B\vdash A\) are provable. Another formulation of \(A\linequiv B\) is
that, for all \(\Gamma\) and \(\Delta\), \(\Gamma\vdash\Delta,A\) is
provable if and only if \(\Gamma\vdash\Delta,B\) is provable.

Two related notions are \hyperref[isomorphism]{isomorphism} (stronger than equivalence)
and \hyperref[equiprovability]{equiprovability} (weaker than equivalence).

\subsection{De Morgan laws}\label{de-morgan-laws}

Negation is involutive: \qquad \(A\linequiv A\biorth\)

Duality between connectives:
\begin{equation*}
\begin{array}{rclcrcl}
\hline
( A \tens B )\orth & \linequiv & A\orth \parr B\orth & \quad &
( A \parr B )\orth & \linequiv & A\orth \tens B\orth\\
\one\orth & \linequiv & \bot & & \bot\orth & \linequiv & \one\\
( A \plus B )\orth & \linequiv & A\orth \with B\orth & &
( A \with B )\orth & \linequiv & A\orth \plus B\orth\\
\zero\orth & \linequiv & \top & & \top\orth & \linequiv & \zero\\
( \oc A )\orth & \linequiv & \wn ( A\orth ) & &
( \wn A )\orth & \linequiv & \oc ( A\orth )\\
( \exists \xi.A )\orth & \linequiv & \forall \xi.( A\orth ) & &
( \forall \xi.A )\orth & \linequiv & \exists \xi.( A\orth )\\
\hline
\end{array}
\end{equation*}

\subsection{Fundamental equivalences}\label{fundamental-equivalences}

\begin{itemize}
\item
  Associativity, commutativity, neutrality:
  \begin{equation*}
    \begin{array}{ccc}
    A \tens (B \tens C) \linequiv (A \tens B) \tens C & A \tens B \linequiv B \tens A & A \tens \one \linequiv A \\
    A \parr (B \parr C) \linequiv (A \parr B) \parr C & A \parr B \linequiv B \parr A & A \parr \bot \linequiv A \\
    A \plus (B \plus C) \linequiv (A \plus B) \plus C & A \plus B \linequiv B \plus A & A \plus \zero \linequiv A \\
A \with (B \with C) \linequiv (A \with B) \with C & A \with B \linequiv B \with A & A \with \top \linequiv A
    \end{array}
  \end{equation*}
\item
  Idempotence of additives:
  \begin{equation*}
    \begin{array}{cc}
      A \plus A \linequiv A & A \with A \linequiv A
    \end{array}
  \end{equation*}
\item
  Distributivity of multiplicatives over additives:
  \begin{equation*}
    \begin{array}{cc}
       A \tens (B \plus C) \linequiv (A \tens B) \plus (A \tens C) & A \tens \zero \linequiv \zero \\
       A \parr (B \with C) \linequiv (A \parr B) \with (A \parr C) & A \parr \top \linequiv \top
    \end{array}
  \end{equation*}
\item
  Defining property of exponentials:
  \begin{equation*}
    \begin{array}{cc}
       \oc(A \with B) \linequiv \oc A \tens \oc B & \oc\top \linequiv \one \\
       \wn(A \plus B) \linequiv \wn A \parr \wn B & \wn\zero \linequiv \bot
    \end{array}
  \end{equation*}
\item
  Monoidal structure of exponentials:
  \begin{equation*}
    \begin{array}{cc}
       \oc A \tens \oc A \linequiv \oc A & \oc \one \linequiv \one \\
       \wn A \parr \wn A \linequiv \wn A & \wn \bot \linequiv \bot
    \end{array}
  \end{equation*}
\item
  Digging:
  \begin{equation*}
    \begin{array}{cc}
       \oc\oc A \linequiv \oc A & \wn\wn A \linequiv \wn A
    \end{array}
  \end{equation*}
\item
  Other properties of exponentials:
  \begin{equation*}
    \begin{array}{cc}
       \oc\wn\oc\wn A \linequiv \oc\wn A & \oc\wn \one \linequiv \one \\
       \wn\oc\wn\oc A \linequiv \wn\oc A & \wn\oc \bot \linequiv \bot
    \end{array}
  \end{equation*}
These properties of exponentials lead to
the \hyperref[lattice-of-exponential-modalities]{lattice of exponential modalities}.
\item
  Commutation of quantifiers (\(\zeta\) does not occur in \(A\)):
  \begin{equation*}
    \begin{array}{cccc}
       \exists \xi. \exists \psi. A \linequiv \exists \psi. \exists \xi. A & \exists \xi.(A \plus B) \linequiv \exists \xi.A \plus \exists \xi.B & \exists \zeta.(A\tens B) \linequiv A\tens\exists \zeta.B & \exists \zeta.A \linequiv A \\
       \forall \xi. \forall \psi. A \linequiv \forall \psi. \forall \xi. A & \forall \xi.(A \with B) \linequiv \forall \xi.A \with \forall \xi.B & \forall \zeta.(A\parr B) \linequiv A\parr\forall \zeta.B & \forall \zeta.A \linequiv A
    \end{array}
  \end{equation*}
\end{itemize}


\subsection{Definability}\label{definability}

The units and the additive connectives can be defined using second-order
quantification and exponentials, indeed the following equivalences hold:

\begin{itemize}
\item \(\zero \linequiv \forall X.X\)
\item \(\one \linequiv \forall X.(X \limp X)\)
\item \(A \plus B \linequiv \forall X.(\oc(A \limp X) \limp \oc(B \limp X) \limp X)\)
\end{itemize}

The constants \(\top\) and \(\bot\) and the connective \(\with\) can be
defined by duality.

Any pair of connectives that has the same rules as \(\tens/\parr\) is
equivalent to it, the same holds for additives, but not for
exponentials.

Other \hyperref[list-of-equivalences]{basic equivalences} exist.

\section{Properties of proofs}\label{properties-of-proofs}

\subsection{Cut elimination and consequences}\label{cut-elimination-and-consequences}

\begin{theorem}[cut elimination]
For every sequent $\Gamma\vdash\Delta$, there is a proof of
$\Gamma\vdash\Delta$ if and only if there is a proof of
$\Gamma\vdash\Delta$ that does not use the cut rule.
\end{theorem}

This property is proved using a set of rewriting rules on proofs, using
appropriate termination arguments (see the specific articles on
\wantedpage{cut elimination} for detailed proofs), it is the
core of the proof/program correspondence.

It has several important consequences:

\begin{definition}[subformula]
The subformulas of a formula $A$ are $A$ and, inductively, the subformulas of its immediate subformulas:
\begin{itemize}
\item the immediate subformulas of $A\tens B$, $A\parr B$, $A\plus B$, $A\with B$ are $A$ and $B$,
\item the only immediate subformula of $\oc A$ and $\wn A$ is $A$,
\item $\one$, $\bot$, $\zero$, $\top$ and atomic formulas have no immediate subformula,
\item the immediate subformulas of $\exists x.A$ and $\forall x.A$ are all the $A[t/x]$ for all first-order terms $t$,
\item the immediate subformulas of $\exists X.A$ and $\forall X.A$ are all the $A[B/X]$ for all formulas $B$ (with the appropriate number of parameters).
\end{itemize}
\end{definition}

\begin{theorem}[subformula property]
A sequent $\Gamma\vdash\Delta$ is provable if and only if it is the conclusion of a proof in which each intermediate conclusion is made of subformulas of the
formulas of $\Gamma$ and $\Delta$.
\end{theorem}

\begin{proof}
By the cut elimination theorem, if a sequent is provable, then it is provable by a cut-free proof.
In each rule except the cut rule, all formulas of the premisses are either
formulas of the conclusion, or immediate subformulas of it, therefore
cut-free proofs have the subformula property.
\end{proof}

The subformula property means essentially nothing in the second-order
system, since any formula is a subformula of a quantified formula where
the quantified variable occurs. However, the property is very meaningful
if the sequent \(\Gamma\) does not use second-order quantification, as
it puts a strong restriction on the set of potential proofs of a given
sequent. In particular, it implies that the first-order fragment without
quantifiers is decidable.

\begin{theorem}[consistency]
The empty sequent $\vdash$ is not provable.
Subsequently, it is impossible to prove both a formula $A$ and its
negation $A\orth$; it is impossible to prove $\zero$ or
$\bot$.
\end{theorem}

\begin{proof}
If a sequent is provable, then it is the conclusion of a cut-free proof.
In each rule except the cut rule, there is at least one formula in conclusion.
Therefore $\vdash$ cannot be the conclusion of a proof.
The other properties are immediate consequences: if $\vdash A\orth$
and $\vdash A$ are provable, then by the left negation rule
$A\orth\vdash$ is provable, and by the cut rule one gets empty
conclusion, which is not possible.
As particular cases, since $\one$ and $\top$ are
provable, $\bot$ and $\zero$ are not, since they are
equivalent to $\one\orth$ and $\top\orth$
respectively.
\end{proof}

\subsection{Expansion of identities}\label{expansion-of-identities}

Let us write \(\pi:\Gamma\vdash\Delta\) to signify that \(\pi\) is a
proof with conclusion \(\Gamma\vdash\Delta\).

\begin{proposition}[$\eta$-expansion]
For every proof $\pi$, there is a proof $\pi'$ with the
same conclusion as $\pi$ in which the axiom rule is only used with
atomic formulas.
If $\pi$ is cut-free, then there is a cut-free $\pi'$.
\end{proposition}

\begin{proof}
It suffices to prove that for every formula $A$, the sequent
$A\vdash A$ has a cut-free proof in which the axiom rule is used
only for atomic formulas.
We prove this by induction on $A$.
\begin{itemize}
\item If $A$ is atomic, then $A\vdash A$ is an instance of the atomic axiom rule.
\item If $A=A_1\tens A_2$ then we have:
\begin{prooftree}
\AxRule{ \pi_1 : A_1 \vdash A_1 }
\AxRule{ \pi_2 : A_2 \vdash A_2 }
\LabelRule{ \tens_R }
\BinRule{ A_1, A_2 \vdash A_1 \tens A_2 }
\LabelRule{ \tens_L }
\UnaRule{ A_1 \tens A_2 \vdash A_1 \tens A_2 }
\end{prooftree}
where $\pi_1$ and $\pi_2$ exist by induction hypothesis.
\item If $A=A_1\parr A_2$ then we have:
\begin{prooftree}
\AxRule{ \pi_1 : A_1 \vdash A_1 }
\AxRule{ \pi_2 : A_2 \vdash A_2 }
\LabelRule{ \parr_L }
\BinRule{ A_1 \parr A_2 \vdash A_1, A_2 }
\LabelRule{ \parr_R }
\UnaRule{ A_1 \parr A_2 \vdash A_1 \parr A_2 }
\end{prooftree}
where $\pi_1$ and $\pi_2$ exist by induction hypothesis.
\item All other connectives follow the same pattern.
\qedhere
\end{itemize}
\end{proof}

The interesting thing with \(\eta\)-expansion is that, we can always
assume that each connective is explicitly introduced by its associated
rule (except in the case where there is an occurrence of the \(\top\)
rule).

\subsection{Reversibility}\label{reversibility}

\begin{definition}[reversibility]\label{reversibledef}
A connective $c$ is called \emph{reversible} if
\begin{itemize}
\item for every proof $\pi:\Gamma\vdash\Delta,c(A_1,\ldots,A_n)$, there is a proof $\pi'$ with the same conclusion in which $c(A_1,\ldots,A_n)$ is introduced by the last rule,
\item if $\pi$ is cut-free then there is a cut-free $\pi'$.
\end{itemize}
\end{definition}

\begin{proposition}\label{reversibilityproperty}
The connectives $\parr$, $\bot$, $\with$, $\top$ and $\forall$ are reversible.
\end{proposition}

\begin{proof}
Using the $\eta$-expansion property, we assume that the axiom rule is only applied to atomic formulas.
Then each top-level connective is introduced either by its associated (left or
right) rule or in an instance of the $\zero_L$ or
$\top_R$ rule.

For $\parr$, consider a proof $\pi:\Gamma\vdash\Delta,A\parr
B$.
If $A\parr B$ is introduced by a $\parr_R$ rule (not
necessarily the last rule in $\pi$), then if we remove this rule
we get a proof of $\vdash\Gamma,A,B$ (this can be proved by a
straightforward induction on $\pi$).
If it is introduced in the context of a $\zero_L$ or
$\top_R$ rule, then this rule can be changed so that
$A\parr B$ is replaced by $A,B$.
In either case, we can apply a final $\parr$ rule to get the
expected proof.

For $\bot$, the same technique applies: if it is introduced by a
$\bot_R$ rule, then remove this rule to get a proof of
$\vdash\Gamma$, if it is introduced by a $\zero_L$ or
$\top_R$ rule, remove the $\bot$ from this rule, then
apply the $\bot$ rule at the end of the new proof.

For $\with$, consider a proof
$\pi:\Gamma\vdash\Delta,A\with B$.
If the connective is introduced by a $\with$ rule then this rule is
applied in a context like
\begin{prooftree}
\AxRule{ \pi_1: \Gamma' \vdash \Delta', A }
\AxRule{ \pi_2: \Gamma' \vdash \Delta', B }
\LabelRule{ \with }
\BinRule{ \Gamma' \vdash \Delta', A \with B }
\end{prooftree}

Since the formula $A\with B$ is not involved in other rules (except
as context), if we replace this step by $\pi_1$ in $\pi$
we finally get a proof $\pi'_1:\Gamma\vdash\Delta,A$.
If we replace this step by $\pi_2$ we get a proof
$\pi'_2:\Gamma\vdash\Delta,B$.
Combining $\pi_1$ and $\pi_2$ with a final
$\with$ rule we finally get the expected proof.
The case when the $\with$ was introduced in a $\top$
rule is solved as before.

For $\top$ the result is trivial: just choose $\pi'$ as
an instance of the $\top$ rule with the appropriate conclusion.

For $\forall$, consider a proof
$\pi:\Gamma\vdash\Delta,\forall\xi.A$.
Up to renaming, we can assume that $\xi$ occurs free only above the
rule that introduces the quantifier.
If the quantifier is introduced by a $\forall$ rule, then if we
remove this rule, we can check that we get a proof of
$\Gamma\vdash\Delta,A$ on which we can finally apply the
$\forall$ rule.
The case when the $\forall$ was introduced in a $\top$
rule is solved as before.

Note that, in each case, if the proof we start from is cut-free, our
transformations do not introduce a cut rule.
However, if the original proof has cuts, then the final proof may have more
cuts, since in the case of $\with$ we duplicated a part of the
original proof.
\end{proof}

A corresponding property for positive connectives is
\hyperref[reversibility-and-focusing]{focusing}, which states that
clusters of positive formulas can be treated in one step, under certain
circumstances.

\section{One-sided sequent calculus}\label{one-sided-sequent-calculus}

The sequent calculus presented above is very symmetric: for every left
introduction rule, there is a right introduction rule for the dual
connective that has the exact same structure. Moreover, because of the
involutivity of negation, a sequent \(\Gamma,A\vdash\Delta\) is provable
if and only if the sequent \(\Gamma\vdash A\orth,\Delta\) is provable.
From these remarks, we can define an equivalent one-sided sequent
calculus:

\begin{itemize}
\item Formulas are considered up to De Morgan duality. Equivalently, one can
  consider that negation is not a connective but a syntactically defined
  operation on formulas. In this case, negated atoms \(\alpha\orth\)
  must be considered as another kind of atomic formulas.
\item Sequents have the form \(\vdash\Gamma\).
\end{itemize}

The inference rules are essentially the same except that the left hand
side of sequents is kept empty:

\begin{itemize}
\item
  Identity group:
\begin{equation*}
  \LabelRule{\rulename{axiom}}
  \NulRule{ \vdash A\orth, A}
  \DisplayProof
  \qquad\qquad
  \AxRule{ \vdash \Gamma, A }
  \AxRule{ \vdash \Delta, A\orth }
  \LabelRule{\rulename{cut}}
  \BinRule{ \vdash \Gamma, \Delta }
  \DisplayProof
\end{equation*}
\item
  Multiplicative group:
\begin{equation*}
\AxRule{ \vdash \Gamma, A
} \AxRule{ \vdash \Delta,
B } \LabelRule{ \tens }
\BinRule{ \vdash \Gamma,
\Delta, A \tens B }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma, A, B }
\LabelRule{ \parr }
\UnaRule{ \vdash \Gamma, A \parr B }
\DisplayProof
\qquad\qquad
\LabelRule{ \one }
\NulRule{ \vdash \one }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma }
\LabelRule{ \bot }
\UnaRule{ \vdash \Gamma, \bot }
\DisplayProof
\end{equation*}
\item
  Additive group:
\begin{equation*}
\AxRule{ \vdash \Gamma, A} \LabelRule{ \plus_1 }
\UnaRule{ \vdash \Gamma, A \plus B }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma, B }
\LabelRule{ \plus_2 }
\UnaRule{ \vdash \Gamma, A \plus B }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Gamma, B }
\LabelRule{ \with }
\BinRule{ \vdash, \Gamma, A \with B }
\DisplayProof
\qquad\qquad
\LabelRule{ \top }
\NulRule{ \vdash \Gamma, \top }
\DisplayProof
\end{equation*}
\item
  Exponential group:
\begin{equation*}
\AxRule{ \vdash \Gamma, A } \LabelRule{ d }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma }
\LabelRule{ w }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma, \wn A, \wn A }
\LabelRule{ c }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \wn\Gamma, B }
\LabelRule{ \oc }
\UnaRule{ \vdash \wn\Gamma, \oc B }
\DisplayProof
\end{equation*}
\item
  Quantifier group (in the \(\forall\) rule, \(\xi\) must not occur free in \(\Gamma\)):
\begin{equation*}
\AxRule{ \vdash \Gamma,
A[t/x] } \LabelRule{ \exists^1 }
\UnaRule{ \vdash \Gamma, \exists x.A }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma, A[B/X] }
\LabelRule{ \exists^2 }
\UnaRule{ \vdash \Gamma, \exists X.A }
\DisplayProof
\qquad\qquad
\AxRule{ \vdash \Gamma, A }
\LabelRule{ \forall }
\UnaRule{ \vdash \Gamma, \forall \xi.A }
\DisplayProof
\end{equation*}
\end{itemize}

\begin{theorem}
A two-sided sequent $\Gamma\vdash\Delta$ is provable if
and only if the sequent $\vdash\Gamma\orth,\Delta$ is provable in
the one-sided system.
\end{theorem}

The one-sided system enjoys the same properties as the two-sided one,
including cut elimination, the subformula property, etc. This
formulation is often used when studying proofs because it is much
lighter than the two-sided form while keeping the same expressiveness.
In particular, \hyperref[proof-nets]{proof-nets} can be seen as a quotient of one-sided
sequent calculus proofs under commutation of rules.

\section{Variations}\label{variations}

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

\begin{itemize}
\item
  The promotion rule, on the right-hand side for example,
\(\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B, \wn B_1, \ldots, \wn B_m }
\LabelRule{ \oc_R }
\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B, \wn B_1, \ldots, \wn B_m }
\DisplayProof\) can be replaced by a \emph{multi-functorial} promotion
rule \(\AxRule{ A_1, \ldots, A_n \vdash B, B_1, \ldots, B_m }
\LabelRule{ \oc_R \rulename{mf}}
\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B, \wn B_1, \ldots, \wn B_m }
\DisplayProof\) and a \emph{digging} rule
\(\AxRule{ \Gamma \vdash \wn\wn A, \Delta }
\LabelRule{\wn\wn}
\UnaRule{ \Gamma \vdash \wn A, \Delta }
\DisplayProof\), without modifying the provability.

Note that digging violates the subformula property.
\item In presence of the digging rule 
\AxRule{ \Gamma \vdash
\wn\wn A, \Delta }
\LabelRule{ \wn\wn}
\UnaRule{ \Gamma \vdash
\wn A, \Delta }
\DisplayProof , the multiplexing rule
\(\AxRule{\Gamma\vdash A^{(n)},\Delta}
\LabelRule{\rulename{mux}}
\UnaRule{\Gamma\vdash \wn A,\Delta}
\DisplayProof\) (where \(A^{(n)}\) stands for $n$ occurrences of formula
\(A\)) is equivalent (for provability) to the triple of rules:
contraction, weakening, dereliction.
\end{itemize}

\subsection{Non-symmetric sequents}\label{non-symmetric-sequents}

The same remarks that lead to the definition of the one-sided calculus
can lead the definition of other simplified systems:

\begin{itemize}
\item A one-sided variant with sequents of the form \(\Gamma\vdash\) could
  be defined.
\item When considering formulas up to De Morgan duality, an equivalent
  system is obtained by considering only the left and right rules for
  positive connectives (or the ones for negative connectives only,
  obviously).
\item \hyperref[intuitionistic-linear-logic]{Intuitionistic linear logic} is the
  two-sided system where the right-hand side is constrained to always
  contain exactly one formula (with a few associated restrictions).
\item Similar restrictions are used in various \hyperref[semantics]{semantics} and \wantedpage{proof search} formalisms.
\end{itemize}

\subsection{Mix rules}\label{mix-rules}

It is quite common to consider \hyperref[mix]{mix rules}:
\(\LabelRule{\rulename{Mix}_0}
\NulRule{\vdash}
\DisplayProof
\qquad
\AxRule{\Gamma \vdash \Delta}
\AxRule{\Gamma' \vdash \Delta'}
\LabelRule{\rulename{Mix}_2}
\BinRule{\Gamma,\Gamma' \vdash \Delta,\Delta'}
\DisplayProof\)


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