% definitions for classical and linear logic connectives
% vladimir@cs.ualberta.ca  May 1996

% latex209 compatibility
\@ifundefined{ensuremath} % latex209
  {\newcommand{\mathcal}[1]{{\cal #1}}
   \newcommand{\textsf}[1]{{\sf #1}}
   \newcommand{\ensuremath}[1]{\ifmmode#1\else$#1$\fi}}
  {\@ifundefined{@latex@e@error}
    {} % latex2e in native mode
    % latex2e in latex209 compatibility mode
    {\renewcommand{\ensuremath}[1]{\ifmmode#1\else$#1$\fi}}}
\@ifundefined{settoheight}
  {\def\settoheight#1#2{\setbox\@tempboxa\hbox{#2}#1\ht\@tempboxa\relax}}{}

\newcommand{\tuple}[1]{\ensuremath{\left\langle#1\right\rangle}}

% CLASSICAL LOGIC
\let\And\wedge \let\Or\vee \let\Not\neg
\let\Impl\Rightarrow \let\If\Leftarrow \let\Iff\Leftrightarrow
\let\Entails\vdash \let\Models\models
\def\BiEntails{\dashv\vdash}

% LINEAR LOGIC
% versions without mathrel space around the symbol
% Can be used in both math and text mode
\let\lNeg\bot
\def\Times{\raisebox{.25ex}{$\otimes$}} \let\Tensor\Times
\def\With{\mbox{\rm\&}}
\def\Plus{\raisebox{.2ex}{$\oplus$}}
\def\implKern{\kern-0.11em}\def\implRaise{.1ex}
\def\lImpl{\raisebox{\implRaise}{$\mathord{-}\implKern\mathord{\circ}$}}
\def\lIf{\raisebox{\implRaise}{$\mathord{\circ}\implKern\mathord{-}$}}
\def\lIff{\raisebox{\implRaise}
  {$\mathord{\circ}\implKern\mathord{-}\implKern\mathord{\circ}$}}
% Reddy's non-commutative multiplicative mixing And-Or properties
\let\Before\rhd \let\mAndOr\Before

% As usual, the troublesome thing is Girard's inverted ampersand (Par).

% Lincoln and Winkler's MetaFont Par. The Right Thing.
% file://ftp.csl.sri.com/pub/linear/fonts/par.tar.Z
\@ifundefined{selectfont}
   {\input{par.sty}\def\Par{{\parfont P}}}
   % file://ftp.csl.sri.com/pub/linear/fonts/par.sty
   {\input{nfpar.sty}          % New Font Selection Scheme
   % file://ftp.csl.sri.com/pub/linear/fonts/nfpar.sty
   \DeclareMathSymbol\parsym{\mathord}{par}{"50}
   \def\Par{\ensuremath{\parsym}}}

% stmaryrd provides lots of nice symbols. 
% ftp://ftp.shsu.edu/tex-archive/fonts/stmaryrd
% Par and With match and scale nicely, but I don't like they are sans-serif.
% \input{stmaryrd.sty \def\With{\binampersand}\def\Par{\bindnasrepma}

% Sprite defines it with a bitmap; I think this doesn't scale well.
% \input{sprite.sty}\input{par-sprite.tex}\def\Par{\ParTensor}
% Ask me for these two files if you decide to use them

% V. Pratt has defined it with vector graphics. Par doesn't match &.
% file://ftp.csl.sri.com/pub/linear/fonts/pratt-par.tex
% \input{pratt-par.tex}\def\Par{\Invamp}

% as a last resort, use the \wp symbol which has some resemblance to Par
%\def\Par{\mathrel{\raisebox{.45ex}{$\wp$}}}

% versions with mathbin space. Also, some "systematic" names.
\let\lNEG\lNeg \let\lNot\lNeg
\def\TIMES{\mathbin{\Times}} \let\TENSOR\TIMES  \let\mAnd\TIMES
\def\PAR{\mathbin{\Par}}                        \let\mOr\PAR
\def\WITH{\mathbin{\With}}                      \let\aAnd\WITH
\def\PLUS{\mathbin{\Plus}}                      \let\aOr\PLUS
\def\lIMPL{\mathrel{\lImpl}}
\def\lIF{\mathrel{\lIf}}
\def\lIFF{\mathrel{\lIff}}
\def\mANDOR{\mathbin{\mAndOr}} \let\mAO\mAndOr

% the units
\def\One{{\bf 1}}  \let\mOne\One   
\def\Zero{{\bf 0}} \let\aZero\Zero
\def\Top{\ensuremath{\top}} \let\aOne\top
\def\Bot{\ensuremath{\bot}} \let\mZero\bot 

% INFERENCE RULES
% There are three types of rules depending on the label (eg \Par\Left)
% - no label. Use when you don't care to identify the rule
% - label with width.
% - label without width. Use for the rightmost rule on a line so that 
%   the rule above it does not expand over the label. NOTE: this causes some
%   ovefull warnings from latex, don't pay attention
% In addition, the label can be set in either math or text mode.
%
% When there is no label, the command has two arguments. Use \qquad (or
% whatever) to separate the top components, if more than one:
%   \Rule{top1 \qquad top2}{bottom}
% When there is a label, it is the second argument:
%   \Rule{top1 \qquad top2}{label}{bottom}, 
% so that it looks good if you nest rules:
%    \Rule{formula1}{label1}
%   {\Rule{formula2}{label2}
%         {formula3}}

\newcommand{\Rule}[2]% no label
  {\ensuremath{\begin{array}[b]{@{}c@{}}#1\\\hline#2\end{array}}}
\newcommand{\RuleMW}[3]% label with width in math mode
  {\RuleLW{#1}{\ensuremath{#2}}{#3}}
\newcommand{\RuleM}[3]% no-width label in math mode
  {\RuleL{#1}{\ensuremath{#2}}{#3}}
\newcommand{\RuleTW}[3]% label with width in text mode
  {\RuleLW{#1}{\textsf{#2}}{#3}}
\newcommand{\RuleT}[3]% no-width label in text mode
  {\RuleL{#1}{\textsf{#2}}{#3}}
% names to be used in math-mode labels
\newcommand{\Intro}{\mathcal{I}}\newcommand{\Elim}{\mathcal{E}}
\newcommand{\Right}{\mathcal{R}}\newcommand{\Left}{\mathcal{L}}
% Vdots to be used in lieu of some inference steps
\newcommand{\Vdots}[2]
  {\begin{array}{c}#1\\\raisebox{0ex}[1.1ex][0ex]{\vdots}\\#2\end{array}}

% implementation
\newsavebox{\infRuleBot}\newsavebox{\infRuleLabel}\newsavebox{\infRule}
\newlength{\infRuleWidth}\newlength{\infRuleLblHeight}\newlength{\infRuleCenter}
\newcommand{\RuleXXX}[4]% #1=top, #2=label, #3=bottom, #4=makebox command
  {\sbox{\infRuleBot}{\ensuremath{#3}}
   \sbox{\infRuleLabel}{#2}
   \sbox{\infRule}{\Rule{#1}{\usebox{\infRuleBot}}}
   \settowidth{\infRuleWidth}{\usebox{\infRule}}
   \settoheight{\infRuleCenter}{\usebox{\infRuleBot}}
   \settoheight{\infRuleLblHeight}{\usebox{\infRuleLabel}}
   \addtolength{\infRuleCenter}{-0.5\infRuleLabel}
   \addtolength{\infRuleCenter}{-0.4ex}
   #4{\usebox{\infRule}%
      \raisebox{\infRuleCenter}{\usebox{\infRuleLabel}}}}
\newcommand{\RuleLW}[3]% label with width
  {\RuleXXX{#1}{#2}{#3}{\makebox}}
\newcommand{\RuleL}[3]% no-width label
  {\RuleXXX{#1}{#2}{#3}{\makebox[\infRuleWidth][l]}}

% The rules of two-sided Classical Linear Logic
% axiom, cut, negation

\newcommand{\Axiom}
  {\RuleTW{}{Axiom}{\phi\Entails\phi}}
\newcommand{\Cut}
  {\RuleTW{\Gamma_1\Entails\phi,\Delta_1 \quad \Gamma_2,\phi\Entails\Delta_2}
  {Cut}
  {\Gamma_1,\Gamma_2\Entails\Delta_1,\Delta_2}}
\newcommand{\lNegLeft}
  {\RuleMW{\Gamma\Entails\phi,\Delta}
  {{}^\lNeg\Left}
  {\Gamma,\phi^\lNeg\Entails\Delta}}
\newcommand{\lNegRight}
  {\RuleMW{\Gamma,\phi\Entails\Delta}
  {{}^\lNeg\Right}
  {\Gamma\Entails\phi^\lNeg,\Delta}}

% multiplicatives

\newcommand{\mAndLeft}
  {\RuleMW{\Gamma,\phi,\psi\Entails\Delta}{\mAnd\Left}
  {\Gamma,\phi\mAnd\psi\Entails\Delta}}
\newcommand{\mAndRight}
  {\RuleMW{\Gamma_1\Entails\phi,\Delta_1 \quad \Gamma_2\Entails\psi,\Delta_2}
  {\mAnd\Right}
  {\Gamma_1,\Gamma_2\Entails\phi\mAnd\psi,\Delta_1,\Delta_2}}
\newcommand{\mOrLeft}
  {\RuleMW{\Gamma_1,\phi\Entails\Delta_1 \quad \Gamma_2,\psi\Entails\Delta_2}
  {\mOr\Left}
  {\Gamma_1,\Gamma_2,\phi\mOr\psi\Entails\Delta_1,\Delta_2}}
\newcommand{\mOrRight}
  {\RuleMW{\Gamma\Entails\phi,\psi,\Delta}
  {\mOr\Right}
  {\Gamma\Entails\phi\mOr\psi,\Delta}}
\newcommand{\lImplLeft}
  {\RuleMW{\Gamma_1\Entails\phi,\Delta_1 \quad \Gamma_2,\psi\Entails\Delta_2}
  {\lImpl\Left}
  {\Gamma_1,\Gamma_2,\phi\lImpl\psi\Entails\Delta_1,\Delta_2}}
\newcommand{\lImplRight}
  {\RuleMW{\Gamma,\phi\Entails\psi,\Delta}
  {\lImpl\Right}
  {\Gamma\Entails\phi\lImpl\psi,\Delta}}

% additives

\newcommand{\aAndLeft}
  {\Rule{\Gamma,\phi\Entails\Delta}
  {\Gamma,\phi\aAnd\psi\Entails\Delta}{\ }
  \RuleMW{\Gamma,\psi\Entails\Delta}
  {\aAnd\Left}
  {\Gamma,\phi\aAnd\psi\Entails\Delta}}
\newcommand{\aAndRight}
  {\RuleMW{\Gamma\Entails\phi,\Delta \quad \Gamma\Entails\psi,\Delta}
  {\aAnd\Right}
  {\Gamma\Entails\phi\aAnd\psi,\Delta}}
\newcommand{\aOrLeft}
  {\RuleMW{\Gamma,\phi\Entails\Delta \quad \Gamma,\psi\Entails\Delta}
  {\aOr\Left}
  {\Gamma,\phi\aOr\psi\Entails\Delta}}
\newcommand{\aOrRight}
  {\Rule{\Gamma\Entails\phi,\Delta}
  {\Gamma\Entails\phi\aOr\psi,\Delta}{\ }
  \RuleMW{\Gamma\Entails\psi,\Delta}{\aOr\Right}
  {\Gamma\Entails\phi\aOr\psi,\Delta}}

% multiplicative units

\newcommand{\mOneLeft}
  {\RuleMW{\Gamma\Entails\Delta}{\mOne\Left}{\Gamma,\mOne\Entails\Delta}}
\newcommand{\mOneRight}
  {\RuleMW{}{\mOne\Right}{\Entails\mOne}}
\newcommand{\mZeroLeft}
  {\RuleMW{}{\mZero\Left}{\mZero\Entails}}
\newcommand{\mZeroRight}
  {\RuleMW{\Gamma\Entails\Delta}{\mZero\Right}{\Gamma\Entails\mZero,\Delta}}

% additive units

\newcommand{\aOneLeft}
  {\hbox{no $\aOne\Left$}}
\newcommand{\aOneRight}
  {\RuleMW{}{\aOne\Right}{\Gamma\Entails\aOne,\Delta}}
\newcommand{\aZeroLeft}
  {\RuleMW{}{\aZero\Left}{\Gamma,\aZero\Entails\Delta}}
\newcommand{\aZeroRight}
  {\hbox{no $\aZero\Right$}}

% structural rulesW and exponentials

\newcommand{\XL}
  {\RuleMW{\Gamma_1,\phi,\psi,\Gamma_2\Entails\Delta}
  {X\Left}
  {\Gamma_1,\psi,\phi,\Gamma_2\Entails\Delta}}
\newcommand{\XR}
  {\RuleMW{\Gamma\Entails\Delta_1,\phi,\psi,\Delta_2}
  {X\Right}
  {\Gamma\Entails\Delta_1,\psi,\phi,\Delta_2}}
\newcommand{\WL}
  {\RuleMW{\Gamma\Entails\Delta}
  {W\Left}
  {\Gamma,!\phi\Entails\Delta}}
\newcommand{\cWL}
  {\RuleMW{\Gamma\Entails\Delta}
  {W\Left}
  {\Gamma,\phi\Entails\Delta}}
\newcommand{\WR}
  {\RuleMW{\Gamma\Entails\Delta}
  {W\Right}
  {\Gamma\Entails?\phi,\Delta}}
\newcommand{\cWR}
  {\RuleMW{\Gamma\Entails\Delta}
  {W\Right}
  {\Gamma\Entails\phi,\Delta}}
\newcommand{\CL}
  {\RuleMW{\Gamma,!\phi,!\phi\Entails\Delta}
  {C\Left}
  {\Gamma,!\phi\Entails\Delta}} 
\newcommand{\cCL}
  {\RuleMW{\Gamma,\phi,\phi\Entails\Delta}
  {C\Left}
  {\Gamma,\phi\Entails\Delta}} 
\newcommand{\CR}
  {\RuleMW{\Gamma\Entails?\phi,?\phi,\Delta}
  {C\Right}
  {\Gamma\Entails?\phi,\Delta}}
\newcommand{\cCR}
  {\RuleMW{\Gamma\Entails\phi,\phi,\Delta}
  {C\Right}
  {\Gamma\Entails\phi,\Delta}}
\newcommand{\DL}
  {\RuleMW{\Gamma,\phi\Entails\Delta}
  {D\Left}
  {\Gamma,!\phi\Entails\Delta}}
\newcommand{\DR}
  {\RuleMW{\Gamma\Entails\phi,\Delta}
  {D\Right}
  {\Gamma\Entails?\phi,\Delta}}
\newcommand{\PL}
  {\RuleMW{!\Gamma,\phi\Entails?\Delta}
  {P\Left}
  {!\Gamma,?\phi\Entails?\Delta}}
\newcommand{\PR}
  {\RuleMW{!\Gamma\Entails\phi,?\Delta}
  {P\Right}
  {!\Gamma\Entails!\phi,?\Delta}}

% quantifiers

\newcommand{\ForallLeft}
  {\RuleMW{\Gamma,\phi[t/x]\Entails\Delta}
  {\forall\Left}
  {\Gamma,\forall x.\phi\Entails\Delta}}
\newcommand{\ForallRight}
  {\RuleMW{\Gamma\Entails\phi[y/x],\Delta}
  {\forall\Right}
  {\Gamma\Entails\forall x.\phi,\Delta}}
\newcommand{\ExistsLeft}
  {\RuleMW{\Gamma,\phi[y/x]\Entails\Delta}
  {\exists\Left}
  {\Gamma,\exists x.\phi\Entails\Delta}}
\newcommand{\ExistsRight}
  {\RuleMW{\Gamma\Entails\phi[t/x],\Delta}
  {\exists\Right}
  {\Gamma\Entails\exists x.\phi,\Delta}}

\newcommand{\AllCLLRules}
{\begin{array}{c}
\begin{array}{rr}
\multicolumn{2}{c}{\hbox{Multiplicatives, Additives and their Units}}\\
\mOneLeft  \hfill\qquad \mAndLeft & \mOneRight  \hfill\qquad \mAndRight \\
\mZeroLeft \hfill\qquad \mOrLeft  & \mZeroRight \hfill\qquad \mOrRight  \\
\aOneLeft  \hfill\qquad \aAndLeft & \aOneRight  \hfill\qquad \aAndRight \\
\aZeroLeft \hfill\qquad \aOrLeft  & \aZeroRight \hfill\qquad \aOrRight  \\
\lImplLeft & \lImplRight
\end{array}
\vspace*{0.2cm}\\
\begin{array}{c}
\begin{array}{c}
\hbox{Reflexivity, Transitivity, Negation}\\
\Axiom    \hfill\qquad \Cut       \\
\lNegLeft \hfill\qquad \lNegRight
\end{array}
\vspace*{0.1cm}\\
\begin{array}{rr}
\multicolumn{2}{c}{\hbox{Quantifiers}}\\
\ForallLeft     & (*)\ForallRight \\
(*)\ExistsLeft  & \ExistsRight    \\
\multicolumn{2}{c}{\hbox{$(*)\ y$ not free in $\Gamma,\Delta$}}
\end{array}
\end{array}
\begin{array}{rr}
\multicolumn{2}{c}{\hbox{Structural Rules and Exponentials}}\\
\XL & \XR \\
\WL & \WR \\
\CL & \CR \\
\DL & \DR \\
\PL & \PR
\end{array}
\end{array}}