\documentclass[10pt,twocolumn]{article}
\usepackage{amsmath,amssymb}
\usepackage{theorem}
\usepackage{times}
\usepackage[dvips]{graphicx}
\usepackage{xspace}
\usepackage{ifthen}
\usepackage{calc}
\usepackage[usenames]{color}
\definecolor{correctioncol}{gray}{.3}
\definecolor{falsecolour}{gray}{.65}
\newcommand{\false}[1]{\raisebox{0pt}[0pt][0pt]{\colorbox{falsecolour}{#1}}}

\makeatletter
% --------------------------------------------------------------- 
%
% $Id: latex8.sty,v 1.2 1995/09/15 15:31:13 ienne Exp $
% 
% by Paolo.Ienne@di.epfl.ch 
%
% --------------------------------------------------------------- 
%
% no guarantee is given that the format corresponds perfectly to 
% IEEE 8.5" x 11" Proceedings, but most features should be ok.
%
% --------------------------------------------------------------- 
% with LaTeX2e:
% =============
%
% use as 
%   \documentclass[times,10pt,twocolumn]{article} 
%   \usepackage{latex8}
%   \usepackage{times}
%
% --------------------------------------------------------------- 

% with LaTeX 2.09:
% ================
%
% use as 
%   \documentstyle[times,art10,twocolumn,latex8]{article}
%
% --------------------------------------------------------------- 
% with both versions:
% ===================
%
% specify \pagestyle{empty} to omit page numbers in the final 
% version
%
% specify references as
%   \bibliographystyle{latex8}
%   \bibliography{...your files...}
%
% use Section{} and SubSection{} instead of standard section{} 
%    and subsection{} to obtain headings in the form 
%    "1.3. My heading"
%
% ---------------------------------------------------------------

\typeout{IEEE 8.5 x 11-Inch Proceedings Style `latex8.sty'.}

% ten point helvetica bold required for captions
% in some sites the name of the helvetica bold font may differ, 
% change the name here:
\font\tenhv  = phvb at 10pt
%\font\tenhv  = phvb7t at 10pt

% eleven point times bold required for second-order headings 
% \font\elvbf  = cmbx10 scaled 1100
\font\elvbf  = ptmb scaled 1100

% set dimensions of columns, gap between columns, and paragraph indent 
\setlength{\textheight}{8.875in}
\setlength{\textwidth}{6.875in}
\setlength{\columnsep}{0.3125in}
\setlength{\topmargin}{0in}
\setlength{\headheight}{0in}
\setlength{\headsep}{0in}
\setlength{\parindent}{1pc}
\setlength{\oddsidemargin}{-.304in}
\setlength{\evensidemargin}{-.304in}

% memento from size10.clo
% \normalsize{\@setfontsize\normalsize\@xpt\@xiipt} 
% \small{\@setfontsize\small\@ixpt{11}}
% \footnotesize{\@setfontsize\footnotesize\@viiipt{9.5}} 
% \scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt}
% \tiny{\@setfontsize\tiny\@vpt\@vipt}
% \large{\@setfontsize\large\@xiipt{14}} 
% \Large{\@setfontsize\Large\@xivpt{18}} 
% \LARGE{\@setfontsize\LARGE\@xviipt{22}} 
% \huge{\@setfontsize\huge\@xxpt{25}}
% \Huge{\@setfontsize\Huge\@xxvpt{30}}

\def\@maketitle
   {
   \newpage
   \null
   \vskip .375in 
   \begin{center}
      {\Large \bf \@title \par} 
      % additional two empty lines at the end of the title 
      \vspace*{24pt} 
      {
      \large 
      \lineskip .5em
      \begin{tabular}[t]{c}
         \@author 
      \end{tabular}
      \par
      } 
      % additional small space at the end of the author name 
      \vskip .5em 
      {
       \large 
      \begin{tabular}[t]{c}
         \@affiliation 
      \end{tabular}
      \par 
      \ifx \@empty \@email
      \else
         \begin{tabular}{r@{~}l}
            E-mail: & {\tt \@email}
         \end{tabular}
         \par
      \fi
      }
      % additional empty line at the end of the title block 
      \vspace*{12pt} 
   \end{center}
   } 

\def\abstract
   {%
   \centerline{\large\bf Abstract}%
   \vspace*{12pt}%
   \it%
   }

\def\endabstract
   {
   % additional empty line at the end of the abstract 
   \vspace*{12pt} 
   }

\def\affiliation#1{\gdef\@affiliation{#1}} \gdef\@affiliation{}

\def\email#1{\gdef\@email{#1}}
\gdef\@email{}

\newlength{\@ctmp}
\newlength{\@figindent}
\setlength{\@figindent}{1pc}

\long\def\@makecaption#1#2{
   \vskip 10pt
   \setbox\@tempboxa\hbox{\tenhv\noindent #1.~#2} 
   \setlength{\@ctmp}{\hsize}
   \addtolength{\@ctmp}{-\@figindent}\addtolength{\@ctmp}{-\@figindent} 
   % IF longer than one indented paragraph line
   \ifdim \wd\@tempboxa >\@ctmp
      % THEN set as an indented paragraph
      \begin{list}{}{\leftmargin\@figindent \rightmargin\leftmargin} 
         \item[]\tenhv #1.~#2\par
      \end{list}
   \else
      % ELSE center
      \hbox to\hsize{\hfil\box\@tempboxa\hfil} 
   \fi}

% correct heading spacing and type
\def\section{\@startsection {section}{1}{\z@}
   {14pt plus 2pt minus 2pt}{14pt plus 2pt minus 2pt} {\large\bf}} 
\def\subsection{\@startsection {subsection}{2}{\z@}
   {13pt plus 2pt minus 2pt}{13pt plus 2pt minus 2pt} {\elvbf}}

% add the period after section numbers 
\newcommand{\Section}[1]{\section{\hskip -1em.~#1}} 
\newcommand{\SubSection}[1]{\subsection{\hskip -1em.~#1}}

% end of file latex8.sty
% ---------------------------------------------------------------

\def\subsection{\@startsection {subsection}{2}{0pt}{-2ex plus -1ex minus 
   -.2ex}{1.5ex plus .2ex minus .3ex}{\@setfontsize\normalsize\@xpt{12}\bf}}

%% Paul Taylor's Proof Trees, 2 August 1996
%% Build proof tree for Natural Deduction, Sequent Calculus, etc.
%% WITH SHORTENING OF PROOF RULES!
%% Paul Taylor, begun 10 Oct 1989
%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! ***
%%
%% 2 Aug 1996: fixed \mscount and \proofdotnumber
%%
%%      \prooftree
%%              hyp1            produces:
%%              hyp2
%%              hyp3            hyp1    hyp2    hyp3
%%      \justifies              -------------------- rulename
%%              concl                   concl
%%      \thickness=0.08em
%%      \shiftright 2em
%%      \using
%%              rulename
%%      \endprooftree
%%
%% where the hypotheses may be similar structures or just formulae.
%%
%% To get a vertical string of dots instead of the proof rule, do
%%
%%      \prooftree                      which produces:
%%              [hyp]
%%      \using                                  [hyp]
%%              name                              .
%%      \proofdotseparation=1.2ex                 .name
%%      \proofdotnumber=4                         .
%%      \leadsto                                  .
%%              concl                           concl
%%      \endprooftree
%%
%% Within a prooftree, \[ and \] may be used instead of \prooftree and
%% \endprooftree; this is not permitted at the outer level because it
%% conflicts with LaTeX. Also,
%%      \Justifies
%% produces a double line. In LaTeX you can use \begin{prooftree} and
%% \end{prootree} at the outer level (however this will not work for the inner
%% levels, but in any case why would you want to be so verbose?).
%%
%% All of of the keywords except \prooftree and \endprooftree are optional
%% and may appear in any order. They may also be combined in \newcommand's
%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation
%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and
%% some standard abbreviations will be found at the end of this file.
%%
%% \thickness specifies the breadth of the rule in any units, although
%% font-relative units such as "ex" or "em" are preferable.
%% It may optionally be followed by "=".
%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be
%% used either in place of \thickness or globally; the default is 0.04em.
%% \proofdotseparation and \proofdotnumber control the size of the
%% string of dots
%%
%% If proof trees and formulae are mixed, some explicit spacing is needed,
%% but don't put anything to the left of the left-most (or the right of
%% the right-most) hypothesis, or put it in braces, because this will cause
%% the indentation to be lost.
%%
%% By default the conclusion is centered wrt the left-most and right-most
%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves
%% it relative to this position. (Not sure about this specification or how
%% it should affect spreading of proof tree.)
%
% global assignments to dimensions seem to have the effect of stretching
% diagrams horizontally.
%
%%==========================================================================

\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%%
\def\andintro{\using{\land}\introrule\justifies}%%
\def\impelim{\using{\Rightarrow}\elimrule\justifies}%%
\def\allintro{\using{\forall}\introrule\justifies}%%
\def\allelim{\using{\forall}\elimrule\justifies}%%
\def\falseelim{\using{\bot}\elimrule\justifies}%%
\def\existsintro{\using{\exists}\introrule\justifies}%%

%% #1 is meant to be 1 or 2 for the first or second formula
\def\andelim#1{\using{\land}#1\elimrule\justifies}%%
\def\orintro#1{\using{\lor}#1\introrule\justifies}%%

%% #1 is meant to be a label corresponding to the discharged hypothesis/es
\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%%
\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%%
\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies}

%%==========================================================================

\newdimen\proofrulebreadth \proofrulebreadth=.05em
\newdimen\proofdotseparation \proofdotseparation=1.25ex
\newdimen\proofrulebaseline \proofrulebaseline=2ex
\newcount\proofdotnumber \proofdotnumber=3
\let\then\relax
\def\hfi{\hskip0pt plus.0001fil}
\mathchardef\squigto="3A3B
%
% flag where we are
\newif\ifinsideprooftree\insideprooftreefalse
\newif\ifonleftofproofrule\onleftofproofrulefalse
\newif\ifproofdots\proofdotsfalse
\newif\ifdoubleproof\doubleprooffalse
\let\wereinproofbit\relax
%
% dimensions and boxes of bits
\newdimen\shortenproofleft
\newdimen\shortenproofright
\newdimen\proofbelowshift
\newbox\proofabove
\newbox\proofbelow
\newbox\proofrulename
%
% miscellaneous commands for setting values
\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 }
\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }%
\afterassignment\setshiftproofbelow\dimen0 }
\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 }
\def\setproofrulebreadth{\proofrulebreadth}

%=============================================================================
\def\prooftree{% NESTED ZERO (\ifonleftofproofrule)
%
% first find out whether we're at the left-hand end of a proof rule
\ifnum  \lastpenalty=1
\then   \unpenalty
\else   \onleftofproofrulefalse
\fi
%
% some space on left (except if we're on left, and no infinity for outermost)
\ifonleftofproofrule
\else   \ifinsideprooftree
        \then   \hskip.5em plus1fil
        \fi
\fi
%
% begin our proof tree environment
\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove,
%               \shortenproofleft, \shortenproofright, \proofrulebreadth)
\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}%
\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl
\let\using\proofusing\let\[\prooftree
\ifinsideprooftree\let\]\endprooftree\fi
\proofdotsfalse\doubleprooffalse
\let\thickness\setproofrulebreadth
\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow
\let\shiftleft\shiftproofbelowneg
\let\ifwasinsideprooftree\ifinsideprooftree
\insideprooftreetrue
%
% now begin to set the top of the rule (definitions local to it)
\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO
\let\wereinproofbit\prooftree
%
% these local variables will be copied out:
\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt
%
% flags to enable inner proof tree to detect if on left:
\onleftofproofruletrue\penalty1
}

%=============================================================================
% end whatever box and copy crucial values out of it
\def\eproofbit{% NESTED TWO
%
% various hacks applicable to hypothesis list 
\ifx    \wereinproofbit\prooftree
\then   \ifcase \lastpenalty
        \then   \shortenproofright=0pt  % 0: some other object, no indentation
        \or     \unpenalty\hfil         % 1: empty hypotheses, just glue
        \or     \unpenalty\unskip       % 2: just had a tree, remove glue
        \else   \shortenproofright=0pt  % eh?
        \fi
\fi
%
% pass out crucial values from scope
\global\dimen0=\shortenproofleft
\global\dimen1=\shortenproofright
\global\dimen2=\proofrulebreadth
\global\dimen3=\proofbelowshift
\global\dimen4=\proofdotseparation
\global\count255=\proofdotnumber
%
% end the box
$\egroup  % NESTED ONE
%
% restore the values
\shortenproofleft=\dimen0
\shortenproofright=\dimen1
\proofrulebreadth=\dimen2
\proofbelowshift=\dimen3
\proofdotseparation=\dimen4
\proofdotnumber=\count255
}

%=============================================================================
\def\proofover{% NESTED TWO
\eproofbit % NESTED ONE
\setbox\proofbelow=\hbox\bgroup % NESTED TWO
\let\wereinproofbit\proofover
$\displaystyle
}%
%
%=============================================================================
\def\proofoverdbl{% NESTED TWO
\eproofbit % NESTED ONE
\doubleprooftrue
\setbox\proofbelow=\hbox\bgroup % NESTED TWO
\let\wereinproofbit\proofoverdbl
$\displaystyle
}%
%
%=============================================================================
\def\proofoverdots{% NESTED TWO
\eproofbit % NESTED ONE
\proofdotstrue
\setbox\proofbelow=\hbox\bgroup % NESTED TWO
\let\wereinproofbit\proofoverdots
$\displaystyle
}%
%
%=============================================================================
\def\proofusing{% NESTED TWO
\eproofbit % NESTED ONE
\setbox\proofrulename=\hbox\bgroup % NESTED TWO
\let\wereinproofbit\proofusing
\kern0.3em$
}

%=============================================================================
\def\endprooftree{% NESTED TWO
\eproofbit % NESTED ONE
% \dimen0 =     length of proof rule
% \dimen1 =     indentation of conclusion wrt rule
% \dimen2 =     new \shortenproofleft, ie indentation of conclusion
% \dimen3 =     new \shortenproofright, ie
%                space on right of conclusion to end of tree
% \dimen4 =     space on right of conclusion below rule
  \dimen5 =0pt% spread of hypotheses
% \dimen6, \dimen7 = height & depth of rule
%
% length of rule needed by proof above
\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft
\advance\dimen0-\shortenproofright
%
% amount of spare space below
\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow
\dimen4=\dimen1
\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift
%
% conclusion sticks out to left of immediate hypotheses
\ifdim  \dimen1<0pt
\then   \advance\shortenproofleft\dimen1
        \advance\dimen0-\dimen1
        \dimen1=0pt
%       now it sticks out to left of tree!
        \ifdim  \shortenproofleft<0pt
        \then   \setbox\proofabove=\hbox{%
                        \kern-\shortenproofleft\unhbox\proofabove}%
                \shortenproofleft=0pt
        \fi
\fi
%
% and to the right
\ifdim  \dimen4<0pt
\then   \advance\shortenproofright\dimen4
        \advance\dimen0-\dimen4
        \dimen4=0pt
\fi
%
% make sure enough space for label
\ifdim  \shortenproofright<\wd\proofrulename
\then   \shortenproofright=\wd\proofrulename
\fi
%
% calculate new indentations
\dimen2=\shortenproofleft \advance\dimen2 by\dimen1
\dimen3=\shortenproofright\advance\dimen3 by\dimen4
%
% make the rule or dots, with name attached
\ifproofdots
\then
        \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0
        \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}%
        \setbox0=\hbox{%
                \advance\dimen6-.5\wd1
                \kern\dimen6
                $\vcenter to\proofdotnumber\proofdotseparation
                        {\leaders\box1\vfill}$%
                \unhbox\proofrulename}%
\else   \dimen6=\fontdimen22\the\textfont2 % height of maths axis
        \dimen7=\dimen6
        \advance\dimen6by.5\proofrulebreadth
        \advance\dimen7by-.5\proofrulebreadth
        \setbox0=\hbox{%
                \kern\shortenproofleft
                \ifdoubleproof
                \then   \hbox to\dimen0{%
                        $\mathsurround0pt\mathord=\mkern-6mu%
                        \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill
                        \mkern-6mu\mathord=$}%
                \else   \vrule height\dimen6 depth-\dimen7 width\dimen0
                \fi
                \unhbox\proofrulename}%
        \ht0=\dimen6 \dp0=-\dimen7
\fi
%
% set up to centre outermost tree only
\let\doll\relax
\ifwasinsideprooftree
\then   \let\VBOX\vbox
\else   \ifmmode\else$\let\doll=$\fi
        \let\VBOX\vcenter
\fi
% this \vbox or \vcenter is the actual output:
\VBOX   {\baselineskip\proofrulebaseline \lineskip.2ex
        \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi
        \hbox   spread\dimen5   {\hfi\unhbox\proofabove\hfi}%
        \hbox{\box0}%
        \hbox   {\kern\dimen2 \box\proofbelow}}\doll%
%
% pass new indentations out of scope
\global\dimen2=\dimen2
\global\dimen3=\dimen3
\egroup % NESTED ZERO
\ifonleftofproofrule
\then   \shortenproofleft=\dimen2
\fi
\shortenproofright=\dimen3
%
% some space on right and flag we've just made a tree
\onleftofproofrulefalse
\ifinsideprooftree
\then   \hskip.5em plus 1fil \penalty2
\fi
}

%==========================================================================
% IDEAS
% 1.    Specification of \shiftright and how to spread trees.
% 2.    Spacing command \m which causes 1em+1fil spacing, over-riding
%       exisiting space on sides of trees and not affecting the
%       detection of being on the left or right.
% 3.    Hack using \@currenvir to detect LaTeX environment; have to
%       use \aftergroup to pass \shortenproofleft/right out.
% 4.    (Pie in the sky) detect how much trees can be "tucked in"
% 5.    Discharged hypotheses (diagonal lines).

\makeatother

\newcounter{l}
\newcommand{\rln}[3]{\setcounter{l}{#2-#1}\put(#1,#3){\line(1,0){\value{l}}}}% x1 x2 y   -
\newcommand{\lln}[3]{\setcounter{l}{#1-#2}\put(#2,#3){\line(1,0){\value{l}}}}% x1 x2 y   -
\newcommand{\uln}[3]{\setcounter{l}{#3-#2}\put(#1,#2){\line(0,1){\value{l}}}}% x y1 y2   |
\newcommand{\dln}[3]{\setcounter{l}{#2-#3}\put(#1,#2){\line(0,-1){\value{l}}}}% x y1 y2   |

\newcommand{\rlink}[4]{\uln{#1}{#3}{#4}\uln{#2}{#3}{#4}\rln{#1}{#2}{#4}}
\newcommand{\llink}[4]{\uln{#1}{#3}{#4}\uln{#2}{#3}{#4}\lln{#1}{#2}{#4}}

\newcommand{\hln}[3]{\ifthenelse{#2 > #1}%  x1 x2 y  -
{\rln{#1}{#2}{#3}}{\lln{#1}{#2}{#3}}}
\newcommand{\vln}[3]{\ifthenelse{#3 > #2}%  x y1 y2   |
{\uln{#1}{#2}{#3}}{\dln{#1}{#2}{#3}}}
\newcommand{\link}[4]{\vln{#1}{#3}{#4}\vln{#2}{#3}{#4}\hln{#1}{#2}{#4}}

\newlength{\boxht}
\newcommand{\obox}[2]{\raisebox{#1}{\makebox[0pt][l]{#2}}}
\newcommand{\oboxlink}[5]{\obox{#1}{\begin{picture}(0,#5)\link{#2}{#3}{#4}{#5}\end{picture}}}
\newcommand{\olinkexplicit}[4]{\oboxlink{\boxht}{#1}{#2}{#3}{#4}}
\newlength{\boxdp}\newlength{\uboxlocalvar}
\newcommand{\ubox}[2]{\settoheight{\uboxlocalvar}{#2}\addtolength{\uboxlocalvar}{#1}%
\raisebox{-\uboxlocalvar}{\makebox[0pt][l]{#2}}}
\newcommand{\uboxlink}[5]{\ubox{#1}{\begin{picture}(0,#5)(0,-#5)\link{#2}{#3}{-#4}{-#5}\end{picture}}}
\newcommand{\ulinkexplicit}[4]{\uboxlink{\boxdp}{#1}{#2}{#3}{#4}}

\newcommand{\olinkbasey}{0}\newcommand{\ulinkbasey}{0}
\newcommand{\olinkspecy}[3]{\olinkexplicit{#1}{#2}{\olinkbasey}{#3}} % spec height of link
\newcommand{\ulinkspecy}[3]{\ulinkexplicit{#1}{#2}{\ulinkbasey}{#3}} % spec height of link

\newcommand{\olinky}{4}\newcommand{\ulinky}{\olinky}
\newcommand{\oolinky}{7}\newcommand{\uulinky}{\oolinky}
\newcommand{\ooolinky}{10}\newcommand{\uuulinky}{\ooolinky}
\newcommand{\olink}[2]{\olinkspecy{#1}{#2}{\olinky}}
\newcommand{\oolink}[2]{\olinkspecy{#1}{#2}{\oolinky}}
\newcommand{\ooolink}[2]{\olinkspecy{#1}{#2}{\ooolinky}}
\newcommand{\ulink}[2]{\ulinkspecy{#1}{#2}{\ulinky}}
\newcommand{\uulink}[2]{\ulinkspecy{#1}{#2}{\uulinky}}
\newcommand{\uuulink}[2]{\ulinkspecy{#1}{#2}{\uuulinky}}
\newcommand{\centredlinks}[2]{% centred meaning underlinks create depth
\settoheight{\boxht}{\ensuremath{#1}}\settodepth{\boxdp}{\ensuremath{#1}}#2\ensuremath{#1}}%{fmla}{u/olks}
\newlength{\updepthboxvar}
\newcommand{\updepthbox}[1]{\settodepth{\updepthboxvar}{#1}\raisebox{\updepthboxvar}{#1}}
\newcommand{\usualdepth}{.1ex}% 1ex
\newcommand{\shiftdown}[1]{\raisebox{-\usualdepth}{#1}}
\newlength{\fattenheight}\newlength{\fattendepth}
\newcommand{\fattenbox}[1]{\settoheight{\fattenheight}{#1}\addtolength{\fattenheight}{.5ex}%
\settodepth{\fattendepth}{#1}\addtolength{\fattendepth}{0ex}\raisebox{0pt}[\fattenheight][\fattendepth]{#1}}
\newcommand{\links}[2]{\fattenbox{\shiftdown{\updepthbox{\centredlinks{#1}{#2}}}}}
\newcommand{\PPperpolink}{\links{P,P\perp}{\olink{4}{17}}}
\newcommand{\PPperpulink}{\links{P,P\perp}{\ulink{3}{16}}}
\newcommand{\QQperpolink}{\links{Q,Q\perp}{\olink{4}{18}}}
\newcommand{\QQperpulink}{\links{Q,Q\perp}{\ulink{3}{17}}}
\newcommand{\RRperpolink}{\links{R,R\perp}{\olink{4}{18}}}
\newcommand{\RRperpulink}{\links{R,R\perp}{\ulink{3}{17}}}
\newcommand{\PperpPolink}{\links{P\perp,P}{\olink{5}{25}}}
\newcommand{\PperpPulink}{\links{P\perp,P}{\ulink{4}{24}}}
\newcommand{\QperpQolink}{\links{Q\perp,Q}{\olink{5}{25}}}
\newcommand{\QperpQulink}{\links{Q\perp,Q}{\ulink{3}{24}}}
\newlength{\commadepth}\settodepth{\commadepth}{,}
\newcommand{\fakecomma}{\raisebox{0ex}[\height][\commadepth]{\strut}}
\newlength{\fakerise}
\newcommand{\fakeulink}%[1]{%
{\ubox{\boxdp}{\begin{picture}(0,\ulinky)\end{picture}}}
\newcommand{\QparQperpolink}{\links{Q\parr Q\perp}{\olink{4}{22}}}
\newcommand{\RparRperpulink}{\links{R\parr R\perp\fakecomma}{\ulink{4}{22}}}
\newcommand{\QparQperpolinkfakeulink}{\links{Q\parr Q\perp}{\olink{4}{22}\fakeulink}}
\newcommand{\QsmallparQperpolink}{\links{Q\smallparr Q\perp}{\olink{4}{22}}}
\newcommand{\RsmallparRperpulink}{\links{R\smallparr R\perp\fakecomma}{\ulink{4}{22}}}
\newcommand{\QsmallparQperpolinkfakeulink}{\links{Q\smallparr Q\perp}{\olink{4}{22}\fakeulink}}

\newlength{\tw}\setlength{\tw}{\textwidth}\addtolength{\tw}{-\arrayrulewidth}
\addtolength{\tw}{-\tabcolsep}
\newenvironment{plainbox}{\begin{flushleft}\begin{tabular}{@{}|c@{}|@{}}\hline 
 \begin{minipage}[b]{\tw}\vspace*{.06in}
 \begingroup\small\baselineskip13pt}{\endgroup\end{minipage} \\ \hline
 \end{tabular}\end{flushleft}}
\newenvironment{labelbox}[1]{\begin{flushleft}\rule{5mm}{0.4pt}%
\hspace*{0.3mm}\raisebox{-3mm}{\rule{0mm}{6mm}}
\raisebox{-0.8mm}{\bf #1}{\rule{0mm}{6mm}}
\hrulefill\vspace*{-3.4mm}
\begin{tabular}{@{}|c@{}|@{}}\begin{minipage}[b]{\tw}\vspace*{5mm}\begingroup}
{\protect\rule{0mm}{1mm}\endgroup\end{minipage}\\
 \hline \end{tabular}\end{flushleft}}
\newenvironment{twolabelbox}[2]{\begin{flushleft}\rule{5mm}{0.4pt}%
\hspace*{0.3mm}\raisebox{-3mm}{\rule{0mm}{6mm}}
\raisebox{-0.8mm}{\bf #1}{\rule{0mm}{6mm}}
\hrulefill%
{\rule{0mm}{6mm}}
\raisebox{-0.8mm}{\bf #2}%
\raisebox{-3mm}{\rule{0mm}{6mm}}%
\hspace*{0.3mm}%
\rule{5mm}{0.4pt}%
\raisebox{-3mm}{\rule{0mm}{6mm}}%
\vspace*{-3.4mm}
\begin{tabular}{@{}|c@{}|@{}}\begin{minipage}[b]{\tw}\vspace*{5mm}\begingroup}
{\protect\rule{0mm}{1mm}\endgroup\end{minipage}\\ 
\hline \end{tabular}\end{flushleft}}

\theoremheaderfont{\scshape}
\theorembodyfont{\normalfont\slshape}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}
\newtheorem{localisedlemma}{Localised Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{altdefinition}{Alternative Definition}
\theorembodyfont{\normalfont}
\newtheorem{remark}{Remark}
\newtheorem{example}{Example}
\newenvironment{proof}
  {\begin{trivlist}\item{}\normalfont\textit{Proof. }}
  {\hfill$\square$\end{trivlist}}
\newlength{\blockskip} \setlength{\blockskip}{1em}
\newcommand\doblockskip{\vspace{\blockskip}}
\newcommand\gappar{\doblockskip\noindent}
\newcommand\gapsubheading[1]{\gappar\textbf{#1 }}
\newcommand{\defn}[1]{{\textit{\textbf{#1}}}}
\newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX
\newbox\PLdot \setbox\PLdot\hbox{{\tiny.}} \def\scl{.07} % resettable scale
\def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply
\PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt
\advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}
\def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}
\def\invamp{\hbox{\PLyy=70pt\draw :::;DMV_gqppyyyyyooooxxxnnwvlutkjaWNE=5-./9%
9:::CCCC:::99/..--544=EENWWaajjjkktttttttNNNVVVVVVVV\end \hskip6pt}}
\newcount\smallPLv\newcount\smallPLw\newcount\smallPLx\newcount\smallPLy\newdimen\smallPLyy\newdimen\smallPLX\newbox\smallPLdot \setbox\smallPLdot\hbox{{\tiny.}} \def\smallscl{.062} \def\smallPLot#1{\smallPLx`#1\advance\smallPLx-42\smallPLy\smallPLx\smallPLv\smallPLx\divide\smallPLy9\smallPLw\smallPLy\multiply \smallPLw9\advance\smallPLx-\smallPLw\advance\smallPLx-4\smallPLy-\smallPLy\advance\smallPLy4\smallPLX=\the\smallPLx pt \advance\smallPLyy\the\smallPLy pt\wd\smallPLdot=\smallscl\smallPLX\raise\smallscl\smallPLyy\copy\smallPLdot} \def\smalldraw#1{\ifx#1\end\let\next=\relax\else\smallPLot#1\let\next=\smalldraw\fi\next} \def\smallinvamp{\hbox{\smallPLyy=70pt\smalldraw :::;DMV_gqppyyyyyooooxxxnnwvlutkjaWNE=5-./99:::CCCC:::99/..--544=EENWWaajjjkktttttttNNNVVVVVVVV\end \hskip6pt}}
\newcommand{\smallparr}{\smallinvamp}

\newcommand{\todo}[1]{{[[\textsf{\textsc{#1}}]]}}
\newcommand{\with}{\mkern1mu\&\mkern1mu}
\newcommand{\plus}{\oplus}
\newcommand{\tensor}{\otimes}
\newcommand{\tightplus}{\!\oplus\!}
\newcommand{\tighttensor}{\!\otimes\!}
\newcommand{\parr}{\invamp}
\newlength{\parrdp}\newlength{\parrht}
\settodepth{\parrdp}{$\&$}\settoheight{\parrht}{$\&$}
\renewcommand{\parr}{\raisebox{-\parrdp}{\raisebox{\parrht}{\rotatebox{180}{$\&$}}}}
\newlength{\smallparrdp}\newlength{\smallparrht}
\settodepth{\smallparrdp}{{\small$\&$}}\settoheight{\smallparrht}{{\small$\&$}}
\renewcommand{\smallparr}
{\mkern1mu\raisebox{-.3\smallparrdp}{\raisebox{\smallparrht}{\rotatebox{180}{$\&$}}}\mkern1mu}
\newcommand{\withs}[1]{\mathcal{W}(#1)}
\newcommand{\axlinks}[1]{\mathcal{L}(#1)}
\newcommand{\withswitchings}[1]{2^{\withs{#1}}}
\newcommand{\switchleft}{\textsf{\textsl{left}}}
\newcommand{\switchright}{\textsf{\textsl{right}}}
\newcommand{\graph}[1]{\mathcal{G}_{#1}}
\newcommand{\slice}[1]{\overline{#1}}
\newcommand{\reducedslice}[2]{\mathcal{G}^{^{-}}_{#1}(#2)}
\newcommand{\toggle}[2]{{#1}^{#2}}
\newcommand{\weight}[2]{\mu^{#2}(#1)}
\newcommand{\linking}[1]{\Lambda_{#1}}
\newcommand{\pair}[2]{\langle{#1},{#2}\rangle}
\newcommand{\switching}[1]{\widehat{#1}}
\newcommand{\var}[1]{p_{#1}}
\newcommand{\track}[1]{\widehat{#1}}
\newcommand{\dropdown}[1]{\overline{#1}}
\newcommand{\elts}[1]{\mathsf{elts}(#1)}
\newcommand{\negate}[1]{\neg{#1}}
\newcommand{\extension}[1]{\overline{#1}}
\newcommand{\weightand}{\,.\,}
\newcommand{\weightor}{\,\vee\,}
\newcommand{\edge}{\rightarrow}
\newcommand{\edgefrom}{\leftarrow}
\newcommand{\edgein}[1]{\stackrel{#1}{\edge}}
\newcommand{\jump}{\edge}
\newcommand{\jumpfrom}{\leftarrow}
\newcommand{\jumpin}[1]{\stackrel{#1}{\edge}}
\newcommand{\inn}{\in}
\newcommand{\notinn}{\not\in}
\newcommand{\sect}[1]{#1}
\newcommand{\fullgraph}{\graph{\theta}}
\newcommand{\support}[2]{\mu_{#2}(#1)}
\newcommand{\strongpath}{\Rightarrow}
\newcommand{\strongpathin}[1]{\strongpath_{#1}}
\newcommand{\dominates}{\sqsupset}
\newcommand{\dominated}{\sqsubset}
\newcommand{\dominatesin}[1]{\dominates_{#1}}
\newcommand{\slide}{\;\mbox{---}\;}
\newcommand{\backback}{\leftarrow\rightarrow}
\newcommand{\faceface}{\rightarrow\leftarrow}
\newcommand{\axedges}[1]{\vec{\mathsf{ax}}(#1)}
\renewcommand{\perp}{^\bot}
\newcommand{\perpp}{^\bot}
\newcommand{\perpof}[1]{{#1}\perpp}
\newcommand{\tensorunit}{\mathbf{1}}
\newcommand{\plusunit}{\mathbf{0}}
\newcommand{\parunit}{\perp}
\newcommand{\withunit}{\top}
\newcommand{\bigtensor}{\bigotimes}
\newcommand{\bigpar}{\bigtensor}
\newcommand{\twist}{\mathsf{tw}}
\newcommand{\identity}{\mathsf{id}}
\newcommand{\mallrule}[3]{\mbox{$\frac{#1}{#2}{#3}$}}
\newcommand{\restr}{\!\restriction\!}
\newcommand{\comment}[1]{\marginpar{\raggedright\scriptsize#1}}
\newcommand{\ie}{\textit{i.e.}}
\newcommand{\etc}{\textit{etc.}}
\newcommand{\eg}{\textit{e.g.}}
\newcommand{\viz}{\textit{viz.}}
\newcommand{\cf}{\textit{c.f.}}
\newcommand{\qed}{\textit{Q.E.D.}}
\newcommand{\dom}[1]{\mathsf{dom}(#1)}
\newcommand{\axiomvertex}{\bullet}
\newcommand{\binwith}{\with_2}
\newcommand{\resolution}[2]{{#2}\restr{#1}}
\newcommand{\delsize}{14}\newcommand{\delrad}{7}
\newcommand{\deletion}{\begin{picture}(0,0)\put(-\delrad,-\delrad){\line(1,1){\delsize}}%
\put(-\delrad,\delrad){\line(1,-1){\delsize}}\end{picture}}
\newcommand{\deletionat}[1]{\begin{picture}(0,0)\put(#1,4){\makebox(0,0){\deletion}}\end{picture}}
\newcommand{\mllof}[1]{\widehat{#1}}
\newcommand{\switch}[1]{\widehat{#1}}
\newcommand{\judgement}{\raisebox{.15ex}{$\mkern9mu\rhd\mkern8mu$}}

\newcommand{\withresolution}[1]{#1^{\star}}
\newcommand{\setsuchthat}[2]{\{\,#1\,:\,#2\,\}}
\newcommand{\cutseq}[2]{[#1]\,#2}
\newcommand{\psjudgement}[3]{#2\judgement\cutseq{#1}{\:#3}}
\newcommand{\shortbig}[1]{\raisebox{0ex}[0ex][0ex]{\ensuremath{\big#1}}}
\newcommand{\biggish}[1]{\text{\large \raisebox{-.08ex}{$#1$}}}
\newcommand{\biggishleft}[1]{\biggish{\mkern-1mu#1}}
\newcommand{\biggishright}[1]{\biggish{#1\mkern-1mu}}
\newcommand{\smallbiggish}[1]{\text{\normalsize \raisebox{-.08ex}{$#1$}}}
\newcommand{\smallbiggishleft}[1]{\smallbiggish{\mkern-1mu#1}}
\newcommand{\smallbiggishright}[1]{\smallbiggish{#1\mkern-1mu}}
\newcommand{\triplebraceleft}{\big\{\biggishleft\{\{}
\newcommand{\triplebraceright}{\big\}\biggishrigh\}\}}
\newcommand{\seqrel}{\rightsquigarrow}

\newcommand{\cut}{\mkern-2mu\ast\mkern-2mu}
\newlength{\cupwidth}
\newcommand{\unionprod}{\odot}
\newcommand{\nth}{^{\text{th}}}

\newcommand{\rulelabel}[1]{\mbox{\small$\mathsf{#1}$}}
\newcommand{\tensorlabel}{\otimes}
\newcommand{\parlabel}{\parr}
\newcommand{\smallparlabel}{\smallparr}
\newcommand{\leftpluslabel}{\oplus_1}
\newcommand{\rightpluslabel}{\oplus_2}
\newcommand{\withlabel}{\with}
\newcommand{\cutlabel}{\rulelabel{cut}}
\newcommand{\axlabel}{\rulelabel{ax}}
\newcommand{\incoh}{{\mkern4mu\stackrel{\smile}{_\frown}}} %smallsmile, amssymb package

\newcommand{\filledbox}{\rule{1.2ex}{1.2ex}}


\title{%
\vspace{-3ex}
{Proof Nets for Unit-free Multiplicative-Additive Linear Logic}\\
\large (Extended abstract)\thanks{This paper appeared in 
Proceedings 18th Annual IEEE Symposium on \textsl{Logic in Computer Science}
(LICS 2003), Ottawa, Canada, June 2003, except for the appendices,
which contain the proofs omitted in the LICS paper.
A preliminary version of some of the material in 
this paper was presented in a talk at the workshop \textsl{Linear Logic 2002}, Copenhagen.}
}
\author{%
   \sc Dominic Hughes \\ 
   \small Stanford University 
\and
   \sc Rob van Glabbeek \\
   \small Stanford University 
}
\date{}
\begin{document}


\advance\textheight 1.15em
\maketitle
\advance\textheight -1.15em
\thispagestyle{empty}
\vspace{-1ex}%
\vspace{-4.6ex}%
{\small\slshape\noindent 
A cornerstone of the theory of proof nets for unit-free multiplicative
linear logic (MLL) is the abstract representation of cut-free proofs
modulo inessential commutations of rules.  The only known extension to
additives, based on monomial weights, fails to preserve this key
feature: a host of cut-free monomial proof nets can correspond to the
same cut-free proof.  Thus the problem of finding a satisfactory
notion of proof net for unit-free multiplicative-additive linear logic
(MALL) has remained open since the inception of linear logic in 1986.
We present a new definition of MALL proof net which remains faithful
to the cornerstone of the MLL theory.  }

\vspace{-1ex}
\section{Introduction}\label{intro}\noindent
The beautiful theory of proof nets for unit-free multiplicative linear
logic (MLL) appeared alongside the introduction of linear logic
\cite{Gir87}.  A proof net is an abstract representation of a proof:
the translation of cut-free proofs into proof nets identifies proofs
modulo inessential commutations of rules.  The identifications have
since been verified as canonical from a semantic perspective, with
numerous full completeness results for MLL, \eg\
\cite{AJ94b,HO93,Loa94,Aud97,BS96a,DHPP99}.  Furthermore, the
identifications correspond to coherences of free star-autonomous
categories 
\cite{BCST96}.

The problem of finding a satisfactory extension of the theory of proof
nets to unit-free multiplicative-additive linear logic (MALL) has
remained open since the inception of linear logic \cite{Gir87}.
Progress towards a solution was made by Girard \cite{Gir96} with a
notion of MALL proof net based on monomial weights.  Unfortunately,
monomial proof nets fail to extend the MLL theory faithfully: a single
cut-free proof may correspond to a host of monomial proof nets, and there
is no natural translation of cut-free proofs into monomial proof nets.
Indeed, to quote Girard, monomial proof nets are ``far from being
absolutely satisfactory'' \cite{Gir96}.  We illustrate the problems in
detail in Section~\ref{monomials-problems}.

In this paper we propose a new notion of MALL proof net
(Section~\ref{cut-free}) which adheres faithfully to the original MLL
theory: we provide a simple inductive translation of cut-free proofs
into cut-free proof nets,
yielding
the sought-after abstract representations of cut-free proofs modulo
inessential commutations of rules.  We define a cut-free proof net on
a sequent $\Gamma$ as a set of linkings on $\Gamma$ satisfying a
geometric correctness criterion
(Definition~\ref{cutfree-proofnet}), and prove that a set of linkings
is the translation of a proof if and only it is a proof net
(Theorem~\ref{main}).

In Section~\ref{cut} we extend our proof nets to include the cut rule,
and present a notion of cut elimination.  Our approach to cut suffers
from the same problem as Girard's monomial proof nets: in the presence
of cuts, multiple proof nets may correspond to the same proof.
However, from a semantic point of view (\viz\ full completeness) the
provision of abstract representations of MALL proofs modulo
inessential rule commutations is crucial only in the cut-free setting.
Moreover, our notion of cut elimination is simply defined, strongly
normalising, and yields a category of proof nets in which $\with$ and
$\plus$ are product and coproduct.

A crisp notion of cut-free MALL proof net is fully motivated from a
proof-theoretic perspective alone.  However, just as MLL has blossomed
through numerous fully complete semantics via cut-free MLL proof
nets, hopefully the new definition of cut-free proof net presented
here will lead to a similar blossoming of MALL.
Since cut-free monomial proof nets for MALL
are unsatisfactory for the reasons mentioned earlier (and detailed in
Section~\ref{monomials-problems}), any MALL full completeness result%
\footnote{The original motivation for this work came as part of a
project by the first author, Gordon Plotkin and Vaughan Pratt aiming
to extend the full completeness of Chu spaces for MLL \cite{DHPP99} to
MALL.  We have since discovered that the result does not extend.}
based on them (\eg\ \cite{AbrMel}, and the work in progress of Blute,
Hamano and Scott on hypercoherence spaces) suffers accordingly,
particularly with regard to faithfulness.  We anticipate that our new
definition of MALL proof net will yield cleaner and more accessible
MALL full completeness results.

\vspace{2.5ex}
\noindent\textbf{Relationship with Girard's monomial proof nets. \:} The
technical starting point for our definition of proof net was Girard's
definition of monomial proof net \cite{Gir96}, and indeed we employ
variants of Girard's ingenious notions of slice and jump.  Each of our
proof nets translates naturally into a non-monomial Girard proof net,
\ie, a Girard proof net without the condition demanding that
weights must be monomials.  Thus one of our contributions relative to
\cite{Gir96} is the successful elimination of the monomial condition.
In \cite{Gir96} Girard remarks that he had been trying to circumvent
this technical limitation since 1990, and Appendix A.1.5 of
\cite{Gir96} lists three specific problems that must be solved in any
attempt to eliminate the monomial condition,
\ie, in any attempt to define what he calls ``more liberal proof-nets'', such as
ours:
\begin{quote}\small\it
  \label{girard-quote} Weights must be monomials.  However, weights of
  the form $p\cup q$ will naturally occur if we want to allow more
  superimpositions.  The present state of affairs is as follows:
\begin{itemize}\small\it
  \item[(1)] in spite of years of efforts, I never succeeded in
  finding the right correctness criterion for these more liberal
  proof-nets; \item[(2)] general boolean coefficients might be
  delicate to represent (on the other hand, the case we consider has a
  natural presentation in terms of coherent spaces); \item[(3)]
  normalization in the full case might be messy.
\end{itemize}
\end{quote}
An important stepping stone towards finding the right criterion
to address (1) was to first settle the open problem of whether
Girard's criterion becomes insufficient upon relaxing the monomial
condition.  We show that this is indeed the case: in
Section~\ref{monomials} we present a non-monomial proof structure that
does not correspond to any proof, yet satisfies Girard's criterion.
We address (2) by leaving weights implied, defining a proof net on a
sequent $\Gamma$ as a set of axiom linkings on an extension $\Gamma^+$
of $\Gamma$ with complementary pairs of cut formula occurrences.
Point (3) is addressed by the fact that our definition of cut
elimination is sufficiently simple that confluence and strong
normalisation are immediate.

The proof that our correctness
criterion captures proof translations hinges on an ordering of
$\with$'s and $\parr$'s which we call
\emph{domination}.  By introducing domination we avoid the use of empires
\cite{Gir87,Gir96}, thereby sidestepping the problem of
stability of maximal empires (\cite{Gir96}, section 1.5.3)---the main
technical problem that led Girard to resort to monomials in the first
place.

\vspace{-1ex}
\paragraph{MALL.}\noindent
By MALL we mean multiplicative-additive linear logic without units
\cite{Gir87}.  Formulas are built from literals (propositional
variables $P,Q,\ldots$ and their negations $P\perpp$, $Q\perpp,\ldots$)
by the binary connectives \defn{tensor}~$\otimes$, \defn{par}~$\parr$,
\defn{with}~$\with$ and \defn{plus}~$\oplus$.  
Negation $(-)\perpp$ extends to arbitrary formulas by de Morgan duality. 
For technical convenience we take sequents to be
unordered, \ie, a sequent is a non-empty set of formula occurrences
$A_1,\ldots,A_n$.  
We omit turnstiles, which are redundant since all sequents are
right-sided.  Sequents are proved using the following rules:
\vspace{-1ex}

{\small
$$
\frac{}{\,P, P\perp}\;\axlabel
\hspace{6ex}
\frac{\Gamma,A\;\;\;\;\;A\perp,\Delta}
     {\Gamma,\Delta}\:\cutlabel
$$
\vspace{.3ex}
$$
\frac{\Gamma,A\;\;\;\;\;B,\Delta}
     {\Gamma,A\tensor B,\Delta}\:\tensorlabel
\hspace{6ex}
\frac{\Gamma,\,A,\,B}
     {\Gamma,\,A\smallparr B}\:\smallparlabel
$$
\vspace{.3ex}
$$
\frac{\Gamma,A\;\;\;\;\;\Gamma,B}
     {\Gamma,A\with B}\:\withlabel
\hspace{6ex}
\frac{\Gamma,\,A}
     {\Gamma,\,A\plus B}\:\leftpluslabel
\hspace{6ex}
\frac{\Gamma,\,B}
     {\Gamma,\,A\plus B}\:\rightpluslabel
$$
}\vspace{.2ex}%
Here, and throughout this document, $P,Q,\ldots$ range over
propositional variables, $A,B,\ldots$ over formulas, and
$\Gamma,\Delta,\ldots$ over sets of formula occurrences.  In
eliminating the permutation rule, we assume an implicit tracking of
formula occurrences above the line of a rule to formula occurrences
below the line.  Without loss of generality (see \cite{Gir87}) we
restrict the axiom rule to literals.

\vspace{-1ex}
\paragraph{Flavour of our approach.}
To give a flavour of our approach, Figure~\ref{intro-translation-eg}
shows an example of the inductive translation of a cut-free proof into
one of our proof nets.
\begin{figure}[tb]
\begin{center}
\vspace{-1ex}
\small\setlength{\unitlength}{.83pt}
\renewcommand{\tensor}{\!\otimes\!}
\renewcommand{\plus}{\!\oplus\!}
\newcommand{\localparr}{\smallparr}
\prooftree
\thickness=0.08em
\[
  \[
    \[  \justifies \PPperpolink \using \axlabel \]
    \[  \justifies \PPperpolink \using \axlabel \]
    \justifies    
    \links{P\tensor P,\,P\perp,P\perp}{\olink{5}{38}\oolink{23}{60}}
    \using\tensorlabel
  \]
  \[
    \[  
       \[ 
          \justifies 
	  \PPperpulink 
          \using \axlabel
       \]
       \justifies
       \links{P,P\perp\plus Q}{\ulink{3}{16}}
       \using \leftpluslabel
    \]
    \[  \justifies \PPperpulink \using \axlabel \]
    \justifies    
    \links{P\tensor P,\,P\perp,P\perp\plus Q}{\ulink{23}{38}\uulink{5}{58}}
    \using \tensorlabel
  \]
  \justifies
  \links{P\tensor P,\,P\perp,P\perp\with (P\perp\plus Q)}
    {\olink{5}{38}\oolink{23}{60}\ulink{23}{38}\uulink{5}{87}}
  \using \withlabel
\]
\justifies 
  \links{(P\tensor P)\smallparr P\perp,P\perp\with (P\perp\plus Q)}
    {\olink{8}{51}\oolink{26}{73}\ulink{26}{51}\uulink{8}{100}}
  \using \parlabel
\endprooftree
\end{center}
\vspace{-1ex}
\caption{Example of the inductive translation of a cut-free proof into a cut-free proof 
net.\label{intro-translation-eg}}\vspace{-3ex}\end{figure}
The concluding proof net consists of two linkings, one drawn above the
sequent, the other below.  Each contains two axiom links.  The proof
nets further up in the derivation have one or two linkings,
correspondingly above and/or below the sequent.  
Had we switched the
order of the right-hand tensor rule and the plus rule, we would have
obtained exactly the same pair of linkings; thus we identify cut-free
proofs modulo a commutation of rules.
Two additional translations are shown in Figure~\ref{cut-eg}.

\begin{figure*}
\vspace{-3ex}%
{\small
\begin{displaymath}
\setlength{\unitlength}{.88pt}
\renewcommand{\tensor}{\!\otimes\!}
\renewcommand{\plus}{\!\oplus\!}
\newcommand{\localparr}{\smallparr}
\newcommand{\localolink}[2]{\begin{picture}(0,6)\uln{#1}{0}{4}\uln{#2}{0}{4}\rln{#1}{#2}{4}\end{picture}}
\newcommand{\localoolink}[2]{\begin{picture}(0,9)\uln{#1}{0}{7}\uln{#2}{0}{7}\rln{#1}{#2}{7}\end{picture}}
\newcommand{\localulink}[2]{\begin{picture}(0,6)\uln{#1}{0}{4}\uln{#2}{0}{4}\rln{#1}{#2}{0}\end{picture}}
\newcommand{\localulinku}[2]{\begin{picture}(0,13)\uln{#1}{4}{8}\uln{#2}{4}{8}\rln{#1}{#2}{4}\end{picture}}
\newcommand{\ulocalulink}[2]{\begin{picture}(0,13)\uln{#1}{1}{8}\uln{#2}{1}{8}\rln{#1}{#2}{1}\end{picture}}
\newcommand{\underax}{\begin{array}{c}P,P\perp\\[-1ex] \localulink{-10}{3}\end{array}}
\newcommand{\overax}{\begin{array}{c}\\[-3.9ex]\localolink{-10}{4}\\[-.3ex]\raisebox{.3ex}{$P,P$\perp}\end{array}}
\newcommand{\overaxQ}{\begin{array}{c}\\[-3.9ex]\localolink{-10}{4}\\[-.3ex]\raisebox{.3ex}{$Q,Q$}\perp\end{array}}
\newcommand{\overlinks}[2]{\raisebox{0ex}[1ex][2.5ex]{$\begin{array}{c}#1\\[-.3ex]#2\end{array}$}}
\newcommand{\underlinks}[2]{\raisebox{0ex}[3ex][0ex]{$\begin{array}{c}#2\\[-1.3ex]#1\end{array}$}}
\begin{array}{ccc}
\begin{array}{c}
\\\\\\\\\\
\prooftree
\thickness=0.08em
  \[  \justifies \PperpPolink \using \axlabel \]
  \justifies
  \PperpPolink\links{{}\plus P\fakecomma}{}
  \using \leftpluslabel~~~~~~~
\endprooftree
\end{array}
& ~~~~~ &
\prooftree
\thickness=0.08em
\[
  \[  \justifies \PperpPolink  
      \using \axlabel\;\;\;\;\; \]
  \[
    \[
      \[  \justifies \QQperpolink \using\axlabel\]
      \justifies    
      \QsmallparQperpolink \using\smallparlabel
    \]
    \mbox{~~~~~~~~~~~~~~~~~~}
    \justifies 
    \links{(\fakecomma}{}\QsmallparQperpolink\links{)\plus(R\smallparr R\perp)\fakecomma}{}
    \using\leftpluslabel
  \]
  \justifies
    \PperpPolink\links{{}\tensor\shortbig((\fakecomma}{}
\QsmallparQperpolink\links{)\plus(R\smallparr R\perp)\shortbig)\fakecomma}{}
  \using \tensorlabel{\;\;\;\;}
\]
\hspace{3ex}
\[
  \[  \justifies \PperpPulink  
      \using \axlabel\;\;\;\;\; \]
  \[
    \mbox{~~~~~~~~~~~~~~~~~~}
    \[
      \[  \justifies \RRperpulink \using\axlabel \]
      \justifies    
      \RsmallparRperpulink
      \using\smallparlabel
    \]
    \justifies 
    \links{(Q\smallparr Q\perp)\plus(}{\fakeulink}\RsmallparRperpulink\links{)}{\fakeulink}
    \using\rightpluslabel
  \]
  \justifies
    \PperpPulink\links{{}\tensor\shortbig((Q\smallparr Q\perp)\plus(}{\fakeulink}\RsmallparRperpulink\links{)\shortbig)}{\fakeulink}\using\tensorlabel
\]
\justifies 
    \links{P\perp\with\,\fakecomma}{\olink{4}{50}\fakeulink}
    \PperpPulink\links{{}\tensor\shortbig((}{\fakeulink}\QsmallparQperpolinkfakeulink\links{)\plus(}{\fakeulink}\RsmallparRperpulink\links{)\shortbig)}{\fakeulink}
\using\withlabel
\endprooftree
\end{array}
\vspace{-.2ex}
\end{displaymath}
}%
\caption{Deriving the proof nets used
in the example of cut elimination.\label{cut-eg}}\vspace{-2ex}
\end{figure*}

Here is an example of a proof net with four linkings:
\begin{center}
\small
\setlength{\unitlength}{.93pt}
\newcommand{\localparr}{\smallparr}
\newcommand{\localtensor}{\!\tensor\!} %\smallparr
\newcommand{\colone}{0}\newcommand{\coltwo}{\colone}
\newcommand{\picheight}{105}
\newcommand{\rowfour}{0}
\newcommand{\rowthree}{30}
\newcommand{\rowtwo}{60}
\newcommand{\rowone}{90}
\newcommand{\seq}{\begin{math}P\with P,\;\;Q\with Q,\;\;(Q\perpp\localtensor P\perpp)\localtensor%
((R\localparr R)\localparr(R\perpp\localtensor R\perpp))\end{math}}
\newcommand{\pone}{-104}
\newcommand{\ptwo}{-87}
\newcommand{\qone}{-70}
\newcommand{\qtwo}{-55}
\newcommand{\qperp}{-32}
\newcommand{\pperp}{-8}
\newcommand{\rone}{26}
\newcommand{\rtwo}{42}
\newcommand{\rperpone}{66}
\newcommand{\rperptwo}{89}
\newcommand{\y}{7}
\newcommand{\yy}{10}
\newcommand{\yyy}{14}
\newcommand{\labelx}{-140}
\newcommand{\labely}{6}
\begin{picture}(0,\picheight)(3,-1)
\put(\colone,\rowone){
 \begin{picture}(0,0) \put(0,0){\makebox(0,0)[c]{\seq}}
 \uln{\pone}{\y}{\yyy} \uln{\qone}{\y}{\yy} \uln{\qperp}{\y}{\yy}
 \uln{\pperp}{\y}{\yyy} \uln{\rone}{\y}{\yy} \uln{\rtwo}{\y}{\yyy}
 \uln{\rperpone}{\y}{\yy} \uln{\rperptwo}{\y}{\yyy}
  \rln{\pone}{\pperp}{\yyy} \rln{\qone}{\qperp}{\yy}
  \rln{\rone}{\rperpone}{\yy} \rln{\rtwo}{\rperptwo}{\yyy}
  \end{picture} }
\put(\colone,\rowtwo){
 \begin{picture}(0,0) \put(0,0){\makebox(0,0)[c]{\seq}}
 \uln{\pone}{\y}{\yyy} \uln{\qtwo}{\y}{\yy} \uln{\qperp}{\y}{\yy}
 \uln{\pperp}{\y}{\yyy} \uln{\rone}{\y}{\yyy} \uln{\rtwo}{\y}{\yy}
 \uln{\rperpone}{\y}{\yy} \uln{\rperptwo}{\y}{\yyy}
  \rln{\pone}{\pperp}{\yyy} \rln{\qtwo}{\qperp}{\yy}
  \rln{\rone}{\rperptwo}{\yyy} \rln{\rtwo}{\rperpone}{\yy}
  \end{picture} }
\put(\coltwo,\rowthree){
 \begin{picture}(0,0) \put(0,0){\makebox(0,0)[c]{\seq}}
 \uln{\ptwo}{\y}{\yyy} \uln{\qone}{\y}{\yy} \uln{\qperp}{\y}{\yy}
 \uln{\pperp}{\y}{\yyy} \uln{\rone}{\y}{\yyy} \uln{\rtwo}{\y}{\yy}
 \uln{\rperpone}{\y}{\yy} \uln{\rperptwo}{\y}{\yyy}
  \rln{\ptwo}{\pperp}{\yyy} \rln{\qone}{\qperp}{\yy}
  \rln{\rone}{\rperptwo}{\yyy} \rln{\rtwo}{\rperpone}{\yy}
  \end{picture} }
\put(\coltwo,\rowfour){
 \begin{picture}(0,0) \put(0,0){\makebox(0,0)[c]{\seq}}
 \uln{\ptwo}{\y}{\yyy} \uln{\qtwo}{\y}{\yy} \uln{\qperp}{\y}{\yy}
 \uln{\pperp}{\y}{\yyy} \uln{\rone}{\y}{\yyy} \uln{\rtwo}{\y}{\yy}
 \uln{\rperpone}{\y}{\yy} \uln{\rperptwo}{\y}{\yyy}
  \rln{\ptwo}{\pperp}{\yyy} \rln{\qtwo}{\qperp}{\yy}
  \rln{\rone}{\rperptwo}{\yyy} \rln{\rtwo}{\rperpone}{\yy}
\end{picture}
}
\end{picture}\label{four-linking}
\end{center}
(To aid presentation, we duplicated the underlying sequent.)  Our
proof nets can be encoded compactly as collections of axiom links
labelled with predicates (`weights').  For example, the four-linking
proof net above can be represented as follows:
\begin{center}
\footnotesize\setlength{\unitlength}{0.86pt}
\newcommand{\localparr}{\smallparr}
\newcommand{\localtensor}{\tensor} %\smallparr
\newcommand{\colone}{35}\newcommand{\coltwo}{\colone}
\newcommand{\rowfour}{0}\newcommand{\rowthree}{37}
\newcommand{\rowtwo}{74}\newcommand{\rowone}{111}
\newcommand{\seq}{\begin{math}P\:\with_p\, P\;\;\;\;\;\;Q\:\with_q\, Q\;\;\;\;\;\;(Q\perpp\localtensor P\perpp)
\,\localtensor\,%
\big(\,(R\:\localparr\, R)\:\:\localparr\:\,(R\perpp\localtensor R\perpp)\,\big)\end{math}}
\newcommand{\pone}{-134}
\newcommand{\ptwo}{-111}
\newcommand{\qone}{-86}
\newcommand{\qtwo}{-61}
\newcommand{\qperp}{-32}
\newcommand{\pperp}{-5}
\newcommand{\rone}{39}
\newcommand{\rtwo}{59}
\newcommand{\rperpone}{92}
\newcommand{\rperptwo}{119}
\newcommand{\y}{8}
\newcommand{\yy}{15}
\newcommand{\yyy}{33}
\newcommand{\labelx}{-140}
\newcommand{\labely}{6}
\begin{picture}(0,80)(33,-40)
\put(\colone,\rowfour){\begin{picture}(0,0) \put(0,0){\makebox(0,0)[c]{\seq}}
 \uln{\pone}{\y}{\yyy} \uln{\qone}{\y}{\yy} \uln{\qperp}{\y}{\yy}
 \uln{\pperp}{\y}{\yyy} \uln{\rone}{\y}{\yy} \uln{\rtwo}{\y}{\yyy}
 \uln{\rperpone}{\y}{\yy} \uln{\rperptwo}{\y}{\yyy}
  \rln{\pone}{\pperp}{\yyy} \rln{\qone}{\qperp}{\yy}
  \rln{\rone}{\rperpone}{\yy} \rln{\rtwo}{\rperptwo}{\yyy}
  \put(\qtwo,\yyy){\makebox(-4,9)[r]{$p$}}
  \put(\qtwo,\yy){\makebox(0,9)[l]{$q$}}
  \put(\rperpone,\yy){\makebox(-20,10){$p\wedge q$}}
  \put(\rperpone,\yyy){\makebox(-2,10){${p}\wedge q$}}
 \renewcommand{\uln}{\dln}
 \renewcommand{\y}{-7}
 \renewcommand{\yy}{-14}
 \renewcommand{\yyy}{-32}
 \uln{\ptwo}{\y}{\yyy} \uln{\qtwo}{\y}{\yy} \uln{\qperp}{\y}{\yy}
 \uln{\pperp}{\y}{\yyy} \uln{\rone}{\y}{\yyy} \uln{\rtwo}{\y}{\yy}
 \uln{\rperpone}{\y}{\yy} \uln{\rperptwo}{\y}{\yyy}
  \rln{\ptwo}{\pperp}{\yyy} \rln{\qtwo}{\qperp}{\yy}
  \rln{\rone}{\rperptwo}{\yyy} \rln{\rtwo}{\rperpone}{\yy}
  \put(\qtwo,\yyy){\makebox(0,-11){$~~~\overline{p}$}}
  \put(\qtwo,\yy){\makebox(10,-11){$~~~~~~~\overline{q}$}}
  \put(\rperpone,\yy){\makebox(-2,-2)[rt]{$\overline p\vee\overline q$}}
  \put(\rperpone,\yyy){\makebox(-2,-2)[rt]{$\overline{p}\vee\overline q$}}
\end{picture}
}
\end{picture}\label{four-linking-weights}
\end{center}
To distinguish the $\with$'s, we have subscripted them.  Every
$\with$-assignment (assignment of `left' or `right' to each of
$\with_p$ and $\with_q$) determines a linking as follows: delete each
axiom link whose predicate does not hold, where we read $p$ (resp.\
$\overline{p}$) as ``$\with_p$ is assigned `left' (resp.\ `right')''
(and $q$ analogously).
The reader can check that taking each of the four possible
$\with$-assignments in turn produces the four original linkings.

We sketch the idea behind our approach to cut elimination with an
example. Consider the proof nets derived in Figure~\ref{cut-eg}.
Viewing MALL formulas as objects\footnote{The example should be
accessible to readers with no knowledge of category theory: focus on
the underlying cut elimination.}, and a proof net on $A\perp,B$
as a morphism $A\to B$, the left proof net is a morphism $P\to
P\tightplus P$ and the right proof net is a morphism $P\tightplus P\to
P\tighttensor\big((Q\parr Q\perpp)\tightplus(R\parr R\perpp)\big)$.
Composition, yielding a morphism $P\to P\tensor\big((Q\parr
Q\perpp)\plus(R\parr R\perpp)\big)$, in other words, a proof net on
the sequent $P\perp, P\tighttensor\big((Q\parr
Q\perpp)\tightplus(R\parr R\perpp)\big)$, proceeds as follows.  First,
we concatenate the two sequents into a combined sequent of four formulas
(omitting commas):
\newcommand{\cutdemocolone}{0}
\newcommand{\cutdemocoltwo}{33}
\newcommand{\cutdemocolthree}{81}
\newcommand{\cutdemocolfour}{101}
\newcommand{\cutdemocolfive}{134}
\newcommand{\cutdemocolsix}{157}
\newcommand{\cutdemocolseven}{174}
\newcommand{\cutdemocoleight}{205}
\newcommand{\cutdemocolnine}{221}
\newcommand{\cutdemolength}{.97pt}
\newcommand{\cutdemowidth}{235}
\newcommand{\localparr}{\smallparr}
\newcommand{\formulas}
  {$P\perpp~~~~~~~[P\tightplus P\,]\cdot\cdot\cdot
  [P\perpp\with P\perpp]~~~~~~~P\tighttensor\big((Q\localparr Q\perpp)\tightplus(R\localparr R\perp)\big)$}
\begin{center}
{\small\setlength{\unitlength}{\cutdemolength}
\begin{picture}(\cutdemowidth,8)
\put(-4,0){\makebox(0,0)[l]{\formulas}}
\end{picture}
}
\end{center}
The cut formulas are annotated with square brackets, and the dotted
line represents the cut.  Next, we merge the two original proof nets
into a proof net on the combined sequent:
\begin{center}
\small\setlength{\unitlength}{\cutdemolength}
\newcommand{\veclen}{3}
\newcommand{\vecx}{105}
\newcommand{\topone}{-9}
\newcommand{\picheight}{13}
\newcommand{\y}{6}
\newcommand{\yy}{9}
\newcommand{\downyy}{-8}
\newcommand{\downy}{-5}
\begin{picture}(\cutdemowidth,\picheight)(0,-\picheight)
\put(0,\topone){\begin{picture}(0,0)(0,0)
  \put(-4,0){\makebox(0,0)[l]{\formulas}}
  \uln{\cutdemocolone}{\y}{\yy}
  \uln{\cutdemocoltwo}{\y}{\yy}
  \uln{\cutdemocolthree}{\y}{\yy}
  \uln{\cutdemocolfive}{\y}{\yy}
  \rln{\cutdemocolone}{\cutdemocoltwo}{\yy}
  \rln{\cutdemocolthree}{\cutdemocolfive}{\yy}
  \uln{\cutdemocolsix}{\y}{\yy}
  \uln{\cutdemocolseven}{\y}{\yy}
  \rln{\cutdemocolsix}{\cutdemocolseven}{\yy}
  \uln{\cutdemocolsix}{\y}{\yy}
  \uln{\cutdemocolseven}{\y}{\yy}
  \rln{\cutdemocolsix}{\cutdemocolseven}{\yy}
  \dln{\cutdemocolone}{\downy}{\downyy}
  \dln{\cutdemocoltwo}{\downy}{\downyy}
  \dln{\cutdemocolfour}{\downy}{\downyy}
  \dln{\cutdemocolfive}{\downy}{\downyy}
  \rln{\cutdemocolone}{\cutdemocoltwo}{\downyy}
  \rln{\cutdemocolfour}{\cutdemocolfive}{\downyy}
  \dln{\cutdemocoleight}{\downy}{\downyy}
  \dln{\cutdemocolnine}{\downy}{\downyy}
  \rln{\cutdemocoleight}{\cutdemocolnine}{\downyy}
 \end{picture}
}
\end{picture}
\end{center}
This new proof net has two linkings, one drawn above the sequent and
one drawn below.\footnote{The link of the original proof net on
$P\perp,P\tightplus P$ appears in both the upper linking and
the lower linking of the new proof net; it is duplicated in the
merging process, to match the fact that the other proof net had two
linkings.}  Each linking consists of three axiom links.
Cut elimination proceeds as follows:
\begin{center}\label{elimination-eg}
\small\setlength{\unitlength}{\cutdemolength}
\newcommand{\veclen}{3}
\newcommand{\vecx}{105}
\newcommand{\topone}{-10}
\newcommand{\topvec}{-35}
\newcommand{\midone}{-55}
\newcommand{\botvec}{-75}
\newcommand{\botone}{-95}
\newcommand{\picheight}{95}
\newcommand{\y}{6}
\newcommand{\yy}{9}
\newcommand{\downyy}{-8}
\newcommand{\downy}{-5}
\begin{picture}(\cutdemowidth,\picheight)(0,-\picheight)
\put(0,\topone){\begin{picture}(0,0)
  \put(-4,0){\makebox(0,0)[l]{\formulas}}
  \uln{\cutdemocolone}{\y}{\yy}
  \uln{\cutdemocoltwo}{\y}{\yy}
  \uln{\cutdemocolthree}{\y}{\yy}
  \uln{\cutdemocolfive}{\y}{\yy}
  \rln{\cutdemocolone}{\cutdemocoltwo}{\yy}
  \rln{\cutdemocolthree}{\cutdemocolfive}{\yy}
  \uln{\cutdemocolsix}{\y}{\yy}
  \uln{\cutdemocolseven}{\y}{\yy}
  \rln{\cutdemocolsix}{\cutdemocolseven}{\yy}
  \uln{\cutdemocolsix}{\y}{\yy}
  \uln{\cutdemocolseven}{\y}{\yy}
  \rln{\cutdemocolsix}{\cutdemocolseven}{\yy}
  \dln{\cutdemocolone}{\downy}{\downyy}
  \dln{\cutdemocoltwo}{\downy}{\downyy}
  \dln{\cutdemocolfour}{\downy}{\downyy}
  \dln{\cutdemocolfive}{\downy}{\downyy}
  \rln{\cutdemocolone}{\cutdemocoltwo}{\downyy}
  \rln{\cutdemocolfour}{\cutdemocolfive}{\downyy}
  \dln{\cutdemocoleight}{\downy}{\downyy}
  \dln{\cutdemocolnine}{\downy}{\downyy}
  \rln{\cutdemocoleight}{\cutdemocolnine}{\downyy}
 \end{picture}
}
\put(\vecx,\topvec){\large$\downarrow$}
\renewcommand{\formulas}
 {$P\perpp~~~~~~~[P\,]\mkern-1mu\cdot\cdot\cdot\cdot\cdot\cdot\cdot\mkern-1mu
  [P\perpp]\mkern2mu~~~~~~~~~~~~~~~P\tighttensor\big((Q\smallparr Q\perpp)\tightplus(R\smallparr R\perp)\big)$}
\put(0,\midone){\begin{picture}(0,0)
  \put(-4,0){\makebox(0,0)[l]{\formulas}}
  \uln{\cutdemocolone}{\y}{\yy}
  \uln{\cutdemocoltwo}{\y}{\yy}
  \uln{\cutdemocolthree}{\y}{\yy}
  \uln{\cutdemocolfive}{\y}{\yy}
  \rln{\cutdemocolone}{\cutdemocoltwo}{\yy}
  \rln{\cutdemocolthree}{\cutdemocolfive}{\yy}
  \uln{\cutdemocolsix}{\y}{\yy}
  \uln{\cutdemocolseven}{\y}{\yy}
  \rln{\cutdemocolsix}{\cutdemocolseven}{\yy}
 \end{picture}
}
\put(\vecx,\botvec){\large$\downarrow$}
\renewcommand{\formulas}
 {$P\perpp\mkern217mu~~P\tighttensor\big((Q\smallparr Q\perpp)\tightplus(R\smallparr R\perp)\big)$}
\put(0,\botone){\begin{picture}(0,0)
  \put(-4,0){\makebox(0,0)[l]{\formulas}}
  \uln{\cutdemocolone}{\y}{\yy}
  \uln{\cutdemocolfive}{\y}{\yy}
  \rln{\cutdemocolone}{\cutdemocolfive}{\yy}
  \uln{\cutdemocolsix}{\y}{\yy}
  \uln{\cutdemocolseven}{\y}{\yy}
  \rln{\cutdemocolsix}{\cutdemocolseven}{\yy}
 \end{picture}
}
  
\end{picture}
\end{center}
The first step, aside from eliminating the $\plus$ and $\with$ to
leave a cut pair of literals $[P]\cdots[P\perp]$, retains only one of
the two original linkings.  The underhanging linking is deleted
because it is `inconsistent': it chooses opposite arguments for the
cut $\plus$ and $\with$ (left and right, respectively).  This is an
instance of our general rule for additive elimination:
\emph{retain precisely the consistent linkings}, those which choose the same argument 
for the cut $\plus$ and $\with$ (in the example above, the upper
linking, which chooses left for both).
The second step is the usual MLL elimination of a cut pair of
literals, which we include in order to frame the example in a familiar
context.  Note that the end result really is a cut-free proof net,
\ie, the translation of a cut-free proof: its witness
is a subproof of the right-hand proof of Figure~\ref{cut-eg} (the left
branch of the final $\with$-rule).


\section{Cut-free MALL proof nets}\label{cut-free}
\noindent
In this section we introduce our definition of cut-free MALL proof net.
As an \textit{aide m\'emoire} we provide a summary of the
definition in the box ahead.
We treat cut in Section~\ref{cut}.

An \defn{additive resolution} of a MALL sequent $\Gamma$ is any result
of deleting one argument subtree of every additive connective ($\with$
or $\plus$) of $\Gamma$.  Thus every remaining $\with$ and $\plus$ is
unary.
\newcommand{\twolinkingsequent}
 {P\perpp\!\plus\!(Q\!\plus\! P\perpp),\;(P\with
 P)\!\tensor\!(R\!\plus\!  R),\;(R\perpp\!\tensor\! R)\smallparr
 R\perpp\hspace{1.2cm}}
For example, two of 12 possible additive resolutions of the sequent
\begin{center}\small
$\twolinkingsequent\hspace{-1.2cm}$
\end{center}
are
\begin{center}
\newcommand{\colone}{20}\newcommand{\coltwo}{\colone}
\newcommand{\rowone}{43}
\newcommand{\rowtwo}{20}
\newcommand{\picheight}{32}
\small\setlength{\unitlength}{.85pt}
\begin{picture}(0,\picheight)(0,\picheight)
\put(\colone,\rowone){\begin{picture}(0,33)(0,-16)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\newcommand{\qperpone}{-127}
\newcommand{\qperptwo}{-79}
\newcommand{\pone}{-97}
\newcommand{\qone}{-46}
\newcommand{\qtwo}{-29}
\newcommand{\rone}{-2}
\newcommand{\rtwo}{17}
\newcommand{\rperp}{41}
\newcommand{\ess}{66}
\newcommand{\sperp}{86}
\newcommand{\topy}{8}
\newcommand{\topyy}{13}
\newcommand{\boty}{-13}
\newcommand{\botyy}{-8}
\put(\qperpone,0){\!\deletion}
\put(\pone,0){\!\!\!\deletion}
\put(\qtwo,0){\!\!\deletion}
\put(\rtwo,0){\!\!\deletion}
\end{picture}
}
\put(\coltwo,\rowtwo){\begin{picture}(0,33)(0,-16)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\newcommand{\qperpone}{-127}
\newcommand{\qperptwo}{-79}
\newcommand{\delplus}{-88}
\newcommand{\delperp}{-72}
\newcommand{\pone}{-97}
\newcommand{\qone}{-46}
\newcommand{\qtwo}{-29}
\newcommand{\rone}{-2}
\newcommand{\rtwo}{17}
\newcommand{\rperp}{41}
\newcommand{\ess}{66}
\newcommand{\sperp}{86}
\newcommand{\topy}{8}
\newcommand{\topyy}{13}
\newcommand{\boty}{-13}
\newcommand{\botyy}{-8}
\put(-88,0){\makebox(0,0){\deletion~~~~~\deletion~~~~~\deletion}}
\put(\qone,0){\makebox(0,0){\!\!\!\!\!\!\!\deletion}}
\put(\rone,0){\makebox(0,0){\!\!\!\!\!\deletion}}
\end{picture}
}
\end{picture}
\end{center}
Let $\Gamma^*$ be an additive resolution of $\Gamma$.  An \defn{axiom
link} on $\Gamma^*$ is a pair of complementary literal occurrences of
$\Gamma^*$.  A
\defn{linking} on $\Gamma^*$ is a partitioning of the set of literal
occurrences of $\Gamma^*$ into axiom links, \ie, a set of disjoint
axiom links whose union contains every literal occurrence of
$\Gamma^*$.
For example, there are two linkings possible on the first of the two
additive resolutions depicted above:
\begin{center}
\small\setlength{\unitlength}{.85pt}
\newcommand{\colone}{20}\newcommand{\coltwo}{\colone}
\newcommand{\rowone}{50}
\newcommand{\rowtwo}{23}
\newcommand{\picheight}{38}
\newcommand{\topy}{7}
\newcommand{\topyy}{11}
\newcommand{\boty}{-11}
\newcommand{\botyy}{-7}
\newcommand{\topyyy}{14}
\newcommand{\qperpone}{-127}
\newcommand{\pone}{-97}
\newcommand{\qperptwo}{-82}
\newcommand{\qone}{-52}
\newcommand{\qtwo}{-30}
\newcommand{\rone}{-5}
\newcommand{\rtwo}{17}
\newcommand{\rperp}{38}
\newcommand{\ess}{64}
\newcommand{\sperp}{86}
\begin{picture}(0,\picheight)(0,\picheight)
\put(\colone,\rowone){\begin{picture}(0,33)(0,-16)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\uln{\qperptwo}{\topy}{\topyy}
\uln{\qone}{\topy}{\topyy}
\uln{\rone}{\topy}{\topyy}
\uln{\rperp}{\topy}{\topyy}
\uln{\ess}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyy}
\rln{\qperptwo}{\qone}{\topyy}
\rln{\rone}{\rperp}{\topyy}
\rln{\ess}{\sperp}{\topyy}
\put(\qperpone,0){\!\deletion}
\put(\pone,0){\!\!\!\deletion}
\put(\qtwo,0){\!\!\deletion}
\put(\rtwo,0){\!\!\deletion}
\end{picture}
}
\put(\coltwo,\rowtwo){\begin{picture}(0,33)(0,-16)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\uln{\qperptwo}{\topy}{\topyy}
\uln{\qone}{\topy}{\topyy}
\uln{\rone}{\topy}{\topyyy}
\uln{\rperp}{\topy}{\topyy}
\uln{\ess}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyyy}
\rln{\qperptwo}{\qone}{\topyy}
\rln{\rone}{\sperp}{\topyyy}
\rln{\rperp}{\ess}{\topyy}
\put(\qperpone,0){\!\deletion}
\put(\pone,0){\!\!\!\deletion}
\put(\qtwo,0){\!\!\deletion}
\put(\rtwo,0){\!\!\deletion}
\end{picture}
}
\end{picture}
\end{center}

Every additive resolution $\Gamma^*$ of $\Gamma$ induces an MLL
sequent, namely by collapsing its additive connectives, which are unary in
$\Gamma^*$.  A linking $\lambda$ on $\Gamma^*$, viewed as being on the
induced MLL sequent, is exactly an MLL proof structure in the standard
sense \cite{Gir87}, which we call the \defn{MLL proof structure
induced by $\lambda$}.  For example, the MLL proof structure induced by
the first of the two linkings  above is:
\newcommand{\mllsequent}
 {P\perpp,\;P\tensor R,\;(R\perpp\!\tensor\! R)\parr R\perpp}
\begin{center}
\small\setlength{\unitlength}{.85pt}
\begin{picture}(0,8)(0,0)
\put(0,0){\makebox(0,0){$\mllsequent$}}
\newcommand{\qperp}{-59}
\newcommand{\qone}{-37}
\newcommand{\rone}{-15}
\newcommand{\rperp}{7}
\newcommand{\ess}{31}
\newcommand{\sperp}{53}
\newcommand{\topy}{8}
\newcommand{\topyy}{13}
\uln{\qperp}{\topy}{\topyy}
\uln{\qone}{\topy}{\topyy}
\uln{\rone}{\topy}{\topyy}
\uln{\rperp}{\topy}{\topyy}
\uln{\ess}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyy}
\rln{\qperp}{\qone}{\topyy}
\rln{\rone}{\rperp}{\topyy}
\rln{\ess}{\sperp}{\topyy}
\end{picture}
\end{center}

\begin{figure}
\vspace{-1ex}
\renewcommand{\tensor}{\tighttensor}
\begin{displaymath}\!\frac{}
     {\big\{\{\mkern2mu\{P,P\perp\}\mkern2mu\}\big\}\judgement P,P\perp}\:\axlabel
\end{displaymath}
\vspace{.2ex}
\begin{displaymath}\frac{\theta\judgement\Gamma,A\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\theta'\judgement B,\Delta}
     {\{\lambda\cup\lambda'\,:\,\lambda\in\theta,
     \lambda'\in\theta'\}\judgement \Gamma,A\tensor
     B,\Delta}\:\tensorlabel
\end{displaymath}
\vspace{.2ex}
\begin{displaymath}
\frac{\theta\judgement\Gamma,A,B}
     {\theta\judgement\Gamma,A\parr B}\:\parlabel
\hspace{6ex}
\frac{\theta\judgement\Gamma,A\;\;\;\;\;\theta'\judgement\Gamma,B}
     {\theta\cup\theta'\judgement\Gamma,A\with B}\:\withlabel
\end{displaymath}
\vspace{.2ex}
\begin{displaymath}
\frac{\theta\judgement\Gamma,A}
     {\theta\judgement\Gamma,A\plus B}\:\leftpluslabel
\hspace{6ex}
\frac{\theta\judgement\Gamma,B}
     {\theta\judgement\Gamma,A\plus B}\:\rightpluslabel
\end{displaymath}
\vspace{-2ex}
\caption{The inductive translation of cut-free MALL proofs into sets of linkings.\label{cut-free-induction}}
\vspace{-4ex}
\end{figure}
A \defn{linking on} a MALL sequent $\Gamma$ is a linking on an
additive resolution of $\Gamma$.  
Write $\resolution{\lambda}{\Gamma}$ for the additive resolution
associated with a linking $\lambda$.
Every cut-free MALL proof of $\Gamma$ defines a set of linkings on
$\Gamma$ by a simple induction, as in Figure~\ref{cut-free-induction},
where $\theta\judgement\Gamma$ is the judgement ``$\theta$ is
a set of linkings on $\Gamma$''.
(We use the implicit tracking of literal occurrences
downwards through rules.)  The base case $\axlabel$ is a singleton set
of linkings whose only linking comprises a single axiom link,
between $P$ and $P\perp$.
Examples of the inductive translation of cut-free proofs into sets
of linkings were presented in
Figures~\ref{intro-translation-eg} and \ref{cut-eg}.
Note that if a cut-free proof $\Pi'$ can be obtained from $\Pi$ by a series of
rule commutations, then $\Pi$ and $\Pi'$ translate to the same set of
linkings.


\paragraph{Geometric characterisation of proof translations.}\label{geomchar}
We present a geometric characterisation of those sets
of linkings that arise as the translations of cut-free MALL proofs,
and call them \emph{proof nets}.  Analogous to
\cite{Gir96}, as a stepping stone to the definition of a proof net, we
introduce the less restrictive notion of a \emph{proof structure}.

A \defn{$\with$-resolution} $\withresolution{\Gamma}$ of a sequent
$\Gamma$ is any result of deleting one argument subtree of every
$\with$ of $\Gamma$.  A linking $\lambda$ on $\Gamma$ is \defn{on
$\withresolution{\Gamma}$} if every literal occurrence of $\lambda$ is
in $\withresolution{\Gamma}\!$. 
A set of linkings $\theta$ on $\Gamma$ is a \defn{proof structure} on
$\Gamma$ if it satisfies
\begin{enumerate}
\item[\,(P1)\!]\:
\slshape
For every $\with$-resolution $\,\withresolution{\Gamma}$ of $\:\Gamma$,
exactly one linking of $\theta$ is on $\,\withresolution{\Gamma}$.\hspace{.2ex}%
\footnote{\label{coh}Therefore, a proof structure on $\Gamma$ is a maximal clique
in the coherence space of linkings on $\Gamma$ with incoherence
$\lambda\incoh\lambda'$ iff there exists a $\with$-resolution
$\withresolution{\Gamma}$ of $\Gamma$ such that both $\lambda$ and
$\lambda'$ are on $\withresolution{\Gamma}$.}
\end{enumerate} 
We invite the reader to verify (P1) for the sets of linkings in
Figures~\ref{intro-translation-eg} and \ref{cut-eg}.  
Any proof structure can be represented compactly as a set of axiom
links labelled with predicates (`weights'), using the encoding
described on the third page of the Introduction. 
In Section~\ref{Girard} we relate our proof structures to those of
Girard.

The second requirement for a set of linkings $\theta$ to be a proof
net is ``pointwise MLL correctness'':
\begin{enumerate}
\item[\,(P2)\!]\,
\slshape
Every linking of $\theta$ induces an MLL proof net.
\end{enumerate}
In other words, for each linking $\lambda\in\theta$, the MLL proof
structure induced by $\lambda$ is an MLL proof net, in the usual sense
\cite{Gir87,DR}.  To be self-contained, we characterise (P2) explicitly below.

\begin{table*}\vspace{-3ex}
\begin{twolabelbox}{Definition of cut-free MALL proof net}{\emph{aide m\'emoire}}
\defn{Additive resolution} of $\Gamma$: any result of deleting one
  argument subtree of every $\with$ or $\plus$ of
  $\Gamma$. (\defn{$\with$-resolution} analogously.)

\defn{Axiom link}: pair of complementary literal occurrences.

\defn{Linking} $\lambda$ on $\Gamma$: partitioning of the set of literal
  occurrences in an additive resolution $\resolution{\lambda}{\Gamma}$
  of $\Gamma$ into axiom links.
\\[2ex]
\defn{Graph $\graph{\lambda}$}: $\resolution{\lambda}{\Gamma}$ + $\lambda$ +
  edges from each axiom link in $\lambda$ to its two literal
  occurrences in $\resolution{\lambda}{\Gamma}$.

\defn{Switching} of a linking $\lambda$: any subgraph of
$\graph{\lambda}$ obtained by deleting
one of the two argument edges of each $\parr$-vertex.
\\[2ex]
A set of linkings $\Lambda$ \defn{toggles} a $\with$-occurrence $w$ of
$\Gamma$ if both arguments of $w$ are present in
$\bigcup_{\lambda \in \Lambda}\resolution{\lambda}{\Gamma}$.

An axiom link \defn{$a$ depends on $w$ within $\Lambda$} if
$\exists \lambda,\lambda'\in\Lambda$ such that $a\in\lambda$,
$a\not\in\lambda'$, and $w$ is the only $\with$ toggled by
$\{\lambda,\lambda'\}$.

\defn{Graph $\graph{\Lambda}$}: $\bigcup_{\lambda \in \Lambda}
 \graph{\lambda}$ + \defn{jump} edges between each
 axiom link in $\Lambda$ and any $\with$ on which it depends within $\Lambda$.

\defn{Switch edge} of a $\with$- or $\parr$-vertex $x$ in $\graph{\Lambda}$:
any argument or jump edge of $x$.

\defn{Switching cycle} of $\Lambda$:
a (non self-intersecting) cycle in $\graph{\Lambda}$ containing at
most one switch edge of each $\with$ and $\parr$.

\begin{tabbing}
A set of linkings $\theta$ is a \defn{proof net} if it satisfies\\
(P1)~~For every $\with$-resolution $\withresolution{\Gamma}$ of $\Gamma$,
      exactly one linking of $\theta$ is on $\withresolution{\Gamma}$.\\
(P2)~~Every switching of every linking of $\theta$ is a tree (acyclic and connected).\\
(P3)~~Every set $\Lambda$ of two or more linkings of $\theta$ toggles a
      $\with$ that is not in any switching cycle of $\Lambda$.$^\text{\ref{saturated}}$
\end{tabbing}
\vspace{-4ex}
\end{twolabelbox} 
\label{cut-free-defn-summary}
\vspace{-2ex}
\end{table*}

Henceforth view a sequent $\Gamma$ as a graph: a disjoint union of
parse trees, with literals above.  For a linking $\lambda$ on $\Gamma$
obtain the \defn{graph $\graph{\lambda}$ of $\lambda$} from the
additive resolution $\resolution{\lambda}{\Gamma}$ (a subgraph of
$\Gamma$) by adding each axiom link $a$ of $\lambda$ as a vertex above
$\resolution{\lambda}{\Gamma}$, with edges from $a$ down to its two
literal occurrences.
A \defn{switching} of a linking $\lambda$ on $\Gamma$ is any subgraph
of $\graph{\lambda}$ obtained by deleting one of the two argument
edges of each $\parr$-vertex.  (P2) holds if and only if every
switching of every linking of $\theta$ is a tree (acyclic and
connected).

We require some auxiliary concepts to state our third and last
requirement for a set of linkings to be a proof net.
A set of linkings $\Lambda$ \defn{toggles} a $\with$-occurrence $w$ of
$\Gamma$ if both arguments of $w$ are present in
$\bigcup_{\lambda \in \Lambda}\resolution{\lambda}{\Gamma}$.
An axiom link 
\defn{$a$ depends on $w$ within $\Lambda$} if,
within  $\Lambda$, $a$ can be made to vanish by toggling $w$ alone: 
there are $\lambda,\lambda'\in\Lambda$ such that $a\!\in\!\lambda$,
$a\!\not\in\!\lambda'$, and $w$ is the only $\with$ toggled by
$\{\lambda,\lambda'\}$.
\pagebreak[3]
\begin{example}\label{non-net-example}
Consider the two linkings
{% twolinkingexample begins
\newcommand{\twolambdalength}{.87pt}
\newcommand{\topy}{8}
\newcommand{\topyy}{12}
\newcommand{\boty}{-11}
\newcommand{\botyy}{-7}
\newcommand{\qperpone}{-127}% really P perp
\newcommand{\qperptwo}{-80} % really Q
\newcommand{\pone}{-98} % really P perp
\newcommand{\qone}{-51} % really P
\newcommand{\qtwo}{-33} % really P
\newcommand{\rone}{-6}
\newcommand{\rtwo}{12}
\newcommand{\rperp}{35}
\newcommand{\ess}{61}
\newcommand{\sperp}{82}
\begin{center}\label{two-linking}
\small
\setlength{\unitlength}{\twolambdalength}
\begin{picture}(0,16)(-40,-7)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\uln{\qperptwo}{\topy}{\topyy}
\uln{\qone}{\topy}{\topyy}
\uln{\rone}{\topy}{\topyy}
\uln{\rperp}{\topy}{\topyy}
\uln{\ess}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyy}
\uln{\qperpone}{\boty}{\botyy}
\uln{\qtwo}{\boty}{\botyy}
\uln{\rtwo}{\boty}{\botyy}
\uln{\rperp}{\boty}{\botyy}
\uln{\ess}{\boty}{\botyy}
\uln{\sperp}{\boty}{\botyy}
\rln{\qperptwo}{\qone}{\topyy}
\rln{\rone}{\rperp}{\topyy}
\rln{\ess}{\sperp}{\topyy}
\rln{\qperpone}{\qtwo}{\boty}
\rln{\rtwo}{\rperp}{\boty}
\rln{\ess}{\sperp}{\boty}
\put(-160,9){\makebox(0,0){$\lambda_1:$}}
\put(-160,-9){\makebox(0,0){$\lambda_2:$}}
\end{picture}
\end{center}
\pagebreak[3]
Here are $\lambda_1$ and $\lambda_2$ on their respective
additive resolutions:
\begin{center}
\small
\setlength{\unitlength}{\twolambdalength}
\begin{picture}(0,45)(-38,-18)
\put(0,0){\begin{picture}(0,33)(0,-16)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\uln{\qperptwo}{\topy}{\topyy}
\uln{\qone}{\topy}{\topyy}
\uln{\rone}{\topy}{\topyy}
\uln{\rperp}{\topy}{\topyy}
\uln{\ess}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyy}
\rln{\qperptwo}{\qone}{\topyy}
\rln{\rone}{\rperp}{\topyy}
\rln{\ess}{\sperp}{\topyy}
\put(\qperpone,0){\makebox(0,0){\deletion}}
\put(\pone,0){\makebox(0,0){\deletion}}
\put(\qtwo,0){\makebox(0,0){\!\deletion}}
\put(\rtwo,0){\makebox(0,0){\!\deletion}}
\put(-160,5){\makebox(0,0){$\lambda_1:$}}
\end{picture}
}
\put(0,-26){\begin{picture}(0,33)(0,-16)
\put(0,0){\makebox(0,0){$\twolinkingsequent$}}
\uln{\qperpone}{\boty}{\botyy}
\uln{\qtwo}{\boty}{\botyy}
\uln{\rtwo}{\boty}{\botyy}
\uln{\rperp}{\boty}{\botyy}
\uln{\ess}{\boty}{\botyy}
\uln{\sperp}{\boty}{\botyy}
\rln{\qperpone}{\qtwo}{\boty}
\rln{\rtwo}{\rperp}{\boty}
\rln{\ess}{\sperp}{\boty}
\put(-85,0){\makebox(0,0){\deletion~~~~~\deletion~~~~~\deletion}}
\put(\qone,0){\makebox(0,0){\!\deletion}}
\put(\rone,0){\makebox(0,0){\!\deletion}}
\put(-160,-5){\makebox(0,0){$\lambda_2:$}}
\end{picture}
}%
\end{picture}
\end{center}
}% twolinkingexample ends
\noindent Let $w$ be the $\with$ of the sequent, and let
$\Lambda=\{\lambda_1,\lambda_2\}$.  The axiom link between the
left-most $R\perp$ and the left-most $R$ depends on $w$ within
$\Lambda$: it is present in $\lambda_1\!\in\!\Lambda$ but not in
$\lambda_2\!\in\!\Lambda$, and $w$ is the only $\with$ toggled 
by $\{\lambda_1, \lambda_2\}$.
The axiom link between the right-most $R$ and $R\perp$ does not depend
on $w$ within $\Lambda$, since it is present in both $\lambda_1$ and
$\lambda_2$.  It is the only one of the 5 axiom links in
$\Lambda$ (more precisely, in $\bigcup\Lambda$) that does not
depend on $w$ within $\Lambda$.
\end{example}
We now extend the definition of the graph of a linking to the graph
of a set of linkings. Given a set $\Lambda$ of linkings on $\Gamma$,
obtain the \defn{graph $\graph{\Lambda}$ of $\Lambda$} from
$\bigcup_{\lambda\in\Lambda} \graph{\lambda}$ by adding,
for every $\with$-vertex $w$ and every axiom link $a$ depending on $w$
within $\Lambda$,
an edge between $w$ and $a$.  Each edge of the latter
form, between a $\with$-vertex $w$ and an axiom link, is called a
\defn{jump} of $w$.
Figure~\ref{jumpfig} shows $\graph{\{\lambda_1,\lambda_2\}}$
for $\lambda_1$ and $\lambda_2$ of Example~\ref{non-net-example}, with
four jumps (the curved edges).  In drawing an axiom link $\sqcap$, we
view the horizontal section as a vertex, and the two verticals as
edges.  We overlap edges from axiom links coming down into the same
literal occurrence (\ie,
\begin{picture}(7,9)
\put(5,0){\line(0,1){9}}
\put(0,9){\line(1,0){5}}
\put(0,5){\line(1,0){5}}
\end{picture}
means
\begin{picture}(10,9)
\put(7,0){\line(0,1){9}}
\put(0,9){\line(1,0){7}}
\put(5,0){\line(0,1){5}}
\put(0,5){\line(1,0){5}}
\end{picture}).
There is no jump to the right-most axiom link, since it
does not depend on the $\with$ within $\{\lambda_1,\lambda_2\}$.
Note that if $\Lambda\subseteq\Lambda'$, then $\graph{\Lambda}$ is a
subgraph of $\graph{\Lambda'}$, and that for any linking $\lambda$,
$\graph{\{\lambda\}}$ is precisely $\graph{\lambda}$ defined on the
previous page.  ($\graph{\{\lambda\}}$ has no jumps, 
since no $\with$ is toggled.)

\begin{figure}\footnotesize
\begin{center}
\setlength{\unitlength}{1.25pt}
\label{graph}
\begin{picture}(0,50)(-15,-12)
\newcommand{\qperpone}{-110}
\newcommand{\leftmostplus}{-94.5}
\newcommand{\leftplus}{-83}
\newcommand{\qperp}{-73}
\newcommand{\qone}{-45}
\newcommand{\qwith}{-36}
\newcommand{\qtwo}{-29}
\newcommand{\maintensor}{-12}
\newcommand{\rone}{-1}
\newcommand{\rplus}{7}
\newcommand{\rtwo}{15}
\newcommand{\rperp}{41}
\newcommand{\rtensor}{51}
\newcommand{\ess}{60}
\newcommand{\spar}{62}
\newcommand{\sperp}{78}
\newcommand{\toprow}{15}
\newcommand{\midrow}{0}
\newcommand{\botrow}{-15}
\newcommand{\topy}{19}
\newcommand{\topyy}{25}
\newcommand{\topyyy}{30}
\newcommand{\shortest}{6}
\put(\qperpone,\toprow){\makebox(0,1){$~~~P\perpp$}}
\put(\leftmostplus,\botrow){\makebox(0,0){$\plus$}}
\put(\leftplus,\midrow){\makebox(0,0){$\plus$}}
\put(\qperp,\toprow){\makebox(0,1){$~~~P\perpp$}}
\put(\qwith,\midrow){\makebox(0,0){$\with$}}
\put(\qone,\toprow){\makebox(0,0){$P$}}
\put(\qtwo,\toprow){\makebox(0,0){$P$}}
\put(\maintensor,\botrow){\makebox(0,0){$\tensor$}}
\put(\rone,\toprow){\makebox(0,0){$R$}}
\put(\rplus,\midrow){\makebox(0,0){$\plus$}}
\put(\rtwo,\toprow){\makebox(0,0){$R$}}
\put(\rperp,\toprow){\makebox(0,1){$~~~R\perpp$}}
\put(\rtensor,\midrow){\makebox(0,0){$\tensor$}}
\put(\ess,\toprow){\makebox(0,0){$R$}}
\put(\spar,\botrow){\makebox(0,0){$\smallparr$}}
\put(\sperp,\toprow){\makebox(0,1){$~~~R\perpp$}}
\uln{\qperpone}{\topy}{\topyyy}
\uln{\qperp}{\topy}{\topyy}
\uln{\qone}{\topy}{\topyy}
\uln{\rone}{\topy}{\topyyy}
\uln{\rperp}{\topy}{\topyyy}
\uln{\ess}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyy}
\uln{\qperp}{\topy}{\topyy}
\uln{\qtwo}{\topy}{\topyyy}
\uln{\rtwo}{\topy}{\topyy}
\uln{\rperp}{\topy}{\topyy}
\uln{\sperp}{\topy}{\topyy}
\rln{\qperp}{\qone}{\topyy}
\rln{\qperpone}{\qtwo}{\topyyy}
\rln{\rone}{\rperp}{\topyyy}
\rln{\rtwo}{\rperp}{\topyy}
\rln{\ess}{\sperp}{\topyy}
\put(-97,-12){\line(-1,2){11.5}}
\put(-92,-12){\line(3,4){6.5}}
\put(-81,3){\line(3,4){\shortest}}
\put(-38,3){\line(-3,4){\shortest}}
\put(-34,3){\line(3,4){\shortest}}
\put(-15,-13){\line(-5,3){18}}
\put(-9,-13){\line(4,3){14}}
\put(5,3){\line(-3,4){\shortest}}
\put(9,3){\line(3,4){\shortest}}
\put(49,3){\line(-3,4){\shortest}}
\put(53,3){\line(3,4){\shortest}}
\put(60,-12){\line(-3,4){7}}
\put(64,-12){\line(3,5){13.5}}
\qbezier(-33,1)(-20,8)(-14,20)\qbezier(-14,20)(-2,48)(10,\topyyy)
\qbezier(-33.5,2)(-22,10)(-18,24)\qbezier(-18,24)(-2,68)(25,\topyy)
\qbezier(-36,4)(-35,22)(-40,\topyyy)
\qbezier(-40,1)(-60,5)(-58,\topyy)
\end{picture}
\end{center}
\caption{The graph $\graph{\{\lambda_1,\lambda_2\}}$ of Example~\ref{non-net-example}.\label{jumpfig}}
\vspace{-2ex}
\end{figure}
\begin{figure*}[t]
$$
\renewcommand{\tensor}{\tighttensor}
\hspace{4ex}
\frac{}
     {\psjudgement{\,}{\big\{\smallbiggishleft\{\{P,P\perp\}\smallbiggishright\}\big\}}{P,P\perp}}
  \axlabel    
\hspace{11ex}
\frac{\psjudgement{\Omega}{\theta}{\Gamma,A}
      \hspace{13ex}
      \psjudgement{\Omega'}{\theta'}{A\perp,\Delta}}
     {\psjudgement{\Omega,\Omega',A\cut A\perp}
         {\{\lambda\cup\lambda'\,:\,\lambda\in\theta,\lambda'\in\theta'\}}{\Gamma,\Delta}}
    \cutlabel
$$
\vspace{1ex}
$$
\frac{\psjudgement{\Sigma,\Omega}{\theta}{\Gamma,A}
      \;\;\;\;\; \psjudgement{\Sigma,\Omega'}{\theta'}{\Gamma,B}}
      {\psjudgement{\Sigma,\Omega,\Omega'}{\theta\cup
      \theta'}{\Gamma,A\with B}} 
\withlabel
\hspace{7ex}
\frac{\psjudgement{\Omega}{\theta}{\Gamma,A}
      \hspace{13ex}
      \psjudgement{\Omega'}{\theta'}{B,\Delta}
     }
     {\psjudgement{\Omega,\Omega'}{\{\lambda\cup\lambda'\,:\,\lambda\in\theta,\lambda'\in\theta'\}}
            {\Gamma,A\tensor B,\Delta}}
\tensorlabel
$$
\vspace{0.4ex}\label{ps-rules}
$$
\frac{\psjudgement{\Omega}{\theta}{\Gamma,A}}
     {\psjudgement{\Omega}{\theta}{\Gamma,A\tightplus B}}
\leftpluslabel
\hspace{13ex}
\frac{\psjudgement{\Omega}{\theta}{\Gamma,B}}
     {\psjudgement{\Omega}{\theta}{\Gamma,A\tightplus B}}
\rightpluslabel
\hspace{13ex}
\frac{\psjudgement{\Omega}{\theta}{\Gamma,A,B}}
     {\psjudgement{\Omega}{\theta}{\Gamma,A\parr B}}
\parlabel
$$
\vspace{-2ex}
\caption{Rules for deriving sequentialisable sets of linkings on MALL cut
  sequents.\label{sequentialisable}}%
\vspace{-2ex}\end{figure*}

A \defn{switch edge} of a $\with$- or $\parr$-vertex $x$ of
$\graph{\Lambda}$ is an edge between $x$ and one of its arguments, or
a jump of $x$ (if $x$ is a $\with$).  
A \defn{switching cycle} of a set of linkings
$\Lambda$ is 
a cycle in $\graph{\Lambda}$ containing at most one switch edge of
each $\with$ and $\parr$.  (We do not permit a cycle to intersect
itself.)  For example, in $\graph{\{\lambda_1,\lambda_2\}}$ of Figure~\ref{jumpfig},
the cycle ``$\with$ $\to$
$\tighttensor$ $\to$ $\tightplus$ $\to$ left-$R$ $\to$
left-$\{R,R\perp\}$
\raisebox{-.1ex}[0pt]{$\stackrel{\!\text{\tiny jump}}{\longrightarrow}$}
$\with$'' contains only one switch edge of the $\with$, and is
therefore a switching cycle of
$\{\lambda_1,\lambda_2\}$ of Example~\ref{non-net-example}.
\begin{definition}\label{cutfree-proofnet}
A set $\theta$ of linkings on a MALL sequent $\Gamma$ is a
\defn{cut-free proof net} if it satisfies (P1), (P2)$\mkern1mu$\footnote{By
dropping connectedness from (P2) we obtain a cut-free 
proof net for MALL with the \textsc{mix} rule (hypotheses $\Gamma$ and
$\Delta$, conclusion $\Gamma,\Delta$).\label{cutfree-mixnote}} and:
\begin{enumerate}
\item[\,\rm(P3)\!]
Every set $\Lambda$ of two or more linkings of $\theta$ toggles a
$\with$ that is not in any switching cycle of $\Lambda$.%
\footnote{\label{saturated}In fact, one need only verify (P3) for those $\Lambda$ which
are \defn{saturated}, namely, such that any strictly larger subset of
$\theta$ toggles more $\with$'s than $\Lambda$.  Note that there is
exactly one saturated set of linkings in $\theta$ for each
\defn{partial $\with$-resolution} of $\Gamma$, the latter being any result of deleting one
argument subtree of some of the $\with$'s of $\Gamma$.}
\end{enumerate}
\end{definition}
\begin{example}\label{not-a-proof-net}
The set of linkings $\{\lambda_1,\lambda_2\}$ of
Example~\ref{non-net-example} is not a proof net.  It fails (P3) since
$\graph{\{\lambda_1,\lambda_2\}}$ (Figure~\ref{jumpfig}) contains a
switching cycle through the $\with$.
\end{example}
\begin{example}
\newcommand{\twistsequent}{P\perp\with P\perp,P\tightplus P}
Consider the pair of linkings on the sequent $\Gamma\equiv\twistsequent$ obtained
as follows:
\begin{center}
\small\setlength{\unitlength}{.87pt}
\renewcommand{\plus}{\tightplus}
\prooftree
\thickness=0.08em
\[
  \[ \justifies \PperpPolink
  \using \axlabel
  \] 
  \justifies \links{P\perp,P\plus P}{\olink{4}{43}}
  \using \rightpluslabel
\]
\[
  \[ \justifies \PperpPulink
  \using \axlabel
  \] \justifies 
  \links{P\perp,P\plus P}{\ulink{4}{23}} 
  \using \leftpluslabel
\]
\justifies 
  \links{P\perp \with P\perp,P\plus P}{\ulink{28}{48}\olink{4}{67}} 
\using \withlabel
\endprooftree
\end{center}
Let $\lambda_1$ and $\lambda_2$ be the upper- and lower linking
respectively (each having just one axiom link).  We shall verify
that $\{\lambda_1,\lambda_2\}$ is a cut-free proof net.
$\Gamma$ has two $\with$-resolutions,
$\Gamma^*_1\equiv\twistsequent\deletionat{-40}$ and
$\Gamma^*_2\equiv\twistsequent\deletionat{-61}$.  ~~(P1) holds, since
$\{\lambda_1,\lambda_2\}$ contains exactly one linking on
$\Gamma^\star_i$, namely $\lambda_i$.
Here are the graphs $\graph{\lambda_1}$, $\graph{\lambda_2}$, and
$\graph{\{\lambda_1,\lambda_2\}}$:
\begin{center}
\small\setlength{\unitlength}{.87pt}
\vspace{-2ex}
\setlength{\unitlength}{1.6pt}
\newcommand{\pperpone}{-92}
\newcommand{\pwith}{-83}
\newcommand{\pperptwo}{-74}
\newcommand{\pone}{-45}
\newcommand{\pplus}{-36}
\newcommand{\ptwo}{-27}
\newcommand{\topy}{19}
\newcommand{\topyy}{23}
\newcommand{\topyyy}{27}
\newcommand{\toprow}{14}
\newcommand{\midrow}{0}
\newcommand{\diagbot}{3}
\newcommand{\labelcol}{5}
\newcommand{\labelrow}{10}
\begin{picture}(0,103)(-48,25)
\put(0,80){\begin{picture}(0,0)(0,-18)
\put(\labelcol,\labelrow){\makebox(0,0)[l]{$\graph{\lambda_1}$}}
\put(\pperpone,\toprow){\makebox(0,0){$~~~P\perpp$}}
\put(\pwith,\midrow){\makebox(0,0){$\with$}}
\put(\pplus,\midrow){\makebox(0,0){$\tightplus$}}
\put(\ptwo,\toprow){\makebox(0,0){$P$}}
\uln{\pperpone}{\topy}{\topyyy}\uln{\ptwo}{\topy}{\topyyy}\rln{\pperpone}{\ptwo}{\topyyy}
\put(-86,\diagbot){\line(-3,4){5}}
\put(-34,\diagbot){\line(3,4){5}}
\end{picture}}
\put(0,46){\begin{picture}(0,0)(0,-18)
\put(\labelcol,\labelrow){\makebox(0,0)[l]{$\graph{\lambda_2}$}}
\put(\pperptwo,\toprow){\makebox(0,0){$~~~P\perpp$}}
\put(\pwith,\midrow){\makebox(0,0){$\with$}}
\put(\pone,\toprow){\makebox(0,0){$P$}}
\put(\pplus,\midrow){\makebox(0,0){$\tightplus$}}
\uln{\pperptwo}{\topy}{\topyy}\uln{\pone}{\topy}{\topyy}\rln{\pperptwo}{\pone}{\topyy}
\put(-81,\diagbot){\line(3,4){5}}
\put(-39,\diagbot){\line(-3,4){5}}
\end{picture}}
\put(0,7){\begin{picture}(0,0)(0,-18)
\put(\labelcol,\labelrow){\makebox(0,0)[l]{$\graph{\{\lambda_1,\lambda_2\}}$}}
\put(\pperpone,\toprow){\makebox(0,0){$~~~P\perpp$}}
\put(\pperptwo,\toprow){\makebox(0,0){$~~~P\perpp$}}
\put(\pwith,\midrow){\makebox(0,0){$\with$}}
\put(\pone,\toprow){\makebox(0,0){$P$}}
\put(\pplus,\midrow){\makebox(0,0){$\tightplus$}}
\put(\ptwo,\toprow){\makebox(0,0){$P$}}
\uln{\pperpone}{\topy}{\topyyy}\uln{\ptwo}{\topy}{\topyyy}\rln{\pperpone}{\ptwo}{\topyyy}
\uln{\pperptwo}{\topy}{\topyy}\uln{\pone}{\topy}{\topyy}\rln{\pperptwo}{\pone}{\topyy}
\put(-86,\diagbot){\line(-3,4){5}}
\put(-81,\diagbot){\line(3,4){5}}
\put(-39,\diagbot){\line(-3,4){5}}
\put(-34,\diagbot){\line(3,4){5}}
\qbezier(-83,5)(-79,20)(-83,\topyyy)
\qbezier(-79,1)(-60,10)(-58,\topyy)
\end{picture}
}
\end{picture}
\end{center}
Each $\lambda_i$ has just one switching, namely $\graph{\lambda_i}$.
Since each $\graph{\lambda_i}$ is a tree, (P2) holds.  Finally, (P3)
holds since $\{\lambda_1,\lambda_2\}$ toggles the $\with$, and the
$\with$ is not in any switching cycle of $\{\lambda_1,\lambda_2\}$.
\end{example}

\begin{theorem}\label{main}
A set of linkings is the translation of a cut-free proof iff it is a
cut-free proof net.
\end{theorem}
By a simple induction, the translation of a cut-free proof is a
cut-free proof net.
The proof of the converse reduces to a simple induction on the number
of $\parr$'s and $\with$'s, spelled out in
Appendix~\ref{appendix-induction}, once we prove the \emph{Separation
Lemma}: for any cut-free proof net $\theta$,
\emph{if $\graph{\theta}$ has a $\parr$ or
$\with$, then it has a $\parr$ or $\with$ that separates.}  Here a $\parr$-
or $\with$-vertex $x$ \defn{separates} if it is not an argument (\ie, is
an outermost connective), or
it is the argument of $y$ and deleting the edge between $x$ and $y$
disconnects $\graph{\theta}$.
We prove the Separation Lemma via an ordering on $\with$'s and
$\parr$'s which we call \emph{domination}\footnote{Unrelated to domination in
flowgraphs.}, a concept reminiscent of the ordering induced by the
notion of an \emph{empire} of \cite{Gir96}, but different in an
essential way.
The details are in Appendix~\ref{appendix-proof}.
The proof in the case of \textsc{mix} (see footnote~\ref{cutfree-mixnote})
requires only minor changes.


\section{Cut}\label{cut}\vspace{-1ex}

\noindent
A \defn{cut} is a pair $\{A,A\perp\}$ of complementary MALL formulas.
We write $A\cut A\perp$ for $\{A,A\perp\}$, and treat $A\cut A\perp$
akin to a MALL formula, referring to $\,\cut\:$ as the \defn{cut
connective}.
(In the cut elimination example in the Introduction we drew a cut
$A\cut A\perp$ informally as $[A]\cdots[A\perp]$.)  A \defn{cut
sequent} is a non-empty set of occurrences of MALL formulas and cuts.
A \defn{cut-additive resolution} of a cut sequent $\Delta$ is any
result of deleting some cuts from $\Delta$ and one argument
subtree of every remaining additive connective ($\with$ or $\plus$).
Thus every remaining $\with$ and $\plus$ is unary.  For example, here
is a cut sequent followed by one of its cut-additive resolutions:
\newcommand{\localseq}%
{P\tighttensor P,\;Q\cut Q\perp,\;P\perp\tightplus Q,\;(R\tightplus S)\cut(R\perp\with S\perp)}%
{\small\setlength{\unitlength}{.86pt}%
\vspace{-.6ex}
$$\localseq$$
\vspace{-3ex}
$$
\deletionat{40}
\deletionat{48}
\deletionat{56}
\deletionat{102}
\deletionat{122}
\deletionat{189}
\localseq
$$
}%
\vspace{.3ex}%
\noindent%
An \defn{axiom link} on a cut-additive resolution $\Delta^*$ of a cut sequent
$\Delta$ is a pair of complementary literal occurrences of $\Delta^*$.
A \defn{linking} on $\Delta^*$ is a partitioning of the literal occurrences
of $\Delta^*$ into axiom links, \ie, a set of disjoint axiom links on
$\Delta^*$ whose union contains every literal occurrence of $\Delta^*$.
A \defn{linking on $\Delta$} is a linking on a cut-additive resolution of $\Delta$.
We write $\resolution{\lambda}{\Delta}$ for the cut-additive resolution associated
with a linking $\lambda$.

Write $\cutseq{\Omega}{\Gamma}$ for the cut sequent obtained by taking
the disjoint union of a set $\Omega$ of cut occurrences and a MALL
sequent $\Gamma$.  A set of linkings on $\cutseq{\Omega}{\Gamma}$ is
\defn{sequentialisable} if it can be derived from the rules in
Figure~\ref{sequentialisable}, in which
$\psjudgement{\Omega}{\theta}{\Gamma}$ is the judgement ``$\theta$ is
a sequentialisable set of linkings on the cut sequent
$\cutseq{\Omega}{\Gamma}$''.  (We once again use the implicit tracking
of literal occurrences downwards through rules.)  The base case
$\axlabel$ is a single linking with a single axiom link and no cuts.
Figure~\ref{cut-multiple} shows two examples.
\begin{figure}
\begin{center}\label{cut-translation-eg}
\vspace{-.1ex}
\small\setlength{\unitlength}{.91pt}
\renewcommand{\plus}{\tightplus}
\newcommand{\localolink}[2]{\begin{picture}(0,7)\uln{#1}{-2}{2}\uln{#2}{-2}{2}\rln{#1}{#2}{2}\end{picture}}
\newcommand{\localulink}[2]{\begin{picture}(0,0)\uln{#1}{1}{5}\uln{#2}{1}{5}\rln{#1}{#2}{1}\end{picture}}
\newcommand{\overlinks}[2]{\begin{array}{c}\\[-3.6ex]#1\\[-.3ex]\raisebox{.3ex}{$#2$}\end{array}}
\newcommand{\underlinks}[2]{\begin{array}{c}\\[-2.5ex]#2\\[-1.1ex] #1\end{array}}
\renewcommand{\cut}{\mkern-3mu\ast\mkern-3mu}
\newcommand{\topchunk}{
\[
  \[ \justifies 
     \PPperpolink
     \using \axlabel~~~~~
 \]
 \[
   \justifies 
   \PPperpolink
     \using \axlabel~~~~~
 \]
 \justifies
   \links{P,\,P\perp\cut P,\,P\perp}{\olink{4}{18}\olink{36}{50}}
 \using \cutlabel~~~~~
\]
\[
 \[
    \justifies 
    \PPperpulink 
     \using \axlabel~~~~~
 \]
 \[
   \justifies 
   \PPperpulink
     \using \axlabel~~~~~
 \]
 \justifies
  \links{P,\,P\perp\cut P,\,P\perp}
  {\ulink{3}{16}\ulink{36}{50}} 
 \using \cutlabel
\]
}
\begin{math}
\begin{array}{ccc}
\prooftree
\thickness=0.08em
 \topchunk
 \justifies 
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp\with P\perp}
  {\olink{4}{18}\ulink{4}{52}\olink{39}{86}\ulink{72}{109}}
 \using \withlabel
\endprooftree
\\
\\[2ex]
\prooftree
\thickness=0.08em
\topchunk
\justifies 
  \links
  {P,\,P\perp\cut P,\,P\perp\with P\perp}
  {\olink{4}{16}\ulink{4}{16}\olink{37}{52}\ulink{37}{75}}
  \using \withlabel
\endprooftree
\end{array}
\end{math}
\vspace{-1ex}
\end{center}
\caption{Examples of the translation of a proof with cuts.\label{cut-multiple}}
\vspace{-4ex}\end{figure}
Each of the 
conclusions is a set of
two linkings, one drawn above
the cut sequent and one drawn below.
The only difference between the derivations is the final
$\withlabel$-rule.  The left application keeps the cuts in the
hypotheses separate (an instance of the $\withlabel$-rule taking
$\Sigma$ empty and $\Omega=\Omega'=P\perp\cut P$), whereas the right
application superimposes the two cuts ($\Sigma=P\perp\cut\,P$
and $\Omega$, $\Omega'$ empty).

Any derivation of a
set of linkings using the rules of
Figure~\ref{sequentialisable} projects in an obvious way to a MALL
proof, namely, by restricting to the underlying sequents (\viz, read
$\Gamma$ for $\psjudgement{\Omega}{\theta}{\Gamma}$).  For example,
the two derivations of Figure~\ref{cut-multiple} each yield the same
MALL proof of $P,P\perp\with P\perp$.

Write $\Pi\seqrel\theta$ if $\Pi$ is the MALL proof obtained from a
derivation of a
set of linkings $\theta$, and say that $\Pi$ is a
\defn{sequentialisation} of $\theta$.
If a MALL proof $\Pi'$ can be obtained from $\Pi$ by a series of rule
commutations in which no $\withlabel$-rules are moved upwards, then
$\Pi$ and $\Pi'$ are sequentialisations of the same
set of linkings.
In the cut-free case, $\seqrel$ is a function from proofs to
sets of linkings, exactly the translation defined in
Figure~\ref{cut-free-induction}.
In the presence of cuts, more than one
set of linkings may correspond
to the same proof.  For example, since the two derivations in
Figure~\ref{cut-multiple} have the same underlying MALL proof (say
$\Pi$), the concluding
sets of linkings
(say $\theta$ and $\theta'$) have a common sequentialisation:
$\Pi\seqrel\theta$, $\Pi\seqrel\theta'$, and
$\theta\neq\theta'$.

We can of course extend the cut-free translation of proofs by always
choosing $\Sigma$ to be empty in the $\withlabel$-rule (\ie, ``never
superimpose cuts'').  However, our notion of proof net defined below,
which characterises sequentialisability, does not characterise the image
of this translation, since there would exist sequentialisable
sets of linkings that are not proof translations, such as
\vspace{-1ex}
{\renewcommand{\cut}{\mkern-3mu\ast\mkern-3mu}
$$
\setlength{\unitlength}{.91pt}
\links {P\tightplus P,\,P\perp\cut
P,\,P\perp\with P\perp}
{\olink{22}{36}\ulink{4}{36}\olink{60}{73}\ulink{60}{99}}
$$
Moreover, under this convention two proofs that differ only in a
commutation of $\mathsf{cut}$ and $\withlabel$-rules would be translated
to different
sets of linkings.

Note that the alternative of taking $\Sigma$ maximal (\ie, ``superimpose
as many cuts as possible'') does not define a canonical function from
proofs to
sets of linkings, since there may be a choice of how to make
the identifications.  The following two $\withlabel$-rules
illustrate such a choice.
$$
\setlength{\unitlength}{1pt}
\prooftree
\thickness=0.08em
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp}
  {\olink{4}{16}\olink{37}{50}\olink{70}{83}}
 \hspace{6ex}
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp}
  {\ulink{4}{16}\ulink{37}{50}\ulink{70}{83}}
 \justifies 
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp\with P\perp}
  {\olink{4}{16}\ulink{4}{16}\olink{37}{50}\ulink{37}{50}\olink{70}{83}\ulink{70}{105}}
 \using \withlabel
\endprooftree
\vspace{.7ex}
$$ 
$$
\setlength{\unitlength}{1pt}
\prooftree
\thickness=0.08em
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp}
  {\olink{4}{16}\olink{37}{50}\olink{70}{83}}
 \hspace{6ex}
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp}
  {\ulink{4}{16}\ulink{37}{50}\ulink{70}{83}}
 \justifies 
 \links
  {P,\,P\perp\cut P,\,P\perp\cut P,\,P\perp\with P\perp}
  {\olink{4}{16}\ulink{4}{50}\olink{37}{50}\uulink{16}{70}\olink{70}{83}\uuulink{37}{105}}
 \using \withlabel
\endprooftree
\vspace{.8ex}
$$ 
}%
Girard was aware of this issue in the context of
monomial proof nets; see Appendix A.1.6 of \cite{Gir96}.

\paragraph{Geometric characterisation of sequentialisability.~~~~}
In the presence of cut, we update all the auxiliary definitions of
Section~\ref{cut-free} ($\with$-resolution, $\graph{\Lambda}$,
switching cycle, \etc{})
by substituting ``cut sequent'' for ``sequent'' and
``cut-additive resolution'' for ``additive resolution'' throughout.

\begin{figure*}
\begin{center}
\vspace{-2ex}
\setlength{\unitlength}{.93pt}
\footnotesize
\renewcommand{\tensor}{\!\otimes\!}
\renewcommand{\plus}{\!\oplus\!}
\newcommand{\concy}{0}\newcommand{\yy}{20}
\newcommand{\yyy}{40}\newcommand{\yyyy}{60}
\newcommand{\liney}{10}\newcommand{\lineyy}{30}\newcommand{\lineyyy}{50}
\newcommand{\concx}{0}
\newcommand{\rx}{170}\newcommand{\lx}{-\rx}
\newcommand{\rlx}{15}\newcommand{\rrx}{220}
\newcommand{\lrx}{-\rlx}\newcommand{\llx}{-\rrx}
\newcommand{\rrrx}{220}\newcommand{\rrlx}{133}
\newcommand{\rlrx}{104}\newcommand{\rllx}{15}
\newcommand{\lllx}{-\rrrx}\newcommand{\llrx}{-\rrlx}
\newcommand{\lrlx}{-\rlrx}\newcommand{\lrrx}{-\rllx}
\newcommand{\pfydots}{76}
\newcommand{\pfyidtw}{85}
\newcommand{\remp}{P,Q\with Q,(Q\perpp\tensor P\perpp)\tensor A}
\newcommand{\rempq}{P,Q,(Q\perpp\tensor P\perpp)\tensor A}
\newcommand{\rempqA}{P,Q,Q\perpp\tensor P\perpp}
\newcommand{\pfAdots}{\mbox{\scriptsize$\vdots$}~~}
\newcommand{\pftw}{\twist~~}
\newcommand{\pfid}{\identity~~}
\newcommand{\pfdots}{\hspace{2.6cm}\vdots}
\begin{picture}(0,90)(5,0)
\put(\concx,\concy)
{\makebox(0,0){$P\with P,Q\with Q,(Q\perpp\tensor P\perpp)\tensor A$}}
\rln{\lx}{\rx}{\liney}
\put(\lx,\yy){\makebox(0,0)[l]{$~~\remp$}}
\put(\rx,\yy){\makebox(0,0)[r]{$\remp~$}}
\rln{\llx}{\lrx}{\lineyy}
\rln{\rlx}{\rrx}{\lineyy}
\put(\llx,\yyy){\makebox(0,0)[l]{$~\rempq$}}
\put(\lrx,\yyy){\makebox(0,0)[r]{$\rempq$}}
\put(\rlx,\yyy){\makebox(0,0)[l]{$~\rempq$}}
\put(\rrx,\yyy){\makebox(0,0)[r]{$\rempq$}}
\rln{\lllx}{\llrx}{\lineyyy}
\rln{\lrlx}{\lrrx}{\lineyyy}
\put(\lllx,\yyyy){\makebox(0,0)[l]{$~\rempqA$}}
\put(\lrlx,\yyyy){\makebox(0,0)[l]{$~\rempqA$}}
\put(\llrx,\yyyy){\makebox(0,0)[r]{$A$}}
\put(\lrrx,\yyyy){\makebox(0,0)[r]{$A$}}
\rln{\rllx}{\rlrx}{\lineyyy}
\rln{\rrlx}{\rrrx}{\lineyyy}
\put(\rllx,\yyyy){\makebox(0,0)[l]{$~\rempqA$}}
\put(\rrlx,\yyyy){\makebox(0,0)[l]{$~\rempqA$}}
\put(\rlrx,\yyyy){\makebox(0,0)[r]{$A$}}
\put(\rrrx,\yyyy){\makebox(0,0)[r]{$A$}}
\put(\rrrx,\pfydots){\makebox(0,0)[c]{$\pfAdots$}}
\put(\rrrx,\pfyidtw){\makebox(0,0)[c]{$\pftw$}}
\put(\rlrx,\pfydots){\makebox(0,0)[c]{$\pfAdots$}}
\put(\rlrx,\pfyidtw){\makebox(0,0)[c]{$\pftw$}}
\put(\lrrx,\pfydots){\makebox(0,0)[c]{$\pfAdots$}}
\put(\lrrx,\pfyidtw){\makebox(0,0)[c]{$\pftw$}}
\put(\llrx,\pfydots){\makebox(0,0)[c]{$\pfAdots$}}
\put(\llrx,\pfyidtw){\makebox(0,0)[c]{$\pfid$}}
\put(\rx,\liney){\makebox(0,0)[l]{$~~p$}}
\put(\rrx,\lineyy){\makebox(0,0)[l]{$~~q$}}
\put(\lrx,\lineyy){\makebox(0,0)[l]{$~~q$}}
\put(\rrrx,\lineyyy){\makebox(0,0)[l]{$~~t$}}
\put(\rlrx,\lineyyy){\makebox(0,0)[l]{$~~t$}}
\put(\lrrx,\lineyyy){\makebox(0,0)[l]{$~~t$}}
\put(\llrx,\lineyyy){\makebox(0,0)[l]{$~~t$}}
\end{picture}
\vspace{-2ex}
\end{center}
\caption{The proof $\Pi_{tqp}$.\label{fig-proof} \rm (We omit the
unique cut-free proof of $P,Q,Q\perpp\tensor P\perpp$.)}
\vspace{-2ex}\end{figure*}

\begin{definition}\label{proofnet}
A
set $\theta$ of linkings
on a cut sequent $\Delta$ is a
\defn{proof net} if:
\begin{enumerate}
\item[\,\rm(P0)\!]
At least one literal occurrence of every cut is in $\theta$ (\ie, in
some axiom link of some linking of $\theta$).
\item[\,\rm(P1)\!]
For every $\with$-resolution $\withresolution{\Delta}$ of $\Delta$,
exactly one linking of $\theta$ is on $\withresolution{\Delta}$.
\item[\,\rm(P2)\!]
Every switching of every linking of $\theta$ is a tree (acyclic and
connected\,\footnote{By dropping connectedness, we obtain a proof net
for MALL augmented by the \textsc{mix} rule.\label{mixnote}}).
\item[\,\rm(P3)\!]
Every set $\Lambda$ of two or more linkings of $\theta$ toggles a
$\with$ that is not in any switching cycle of $\Lambda$.
\end{enumerate}
$\theta$ is a \defn{proof structure} if it satisfies (P0) and (P1).
\end{definition}
Note that (P1)--(P3) are inherited from the cut-free case.
\begin{theorem}[Sequentialisation]
A
set of linkings is sequentialisable iff it is a proof net.
\end{theorem}
The proof is essentially the same as the proof of Theorem~\ref{main};
the cut connective $\,\cut\:$ is akin to an outermost $\tensor$.

\paragraph{Cut elimination.}
\newcommand{\localcutseq}{\Delta}
\newcommand{\localcuts}{\Delta}
Let $\theta$ be a
set of linkings on the cut sequent $\localcutseq$, and let $A\cut A\perpp$
be a cut of $\localcuts$.  Define the \defn{elimination} of $A\cut A\perpp$
as follows.
\vspace{-.2ex}
\begin{itemize}
\item If $A$ is a literal, delete $A\cut A\perpp$ from $\Delta$, and
  replace any pair of axiom links $\{l,A\},\{A\perpp,l'\}$ in a
  linking of $\theta$ ($l$ and $l'$ being other occurrences of
  $A\perpp$ and $A$ respectively) with the axiom link $\{l,l'\}$.
\vspace{-1ex}
\item If $A=A_1\tensor A_2$ and $A\perp=A_1\perp\parr A_2\perp$ (or vice versa), 
  replace 
  $A\cut A\perp$ 
  with two cuts $A_1\cut A_1\perp$
  and $A_2\cut A_2\perp$.  Retain all the original linkings.
\vspace{-1ex}
\item If $A=A_1\with A_2$ and $A\perp=A_1\perp\plus A_2\perp$ (or vice versa)
  replace $A\cut A\perp$ with two cuts $A_1\cut A_1\perp$
  and $A_2\cut A_2\perp$.  Retain precisely the `consistent' linkings:
  delete any linkings $\lambda$ such that in
  $\resolution{\lambda}{\localcutseq}$ the (now unary) $\with$ and $\plus$
  take opposite arguments (\ie, such that the right argument of the
  $\with$ is in $\resolution{\lambda}{\localcutseq}$ and the left argument
  of the $\plus$ is in $\resolution{\lambda}{\localcutseq}$, or vice versa).
  Finally, `garbage collect' by deleting $A_i\cut A_i\perp$ if no
  literal occurrence of $A_i\cut A_i\perpp$ is in any of the
  remaining linkings.
\end{itemize}
\vspace{-.2ex}
An example of cut elimination was presented in the Introduction.
\begin{proposition}\label{preservation}
Eliminating a cut from a proof net yields a proof net.
\end{proposition}
Proposition~\ref{preservation} is proved in
Appendix~\ref{appendix-cut-elimination}.

\begin{theorem}  Cut elimination of proof nets is strongly normalising.
\end{theorem}

\begin{proof}
  Confluence is immediate from the definition; cut elimination reduces
  the size of the cut sequent, and is therefore strongly
  normalising.
\end{proof}

\paragraph{A category of proof nets.}
Our cut elimination allows us to define a category of MALL proof nets.
Objects are MALL formulas, and a morphism $A\to B$ is a cut-free proof
net on the sequent $A\perp,B$.  The composition of $\theta:A\to B$ and
$\theta':B\to C$ is the normal form of the proof net
$\{\lambda\cup\lambda'\,:\,\lambda\in\theta,\lambda'\in\theta'\}$
on $A\perp,B\cut B\perp,C$.
Composition is associative,
since cut elimination is strongly normalising.  The identity $A\to
A$ contains a linking $\lambda$ on $A\perp,A$ iff $\lambda$ matches
the $i\nth$ literal of $A\perp$ with the $i\nth$ literal of $A$.  This
category has the structure of a star-autonomous category minus the
units; $\with$ is product, and $\plus$ is coproduct.


\vspace{-0.5ex}
\section{Girard's monomial proof nets}\label{Girard}
\vspace{-0.5ex}
\noindent
In this section we relate our MALL proof nets to the monomial proof nets
of Girard \cite{Gir96}.

\subsection{Monomial proof nets are unsatisfactory}\label{monomials-problems}

\begin{figure*}
\begin{center}
\setlength{\unitlength}{3pt}
\footnotesize
\newcommand{\y}{2}
\newcommand{\yy}{4}
\newcommand{\yyy}{7}
\newcommand{\lity}{0}
\newcommand{\litupperargy}{-6}
\newcommand{\pary}{-8}
\newcommand{\litlowerargy}{-9}
\newcommand{\withy}{-11}
\newcommand{\parargy}{-13}
\newcommand{\plusy}{-14}
\newcommand{\withargy}{-20.5}
\newcommand{\plusargy}{-21}
\newcommand{\tensory}{-22}
\newcommand{\polarity}{-}
\newcommand{\revpolarity}{}
\newcommand{\qx}{\polarity60}
 \newcommand{\qargx}{\polarity56}
\newcommand{\outerparx}{\polarity55}
 \newcommand{\qperpargx}{\polarity54}
\newcommand{\qperpx}{\polarity50}
 \newcommand{\outerparargx}{\polarity47}
\newcommand{\plusx}{\polarity45}
 \newcommand{\innerparargx}{\polarity43}
\newcommand{\rx}{\polarity40}
 \newcommand{\rargx}{\polarity36}
\newcommand{\innerparx}{\polarity35}
 \newcommand{\rperpargx}{\polarity34}
\newcommand{\rperpx}{\polarity30}
 \newcommand{\plusargx}{\polarity27}
\newcommand{\tensorx}{\polarity25}
 \newcommand{\withargx}{\polarity23.5}
\newcommand{\outerpx}{\polarity20}
 \newcommand{\outerpargx}{\polarity16}
\newcommand{\withx}{\polarity15}
 \newcommand{\innerpargx}{\polarity14}
\newcommand{\innerpx}{\polarity10}
\newcommand{\pperpx}{0}
\newcommand{\innerpweightx}{}
\newcommand{\outerpweightx}{}
\newcommand{\botinnerpweightx}{\polarity5}
\newcommand{\botouterpweightx}{\polarity10}
\newcommand{\topinnerpweightx}{0}
\newcommand{\topouterpweightx}{\polarity5}
\newcommand{\subscript}{1}
\newcommand{\makeperp}[1]{~#1\perp}
\newcommand{\makeperpp}[1]{#1}
\newcommand{\makeneg}[1]{\overline{#1}}
\newcommand{\negone}[1]{\makeneg{#1}}
\newcommand{\negtwo}[1]{#1}
\newcommand{\qsymbol}{\makebox(0,0){$\makeperpp{~Q_{\subscript}}$}}
\newcommand{\outerparsymbol}{\makebox(0,0){$\makeperpp{\smallparr}$}}
\newcommand{\qperpsymbol}{\makebox(0,.5){$\makeperp{~Q_{\subscript}}$}}
\newcommand{\plussymbol}{\makebox(0,0){$\makeperpp{\tightplus}$}}
\newcommand{\rsymbol}{\makebox(0,0){$\makeperpp{~R_{\subscript}}$}}
\newcommand{\innerparsymbol}{\outerparsymbol}
\newcommand{\rperpsymbol}{\makebox(0,.5){$\makeperp{~R_{\subscript}}$}}
\newcommand{\tensorsymbol}{\makebox(0,0){$\makeperpp{\tighttensor}$}}
\newcommand{\outerpsymbol}{\makebox(0,0){$\makeperpp{~P_{\subscript}}$}}
\newcommand{\withsymbol}{\makebox(0,0){$\makeperpp{~~~\with_{p_{\subscript}}}$}}
\newcommand{\innerpsymbol}{\outerpsymbol}
\newcommand{\innerpweight}{\makebox(0,0)[t]{\raisebox{-1.7ex}{$~\negone{p}_{\subscript}$}}}
\newcommand{\outerpweight}{\makebox(0,0)[b]{\raisebox{1.1ex}{$\negtwo{p}_{\subscript}$}}}
\newcommand{\qweight}{}
\newcommand{\rweight}{}
\newcommand{\qweightlabel}{\makebox(0,0)[b]{\raisebox{1.1ex}{$\qweight$}}}
\newcommand{\rweightlabel}{\makebox(0,0)[b]{\raisebox{1.1ex}{$\rweight$}}}
\newcommand{\fourleaf}{%
    \put(\qx,\lity){\qsymbol}
    \put(\qargx,\litupperargy){\line(\polarity2,3){2.5}}
    \put(\outerparx,\pary){\outerparsymbol}
    \put(\qperpargx,\litupperargy){\line(\revpolarity2,3){2.5}}
    \put(\qperpx,\lity){\qperpsymbol}
    \put(\outerparargx,\parargy){\line(\polarity3,2){6}}
    \put(\plusx,\plusy){\plussymbol}
    \put(\innerparargx,\parargy){\line(\revpolarity3,2){6}}
    \put(\rx,\lity){\rsymbol}
    \put(\rargx,\litupperargy){\line(\polarity2,3){2.5}}
    \put(\innerparx,\pary){\innerparsymbol}
    \put(\rperpargx,\litupperargy){\line(\revpolarity2,3){2.5}}
    \put(\rperpx,\lity){\rperpsymbol}}
\newcommand{\branch}{\begin{picture}(0,0)
  \fourleaf
  \put(\plusargx,\plusargy){\line(\polarity5,2){16}}
 \put(\tensorx,\tensory){\tensorsymbol}
  \put(\withargx,\withargy){\line(\revpolarity1,1){7.5}}
   \put(\outerpx,\lity){\outerpsymbol}
   \put(\outerpargx,\litlowerargy){\line(\polarity1,2){3.2}}
  \put(\withx,\withy){\withsymbol}
   \put(\innerpargx,\litlowerargy){\line(\revpolarity1,2){3.2}}
   \put(\innerpx,\lity){\innerpsymbol}
 \rlink{\qx}{\qperpx}{\y}{\yy}
 \rlink{\rx}{\rperpx}{\y}{\yy}
 \rlink{\outerpx}{\pperpx}{\y}{\yyy}
 \rlink{\innerpx}{\pperpx}{\y}{\yy}
 \put(\outerpweightx,\yyy){\outerpweight}
 \put(\innerpweightx,\yy){\innerpweight}
 \put(\outerparx,\yy){\qweightlabel}
 \put(\innerparx,\yy){\rweightlabel}
	\end{picture}}
\newcommand{\settotop}{
 \renewcommand{\innerpweightx}{\topinnerpweightx}
 \renewcommand{\outerpweightx}{\topouterpweightx}
 \renewcommand{\pperpx}{\revpolarity10}
}
\newcommand{\settobot}{
 \renewcommand{\innerpweightx}{\botinnerpweightx}
 \renewcommand{\outerpweightx}{\botouterpweightx}
 \renewcommand{\pperpx}{0}
}
\begin{picture}(0,68)(0,-58)
 \settotop
 \renewcommand{\subscript}{1}
 \renewcommand{\qweight}{~\overline{p}_2\wedge p_3\wedge\overline{p}_4}
 \renewcommand{\rweight}{~~{p}_2\vee \overline{p}_3\vee p_4}
 \put(-15,0){\branch}
 \settobot
 \renewcommand{\subscript}{4}
 \renewcommand{\qweight}{~{p}_1\wedge p_2\wedge{p}_3}
 \renewcommand{\rweight}{~\overline{p}_1\vee \overline{p}_2\vee \overline{p}_3}
 \put(-15,-35){\branch}
   \put(5,\y){\line(0,-1){35}}
   \put(-5,\y){\line(0,-1){35}}
 \settotop
 \renewcommand{\polarity}{}
 \renewcommand{\revpolarity}{-}
 \renewcommand{\subscript}{2}
 \renewcommand{\qweight}{~{p}_1\wedge \overline{p}_3\wedge{p}_4}
 \renewcommand{\rweight}{~\overline{p}_1\vee {p}_3\vee \overline{p}_4}
 \renewcommand{\rlink}{\llink}
 \renewcommand{\negone}[1]{#1}
 \renewcommand{\negtwo}[1]{\makeneg{#1}}
 \put(15,0){\branch}
 \settobot
 \renewcommand{\subscript}{3}
 \renewcommand{\qweight}{~\overline{p}_1\wedge {p}_2\wedge{p}_4}
 \renewcommand{\rweight}{~{p}_1\vee \overline{p}_2\vee \overline{p}_4}
 \put(15,-35){\branch}
 \renewcommand{\plussymbol}{\makebox(0,0){$\tighttensor$}}
 \renewcommand{\outerparsymbol}{\plussymbol}
 \renewcommand{\innerparsymbol}{\plussymbol}
 \renewcommand{\qsymbol}{\makebox(0,.5){$~~P_3\perp$}}
 \renewcommand{\qperpsymbol}{\makebox(0,.5){$~~P_2\perp$}}
 \renewcommand{\rsymbol}{\makebox(0,.5){$~~P_1\perp$}}
 \renewcommand{\rperpsymbol}{\makebox(0,.5){$~~P_4\perp$}}
 \put(-45,-35){\begin{picture}(0,0) \fourleaf \end{picture}}
\end{picture}
\end{center}%
\vspace{-3ex}%
\caption{Girard's correctness criterion is insufficient without
monomials: this (abbreviated) non-monomial Girard proof net is
not sequentialisable.%
\label{counterexamplefig}}\vspace{-4ex}
\end{figure*}

\noindent
We give a detailed account of how monomial proof nets \cite{Gir96}
fail to provide abstract representations of cut-free MALL proofs
modulo inessential commutations of rules.  A single cut-free proof may
correspond to a host of monomial proof nets, and there is no natural
translation of cut-free MALL proofs into monomial proof nets.  (The
reader unfamiliar with monomial proof nets should be able to follow
the general shape of the argument.)

Consider the following pair of cut-free monomial proof nets:
\begin{center}
\setlength{\unitlength}{.96pt}
\footnotesize
\newcommand{\rowone}{0}
\newcommand{\rowonebez}{7}
\newcommand{\rowtwounderbez}{18}
\newcommand{\rowtwo}{25}
\newcommand{\rowtwooverbez}{32}
\newcommand{\rowthreeunderbez}{44}
\newcommand{\rowthree}{50}
\newcommand{\rowthreeoverbez}{58}
\newcommand{\rowlowerlink}{65}
\newcommand{\rowupperlink}{73}
\newcommand{\coll}{-50}
\newcommand{\collbezl}{-54}
\newcommand{\collbezr}{-46}
\newcommand{\colm}{0}
\newcommand{\colmbezl}{-4}
\newcommand{\colmbezr}{4}
\newcommand{\colr}{50}
\newcommand{\colrbezl}{46}
\newcommand{\colrbezr}{54}
\newcommand{\colll}{-62}
\newcommand{\collr}{-37}
\newcommand{\colml}{-12}
\newcommand{\colmr}{12}
\newcommand{\colrl}{37}
\newcommand{\colrr}{62}
\newcommand{\linkll}{-15}
\newcommand{\linklr}{-12}
\newcommand{\linkrl}{11}
\newcommand{\linkrr}{15}
\newcommand{\commonpart}{\begin{picture}(0,50)%
\put(\coll,\rowone){\makebox(0,0){$P\with P$}}%
\put(\colm,\rowone){\makebox(0,0){$~P\perpp\tensor Q\perpp$}}%
\put(\coll,\rowtwo){\makebox(0,0){$~~~\with_p$}}%
\put(\colm,\rowtwo){\makebox(0,0){$\tensor$}}%
\uln{\coll}{\rowonebez}{\rowtwounderbez}
\uln{\colm}{\rowonebez}{\rowtwounderbez}
\put(\colll,\rowthree){\makebox(0,0){$P$}}
\put(\collr,\rowthree){\makebox(0,0){$P$}}
\put(\colml,\rowthree){\makebox(0,2){$~~~P\perpp$}}
\put(\colmr,\rowthree){\makebox(0,2){$~~~Q\perpp$}}
\put(\colrl,\rowthree){\makebox(0,0){$\,Q$}}
\put(\colrr,\rowthree){\makebox(0,0){$\,Q$}}
\put(\collbezl,\rowtwooverbez){\line(-2,3){7}}
\put(\collbezr,\rowtwooverbez){\line(2,3){7}}
\put(\colmbezl,\rowtwooverbez){\line(-2,3){7}}
\put(\colmbezr,\rowtwooverbez){\line(2,3){7}}
\put(\colrbezl,\rowtwooverbez){\line(-2,3){7}}
\put(\colrbezr,\rowtwooverbez){\line(2,3){7}}
\uln{\colll}{\rowthreeoverbez}{\rowupperlink}
\uln{\collr}{\rowthreeoverbez}{\rowlowerlink}
\uln{\linkll}{\rowthreeoverbez}{\rowlowerlink}
\uln{\linklr}{\rowthreeoverbez}{\rowupperlink}
\uln{\colrl}{\rowthreeoverbez}{\rowlowerlink}
\uln{\colrr}{\rowthreeoverbez}{\rowupperlink}
\rln{\colll}{\linklr}{\rowupperlink}
\rln{\collr}{\linkll}{\rowlowerlink}
\put(\collr,\rowlowerlink){\makebox(-7,-4){$\overline p$}}
\end{picture}}%
\begin{picture}(0,185)(0,0)
\put(0,0){\begin{picture}(0,0)(0,-119)
 \put(0,0){\commonpart}
 \put(\colr,\rowone){\makebox(0,0){$Q\with Q$}}
 \uln{\colr}{\rowonebez}{\rowtwounderbez}
 \rln{\linkrr}{\colrl}{\rowlowerlink}
 \rln{\linkrl}{\colrr}{\rowupperlink}
 \uln{\linkrl}{\rowthreeoverbez}{\rowupperlink} 
 \uln{\linkrr}{\rowthreeoverbez}{\rowlowerlink} 
 \put(\colll,\rowupperlink){\makebox(-10,-4){${p}$}}
 \put(\colrl,\rowlowerlink){\makebox(14,-4){${q}$}}
 \put(\colrr,\rowupperlink){\makebox(14,-4){$\overline q$}}
 \put(\colr,\rowtwo){\makebox(0,0){$~~~\with_{q}$}}%
 \end{picture}
 \newcommand{\colqwq}{75}
 \newcommand{\farcol}{100}
 \newcommand{\farcoll}{87}
 \newcommand{\farcolr}{112}
 \newcommand{\farcolbezl}{96}
 \newcommand{\farcolbezr}{104}
 \newcommand{\toplinky}{95}
 \newcommand{\nextlinky}{84}
 \newcommand{\qperpll}{8}
 \newcommand{\qperplr}{11}
 \newcommand{\qperprl}{14}
 \newcommand{\qperprr}{17}
 \newcommand{\newaxl}{-65}
 \newcommand{\newaxr}{-9}
 \begin{picture}(0,0)(50,0)
 \put(0,0){\commonpart}
 \put(\colr,\rowtwo){\makebox(0,0){$~~~~\with_{q_1}$}}%
 \put(\colqwq,\rowone){\makebox(0,0){$~Q\with Q$}}
 \put(70,\rowonebez){\line(-4,3){14}}
 \put(80,\rowonebez){\line(4,3){14}}
 \put(\farcol,\rowtwo){\makebox(0,0){$~~~~\with_{q_2}$}}%
 \put(\farcoll,\rowthree){\makebox(0,0){$\,Q$}}
 \put(\farcolr,\rowthree){\makebox(0,0){$\,Q$}}
 \put(\farcolbezl,\rowtwooverbez){\line(-2,3){7}}
 \put(\farcolbezr,\rowtwooverbez){\line(2,3){7}}
 \uln{\qperpll}{\rowthreeoverbez}{\toplinky}
 \uln{\qperplr}{\rowthreeoverbez}{\nextlinky}
 \uln{\qperprl}{\rowthreeoverbez}{\rowupperlink}
 \uln{\qperprr}{\rowthreeoverbez}{\rowlowerlink}
 \uln{\farcoll}{\rowthreeoverbez}{\nextlinky}
 \uln{\farcolr}{\rowthreeoverbez}{\toplinky}
 \uln{\newaxl}{\rowthreeoverbez}{\nextlinky}
 \uln{\newaxr}{\rowthreeoverbez}{\nextlinky}
 \rln{\qperpll}{\farcolr}{\toplinky}
 \rln{\qperplr}{\farcoll}{\nextlinky}
 \rln{\qperprl}{\colrr}{\rowupperlink}
 \rln{\qperprr}{\colrl}{\rowlowerlink}
 \rln{\newaxl}{\newaxr}{\nextlinky}
 \put(\colll,\rowupperlink){\makebox(18,-12){${p}\overline q_1$}}
 \put(\colrl,\rowlowerlink){\makebox(18,-4){${p}{q}_1$}}
 \put(\colrr,\rowupperlink){\makebox(18,-4){${p}\overline q_1$}}
 \put(\farcoll,\nextlinky){\makebox(18,-4){$\overline p{q}_2$}}
 \put(\farcolr,\toplinky){\makebox(18,-4){$\overline p\,\overline q_2$}}
 \put(\newaxl,\nextlinky){\makebox(-16,-4){${p}{q}_1$}}
 \end{picture}
}
\end{picture}
\end{center}
(Eigenvariables associated with $\with$'s are shown as subscripts; we
omit implied weights.)  These two monomial proof nets correspond to
the same proof.  The second monomial proof net has two forms of
redundancy relative to the first: (i) the $\with$ with eigenweight $q$
has been replaced by two similar `copies', and (ii) the axiom link of
weight ${p}$ has been split into two.

Even if one attempts to fix a choice of representation (\textit{e.g.}\
favouring the first monomial proof net above over the second),
one still runs into difficulty.  As a concrete illustration, we
exhibit cut-free proofs $\Pi_\alpha$ and monomial proof nets
$\theta_\beta$ for which the binary relation of sequentialisation is
\begin{center}
\setlength{\unitlength}{.7pt}
\newcommand{\toprow}{10}\newcommand{\botrow}{-\toprow}
\newcounter{insertgap}\setcounter{insertgap}{6}
\newcounter{maingap}\setcounter{maingap}{18}
\newcounter{xx}\setcounter{xx}{0}
\newcounter{xxx}
\newcounter{longdiagx}
\newcommand{\yy}{20}
\begin{picture}(0,49)(100,-14)
\addtocounter{xx}{\theinsertgap}
\put(\thexx,\yy){\makebox(0,20){$\Pi_{ptq}$}}
\addtocounter{xx}{\theinsertgap}
\setcounter{xxx}{\thexx}
\addtocounter{xx}{\themaingap}
\setcounter{l}{\thexxx-\thexx}
\put(\thexx,0){\line(-1,1){\yy}}
\addtocounter{xx}{\theinsertgap}
\put(\thexx,0){\makebox(0,-20){$\,\theta_{\overline q,\overline p{q}}
$}}
\addtocounter{xx}{\theinsertgap}
\setcounter{xxx}{\thexx}
\addtocounter{xx}{\themaingap}
\setcounter{l}{\thexxx-\thexx}
\put(\thexxx,0){\line(1,1){\yy}}
\setcounter{longdiagx}{\thexxx+8}
\put(\thelongdiagx,0){\line(5,2){60}}
\addtocounter{xx}{\theinsertgap}
\put(\thexx,\yy){\makebox(0,20){$\,\Pi_{tpq}$}}
\addtocounter{xx}{\theinsertgap}
\setcounter{xxx}{\thexx}
\addtocounter{xx}{\themaingap}
\put(\thexx,0){\line(-1,1){\yy}}
\addtocounter{xx}{\theinsertgap}
\put(\thexx,0){\makebox(0,-20){$\,\theta_{\overline p\,\overline q,
  {p}\overline q,\overline p{q}}$}}
\addtocounter{xx}{\theinsertgap}
\setcounter{xxx}{\thexx}
\addtocounter{xx}{\themaingap}
\put(\thexxx,0){\line(1,1){\yy}}
\addtocounter{xx}{\theinsertgap}
\put(\thexx,\yy){\makebox(0,20){$\,\Pi_{tqp}$}}
\addtocounter{xx}{\theinsertgap}
\setcounter{xxx}{\thexx}
\addtocounter{xx}{\themaingap}
\put(\thexx,0){\line(-1,1){\yy}}
\setcounter{longdiagx}{\thexx-8}
\put(\thelongdiagx,0){\line(-5,2){60}}
\addtocounter{xx}{\theinsertgap}
\put(\thexx,0){\makebox(0,-20){$\,\theta_{\overline p,{p}\overline q}$}}
\addtocounter{xx}{\theinsertgap}
\setcounter{xxx}{\thexx}
\addtocounter{xx}{\themaingap}
\put(\thexxx,0){\line(1,1){\yy}}
\addtocounter{xx}{\theinsertgap}
\put(\thexx,\yy){\makebox(0,20){$\,\Pi_{qtp}$}}
\end{picture}
\end{center}
Define $\Pi_{tqp}$ to be the proof shown in Figure~\ref{fig-proof},
where $A=(R\,\parr\, R)\,\parr\,(R\perpp\tighttensor\, R\perpp)$, $\identity$ denotes
the identity proof and $\twist$ denotes the twist proof.  Let
$\Pi_{tpq}$ be the result of commuting rules $q$ and $p$ in
$\Pi_{tqp}$, let $\Pi_{qtp}$ be the result of commuting $t$ and $q$ in
the right half of $\Pi_{tqp}$, and let $\Pi_{ptq}$ be the result of
commuting $t$ and $p$ in the right half of $\Pi_{tpq}$.
Define the monomial proof nets $\theta_\beta$ as follows.  To specify
$\theta_\beta$ it suffices to present a configuration of weighted
axiom links.  On $P$ and $Q$ literals, fix the configuration as
below-left:
\begin{center}
\setlength{\unitlength}{1pt}
\footnotesize
\newcommand{\rowone}{0}
\newcommand{\rowonebez}{7}
\newcommand{\rowtwounderbez}{18}
\newcommand{\rowtwo}{25}
\newcommand{\rowtwooverbez}{32}
\newcommand{\rowthreeunderbez}{44}
\newcommand{\rowthree}{50}
\newcommand{\rowthreeoverbez}{58}
\newcommand{\rowlowerlink}{64}
\newcommand{\rowupperlink}{70}
 \newcommand{\nextlinky}{78}
 \newcommand{\toplinky}{84}
\newcommand{\coll}{-50}
\newcommand{\collbezl}{-54}
\newcommand{\collbezr}{-46}
\newcommand{\colm}{0}
\newcommand{\colmbezl}{-4}
\newcommand{\colmbezr}{4}
\newcommand{\colr}{50}
\newcommand{\colrbezl}{46}
\newcommand{\colrbezr}{54}
\newcommand{\colll}{-63}
\newcommand{\collr}{-38}
\newcommand{\colml}{-13}
\newcommand{\colmr}{13}
\newcommand{\colrl}{38}
\newcommand{\colrr}{63}
\newcommand{\linkll}{35}
\newcommand{\linklr}{40}
\newcommand{\linkrl}{60}
\newcommand{\linkrr}{65}
 \newcommand{\qperpll}{8}
 \newcommand{\qperplr}{11}
 \newcommand{\qperprl}{14}
 \newcommand{\qperprr}{17}
\begin{picture}(0,85)(0,0)
\put(-40,0){\begin{picture}(0,0)
 \put(\coll,\rowone){\makebox(0,0){$P\with\mkern2mu P$}}%
 \put(\colm,\rowone){\makebox(0,0){$Q\with\mkern2mu  Q$}}%
 \put(\colr,\rowone){\makebox(0,0){$~Q\perpp\mkern-2mu\tensor P\perpp$}}
 \put(\coll,\rowtwo){\makebox(0,0){$~~~\with_p$}}%
 \put(\colm,\rowtwo){\makebox(0,0){$~~~\with_q$}}%
 \put(\colr,\rowtwo){\makebox(0,0){$\tensor$}}%
 \uln{\coll}{\rowonebez}{\rowtwounderbez}
 \uln{\colm}{\rowonebez}{\rowtwounderbez}
 \uln{\colr}{\rowonebez}{\rowtwounderbez}
 \put(\colll,\rowthree){\makebox(0,0){$P$}}
 \put(\collr,\rowthree){\makebox(0,0){$P$}}
 \put(\colml,\rowthree){\makebox(0,0){$\,Q$}}
 \put(\colmr,\rowthree){\makebox(0,0){$\,Q$}}
 \put(\colrl,\rowthree){\makebox(0,2){$~~~Q\perpp$}}
 \put(\colrr,\rowthree){\makebox(0,2){$~~~P\perpp$}}
 \put(\collbezl,\rowtwooverbez){\line(-2,3){7}}
 \put(\collbezr,\rowtwooverbez){\line(2,3){7}}
 \put(\colmbezl,\rowtwooverbez){\line(-2,3){7}}
 \put(\colmbezr,\rowtwooverbez){\line(2,3){7}}
 \put(\colrbezl,\rowtwooverbez){\line(-2,3){7}}
 \put(\colrbezr,\rowtwooverbez){\line(2,3){7}}
 \uln{\colll}{\rowthreeoverbez}{\toplinky}
 \uln{\collr}{\rowthreeoverbez}{\nextlinky}
 \uln{\colml}{\rowthreeoverbez}{\rowupperlink}
 \uln{\colmr}{\rowthreeoverbez}{\rowlowerlink}
 \uln{\linkll}{\rowthreeoverbez}{\rowlowerlink}
 \uln{\linklr}{\rowthreeoverbez}{\rowupperlink}
 \uln{\linkrl}{\rowthreeoverbez}{\nextlinky}
 \uln{\linkrr}{\rowthreeoverbez}{\toplinky}
 \rln{\colll}{\linkrr}{\toplinky}
 \rln{\collr}{\linkrl}{\nextlinky}
 \rln{\colml}{\linklr}{\rowupperlink}
 \rln{\colmr}{\linkll}{\rowlowerlink}
 \put(\colll,\toplinky){\makebox(-11,-4){${p}$}}
 \put(\collr,\nextlinky){\makebox(-10,-4){$\overline p$}}
 \put(\colml,\rowupperlink){\makebox(-10,-4){${q}$}}
 \put(\colmr,\rowlowerlink){\makebox(-9,-4){$\overline q$}}
 \end{picture}
}
\end{picture}
\footnotesize
\newcommand{\xrr}{28}
\newcommand{\xr}{10}
\newcommand{\xll}{-\xrr}
\newcommand{\xl}{-\xr}
\newcommand{\yy}{9}
\newcommand{\yyy}{16}
\newcommand{\yyyy}{24}
\newcommand{\core}{%
 \begin{picture}(0,0)
  \put(\xll,0){\makebox(0,0)[b]{$R$}}
  \put(\xl,0){\makebox(0,0)[b]{$R$}}
  \put(\xr,0){\makebox(0,0)[b]{$~R\perpp$}}
  \put(\xrr,0){\makebox(0,0)[b]{~$R\perpp$}}
  \put(\xr,\yyy){\makebox(12,0)[c]{$w$}}
  \put(\xrr,\yyyy){\makebox(12,0)[c]{$w$}}
 \end{picture}
}
\begin{picture}(0,33)(-73,-10)
 \put(0,45){\begin{picture}(0,0)
  \put(0,0){\core} 
  \uln{\xll}{\yy}{\yyy} 
  \uln{\xl}{\yy}{\yyyy}
  \uln{\xr}{\yy}{\yyy} 
  \uln{\xrr}{\yy}{\yyyy}
  \rln{\xll}{\xr}{\yyy}
  \rln{\xl}{\xrr}{\yyyy}
  \put(-24,25){\makebox(0,0){$(\identity_w)$}} \end{picture} }
  \put(0,-14){\begin{picture}(0,0)%
  \put(0,0){\core}
  \uln{\xll}{\yy}{\yyyy} 
  \uln{\xl}{\yy}{\yyy} 
  \uln{\xr}{\yy}{\yyy}
  \uln{\xrr}{\yy}{\yyyy}
  \rln{\xll}{\xrr}{\yyyy}
  \rln{\xl}{\xr}{\yyy}
  \put(-24,35){\makebox(0,0){$(\twist_w)$}}
  \end{picture}
}
\end{picture}
\end{center}
We have taken as eigenweights the labels of the $\with$-rules of the
$\Pi_\alpha$.  The configuration of axiom links on $A$ will be a
disjoint union of axiom links in the identity and twist
configurations:
$\identity_w$ and $\twist_w$ (above-right) denote a pair of axiom
links of weight $w$ in the identity and twist configurations,
respectively.  We specify the $\theta_\beta$ by
the following disjoint unions of weighted identity and twist
configurations on $A$:
\begin{displaymath}
\begin{array}{r@{:\hspace{1.5ex}}l}
\theta_{\overline p,{p}\overline q} & 
 \identity_{{p}{q}}\sqcup \twist_{\overline
 p}\sqcup\twist_{{p}\overline q} 
\\
\theta_{\overline q,\overline p{q}} & 
 \identity_{{p}{q}}\sqcup \twist_{\overline q}\sqcup\twist_{\overline
 p{q}} 
\\
\theta_{\overline p\,\overline q,{p}\overline q,\overline p{q}} & 
 \identity_{{p}{q}}\sqcup \twist_{\overline p\,\overline
 q}\sqcup\twist_{{p}\overline q}\sqcup\twist_{\overline p{q}}
\end{array}
\end{displaymath}
(By redundancies of type (i) and (ii) illustrated earlier, there are
of course a host of other monomial proof nets $\theta_\beta$ which
are parodies of the three above.)  Since the $\Pi_\alpha$ are equivalent
modulo inessential rule commutations, any satisfactory theory of proof
nets should provide a canonical representation uniting all of them.
With monomial proof nets one would have to close under the
sequentialisation relation between proofs and monomial proof nets
depicted earlier, thereby creating a matching between the set of
proofs $\Pi_\alpha$ and the set of monomial proof nets $\theta_\beta$,
and then artificially choose a representative from amongst the
$\theta_\beta$.

By contrast, in our setting we associate the same proof net with each
$\Pi_\alpha$: the four-linking proof net on the second page of
the Introduction.  Thus we preserve the spirit of MLL proof nets by
providing an abstract representation of all of the $\Pi_\alpha$ in
one.

\subsection{\hspace{-5pt}Girard's criterion is insufficient without monomials\hspace{-5pt}}
\label{monomials}

A key stepping stone towards our formulation of a new definition of
proof net was to first settle the open problem of whether Girard's
proof net correctness criterion
\cite{Gir96} becomes insufficient upon relaxing the dependency condition,
which is the requirement that every weight be a monomial.
The answer is yes: in Figure~\ref{counterexamplefig} we present a
cut-free non-monomial Girard proof net $\theta$ which is not
sequentialisable.  By \defn{non-monomial Girard proof net} we mean a
proof net as in \cite{Gir96} but for the omission of the dependency
condition.
Strictly speaking $\theta$ is merely an abbreviation of a non-monomial Girard proof
net:
view each $p_i$ as an eigenvariable and split each $\plus$ into a
separate $\plus_1$ and $\plus_2$; formulas and remaining weights are
implied.

Figure~\ref{counterexamplefig} also encodes one of our proof
structures $\theta$, via the notion of weight described on the third
page of the Introduction.
It is not a proof net, since (P3) fails:
$\graph{\theta}$ contains a switching cycle passing through all four
$\with$'s
(follow the four jumps $\with_{p_i}$ to the axiom link
$\{R\perp_{i+1},R_{i+1}\}$ (mod $4$)).


\subsection{Mapping monomial proof structures to ours}\label{translating}

\noindent
Let a \defn{non-monomial Girard proof structure} be a proof structure
as in \cite{Gir96} but for the omission of the dependency condition.
Define a non-monomial Girard proof structure to be \defn{compact} if
(a) any non-literal formula occurrence is the conclusion of exactly
one link, except that a formula $A \plus B$ may be the conclusion of
both a $\plus_1$- and a $\plus_2$-link, and
(b) any two literal occurrences constitute the conclusions of at
most one axiom link.
Each non-monomial Girard proof structure, and thus also each monomial
one, can be collapsed into a compact non-monomial Girard proof
structure by identifying, along with their premises, links of the same
type with the same conclusion(s), and summing the weights of links and
formulas so identified.  This collapse does not preserve the
dependency condition.  Any compact non-monomial Girard
proof \false{structure} can be obtained as the
collapse of a (monomial) Girard proof \false{struc-}\hfill\\\false{ture}.%
\marginpar{\begin{picture}(0,0)\put(-20,-160){\rotatebox{90}{\color{correctioncol}%
\shortstack[l]{The shaded occurrences of \emph{structure} should read \emph{net}.  
Accordingly, \emph{surjective} has been\\ struck three sentences later. 
Thanks to Masahiro Hamano for this correction.}}}\end{picture}}

Compact non-monomial Girard proof structures are in bijection with our
proof structures.  
The counterpart of Girard's ``technical condition'' is implied by (P1)
and our definition of a set of linkings in terms of additive
resolutions.  The \begin{picture}(0,0)\put(-1.2,2.5){\line(1,0){41}}\end{picture}surjective map from (monomial) Girard proof structures
to our proof structures obtained by composing the collapse and the
bijection preserves the property of being a sequentialisation of a
particular MALL proof.

Given a set of linkings $\theta$ on a sequent $\Gamma$ and a subset
$\Lambda \subseteq \theta$, let ${\cal G}_\Lambda^\theta$ be defined
as $\graph{\Lambda}$, but with jump edges between every $\with$-vertex
$w \in \graph{\Lambda}$ and every axiom link $a \in \graph{\Lambda}$
depending on $w$ \emph{within} $\theta$.  Note that $\graph{\Lambda} =
{\cal G}_\Lambda^\Lambda$. Define the variant (P2$^*$) of (P2) by
using ${\cal G}_{\{\lambda\}}^\theta$ in place of $\graph{\lambda}$ in
the definition of a switching of $\lambda$, also deleting all but one
switch edge of each $\with$.
(P2$^*$) clearly implies (P2), since it involves more switchings.  In
fact, (P2$^*$) is strictly stronger than (P2): for $\theta =
\{\lambda_1,\lambda_2\}$ of Example~\ref{non-net-example}, the graph
${\cal G}_{\lambda_1}^\theta$ has a switching cycle (the one presented
below Figure~\ref{jumpfig}),
whereas $\graph{\lambda_1}$ does
not.  However, it is not hard to check that (P2$^*$) is implied by
(P2) and (P3) together.  

The bijection between compact non-monomial Girard proof structures and
our proof structures can now be further refined: compact non-monomial
Girard proof nets are in bijection with sets of linkings in our sense
which satisfy (P1) and (P2$^*$).  


\section{Work in progress}\vspace{-1ex}
\noindent
The equivalence relation on cut-free MLL proofs induced by their
translation into cut-free MLL proof nets is canonical in sense that
the equivalence corresponds to coherence in a star-autonomous category
\cite{BCST96}.  We conjecture that the equivalence on cut-free
MALL proofs induced by our translation into proof nets corresponds
to coherence in a star-autonomous category with products (hence sums).

We are seeking a reformulation of cut that preserves the elegance of
the cut-free definition, in the sense of retaining a natural
translation from proofs to proof nets.

We are investigating whether the following variant of (P3) yields an
alternative definition of proof net:
for any switching cycle $S$ of a set of linkings $\Lambda$, at least
one $\with$ toggled in $\Lambda$ is not in $S$.  


\vspace{-2ex}
\paragraph{Acknowledgements.} Vaughan Pratt, for invaluable feedback during the
development of this work.  Paul-Andr\'e Melli\`es, for suggesting to
the first author that the search for a satisfactory notion of MALL
proof net was an interesting and potentially fruitful research topic.

\small
\bibliographystyle{alpha}
\begin{thebibliography}{DHPP99}
\vspace{-1ex}

\bibitem[AJ94]{AJ94b}
{\sc S.~Abramsky \& R.~Jagadeesan} (1994):
\newblock {\em Games and full completeness for multiplicative linear logic.}
\newblock {\sl Journal of Symbolic Logic} 59(2), pp. 543--574.

\bibitem[AM99]{AbrMel}
{\sc S.~Abramsky \& P.-A.~Melli\`es} (1999):
\newblock {\em Concurrent games and full completenes.}
\newblock In {\sl Proc. LICS'99}, IEEE, pp. 431--442.

\bibitem[BCST96]{BCST96}
{\sc R.~F.~Blute, J.~R.~B.~Cockett, R.~A.~G.~Seely \& T.~H.~Trimble} (1996):
\newblock {\em Natural deduction and coherence for weakly distributive categories.}
\newblock {\sl Journal of Pure and Applied Algebra} 113, pp. 229--296.

\bibitem[BS96]{BS96a}
{\sc R.~F.~Blute \& P.~J.~Scott} (1996):
\newblock {\em Linear {L\"a}uchli semantics.}
\newblock {\sl Annnals of Pure \& Applied Logic} 77, pp. 101--142.

\bibitem[DHPP99]{DHPP99}
{\sc H.~Devarajan, D.~Hughes, G.~Plotkin \& V.~R.~Pratt} (1999):
\newblock {\em Full completeness of the multiplicative linear logic of chu spaces.}
\newblock In {\sl Proc. LICS'99}, IEEE, pp. 234--245.

\bibitem[DR89]{DR}
{\sc V.~Danos \& L.~Regnier} (1989):
\newblock {\em The structure of multiplicatives.}
\newblock {\sl Arch.~Math.~Logic} 28, pp.~181--203.

\bibitem[Gir87]{Gir87}
{\sc J.-Y.~Girard} (1987):
\newblock {\em Linear logic.}
\newblock {\sl Theoretical Computer Science} 50, pp. 1--102.

\bibitem[Gir96]{Gir96}
{\sc J.-Y.~Girard} (1996):
\newblock {\em Proof-nets: the parallel syntax for proof theory.}
\newblock {\sl Logic and Algebra}. Marcel~Dekker.

\bibitem[HO93]{HO93}
{\sc J. M. E.~Hyland \& C.-H. L.~Ong} (1993):
\newblock {\em Fair games and full completeness for multiplicative linear logic without the \textsc{mix}-Rule.}
\newblock On Ong's web page.

\bibitem[Loa94]{Loa94}
{\sc R.~Loader} (1994):
\newblock {\em Linear logic, totality and full completeness.}
\newblock In {\sl Proc. LICS'94}, IEEE, pp. 292--298.

\bibitem[Tan97]{Aud97}
{\sc A.~Tan} (1997):
\newblock {\em Full completeness for models of linear logic}.
\newblock PhD thesis, University of Cambridge.

\end{thebibliography}


\clearpage
\normalsize
\appendix
\section{Appendix: Separation}\label{appendix-proof}

\noindent
Throughout this appendix $\theta$ is 
a proof net on a cut sequent $\Gamma$.%
\footnote{Readers concerned only
with the cut-free case may ignore the full generality of this
reference to cut, and assume that $\theta$ is a cut-free proof net on
a MALL sequent $\Gamma$.}
For vertices $x$ and $y$ of the graph $\fullgraph$,
write $x\edge y$ iff $x$ is an argument of $y$, or $x$ is an axiom
link and $y$ is either a $\with$ on which $x$ depends in $\theta$ or
one of the two literals linked by $x$, thus directing the edges of
$\fullgraph$ downwards.  Property (P2) implies $\graph{\theta}$ is
connected.

A subset $\Lambda \subseteq \theta$ is \defn{saturated} if any
strictly larger subset of $\theta$ toggles more $\with$'s than $\Lambda$.
Clearly $\theta$ itself is saturated.
For $\Lambda$ a set of linkings and $w$ a $\with$
of $\Gamma$ let $\Lambda^{\!w}$ denote the set of all linkings in
$\Lambda$ whose additive resolution does not contain the right argument of $w$.
Write $\lambda \stackrel{w}{=} \lambda'$ if linkings
$\lambda,\lambda'\in \theta$ are either equal or $w$ is the only
$\with$ toggled between \mbox{$\resolution{\lambda}{\Gamma}$} and
$\resolution{\lambda'}{\Gamma}$. It is straightforward to check that:
\begin{itemize}\label{segment-properties}
\item[\,(S1)\!] If $\Lambda$ is saturated and toggles 
$w$ then also $\Lambda^{\!w}$ is saturated.
\item[\,(S2)\!] If $\Lambda$ is saturated and toggles $w$ and $\lambda \in
      \Lambda$ then 
      $\lambda \stackrel{w}{=} \lambda_w$ for some $\lambda_w \in
      \Lambda^{\!w}$.
\item[\,(S3)\!] If $\Lambda$ is saturated and toggles $w$ and $\lambda
      \stackrel{x}{=} \lambda'$ for $\lambda, \lambda' \in \Lambda$
      then
     $\lambda \stackrel{w}{=} \lambda_w
      \stackrel{x}{=} \lambda'_w \stackrel{w}{=} \lambda'$
      for some $\lambda_w, \lambda'_w \in
      \Lambda^{\!w}$.
\end{itemize}
\begin{lemma}\label{edge-dep}
  Let $w$ be a $\with$ toggled by a saturated set $\Lambda \subseteq \theta$, and
  let $e$ be an edge in $\graph{\Lambda}$ originating from an axiom
  link $a$, such that $e \not\in \graph{\Lambda^{\!w}}$.
  Then the jump $a\jump w$ is in $\graph{\Lambda}$.
\end{lemma}
\begin{proof}
Let $e$ be $a \edge x$.  If $e$ is not a jump, $e \not\in
\graph{\Lambda^{\!w}}$ implies $a \not\in \graph{\Lambda^{\!w}}$.
Choose $\lambda \in \Lambda$ with $a \in \lambda$.
By (S2) $\lambda \stackrel{w}{=} \lambda_w$ for some $\lambda_w \in
\Lambda^{\!w}$.  Since $a \not\in \lambda_w$ (for $a\not\in
\graph{\Lambda^{\!w}}$), the jump $a\jump w$ is in $\graph{\Lambda}$.

If $e$ is a jump, we have $\lambda, \lambda' \in \Lambda$ with $a
\in \lambda$, $a \not\in \lambda'$ and $\lambda
\stackrel{x}{=} \lambda'$.
By (S3) 
$\lambda
\stackrel{w}{=} \lambda_w \stackrel{x}{=} \lambda'_w \stackrel{w}{=} \lambda'$
for $\lambda_w, \lambda'_w \in \Lambda^{\!w}$.  Either $a \not\in
\lambda_w$ or $a \in \lambda'_w$, else $e \in
\graph{\Lambda^{\!w}}$; either way, the jump $a\jump w$ is in
$\graph{\Lambda}$.
\end{proof}
\begin{lemma}\label{jump-into-L}
  Every non-empty union $S$ of switching cycles in $\fullgraph$ has a
  jump out of it, \ie, for some axiom link $a\!\in\! S$ and
  $\with$-vertex $w\!\not\in\! S$, there is a jump $a\!\jump\!w$ in
  $\fullgraph$.
\end{lemma}
\begin{proof}
  Let $\Lambda$ be a minimal saturated subset of $\theta$ with
  $\graph{\Lambda}$ containing $S$. Switchings of singleton subsets
  of $\theta$ are cycle-free by (P2), so $\Lambda$ contains at least
  two linkings. Let $w$ be a $\with$ toggled by $\Lambda$ that is not
  in any switching cycle of $\Lambda$ (existing by (P3)), so $w
  \not\in S$.  Since $\Lambda$ is minimal,
  $S\not\subseteq\graph{\Lambda^{\!w}}$ (using (S1)), so some edge $e$ of $S$ is in
  $\graph\Lambda$ but not in $\graph{\Lambda^{\!w}}$.
  Without loss of generality $e$ is an edge from an axiom link $a$,
  because for any other edge $y \edge x$ in $S$ we have $a \edge
  z_1\to\ldots\to z_n=y\to x$ in $S$ for some axiom link $a$, and
  $y\edge x$ is in $\graph{\Lambda^{\!w}}$ whenever $a\edge z_1$ is in
  $\graph{\Lambda^{\!w}}$.
  By Lemma~\ref{edge-dep} the jump $a\jump w$ is in
  $\graph\Lambda$, hence also in $\fullgraph$.
\end{proof}%
\nopagebreak%
Henceforth ``$\parr$/$\with$'' abbreviates ``$\parr$ or $\with$''.  A
\defn{path} from $x_0$ to $x_n$ in $\graph\theta$ is a sequence of
distinct vertices $x_0x_1\ldots x_n$ such that for each $i$ either
$x_i\edge x_{i+1}$ or $x_{i}\edgefrom x_{i+1}$ (note that we do not
allow cycles).  A \defn{switching path} is
a path in $\graph\theta$ 
that does not traverse two switch edges of any $\parr$ or $\with$ in
succession. 
A switching path $x_0\ldots x_n$ is
\defn{strong} if it does not end by entering a $\parr$/$\with$ along
one of its switch edges (\ie, $x_{n-1}\edge x_n$ only if $x_n$ is not
a $\parr$/$\with$).  
Suppose paths $\pi=x_0\ldots x_n$ and $\pi'=y_0\ldots y_m$ are
disjoint but for $x_n=y_0$.  If $\pi$ and $\pi'$ are switching paths,
then their composite $\pi;\pi'=x_0\ldots x_ny_1\ldots y_m$ is not
necessarily a switching path (namely if $x_n=y_0$ is a $\with/\parr$
and\linebreak $x_{n-1}\edge x_n=y_0\edgefrom y_1$), whereas if $\pi$ and $\pi'$
are strong switching paths then $\pi;\pi'$ is also a strong switching
path.

Write $x\strongpathin{G}y$ if the subgraph $G$ of $\fullgraph$
contains a strong switching path from $x$ to $y$.  An \defn{$x$-zone}
$X$ is a subgraph of $\fullgraph$ such that for all $x'\in X$, there
exists $y$ such that $x\edgefrom y\strongpathin{X}x'$.\footnote{The
  union of all $x$-zones is itself an $x$-zone, which could be called
  the \defn{realm} of $x$, a concept reminiscent of the notion of
  \defn{empire} of \cite{Gir96}, but different in an essential way.}
Given a $\parr$/$\with$-vertex $x$ and a vertex $y$, define $x$
\defn{dominates} $y$, denoted $x\dominates y$, if $y$ is in an
$x$-zone.
If $x$ is not dominated, it is \defn{free}.
\begin{lemma}\label{dominance-trans}
Domination $\dominates$ is transitive.
\end{lemma}
\begin{proof}
We show that if $X$ is an $x$-zone, $y\in X$ and $Y$ is a $y$-zone,
then $X\cup Y$ is an $x$-zone.
Take $z\in Y\setminus X$.  We have $x\edgefrom
x'\strongpathin{X}y\edgefrom y'\strongpathin{Y}z$ for some $x'\in X$
and $y'\in Y$.  If the strong switching path $y'\strongpathin{Y}z$
does not intersect $X$, then $x'\strongpathin{X}y\edgefrom
y'\strongpathin{Y}z$ constitutes a strong switching path, so we are done.
Otherwise let $y''$ be the last vertex along $y'\strongpathin{Y}z$
that is in $X$.  Since $y''\in X$ we have $x\edgefrom
x''\strongpathin{X}y''$, and the sub-path of $y'\strongpathin{Y}z$
from $y''$ to $z$ is a strong switching path $y''\strongpathin{Y}z$; the
composition of these paths yields $x\edgefrom x''\strongpathin{X\cup
  Y}z$, since the only common vertex is $y''$.
\end{proof}
\begin{lemma}\label{w-jump-switching-cycle}
  Let $C$ be a switching cycle in $\fullgraph$ containing an axiom
  link with a jump to a $\with$-vertex $w\not\in C$.  Then $w$
  dominates every vertex of $C$.
\end{lemma}
\begin{proof}
$C$ is a $w$-zone.
\end{proof}
\begin{lemma}\label{w-dom-v}
  If $x$ is in a switching cycle in $\fullgraph$ then $w\dominates x$
  for some $\with$-vertex $w$ in no switching cycle in $\fullgraph$.
\end{lemma}
\begin{proof}
Apply Lemma~\ref{jump-into-L} repeatedly, growing a collection of
switching cycles one cycle at a time, until jumping to a
$\with$-vertex $w$ that is not in a switching cycle.  This must happen
eventually, since (P3) implies $\fullgraph$ contains a $\with$ that is
not in any switching cycle.
The result follows by Lemma~\ref{w-jump-switching-cycle}
and the transitivity of $\dominates$.
\end{proof}
\begin{lemma}\label{dominance-switching-cycle}
If $x\dominates x$ then $x$ is in a switching cycle in $\fullgraph$.
\end{lemma}
\begin{proof}
If $x\dominates x$ then $x\edgefrom y\strongpathin{X} x$ for some $x$-zone
$X$, hence $x$ is in a switching cycle in $\fullgraph$.
\end{proof}
\begin{lemma}\label{free}
  Every $\parr$/$\with$ of $\fullgraph$ is either free or is dominated by
  a free $\parr$/$\with$.
\end{lemma}
\begin{proof}
  If $x_0$ is neither free nor dominated by a free $\parr$/$\with$-vertex, then we can
  build an infinite chain $x_0\dominated x_1\dominated\ldots$ of
  distinct vertices with the same property.  If $x_i$ is in a
  switching cycle then take $x_{i+1}$ to be the vertex given by
  Lemma~\ref{w-dom-v}, which is not in a switching cycle; $x_{i+1}$ is
  fresh otherwise $x_{i+1}\dominated x_{i+1}$ whence $x_{i+1}$ is in a
  switching cycle (contradiction).  If $x_i$ is in no switching cycle
  then $x_{i+1}$ exists since $x_i$ is not free; $x_{i+1}$ is fresh
  otherwise $x_i\dominated x_i$, whence $x_i$ is in a switching cycle
  (contradiction).
\end{proof}
\begin{corollary}\label{exists-free}
  If $\fullgraph$ has a $\parr$/$\with$ then it has a free $\parr$/$\with$.
\end{corollary}
\begin{lemma}\label{path}
  If $x \dominates y_0$ and there is a path $y_0y_1\ldots y_n$ in
  $\fullgraph$ which never enters a $\parr$/$\with$ from above
  (\ie, $y_{i-1} \edge y_i$ only if $y_i$ is not a $\parr$/$\with$),
  then $x \dominates y_n$.
\end{lemma}
\begin{proof}
  Let $X$ be an $x$-zone containing $y_0$, and let $y_i$ be the last
  vertex on $y_0y_1\ldots y_n$ that is in $X$.  Then $x\!\edgefrom\!
  z\!\strongpathin{X}\!y_i$ for some $z$. Now $Y\!=\!X\!\cup\!
  \{y_i,...,y_n\}$ is an $x$-zone, since $x\!\edgefrom\!
  z\!\strongpathin{Y}\!y_i\!\strongpathin{Y}\!y_j$ for $j\!=\!i,...,n$.
\end{proof}
Distinct $\parr$/$\with$-vertices $x$ and $y$ or $\fullgraph$ are
\defn{back-to-back}, denoted $x\backback y$, if there is a switching
path $xz_0\ldots z_ny$ in $\fullgraph$ such that $x\edgefrom z_0$ and
$z_n\edge y$,
and are \defn{face-to-face}, denoted $x\faceface y$, if there exists a
path $xz_0\ldots z_ny$ in $\fullgraph$ such that $x\edge z_0$ and
$z_n\edgefrom y$, and none of the $z_i$ are $\parr$/$\with$-vertices
(so in particular $xz_0\ldots z_ny$ is a strong switching path).

\begin{lemma}\label{realm-intersect}
If $x \dominates z$ and $y \dominates z$ for distinct free
$\parr$/$\with$-vertices $x$ and $y$, then $x \backback y$.
\end{lemma}
\begin{proof}
  Let $X$ be an $x$-zone containing $z$, so that for some $x'$ we have
  $x\edgefrom x'$ and a strong switching path $\pi=x'\ldots z$ in $X$.
  Let $z'$ be the first vertex of $x\pi$ with $y \dominates z'$.  By
  Lemma~\ref{path} the predecessor $z''$ of $z'$ in $x\pi$ is a
  $\parr$/$\with$ and $z''\edgefrom z'$, so the prefix $\pi'$ of $\pi$
  up to $z'$ is strong.  Since $y\dominates z'$ there is a strong
  switching path $\pi''=y_1\ldots y_nz'$ in a $y$-zone, with
  $y\edgefrom y_1$.  The concatenation $x\pi' y_n\ldots y_1y$ is a
  switching path (since none of the $y_i$ is in $\pi'$) witnessing
  $x\backback y$.
\end{proof}
A $\parr/\with$-vertex $x$ of $\fullgraph$ \defn{separates} if it is not
an argument (\ie, is an outermost connective), or it is the argument
of $y$ and deleting the edge between $x$ and $y$ disconnects $\graph{\theta}$.
\begin{lemma}\label{back-face}
If a $\parr$/$\with$-vertex $x$ is free and does not separate, then
$x\faceface y$ and $x\backback z$ for free $y$ and $z$.
\end{lemma}
\begin{proof}
Since $x$ does not separate, it is in a cycle $C$ (say clockwise)
whose first (resp.\ last) edge is oriented out of (resp.\ into) $x$.
Take $y$ to be the first $\parr$/$\with$ reached clockwise along
$C$ from $x$.  Then $x\faceface y$ (otherwise $y\dominates x$ by Lemma~\ref{path}) and
$y$ is free since $y'\dominates y$ implies $y'\dominates x$ by
Lemma~\ref{path}, contradicting the freedom of $x$.

Let $z$ be the first vertex reached anti-clockwise from $x$ that is not
dominated by $x$, and let $z'$ be its predecessor.  By
Lemma~\ref{path}, $z$ is a $\parr$/$\with$, and $x \dominates z' \edge
z$, therefore $x\backback z$.  If $z$ is not free, replace it by a free
$\parr$/$\with$ dominating $z$ (hence also $z'$) provided by
Lemma~\ref{free}, and appeal to Lemma~\ref{realm-intersect}.
\end{proof}
\begin{lemma}\label{one-spike}
  Let $x$ be a $\parr$/$\with$ and let $z_0\ldots z_n$ be a switching
  path in $\fullgraph$ such that $z_0\edge x$ and $z_n\edge x$.  Then $x$
  dominates every vertex of $\{z_0,\ldots,z_n\}$.
\end{lemma}
\begin{proof}
$\{z_0,\ldots,z_n\}$ is a $x$-zone.
\end{proof}
\begin{trivlist}\item {\sc Separation Lemma\;}
  If $\fullgraph$ has a $\parr$/$\with$-vertex then it has a
  $\parr$/$\with$-vertex that separates.
\end{trivlist}
\begin{proof}
  Had $\fullgraph$ no separating $\parr$/$\with$-vertex then
  $x_0\faceface x_1\backback x_2\faceface x_3\backback \ldots$ for
  free $\parr$/$\with$-vertices $x_i$ with $x_{i+1} \neq x_i$ by
  Lemma~\ref{back-face} ($x_0$ exists by Corollary~\ref{exists-free}).
  The composition $\pi$ of the paths witnessing the $\faceface$ and
  $\backback$ relations eventually intersects itself at a vertex $x$,
  yielding a path $\pi'=xz_0\ldots z_n$ such that
  $\{x,z_0,\ldots,z_n\}$ is a cycle.  Since each witness is a
  switching path, $\pi'$ is a switching path (by design, composition at
  each $x_i$ avoids introducing consecutive switch edges of $x_i$).
  Furthermore, one of the $x_i$ must be among the $z_j$.  
  Using Lemma~\ref{w-dom-v} if $\{x,z_0,\ldots,z_n\}$
  is a switching cycle, and Lemma~\ref{one-spike} otherwise, this
  $x_i$ is dominated, a contradiction (since $x_i$ is free).
\end{proof}

\section{Appendix: Proof that every cut-free proof net is the
translation of a cut-free proof}\label{appendix-induction}

\noindent
With the Separation Lemma in hand, the proof that every cut-free
proof net is the translation of a cut-free proof reduces to simple
induction.

Let $\theta$ be a proof net on $\Gamma$.
We proceed by induction on the sum the number of $\parr$'s and
$\with$'s of $\fullgraph$.

\paragraph*{Base case (primary induction)} 
$\Gamma$ is $\parr$/$\with$-free, hence $\theta$ comprises a single
linking $\lambda$ on $\Gamma$.  We proceed by induction on the
number of connectives of $\Gamma$. 
\begin{itemize}
  
\item \emph{Base case (secondary induction).}  $\Gamma$ contains no
  connectives, so $\Gamma=P_1,P_1\perpp,\ldots, P_n,P_n\perpp$ for
  $n\geq 0$ and propositional variables $P_1,\ldots,P_n$, and
  $\lambda$ links the complementary literal occurrences $P_i$ and
  $P_i\perpp$ for $i=1,...,n$. By (P2) $n=1$.  The axiom rule with
  conclusion $P_1,P_1\perpp$ is a sequentialisation of $\theta$.
  
\item \emph{Induction step (secondary induction).} Being void of
  $\parr$'s, $\graph{\lambda}$ is the unique switching
  of $\lambda$, so by (P2) $\graph{\lambda}$ is a tree.

\newenvironment{itemise2}{\begin{list}{{\bf --}}{\leftmargin 15pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        }}{\end{list}}
\begin{itemise2}
  
\item Suppose $\Gamma=\Delta,A\plus B$, with $\oplus$-vertex
  $x\in\graph{\lambda}$ corresponding to $A\plus B$. Since
  $\resolution{\lambda}{\Gamma}$ is an additive resolution, $x$ is
  unary in $\graph{\lambda}$, \ie, there is a unique $y \in
  \graph{\lambda}$ with $y\edge x$. If this $y$ is the left (resp.\
  right) argument of $x$, consider the left (resp.\ right)
  $\oplus$-rule $\rho$ with conclusion $\Delta,A\plus B$ and
  hypothesis $\Gamma'=\Delta,A$ (resp.\ $\Delta,B$). The linking
  $\lambda$ on $\Gamma$ also constitutes a linking $\lambda'$ on
  $\Gamma'$, since no literals of the deleted $\oplus$-argument were
  incident with an axiom link of $\lambda$. The graph
  $\graph{\lambda'}$ is a tree, because $\graph{\lambda}$ is a
  tree. Hence $\theta'=\{\lambda'\}$ is a proof net on $\Gamma'$.  By
  induction, $\theta'$ is the translation of a cut-free MALL proof of
  $\Gamma'$, which when followed by $\rho$ constitutes a cut-free MALL
  proof of $\Gamma$ whose translation is $\theta$.
  
\item
Suppose $\Gamma=\Delta,A_0\tensor A_1$, with $\tensor$-vertex
$x\in\graph{\lambda}$ corresponding to $A_0\tensor A_1$.  Deleting
$x$ separates the tree $\graph{\lambda}$ into a left tree $T_0$ and
right tree $T_1$ whose respective conclusions define sequents
$\Delta_0$ and $\Delta_1$, a partitioning of $\Delta$.  Consider the
$\tensor$-rule $\rho$ with conclusion $\Gamma$ and hypotheses
$\Delta_0,A_0$ and $\Delta_1,A_1$.  Since $\graph{\lambda}$ is a
tree, no axiom link of $\lambda$ goes between $\Delta_0,A_0$ and
$\Delta_1,A_1$, hence $\lambda$ partitions to form linkings $\lambda_0$
and $\lambda_1$, respectively, on $\Delta_0,A_0$ and $\Delta_1,A_1$.
Each $\theta_i = \{\lambda_i\}$ is a proof net on $\Delta_i,A_i$ since
each $\graph{\lambda_i} = T_i$ is a tree.  Appeal to the induction
hypothesis with $\theta_0$ and $\theta_1$, in the manner of the
$\oplus$ case above.

\end{itemise2}
\end{itemize}

\paragraph*{Induction step (primary induction)}  $\Gamma$ has at least 
  one $\parr$ or $\with$. By (P2) $\fullgraph$ is connected.

\begin{itemize}
  
\item Suppose $\Gamma=\Delta,A\parr B$, with $\parr$-vertex $x\in\fullgraph$
  corresponding to $A\parr B$.  Consider the $\parr$-rule $\rho$ with
  conclusion $\Gamma$ and hypothesis $\Gamma'=\Delta,A,B$.  The
  sequents $\Gamma$ and $\Gamma'$ have the same literal occurrences
  and essentially the same $\with$- and additive resolutions, so
  $\theta$ constitutes a proof structure $\theta'$ on $\Gamma'$.  The
  switchings of the linkings of $\theta'$ are trees, since they are
  obtained from those of $\theta$ by deleting $x$.  Moreover, $\theta$
  and $\theta'$ have the same subsets $\Lambda$ of linkings, toggling
  the same $\with$s and having the same switching cycles (because the
  vertex $x$ cannot be in a switching cycle of any $\Lambda \subseteq
  \theta$).  Therefore $\theta'$ is a proof net on $\Gamma'$.  Appeal
  to the induction hypothesis with $\theta'$.
  
\item Suppose $\Gamma=\Delta,A_0\with A_1$, with vertex
  $w\in\fullgraph$ corresponding to $A_0\with A_1$.  Consider the
  $\with$-rule $\rho$ with conclusion $\Gamma$ and left and right
  hypotheses $\Gamma_0=\Delta,A_0$ and $\Gamma_1=\Delta,A_1$,
  respectively.  Define the sets of linkings $\theta_i$ on $\Gamma_i$ to
  comprise those linkings of $\theta$ which are on $\Gamma_i\subseteq \Gamma$.
  Each $\theta_i$ is a proof net since any switching cycle of
  $\sect{\theta_i}$ is a switching cycle of $\fullgraph$.  Appeal to
  the induction hypothesis with each $\theta_i$.

\item

Suppose $\fullgraph$ has no $\to$-terminal (\ie\ concluding) $\parr$
or $\with$.  By the Separation Lemma $\fullgraph$ has a
$\parr$/$\with$-vertex $x$ such that the deletion of the edge $x\edge
y$ disconnects $\fullgraph$ into $G_0$ and $G_1$.\parskip 0pt plus 2pt
\parindent 10pt

Let $G_0$ be the component containing $x$, and let $\Gamma_0$
comprise the formula-occurrences corresponding to the $\to$-terminal
vertices of $G_0$ (some formulas of $\Gamma$ together with the
subformula occurrence $A\with B$ corresponding to $x$).
Define $\theta_0=\{\lambda\restr\Gamma_0:\lambda\in\theta\}$ on $\Gamma_0$
(each $\lambda\restr \Gamma_0$ is well-defined since no $a\in\lambda$ goes
between $G_0$ and $G_1$).  

  Let $\Gamma_1$ be the subsequent of $\Gamma$ containing the formulas
  corresponding to the $\to$-terminal vertices of $G_1$.  
  In $G_1$, $y$ is $\to$-initial.  Form $G_1^+$ by adding literals $P$
  and $P\perpp$, the axiom link $a=\{P,P\perpp\}$, and edges
  $y\edgefrom P\edgefrom a\edge P\perpp$.  Let $\widehat{\Gamma}_1$ be
  $\Gamma_1$ with $P$ substituted for the subformula occurrence
  $A\with B$ corresponding to $x$, and let
  $\Gamma_1^+=\widehat{\Gamma}_1,P\perpp$.  
  Define $\theta_1=\{\lambda\restr\widehat\Gamma_1 \cup
  \{a\}:\lambda\in\theta\}$ on $\Gamma_1^+$.

\vspace{1ex}

{\em Claim:} $x \in \resolution{\lambda}{\Gamma}$ for all $\lambda\in\theta$.

{\em Proof.} If not, there is $\lambda\in\theta$ and a
$\&$-vertex $w$ with $x$ in $\resolution{\lambda}{\Gamma}$ but not in
$\resolution{\lambda_w}{\Gamma}$ for some $\lambda_w\in\theta$ such
that $\lambda\stackrel{w}{=}\lambda_w$. Thus there is a jump
$b\rightarrow w$ in $\fullgraph$ for some $b\in G_0$ with $b
\in\lambda\setminus\lambda_w$.  Since
linkings are total on additive resolutions there exists an axiom link
$c\in\lambda_w\setminus\lambda$ connecting to the formula containing
$x$, but not satisfying $c \rightarrow \cdots \edge x$, so there is a
jump $c\edge w$ in $\fullgraph$.  If $w \in G_0$ then $c\edge w$ is a
jump from $G_1$ to $G_0$, and if $w \in G_1$ then $b \edge w$ is a
jump from $G_0$ to $G_1$; either case violates the disconnectedness of
$G_0$ from $G_1$.\hfill\filledbox

\vspace{1ex}

  The claim implies that $\theta_0$ and $\theta_1$ are sets of
  linkings on $\Gamma_0$ and $\Gamma_1^+$, respectively. Moreover,
  $\graph{\theta_0} = G_0$ and $\graph{\theta_1} = G_1^+$.  We now
  check that $\theta_0$ and $\theta_1$ are proof nets, \ie, satisfy
  (P1)--(P3).  Since $\theta$ satisfies (P1), $\theta_0$ (resp.\
  $\theta_1$) has at least one linking on every $\with$-resolution of
  $\Gamma_0$ (resp.\ $\Gamma_1^+$). Had $\theta_i$ two
  distinct linkings on the same $\with$-resolution, there would be a
  jump from an axiom link in $G_i$ to a $\with$ in $G_{1-i}$,
  violating the disconnectedness of $G_0$ from $G_1$. Thus $\theta_i$
  satisfies (P1).  (P2) is trivially inherited from $\theta$.
  Finally, (P3) holds since any set of linkings $\Lambda'$ in
  $\theta_0$ or $\theta_1$ corresponds to a set of linkings
  $\Lambda$ in $\theta$ toggling the same $\with$s, such that any
  switching cycle of $\Lambda'$ is a switching cycle of $\Lambda$.

By induction $\theta_0$ is the translation of a cut-free proof $\Pi_0$
of $\Gamma_0$ and likewise $\theta_1$ is the translation of
$\Pi_1$. Substituting $\Pi_0$ for the axiom rule with
conclusion $P,P\perpp$ in $\Pi_1$ yields a proof whose translation is
$\theta$. \hfill$\Box$
\end{itemize}
In the case of MALL+\textsc{mix}, the connectedness
requirement of (P2) does not apply. This condition is used three times
in the above proof.  To prove that a set of linkings is the translation 
of a cut-free MALL+\textsc{mix} proof iff it is a cut-free mix net,
where a \defn{mix net} is a set of linkings satisfying (P1)--(P3)
minus the connectedness requirement of (P2), in
each part of the inductive proof above, the case that
$\fullgraph$ is not connected can be dealt with by partitioning
$\Gamma$ into a number of non-empty subsequents $\Gamma_i$, each
harbouring a connected component of $\fullgraph$.  
The mix net $\theta$ projects to mix nets $\theta_i$ on
$\Gamma_i$, which by induction are translations of cut-free MALL+\textsc{mix}
proofs $\Pi_i$. By the \textsc{mix} rule these combine into a
proof that translates to $\theta$.

\section{Appendix: Proof that eliminating a cut from a proof net
yields a proof net}
\label{appendix-cut-elimination}

\noindent
In this appendix we establish that cut elimination preserves (P0)--(P3).
Preservation of (P0) is trivial.
Preservation of (P1) for a literal or multiplicative cut is also trivial;
for an additive cut it is an immediate consequence of the following lemma.

\begin{lemma}
Let $A\cut A\perp$ be an additive cut in a cut sequent $\Gamma$ with
$A=A_0\with A_1$ and $A\perp=A_0\perp\plus A_1\perp$ (or vice versa),
and let $\lambda$, $\lambda'$ be linkings of a proof net on $\Gamma$
such that the cut $\with$ is the only $\with$ toggled between
$\resolution{\lambda}{\Gamma}$ and $\resolution{\lambda'}{\Gamma}$.
Then $\lambda$ and $\lambda'$ take the same argument of $A\perp$,
\ie, exactly one of $A_0\perp$ and $A_1\perp$ occurs in both
$\resolution{\lambda}{\Gamma}$ and $\resolution{\lambda'}{\Gamma}$.
\end{lemma}

\begin{proof}
If $\lambda$ and $\lambda'$ took opposite arguments of
$A\perp$, an axiom link above $A\perp$ would depend on the cut $\with$.
The resulting jump yields a switching cycle of
$\{\lambda,\lambda'\}$ containing the only $\with$ toggled by
$\{\lambda,\lambda'\}$, in violation of (P3).
\end{proof}
Preservation of (P2) is straightforward for a literal or additive cut,
since switchings correspond before and after the elimination.
Preservation of (P2) for a multiplicative cut is a corollary of the
well-definedness of cut elimination for MLL proof nets, since the
elimination of a multiplicative cut from one of our proof nets
corresponds precisely to the parallel elimination of copies of the cut
in the induced MLL proof nets.%
\footnote{To be self-contained, we give a direct proof.  
Let $\Gamma$ (resp.\ $\Gamma'$) be the cut sequent before (resp.\
after) the elimination.
By definition, the linkings remain the same.
We prove the following stronger result:
if every switching of a linking $\lambda$ on $\Gamma$ is a tree, then
every switching of $\lambda$ on $\Gamma'$ is a tree.
If the eliminated cut vertex $c$ is absent from
$\resolution{\Gamma}{\lambda}$, every switching of $\lambda$ on
$\Gamma'$ is a switching of $\lambda$ on $\Gamma$, hence a
tree; therefore assume $c$ is present.
Let $x$ be the eliminated \raisebox{-.2ex}{$\smallparr$}, with
arguments $x_0,x_1$, and let $y$ be the eliminated $\tensor$, with
arguments $y_0,y_1$.  Thus $x_i\to x\to c\leftarrow y\leftarrow y_i$
in $\Gamma$.
Let $\hat\Gamma$ be the result of deleting $x$, $c$ and $y$ (and
associated edges) from $\Gamma$.  Claim: every switching $\sigma$ of
$\lambda$ on $\hat\Gamma$ is the disjoint union of three trees, one
containing the $x_i$, one containing $y_0$, and one containing
$y_1$.  Proof: let $\sigma_i$ be the switching of $\lambda$ on
$\Gamma$ obtained from $\sigma$ by adding $x_i\to x\to c\leftarrow y$
and $y_0\to y\leftarrow y_1$, \emph{a priori} a tree; were the $y_i$
connected by a path $\pi$ in $\sigma$ then $y\pi y$ would be a cycle
in each $\sigma_i$; were $x_j$ and $y_k$ connected by a path $\pi$ in
$\sigma$ then $cxx_j\pi y_kyc$ would be a cycle in $\sigma_j$; were
the $x_i$ disconnected in $\sigma$ then (given the disconnection of
the $x_i$ from the $y_i$) they would be disconnected in each
$\sigma_i$.
A switching of $\lambda$ on $\Gamma'$ is a switching of $\lambda$ on
$\hat\Gamma$ together with cuts $x_0\to c_0\leftarrow y_0$ and $x_1\to
c_1\leftarrow y_1$, and is therefore (by the claim) a tree.}

The remainder of this appendix is
devoted to the proof that cut elimination preserves (P3).

Fix a proof net $\theta$ on a cut sequent $\Gamma$.
We localise the notion of domination of Appendix~\ref{appendix-proof}
from $\theta$ to any saturated set of linkings $\Lambda\subseteq\theta$.
Write $x\edge_\Lambda y$ if the edge $x\edge y$ of $\fullgraph$ is in
$\graph{\Lambda}\!$. A subgraph $X$ of $\graph{\Lambda}$ is an
\defn{$x$-zone under $\Lambda$} if for all $x' \in X$ there exists $y$
with \mbox{$x \edgefrom_\Lambda y \strongpathin{X} x'$}; given a
$\parr$/$\with$-vertex $x\in\graph{\Lambda}$ and a vertex
$y\in\graph{\Lambda}$, define $x$ \defn{dominates $y$ in $\Lambda$},
denoted $x\dominatesin{\Lambda}y$, if $y\in X$ for some $x$-zone $X$ under $\Lambda$.
Lemmas~\ref{jump-into-L},~\ref{dominance-trans},~\ref{w-jump-switching-cycle},%
~\ref{w-dom-v},~\ref{dominance-switching-cycle},~\ref{path},
and~\ref{one-spike} of Appendix~\ref{appendix-proof} localise from
$\theta$ to any saturated set of linkings $\Lambda\subseteq \theta$,
as follows:

\setcounter{localisedlemma}{1}
\begin{localisedlemma}
\label{localised-jump-into-L}
  For every non-empty union $S$ of switching cycles in $\graph\Lambda$
  there is a jump $a\!\jump\!w$ in $\graph\Lambda$ between an axiom
  link $a\in S$ and a $\with$-vertex $w \!\not\in\! S$ which is
  toggled by $\Lambda$.
\end{localisedlemma}
\begin{localisedlemma}
\label{localised-dominance-trans}
Localised domination $\dominatesin\Lambda$ is transitive.
\end{localisedlemma}

\begin{localisedlemma}
\label{localised-w-jump-switching-cycle}
  Let $C$ be a switching cycle in $\graph\Lambda$ containing an axiom
  link with a jump to a $\with$-vertex $w\not\in C$.  Then $w
  \dominatesin\Lambda x$ for all vertices $x\in C$.
\end{localisedlemma}

\begin{localisedlemma}
\label{localised-w-dom-v}
  If $x$ is in a switching cycle of $\Lambda$ then $w\dominatesin{\Lambda} x$
  for some $\with$-vertex $w$ toggled by $\Lambda$ that is in no switching cycle of $\Lambda$.
\end{localisedlemma}

\begin{localisedlemma}
\label{localised-dominance-switching-cycle}
If $x\dominatesin{\Lambda} x$ then $x$ is in a switching cycle of $\Lambda$.
\end{localisedlemma}

\setcounter{localisedlemma}{7}
\begin{localisedlemma}
\label{localised-path}
  If $x \dominatesin\Lambda y_0$ and there is a path $y_0y_1\ldots y_n$ in
  $\graph\Lambda$ which never enters a $\parr$/$\with$ from above,
   then $x \dominatesin\Lambda y_n$.
\end{localisedlemma}

\setcounter{localisedlemma}{10}
\begin{localisedlemma}
\label{localised-one-spike}
  Let $x$ be a $\parr$/$\with$ and let $z_0\ldots z_n$ be a switching
  path in $\graph\Lambda$ such that $z_0\edge_\Lambda x$ and
  $z_n\edge_\Lambda x$.  Then $x\dominatesin\Lambda z_i$, each $0\le i\le n$.
\end{localisedlemma}
The proof of Localised Lemma~\ref{localised-jump-into-L} is a
relatively straightforward adaptation of the proof of
Lemma~\ref{jump-into-L}; we present it in full below.  The proofs of
the remaining localised lemmas are obtained by making the following
substitutions in the proofs of the originals in
Appendix~\ref{appendix-proof}: $\Lambda$ for $\theta$,
$\dominatesin\Lambda$ for $\dominates$, $\edge_\Lambda$ for $\edge$,
and \emph{zone under $\Lambda$} for \emph{zone}.

\newenvironment{localised-jump-into-proof}
{\begin{trivlist}\item{}\normalfont\textit{Proof of Localised Lemma~\ref{localised-jump-into-L}. }}
  {\hfill$\square$\end{trivlist}}

\begin{localised-jump-into-proof}%
  Let $\Lambda_m$ be a minimal saturated subset of $\Lambda$ with
  $\graph{\Lambda_m}$ containing $S$. Switchings of singleton sets of
  linkings are cycle-free by (P2), so $\Lambda_m$ contains at least
  two linkings. Let $w$ be a $\with$ toggled by $\Lambda_m$ that is not
  in any switching cycle of $\Lambda_m$ (existing by (P3)), so $w
  \not\in S$. Since $\Lambda_m \subseteq \Lambda$, $w$ is certainly
  toggled by $\Lambda$.  Since $\Lambda_m$ is minimal,
  $S\not\subseteq\graph{\Lambda_m^{\!w}}$ (using (S1)), so some edge $e$ of $S$ is in
  $\graph{\Lambda_m}$ but not in $\graph{\Lambda_m^{\!w}}$.\linebreak
  Without loss of generality $e$ is an edge from an axiom link $a$,
  because for any other edge $y \edge x$ in $S$ we have\linebreak $a \edge
  z_1\to\ldots\to z_n=y\to x$ in $S$ for some axiom link $a$, and
  $y\edge x$ is in $\graph{\Lambda_m^{\!w}}$ whenever $a\edge z_1$ is in
  $\graph{\Lambda_m^{\!w}}$.
  By Lemma~\ref{edge-dep} the jump $a\jump w$ is in
  $\graph{\Lambda_m}$, hence also in $\graph\Lambda$.
\end{localised-jump-into-proof}%
\newenvironment{goalproof}
{\begin{trivlist}\item{}\normalfont\textbf{Proof that cut elimination preserves (P3). }}
{\end{trivlist}}
\begin{goalproof}
Preservation is immediate for the elimination of a literal cut $P \cut
P\perpp$, since for every set $\Lambda$ of linkings on $\Gamma$, the
$\with$-vertices toggled by $\Lambda$ and the switching cycles of
$\Lambda$ correspond before and after the elimination.
Thus consider the elimination of an additive cut $(A_0\with
A_1)\cut (A_0\perpp\plus A_1\perpp)$ or a
multiplicative cut $(A_0\parr A_1) \cut (A_0\perpp\tensor A_1\perpp)$.

Let $\theta'$ on the cut sequent $\Gamma'$ be the result of
eliminating $(A_0\with A_1)\cut (A_0\perpp\plus A_1\perpp)$ or
$(A_0\parr A_1) \cut (A_0\perpp\tensor A_1\perpp)$ from the proof
net $\theta$ on $\Gamma$.  Let $x$ be the $\with$ or $\parr$ and $y$
the $\oplus$ or $\tensor$ of the cut, let $x_0,x_1$ and $y_0,y_1$ be the
arguments of $x$ and $y$ respectively, and let $c$ be the cut vertex
$\cut$ between $x$ and $y$.  Thus in $\Gamma'$ each of $c$, $x$ and
$y$ have been deleted, and cut vertices $c_0$ between $x_0$ and $y_0$ and
$c_1$ between $x_1$ and $y_1$ have been added, unless one of
$A_0,A_0\perpp$ or $A_1,A_1\perpp$ disappeared in the `garbage
collection' phase of additive elimination, in which case only one of $c_0$
or $c_1$ is present.

Suppose $\theta'$ fails (P3), \ie, there exists a set of two or more
linkings $\Lambda'\subseteq\theta'$ such that every $\with$ in
$\Gamma'$ toggled by $\Lambda'$ is in a switching cycle of $\Lambda'$
on $\Gamma'$.
\begin{lemma}\label{same-toggles}
There exists a saturated set of linkings $\Lambda\subseteq\theta$ on
$\Gamma$ such that $\Lambda$ on $\Gamma$ toggles the same $\with$'s as
$\Lambda'$ on $\Gamma'$, except perhaps $x$ in addition (in the case
of an additive cut).
\end{lemma}
\begin{proof}
Since cut elimination
simply deletes linkings, $\Lambda'$ can also be viewed as a set of
linkings on $\Gamma$, and $\Lambda'\subseteq\theta$.  Furthermore,
$\Lambda'$ on $\Gamma$ toggles exactly the same $\with$'s as
$\Lambda'$ on $\Gamma'$, except perhaps $x$ in addition (in the case
of an additive cut).  Let $\Lambda$ be a minimal saturated set of
linkings of $\theta$ on $\Gamma$ containing $\Lambda'$. By minimality,
$\Lambda$ on $\Gamma$ toggles the same $\with$'s as $\Lambda'$ on
$\Gamma$.
\end{proof}

\begin{lemma}\label{y-not-in-switching-cycle}
The vertex $y$ is not in a switching cycle of $\Lambda$.
\end{lemma}

\begin{proof}
If $y$ is in a switching cycle, 
then by Localised Lemma~\ref{localised-w-dom-v}, $\Lambda$ toggles a
$\with$-vertex $w\dominatesin{\Lambda}y$ in no switching cycle of
$\Lambda$.  We have $w\dominatesin{\Lambda}x$ by Localised
Lemma~\ref{localised-path}.  Necessarily $w \neq x$, otherwise
$w\dominatesin{\Lambda}w$ and by Localised
Lemma~\ref{localised-dominance-switching-cycle} $w$ is in a switching
cycle of $\Lambda$, a contradiction.  By Lemma~\ref{same-toggles}, $w$
is toggled by $\Lambda'$ on $\Gamma'$, hence%
\footnote{\label{lambda-prime-footnote}%
Recall that $\Lambda'$ was chosen as a witness to the failure of (P3)
for $\theta'$: any $\with$ in $\Gamma'$ toggled by $\Lambda'$ is in a
switching cycle of $\Lambda'$ on $\Gamma'$.}
$w$ is in a switching cycle $C$ of $\Lambda'$ on $\Gamma'$.

Suppose $C$ does not go through both $c_0$ and $c_1$. Then $C$ induces a
switching cycle of $\Lambda$ on $\Gamma$, still containing $w$,
obtained by re-routing a possible passage through $c_0$ or $c_1$ to go
through $c$ instead. This yields a contradiction.

Suppose $C$ goes through both $c_0$ and $c_1$. Re-routing both
passages to go through $c$ instead either yields two switching cycles
through $c$ with $w$ in one of them, a contradiction, or yields a
switching cycle $C_y$ through $y$ and a switching path $P_x =
z_0\ldots z_n$ in $\graph\Lambda$ with $z_0\edge_\Lambda x$ and
$z_n\edge_\Lambda x$, such that $w$ is either in $C_y$ or $P_x$.  The
first possibility immediately yields a contradiction, so assume $w \in
P_x$.  By Localised Lemma~\ref{localised-one-spike},
$x\dominatesin{\Lambda}w$, so by transitivity (Localised
Lemma~\ref{localised-dominance-trans}), $w\dominatesin{\Lambda}w$,
hence by Localised Lemma~\ref{localised-dominance-switching-cycle},
$w$ is in a switching cycle of $\Lambda$, a contradiction.
\end{proof}
\begin{lemma}\label{toggle-implies-in-switching-cycle}
Every $\with$-vertex $v\neq x$ toggled by $\Lambda$ on $\Gamma$ is in
a switching cycle of $\Lambda$ on $\Gamma$.
\end{lemma}
\begin{proof}
By Lemma~\ref{same-toggles}, $v$ is toggled by $\Lambda'$ on
$\Gamma'$, hence$^{\text{\ref{lambda-prime-footnote}}}$ $v$ is in a
switching cycle $C$ of $\Lambda'$ on $\Gamma'$. Suppose $C$ goes
through $c_0$ and/or $c_1$.  By re-routing the passage(s) through
$c_0$ and/or $c_1$ to go through $c$ instead, $C$ induces a switching
cycle of $\Lambda$ on $\Gamma$ that contains $y$, in contradiction
with Lemma~\ref{y-not-in-switching-cycle}.  Thus $C$ does not go
through $c_0$ or $c_1$. Hence $C$ is also a switching cycle of
$\Lambda$ on $\Gamma$, containing $v$.
\end{proof}

\begin{corollary}
If the cut is multiplicative, every $\with$ toggled by $\Lambda$ on
$\Gamma$ is in a switching cycle of $\Lambda$ on $\Gamma$.
\end{corollary}
Thus if the cut is multiplicative, $\theta$ fails to be a proof net, a
contradiction.  Henceforth we assume the cut is additive.
\begin{lemma}\label{unique-toggled-not-switching-cycle}
The $\with$-vertex $x$ is the unique $\with$ toggled by $\Lambda$ that
is not in any switching cycle of $\Lambda$.
\end{lemma} 
\begin{proof}
Since $\theta$ is a proof net, $\Lambda$ toggles a $\with$-vertex $v$
in no switching cycle of $\Lambda$.  By
Lemma~\ref{toggle-implies-in-switching-cycle}, necessarily $v=x$.
\end{proof}
There exist linkings $\lambda_1,\lambda_2 \in \Lambda'$ such that
$y_0 \in \resolution{\Gamma'}{\lambda_1}$ but $y_0 \not\in
\resolution{\Gamma'}{\lambda_2}$, for otherwise $\Lambda$ would not
toggle $x$. Thus there is a jump $a
\edge_\Lambda u$ in $\graph{\Lambda}$ from an axiom link $a$ above
$y_0$ to a $\with$-vertex $u$ toggled by $\Lambda$.
If $u=x$, we immediately obtain a switching cycle $x$, $c$, $y$,
$y_0$,\ldots, $a$, $x$ in $\graph\Lambda$, a contradiction.  Thus $u
\neq x$, so by 
Lemma~\ref{toggle-implies-in-switching-cycle}, $u$ is
in a switching cycle of $\Lambda$, and by Localised
Lemma~\ref{localised-w-dom-v} and
Lemma~\ref{unique-toggled-not-switching-cycle},
$x\dominatesin{\Lambda} u$.  Thus $x$ is in a switching cycle of
$\Lambda$ going through $c$, $y$, $y_0$, $a$ and $u$ (or a shortcut
thereof, if the strong switching path from $x$ to $u$ intersects the
path $x,c,y,y_0,\ldots,a$), a contradiction. Hence $\theta'$
satisfies (P3).
\end{goalproof}

\end{document}
