% \vspace{-7ex} {\LargeClassical logic \;\;=\;\; Fibred MLL\vspace*{-.5ex}% }
\normalsize \sc Dominic Hughes
math0504028.tex
\documentclass[10pt]{article}
\usepackage{times,amsmath,amssymb,theorem}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% 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).

%%%%%%%%%% end of Paul Taylor's Proof Trees


\makeatletter
\def\section{\@startsection{section}{1}{0pt}{-3.25ex plus -1ex minus 
-.2ex}{1.5ex plus .2ex minus .3ex}{\normalfont\large\bf}}
\def\subsection{\@startsection {subsection}{2}{0pt}{-2ex plus -1ex minus 
   -.2ex}{1.5ex plus .2ex minus .3ex}{\@setfontsize\normalsize\@xpt{12}\bf}}
\makeatother

\newcommand{\defn}[1]{{\textit{\textbf{#1}}}}
\newtheorem{theorem}{Theorem}
\newcommand{\ie}{\emph{i.e.}}
\newcommand{\cf}{\emph{cf.}}

\title{%
\vspace{-7ex}
{\Large\bf Classical logic \;\;=\;\; Fibred MLL\vspace*{-.5ex}%
}}%
\author{\normalsize
   \sc Dominic Hughes \\ 
   \small Stanford University 
}
\date{\vspace{-1ex}\small March 25, 2005\thanks{Accepted for a short presentation at \emph{Logic in Computer Science '05}.}}
\begin{document}

\advance\textheight 1.15em
\maketitle
\thispagestyle{empty}
\vspace{-2ex}%
Syntactically, classical logic decomposes thus \cite{Gir87}:
\begin{center}
\sl Classical logic \;\;=\;\; MLL \;+\; Superposition
\end{center}
where MLL is Multiplicative Linear Logic, and superposition means
contraction (binary case) and weakening (nullary case).
%
Proof nets for classical logic have been proposed \cite{Gir91,Rob03},
containing explicit contraction and weakening nodes.  Just as the
logical sequent rules of conjuction (tensor) and disjunction (par)
are represented explicitly in the net, so are the structural rules,
contraction and weakening.
%
Unfortunately, this explicit representation of structural rules
retains some of the redundancy (or `syntactic bureaucracy') of sequent
calculus.  For example, in the net presentation of classical
categories in \cite{FP05} one has to quotient by equations on nets,
involving contraction and weakening.
%
Thus, proof nets for classical logic fail to achieve the same elegance
as the proof nets for MLL.


We present a representation of a proof which is more abstract than a
proof net, which we call a \emph{combinatorial proof}: superposition
is modelled \emph{mathematically}, as a lax form of fibration, rather
than syntactically (as in proof nets, which involve contraction and
weakening nodes).
%
This draws a nice boundary between logical rules and structural rules:
the former are modeled with explicit nodes, the latter as actual
superposition, in an abstract mathematical sense, without nodes.
%
We can summarise the situation thus:\vspace{-1ex}
\begin{center}
\begin{tabular}{cc}
Sequent proofs
& ($\wedge,\vee,\textsf{C},\textsf{W}$-bureaucracy)\\[1ex]
\Large$\downarrow$\\[.5ex]
Proof nets
& ($\textsf{C},\textsf{W}$-bureaucracy)\\[1ex]
\Large$\downarrow$\\[.5ex]
Combinatorial proofs
\end{tabular}
\end{center}
The arrows represent the abstraction from sequent calculus to proof
nets, and from proof nets to combinatorial proofs.  To the right, we
list the form of `bureaucracy' present at that layer, that is, the
connectives involved in representation redundancy, \ie, sensible rule
transpositions for identifying proofs.  ($\textsf{C}$ and $\textsf{W}$
stand for contraction and weakening.)

The definition of combinatorial proof is very simple, so we can give
it in full here.  Let $A$ be a formula of propositional classical
logic, generated by $\wedge$ and $\vee$ from literals (variables
$P,Q,\ldots$ and their negations $\overline{P},\overline{Q},\ldots$).
We identify a formula $A$ with its parse tree, a tree labelled with
literals at the leaves and $\wedge$ or $\vee$ at internal vertices. An
\defn{$\vee$-resolution} (or \defn{$\vee$-strategy}) 
of $A$ is any result of deleting one argument subtree from each $\vee$
(\cf\ \cite{HG03}).  A set $L$ of leaves of $A$ is a \defn{clique} of
$A$ if it is the set of leaves of a $\vee$-resolution of $A$.  A
\defn{combinatorial proof} of $A$ is an MLL proof net on a formula
$A'$ (viewed as an MLL formula, \ie, $\wedge$ = tensor, $\vee$ = par),
equipped with a label- and clique-preserving function from the leaves
of $A'$ to the leaves of $A$.  For example, here is a combinatorial proof of
Peirce's law, $((P\Rightarrow Q)\Rightarrow P)\Rightarrow
P\;=\;((\overline{P}\vee Q)\wedge
\overline{P})\vee P$\,:
\begin{displaymath}\thicklines
\begin{array}{c}
\\[1ex]
\overline{P}%
        \begin{picture}(0,0)%
                \put(-2,11){\qbezier(0,0)(27,30)(54,0)}%
                \put(-4,-3){\line(0,-1){21}}
        \end{picture}%
\wedge \overline{P}%
        \begin{picture}(0,0)%
                \put(-2,11){\qbezier(0,0)(9,13)(18,0)}%
                \put(0,-3){\qbezier(0,0)(6,-10.25)(12,-20.5)}%
        \end{picture}%
\vee (P%
        \begin{picture}(0,0)%
                \put(-2,-3){\qbezier(0,0)(6,-10.25)(12,-20.5)}%
        \end{picture}%
\vee P%
        \begin{picture}(0,0)%
                \put(-4,-3){\line(0,-1){21}}
        \end{picture}%
) \\[5ex]
\!\!\!\!\!\!((\overline{P}\vee Q)\wedge\overline{P})\!\vee\! P
\end{array}
\end{displaymath}
The MLL proof net is drawn above, with two axiom links.  The label-
and clique-preserving function is shown by the
%
vertical lines.\vspace{-1ex}
\begin{theorem}[Soundness and Completeness]
A formula of classical propositional logic is true (valid)
\emph{iff} it has a combinatorial proof.
\end{theorem}
The label- and clique-preserving function is a lax form of fibration.
(We prove this via \cite{Hug04b}).  Thus a combinatorial proof is a
`fibred' MLL proof net, and we obtain the slogan in the title of the
paper:
\begin{center}
\sl Classical logic \;\;\;=\;\;\; Fibred MLL
\end{center}
Any sequent calculus proof translates to a combinatorial proof in a
relatively obvious way.  For a suitable variant of sequent calculus,
one obtains a surjection (\ie, sequentialisation theorem).  Cut
elimination for combinatorial proofs retains the richness of sequent
calculus: its non-determinism is not confluent.
%
In contrast, direct translation of a sequent proof to a linking (the
set of axiom links traced down from the axioms) leads to a certain
degeneracy: cut elimination becomes confluent \cite{LS05}.  Also in
contrast to \cite{LS05}, the MIX rule in this setting is optional.

Combinatorial proofs, in a somewhat different guise, were first
presented in \cite{Hug04b}, with MIX implicit.

\small
\begin{thebibliography}{Hug04}

\bibitem[FP05]{FP05}
C.~F{\"u}hrmann and D.~Pym.
\newblock Order-enriched categorical models of the classical sequent calculus.
\newblock {\em J.\ Pure and Applied Algebra}, 2005.
\newblock To appear.

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

\bibitem[Gir91]{Gir91}
J.-Y. Girard.
\newblock A new constructive logic: Classical logic.
\newblock {\em Mathematical Structures in Computer Science}, 1(3):255--296,
  1991.

\bibitem[HG03]{HG03}
D.~J.~D. Hughes and R.~J.~van Glabbeek.
\newblock Proof nets for unit-free multiplicative additive linear logic
  (extended abstract).
\newblock {\em Proc.\ Logic in Computer Science '03}, 2003.

\bibitem[Hug04]{Hug04b}
D.~J.~D. Hughes.
\newblock Proofs without syntax.
\newblock Submitted for publication. Archived as math.LO/0408282 at arXiv.org,
  http://boole.stanford.edu/\~{\strut}dominic/papers, August 2004.

\bibitem[LS05]{LS05}
F.~Lamarche and L.~Stra{\ss}burger.
\newblock Naming proofs in classical propositional logic.
\newblock In {\em Proc.\ Typed Lambda Calculus '05}, Lecture Notes in Computer
  Science, 2005.
\newblock To appear.

\bibitem[Rob03]{Rob03}
E.~Robinson.
\newblock Proof nets for classical logic.
\newblock {\em J.\ Logic and Computation}, 13(5):777--797, 2003.

\end{thebibliography}
\end{document}
math0504028.extracted_bib
\begin{thebibliography}{Hug04}

\bibitem[FP05]{FP05}
C.~F{\"u}hrmann and D.~Pym.
\newblock Order-enriched categorical models of the classical sequent calculus.
\newblock {\em J.\ Pure and Applied Algebra}, 2005.
\newblock To appear.

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

\bibitem[Gir91]{Gir91}
J.-Y. Girard.
\newblock A new constructive logic: Classical logic.
\newblock {\em Mathematical Structures in Computer Science}, 1(3):255--296,
  1991.

\bibitem[HG03]{HG03}
D.~J.~D. Hughes and R.~J.~van Glabbeek.
\newblock Proof nets for unit-free multiplicative additive linear logic
  (extended abstract).
\newblock {\em Proc.\ Logic in Computer Science '03}, 2003.

\bibitem[Hug04]{Hug04b}
D.~J.~D. Hughes.
\newblock Proofs without syntax.
\newblock Submitted for publication. Archived as math.LO/0408282 at arXiv.org,
  http://boole.stanford.edu/\~{\strut}dominic/papers, August 2004.

\bibitem[LS05]{LS05}
F.~Lamarche and L.~Stra{\ss}burger.
\newblock Naming proofs in classical propositional logic.
\newblock In {\em Proc.\ Typed Lambda Calculus '05}, Lecture Notes in Computer
  Science, 2005.
\newblock To appear.

\bibitem[Rob03]{Rob03}
E.~Robinson.
\newblock Proof nets for classical logic.
\newblock {\em J.\ Logic and Computation}, 13(5):777--797, 2003.

\end{thebibliography}