path: root/Master/texmf-dist/doc/latex/bussproofs/BussGuide2.tex

%
%Documentation by Peter Smith, July 2004, March 2012
%
%comments to peter_smith@me.com
%

\documentclass[11pt]{article}
\usepackage{graphicx}
\usepackage{amssymb}
%\usepackage{epstopdf}

\usepackage{bussproofs}
\def\fCenter{{\mbox{$\vdash$}}}

\DeclareGraphicsRule{.tif}{png}{.png}{`convert #1 `basename #1 .tif`.png}

\textwidth = 6.5 in
\textheight = 9 in
\oddsidemargin = 0.0 in
\evensidemargin = 0.0 in
\topmargin = 0.0 in
\headheight = 0.0 in
\headsep = 0.0 in
\parskip = 0.0in
\parindent = 0.2in


\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}

\begin{document}

%%%%%%%%%%%%%%%%%%
%%% 
%%% front matter
%%%
%%%%%%%%%%%%%%%%%%

\thispagestyle{empty}
\begin{center}
	\Huge{\LaTeX\ for Logicians}\\[16pt]
	\huge{\texttt{bussproofs.sty}}\\[8pt]
	\huge{A User Guide}\\[16pt]
\end{center}
\vspace{0.5in}
\tableofcontents
\vspace{0.3in}
\begin{center}
	\fbox{\parbox{4.5in}{\begin{center}The latest version of \texttt{bussproofs.sty}
	 is 1.1, July 2011.\end{center}}}
\end{center}
\vspace{0.4in}
\begin{center}
	\small{Guide version 1.1 March 2012. Corrections/suggestions to
	\texttt{peter}\_$\!$\_\texttt{smith@me.com}}
	\\
	\small{\LaTeX\ for Logicians is at \texttt{http://www.logicmatters.net}}
\end{center} 
\newpage

%%%%%%%%%%%%%%%%%%
%%% 
%%% main matter
%%%
%%%%%%%%%%%%%%%%%%
\section{Introduction}

\noindent Sam Buss's powerful and flexible package {\texttt{bussproofs.sty}} offers macros for setting natural deduction and sequent proofs in two different styles. The key difference between the two styles is illustrated by the difference between
\begin{prooftree}
\AxiomC{$\Gamma, A, B \vdash C$}
\UnaryInfC{$\Gamma, A \vdash (B \to C)$}
\UnaryInfC{$\Gamma  \vdash (A \to (B \to C))$}
\end{prooftree}
and
\begin{prooftree}
\Axiom$\Gamma, A, B\ \fCenter\ C$
\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
\end{prooftree}
In one style, the sequents above and below the inference line are centered; in the other, the sequents are placed so as to align their deducibility signs. 

We can divide {\texttt{bussproofs.sty}}'s  commands for building  proofs into four types:
\begin{itemize}\setlength{\itemsep}{0.0in}
\item \emph{the structural commands} for producing proof trees in the  \emph{centering} style;
\item \emph{more structural commands} for producing proof trees in the  \emph{sequent-aligning} style;
\item \emph{additional commands} for adding labels, and changing the setting of inference lines (selecting double, dashed lines, etc.);
\item \emph{fine-tuning commands} for adjusting the spacing and layout of the proof. 
\end{itemize}
{\texttt{bussproofs.sty}} also provides an additional command which enables some very laconic shorthand for the most commonly used commands. We describe these in Section~\ref{abbrev}; but we avoid using shorthand until the full commands have been explained and made familiar.



\section{`Centered' proofs: the structural commands}
\subsection{The commands} There are four basic proof-building commands for producing proofs in the centered style:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\AxiomC{=\textit{form}\verb=}=
\item   \verb=\UnaryInfC{=\textit{form}\verb=}=
\item   \verb=\BinaryInfC{=\textit{form}\verb=}=
\item   \verb=\TrinaryInfC{=\textit{form}\verb=}=
\end{description}
\end{quote}  
where `\textit{form}' holds the place for a formula or sequent. Note
\begin{itemize}\setlength{\itemsep}{0.0in}
\item The use of the surrounding `\verb={}='s is mandatory. 
\item By default, \textit{form} is set in text mode: if you want to set some or all of \textit{form} in math mode, then you need to use \verb=$='s in the usual way.
\end{itemize}
Chaining a series of those commands, however, is not enough to cause a proof to be set. To display a proof you must use one of
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\DisplayProof=, a command placed at the end of a list of proof-building commands, which produces an in-line proof at the current insertion point.
\item   \verb=\begin{prooftree} ... \end{prooftree}=, an environment which contains a list of proof-building commands, and which produces a  proof in a centered display. 
\end{description}
\end{quote}  
Again, note
\begin{itemize}\setlength{\itemsep}{0.0in}
\item The \verb=\DisplayProof= command  allows you to put proofs anywhere normal text might appear; for example, in a paragraph, in a table, in a tabbing environment, etc. 
\item To generate a proof in a centered display, do \emph{not} use \verb=$$ ... $$= or \verb=\[ ... \]=.
\end{itemize}

\subsection{Usage} It will be a \emph{lot} clearer if we start with examples rather than begin with an abstract description of the principles for chaining proof-building commands! So here goes \ldots
\begin{quote}
\begin{verbatim}
\AxiomC{A}
\UnaryInfC{D}
\DisplayProof
\end{verbatim}
\end{quote}
produces the one-step proof
\AxiomC{A}
\UnaryInfC{D}
\DisplayProof
in the current line. While
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\BinaryInfC{D}
\end{prooftree}
\end{verbatim}
\end{quote}
displays the proof 
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\BinaryInfC{D}
\end{prooftree}
centered and set off from the surrounding text. So it will be no surprise to learn that
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\AxiomC{C}
\TrinaryInfC{D}
\end{prooftree}
\end{verbatim}
\end{quote}
produces the proof
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\AxiomC{C}
\TrinaryInfC{D}
\end{prooftree}
Two comments:
\begin{itemize}\setlength{\itemsep}{0.0in}
\item You'll get an error message if there's a mismatch between the arity of the \verb=\...aryInfC= command and the number of inputs.
\item \texttt{bussproof.sty} does not allow arbitrary numbers of premisses appearing as separate \textit{form} items above the inference line.
\end{itemize}

So much for one-step proofs. Now things get a little more fun \ldots. 
Consider
\begin{quote}
\begin{verbatim}
\begin{prooftree}
     \AxiomC{A}
     \AxiomC{B}
     \AxiomC{C}
     \BinaryInfC{D}
     \BinaryInfC{E}
\end{prooftree}
\end{verbatim}
\end{quote}
This produces the proof
\begin{quote}
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\AxiomC{C}
\BinaryInfC{D}
\BinaryInfC{E}
\end{prooftree}
\end{quote}
Why? Think of the first \verb=\BinaryInfC= command as `using up' as premisses the two axioms immediately above it. Then the second \verb=\BinaryInfC= command takes as premisses `D' immediately above it and then searches up to the next `unused' item, i.e. `A'. The inputs to a particular \verb=\BinaryInfC= command are then set right-to-left in the order in which the {command} finds them as it looks {up} the series of commands. Which means, as we want, that {the inputs to a particular inference are set left-to-right in the same order as they occur in the chain of commands}.

It probably helps if we set out the proof-building commands like this:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{A}
                 \AxiomC{B}
                           \AxiomC{C}
                     \BinaryInfC{D}
        \BinaryInfC{E}
\end{prooftree}
\end{verbatim}
\end{quote}
That pretty much replicates the layout of the tree we want. This indeed is one of the \emph{very} nice features of \texttt{bussproofs.sty} -- the instructions to build a proof-tree can be set out to look very like the proof we want. 

Suppose then that we want to set a tree that is arranged like this:
\begin{prooftree}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\end{prooftree}
The following does the trick:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{A}
   \UnaryInfC{B}
                 \AxiomC{C}
        \BinaryInfC{D}
                                \AxiomC{E}
                                              \AxiomC{F}
                                    \BinaryInfC{G}
                                    \UnaryInfC{H}
                    \BinaryInfC{J}
\end{prooftree}
\end{verbatim}
\end{quote}
In sum, then, the rule to produce a given tree is
\begin{quote}
\emph{Set out the commands for the left-hand sub-proof first; and then within a sub-proof, do its left-hand sub-sub-proof first; and so on.}
\end{quote}
Two more points about general structure: 
\begin{itemize}\setlength{\itemsep}{0.0in}
\item The command \verb=\noLine= can be inserted before any inference command to suppress the drawing of an inference line.
\item Null axioms are allowed! 
\end{itemize}
Hence, the commands
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{$A \lor B$}
         \AxiomC{[$A$]}
         \noLine
         \UnaryInfC{$C$}
              \AxiomC{[$B$]}
              \noLine
              \UnaryInfC{$C$}
         \TrinaryInfC{$C$}
\end{prooftree}
\end{verbatim}
\end{quote}
yield
\begin{prooftree}
\AxiomC{$A \lor B$}
\AxiomC{[$A$]}
\noLine
\UnaryInfC{$C$}
\AxiomC{[$B$]}
\noLine
\UnaryInfC{$C$}
\TrinaryInfC{$C$}
\end{prooftree}
And we can use the fact that null axioms are allowed to generate natural deduction proofs with formulae overlined to indicate the discharge of premisses (by treating the formula to be overlined as a unary inference from a null axiom). For example:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{$P$}
                   \AxiomC{}
                   \UnaryInfC{$\neg P$}
          \BinaryInfC{$\bot$}
          \UnaryInfC{$\neg\neg P$}
\end{prooftree}
\end{verbatim}
\end{quote}
generates the proof
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}

\subsection{More than three premisses}

So far we've only considered inference steps that take one premiss (like double negation), two premisses (like modus ponens), or three inputs (like or-elimination). But Buss proofs in fact supplies -- should you want it -- the capacity to deal with four or five premisses. The syntax is as you would expect. We have the two commands
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\QuaternaryInfC{=\textit{form}\verb=}=
\item   \verb=\QuinaryInfC{=\textit{form}\verb=}=
\end{description}
\end{quote}  
These aren't pointless! After all, you might want to illustrate the $\omega$-rule thus:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\AxiomC{$\varphi(0)$}
\AxiomC{$\varphi(1)$}
\AxiomC{$\varphi(2)$}
\AxiomC{$\varphi(3)$}
\AxiomC{$\ldots$}
\QuinaryInfC{$\forall n\varphi(n)$}
\end{prooftree}
\end{verbatim}
\end{quote}
to give
\begin{quote}
\begin{prooftree}
\AxiomC{$\varphi(0)$}
\AxiomC{$\varphi(1)$}
\AxiomC{$\varphi(2)$}
\AxiomC{$\varphi(3)$}
\AxiomC{$\ldots$}
\QuinaryInfC{$\forall n\varphi(n)$}
\end{prooftree}
\end{quote}




\section{`Sequent-aligned' proofs: the structural commands}
\subsection{The commands} There are four basic proof-building commands for producing proofs in the second style:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\Axiom$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\UnaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\BinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\TrinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\end{description}
\end{quote}  
where `\textit{form}' holds the place for a formula or formulae, and \verb=\fCenter= marks the point of alignment.
\begin{itemize}\setlength{\itemsep}{0.0in}
\item This time, the use of the surrounding `\verb=$='s is mandatory; and material between the `\verb=$='s is set in math mode.
\item The `\verb=\fCenter=' is by default just a place-marker; however, it can be redefined to be printed character such as a sequent arrow or turnstile.
\end{itemize}
And for multi-premiss usage, we also have the additional commands:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\QuaternaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\QuinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=\end{description}
\end{quote}  

\subsection{Usage}
The basic usage is illustrated by the following:
\def\fCenter{}
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\Axiom$A, B, C, D,\fCenter\ E, F$
\UnaryInf$A, B,\fCenter\ C,  D, E, F$
\end{prooftree}
\end{verbatim}
\end{quote}
\begin{prooftree}
\Axiom$A, B, C, D,\fCenter\ E, F$
\UnaryInf$A, B,\fCenter\ C,  D, E, F$
\end{prooftree}
Now let's redefine \verb=\fCenter= to be the turnstile surrounded by spaces. Then
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\def\fCenter{\ \vdash\ }
\Axiom$A, B, C, D \fCenter E, F$
\UnaryInf$A, B \fCenter C,  D, E, F$
\end{prooftree}
\end{verbatim}
\end{quote}
produces 
\begin{prooftree}
\def\fCenter{\ \vdash\ }
\Axiom$A, B, C, D \fCenter E, F$
\UnaryInf$A, B \fCenter C,  D, E, F$
\end{prooftree}
However, it is in general preferable to redefine \verb=\fCenter= using an \verb=\mbox= as in the next example (this allows more options):
\begin{quote}
\begin{verbatim}
\def\fCenter{\mbox{\Large$\rightarrow$}}
\begin{prooftree}
\Axiom$\Gamma, A, B\ \fCenter\ B$
\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
\end{prooftree}
\end{verbatim}
\end{quote}
produces
\def\fCenter{\mbox{\Large$\rightarrow$}}
\begin{prooftree}
\Axiom$\Gamma, A, B\ \fCenter\ B$
\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
\end{prooftree}
And this time, since the \verb=\def\fCenter{...}= command precedes the following \verb=prooftree= environment, it will stay in effect until overridden later in the document. 
\begin{itemize}
\item The chaining of multiple sequent-aligning commands to build complex proofs works just as with the earlier centering-style commands.
\item It should go without saying that the point of the \verb=\BinaryInf$...$= command is not to align the sequent turnstile, (arrow, or whatever) in the conclusion of the two-premiss inference with the turnstiles in the premisses, but to provide a new alignment point for later sequents. 
\item Mixing and matching sensible combinations of \verb=C{...}=-type centering commands and \verb=$...$=-type sequent-aligning commands is in fact legitimate. 
\end{itemize}
Thus, to illustrate the last point,  
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}
\AxiomC{$\Gamma \vdash A$}
\AxiomC{$A, B \vdash C$}
\BinaryInf$\Gamma, B \fCenter C$
\UnaryInf$\Gamma \fCenter B \to C$
\end{prooftree}
\end{verbatim}
\end{quote}
is acceptable, and yields
\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}
\AxiomC{$\Gamma \vdash A$}
\AxiomC{$A, B \vdash C$}
\BinaryInf$\Gamma, B \fCenter C$
\UnaryInf$\Gamma \fCenter B \to C$
\end{prooftree}



\section{Additional layout commands}
Conventionally, the proof
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}
needs labelling. This section describes how to add labels to proofs, and also how to change the style of inference-line (to double lines, etc.).

\subsection{Adding labels} There are two commands for decorating a proof with labels:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\LeftLabel{text}= 
\item   \verb=\RightLabel{text}=
 \end{description}
\end{quote}  
These put \verb=text= as a label to the left/right of the next inference line (and they work even if \verb=\noLine= is used and line isn't actually drawn).

So, for example, the commands
\begin{quote}
\begin{verbatim}
\begin{prooftree}
         \AxiomC{$\Gamma, A \vdash B$}
    \LeftLabel{Conditional Proof:}
         \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
\end{verbatim}
\end{quote}
will generate
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \LeftLabel{Conditional Proof:}
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
You can insert spacing commands and other text commands into the label text, so e.g. substituting  \verb=\LeftLabel{Conditional Proof:\quad}= will generate
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \LeftLabel{Conditional Proof:\quad}
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
However, there is also a global command for adjusting the position of labels, and in general it might be better to use that. 

You can reduce the size of the label font, so that 
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
				  \RightLabel{\scriptsize(1)}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \RightLabel{\scriptsize(1)}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}
\end{verbatim}
\end{quote}
will set the conventionally annotated proof
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
				  \RightLabel{\scriptsize(1)}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \RightLabel{\scriptsize(1)}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}
\subsection{Varieties of inference lines} The inference line between premiss and derived conclusion defaults, as we've seen, to a single solid line. But this can be changed, either locally or more globally. The local change commands are
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\noLine=
\item   \verb=\singleLine=
\item   \verb=\doubleLine=
\item   \verb=\solidLine=
\item   \verb=\dottedLine=
\item   \verb=\dashedLine=
\end{description}
\end{quote}
Each applies to the next inference, and line-\emph{number} and line-\emph{type} commands can be combined: so, for example,
\begin{quote}
\begin{verbatim}
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \doubleLine\dashedLine
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
\end{verbatim}
\end{quote}
produces the following:
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \doubleLine\dashedLine
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
There are corresponding global commands that can be placed anywhere in a proof and will affect all succeeding lines unless and until overridden.
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\alwaysNoLine=
\item   \verb=\alwaysSingleLine=
\item   \verb=\alwaysDoubleLine=
\item   \verb=\alwaysSolidLine=
\item   \verb=\alwaysDottedLine=
\item   \verb=\alwaysDashedLine=
\end{description}
\end{quote}
Here `succeeding lines' means `succeeding in the (vertical) order that commands are given' not `logically succeeding'. (Note: Sam Buss comments that \verb=\alwaysNoLine= is `untested': but it seems to work fine on my trials.)

So, for example, the commands
\begin{quote}
\begin{verbatim}
\begin{prooftree}
     \alwaysNoLine
     \AxiomC{$\Pi_1$}
     \UnaryInfC{$A$}
               \AxiomC{[$A$]}
               \UnaryInfC{$\Pi_2$}
               \UnaryInfC{$B$}
               \alwaysSingleLine
               \UnaryInfC{$A \to B$}
         \BinaryInfC{$B$}
\end{prooftree}
\end{verbatim}
\end{quote}
produces the following:
\begin{prooftree}

\alwaysNoLine
\AxiomC{$\Pi_1$}
\UnaryInfC{$A$}
\AxiomC{[$A$]}
\UnaryInfC{$\Pi_2$}
\UnaryInfC{$B$}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\BinaryInfC{$B$}
\end{prooftree}

\subsection{Turning a proof upside down}

Suppose you want to set a proof-tree the other way up, i.e. get a \emph{downward} branching tree with the root at the \emph{top}. Then you need the command \verb=\rootAtTop=. Note, this applies only to the current proof. If you want to make this behaviour persistent, then use \verb=\alwaysRootAtTop=. (The default behaviour can be restored using \verb=\rootAtBottom= and \verb=\alwaysRootAtBottom=.)


\section{Fine-tuning the proof layout}
\texttt{bussproofs.sty} allows a lot of user-modification of the default style of proof lay-out, either by global modifications of parameters, or by local tweakings within a proof. We'll divide these commands into
\begin{itemize}\setlength{\itemsep}{0.0in}
\item commands for determining \emph{where a whole proof is set};
\item commands for \emph{adjusting the `geometry' within a proof};
\item commands for \emph{redefining line styles}.
\end{itemize}

\subsection{Where a proof is set}

\noindent\textbf{i}\quad The amount of \emph{space above and below} a proof-tree display is set by the parameter
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item    \verb=\proofSkipAmount=  
\end{description}
\end{quote}
Its default setting is \verb={\vskip.8ex plus.8ex minus.4ex}=. This can be modified, and negative values of \verb=\vskip= are accepted. 

To change the space above the tree (which you'll want to do if the top lines are null axioms, which generate additional white space), use \verb=\def\proofSkipAmount{\vskip= \emph{new-skip}\verb=}= \emph{before} the opening command \verb=\begin{prooftree}=; the size of the skip after the proof can then be reset by another \verb=\def\proofSkipAmount{...}= command before the proof closes.

\vspace{12pt}\noindent\textbf{ii}\quad  Whole proofs set using the proof-tree environment can be \emph{nudged sideways} by using the command \verb=\hskip= \emph{nudge} (no brackets!) placed e.g. immediately after the command \verb=\begin{prooftree}=. A positive value of \emph{nudge} such as \verb=0.5in= shifts the proof to the right, a negative value such as \verb=-20pt= shifts the proof left.

\EnableBpAbbreviations
\vspace{4pt}\noindent\textbf{iii}\quad  For \emph{vertical positioning of in-line proofs}, compare \AXC{$\phi \land \psi$}\UIC{$\phi$}\DP with \centerAlignProof\AXC{$\phi \land \psi$}\UIC{$\phi$}\DP and \bottomAlignProof\AXC{$\phi \land \psi$}\UIC{$\phi$}\DP\hspace{-6pt}. The first is set vertically centered within the current line (the default position), the second is set rather lower so (at least with a one-step proof) the inference line is on a level with the foot of the current line, and the third is set with the conclusion aligned to the current line. To produce the second tree, use the command \verb=\centerAlignProof=; to produce the third tree, use \verb=\bottomAlignProof=; to restore the default positioning
use \verb=\normalAlignProof=.

\subsection{Layout within a proof}
In this section, we consider the use of

\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\ScoreOverhang= (controls how far inference lines `overhang' the premisses/conclusion)
\item   \verb=\extraVskip= (controls the extra space above and below lines)
\item   \verb=\labelSpacing= (controls horizontal space separating labels and inference lines)
\item   \verb=\defaultHypSeparation= (controls horizontal spread of proof tree)
\item   \verb=\insertBetweenHyps= (can be used to adjust position of hypotheses in next inference)
\item    \verb=\kernHyps= (nudges hypotheses left or right)
\end{description}
\end{quote}

\noindent\textbf{i}\quad The default setting of \verb=\ScoreOverhang= is \verb={4pt}=. This produces e.g. the tree
\begin{prooftree}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\end{prooftree}
Inserting, for example, the line \verb=\def\ScoreOverhang{1pt}= at the beginning of the chain of proof-commands changes (improves!?) the look of the tree by reducing the `overhang' of inference lines:
\begin{prooftree}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\end{prooftree}
\vspace{12pt}
\noindent\textbf{ii}\quad The default setting of \verb=\extraVskip= is \verb={2pt}=, which inserts 2 pt spacing above and below an inference line, as in the last two proofs. To increase this throughout the proof, use e.g.  the line \verb=\def\extraVskip{3pt}= at the beginning of the chain of proof-commands to get
\begin{prooftree}
\def\extraVskip{3pt}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\end{prooftree}
You can also change the interline skip on the fly, during a proof, to improve alignments. Thus compare
\begin{center}
\alwaysNoLine
\AxiomC{$\Pi_1$}
\UnaryInfC{$A$}
\AxiomC{[$A$]}
\UnaryInfC{$\Pi_2$}
\UnaryInfC{$B$}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\BinaryInfC{$B$}
\DisplayProof
\hspace{24pt}
\alwaysNoLine
\AxiomC{$\Pi_1$}
\def\extraVskip{1pt}\UnaryInfC{$A$}
\AxiomC{[$A$]}
\def\extraVskip{2pt}
\UnaryInfC{$\Pi_2$}
\UnaryInfC{$B$}
\def\extraVskip{2.5pt}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\BinaryInfC{$B$}
\DisplayProof
\end{center}
Here, the proof on the left was created by using the default settings, and the one on the right was created by the following commands (with the two proofs being set in the same line in a \verb=\begin{center} ... \end{center}= environment):
\begin{quote}
\begin{verbatim}
\alwaysNoLine
\AxiomC{$\Pi_1$}
\def\extraVskip{1pt}
\UnaryInfC{$A$}
          \AxiomC{[$A$]}
          \def\extraVskip{2pt}
          \UnaryInfC{$\Pi_2$}
          \UnaryInfC{$B$}
          \def\extraVskip{2.5pt}
          \alwaysSingleLine
          \UnaryInfC{$A \to B$}
     \BinaryInfC{$B$}
\DisplayProof
\end{verbatim}
\end{quote}

\vspace{4pt}
\noindent\textbf{iii}\quad The default setting of \verb=\labelSpacing= is \verb={3pt}=, which inserts 3 pt between inference lines and their associated labels. To change this, use the command \verb=\def\labelSpacing{=\emph{new-space}\verb=}= at the beginning of a chain of proof-commands. For example
\begin{prooftree}
\def\extraVskip{2pt}
\def\labelSpacing{8pt}
\def\ScoreOverhang{1.2pt}
\AxiomC{$(\phi \land \psi)$}
\UnaryInfC{$\psi$}
\AxiomC{}
\RightLabel{\scriptsize(1)}
\def\extraVskip{1pt}
\UnaryInfC{$\neg\psi$}
\def\extraVskip{2pt}
\BinaryInfC{$\bot$}
\RightLabel{\scriptsize(1)}
\UnaryInfC{$\neg(\psi \land \phi)$}
\end{prooftree}
is set with \verb=\def\labelSpacing{8pt}=.




\vspace{12pt}

\noindent\textbf{iv}\quad The default setting of \verb=\defaultHypSeparation= is \verb={\hskip.2in}=. Increase this to spread out a spread out a proof horizontally, decrease it to squeeze the proof. Thus compare
\begin{center}
\def\defaultHypSeparation{\hskip .1in}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\DisplayProof
\hspace{24pt}
\def\defaultHypSeparation{\hskip.5in}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\DisplayProof
\end{center}
where the proof commands for the left tree start \verb=\def\defaultHypSeparation{\hskip .1in}=, and for the right tree start \verb=\def\defaultHypSeparation{\hskip .5in}=.

\vspace{12pt}
\noindent\textbf{v}\quad Use the command \verb=\insertBetweenHyps{=\emph{stuff}\verb=}= before a binary or trinary inference command to insert \emph{stuff} between the hypotheses of that inference. The obvious use of this is to adjust the spacing between the hypotheses of that inference, by using e.g. 
\verb=\insertBetweenHyps{\hskip -4pt}=.

\vspace{12pt}
\noindent\textbf{vi}\quad Use the command \verb=\kernHyps{=\emph{kern}\verb=}= before an inference command to nudge the hypotheses of that inference right by the distance \emph{kern}, e.g. \verb=4pt=. Negative values of \emph{kern} nudge the hypotheses to the left.

\subsection{Inference-line styles}

In this section, we consider the use of

\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\ruleScoreFiller= (sets the style of solid rules)
\item   \verb=\dottedScoreFiller= (sets the style of dotted rules)
\item   \verb=\dashedBuildScore= (sets the style of dashed rules)
\end{description}
\end{quote}
\noindent\textbf{i}\quad The default setting of \verb=\ruleScoreFiller= is \verb={\hrule}=, and in \LaTeX\ an unqualified \verb=\hrule= command produces a horizontal line of thickness 0.4 pt. To change the rule's thickness, use the command \verb=\def\ruleScoreFiller{\hrule height= \emph{new-thickness}\verb=}=.

\vspace{12pt}
\noindent\textbf{ii}\quad The default setting of \verb=\dottedScoreFiller= is \verb={\hbox to4pt{\hss.\hss}}=. The default for \verb=\dashedBuildScore= is \begin{quote}
\verb={\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}=
\end{quote} Both defaults can be altered to produce any other desired type of line.
 
\section{Abbreviating the commands}\label{abbrev}
Using the command \verb=\EnableBpAbbreviations= enables some laconic shorthand for various commands:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\AX= and \verb=\AXC= abbreviate \verb=\Axiom= and \verb=\AxiomC=
\item   \verb=\UI= and \verb=\UIC= abbreviate \verb=\UnaryInf= and \verb=\UnaryInfC=
\item   \verb=\BI= and \verb=\BIC= abbreviate \verb=\BinaryInf= and \verb=\BinaryInfC=
\item   \verb=\TI= and \verb=\TIC= abbreviate \verb=\TrinaryInf= and \verb=\TrinaryInfC=
\item   \verb=\DP= abbreviates \verb=\DisplayProof=
\end{description}
\end{quote}
The enabling of these short abbreviations is optional, and users should guard against conflicts with commands  from other
macro packages or their own defined abbreviations.

\end{document}