This page is a brief tutorial about Paul Taylor’s macro script for typestting the kind of proof trees used in Gentzen’s natural deduction and sequent calculus. Please feel free to discuss this script or other related matters on Talk about prooftrees, and correct or expand upon what follows on this page.
Paul Taylor’s prooftree macros for proofs are nice and robust. I have used them for years. Here’s how you use them. A proof tree has the general form
\prooftree X \justifies Y \endprooftree
where <code>X</code> and <code>Y</code> could be anything you can typeset in mathematics mode. In particular, <code>X</code> and <code>Y</code> can both be prooftrees themselves. (The spacing is a bit odd you make <code>Y</code> a prooftree, but that’s OK, because the natural way I think of these things is from bottom up. What justifies <code>Y</code>? It’s this proof from <code>X1</code> to <code>X2</code>…) So, you can typest a complicated more proof like this
\prooftree \prooftree X_1 \justifies X_2 \endprooftree \prooftree X_3 \justifies X_4 \endprooftree \justifies Y \endprooftree
In this case we get a tree like this.
It’s possible to simplify the notation (all that writing <code>prooftree</code> could get tedious.) Instead, inside a prooftree environment the <code>\[</code> and <code>\]</code> brackets are redefined to begin and end proofrees, so you get the simpler
\prooftree \[ X_1 \justifies X_2 \] \[ X_3 \justifies X_4 \] \justifies Y \endprooftree
If you prefix a <code>\justifies</code> with <code>\using{X}</code> then the horizontal justification line is appended with the <code>X</code> (again, in math mode). This is how you typeset rule labels in proofs.
I prefer my rule labels to be smaller than the material in the proof, and my rule labels take the following form <code>[</code> ∧ R<code>]</code>, so I’ve made the following definitions:
\def\usng#1#2{\using{\textrm{\tiny{$[#1$#2$]$}}}} \def\usngsub#1#2#3{\using{\textrm{\tiny{$[#1$#2$_{\textrm{#3}}]$}}}}
So <code>\usng{\land}{R}</code> typesets the left bracket and the conjunction in math mode, the <code>R</code> in text mode, and the right bracket in math mode. <code>\usngsub{\land}{L}{1}</code> does the same sort of thing, but a subscripted 1, in text mode, is added below the <code>L</code>.
Finally, the prooftree environment interacts well with the colour commands available elsewhere in LaTeX. The following code typesets the proof below, with some subproofs shaded different colours to pick them out.
\begin{widematter} $\prooftree \[ p\vdash p \justifies p\land (q\lor(r_{1}\land r_{2}))\vdash p \] \hspace{-0.2cm} \[ \colorbox{Faintest}{\[ \[ q\vdash q \usng{\lor}{R$_{1}$}\justifies q\vdash q\lor(r_{1}\land r_{2}) \] \hspace{-0.1cm} \[ \colorbox{Fainter}{\[ \[ r_{1}\vdash r_{1} \usng{\land}{L$_{1}$}\justifies r_{1}\land r_{2}\vdash r_{1} \] \[ r_{2}\vdash r_{2} \usng{\land}{L$_{2}$}\justifies r_{1}\land r_{2}\vdash r_{2} \] \usng{\land}{R}\justifies r_{1}\land r_{2}\vdash r_{1}\land r_{2} \]} \usng{\lor}{R$_{2}$}\justifies r_{1}\land r_{2}\vdash q\lor(r_{1}\land r_{2}) \] \usng{\lor}{L}\justifies q\lor(r_{1}\land r_{2})\vdash q\lor(r_{1}\land r_{2}) \]} \justifies p\land (q\lor(r_{1}\land r_{2}))\vdash q\lor(r_{1}\land r_{2}) \] \justifies p\land (q\lor(r_{1}\land r_{2}))\vdash p\land (q\lor(r_{1}\land r_{2})) \endprooftree$ \end{widematter}
Notice the use of a <code>widematter</code> environment (see PnC Page Layout for more on this), and the use of a <code>\hspace</code> directive to push two subproofs just a little closer together.
The colour declarations are
\definecolor{Faint}{rgb}{0.75,0.75,0.75} \definecolor{Fainter}{rgb}{0.84,0.84,0.84} \definecolor{Faintest}{rgb}{0.92,0.92,0.92}
If you have any comments on these prooftrees, or questions about how to make prooftree do what you want it to, don’t hesitate to add questions here.