4. Tree proofs

A non-closing tree

The task is to set proof-trees in the style of the illustrated tree, the sort of tableau that appears in e.g. Richard Jeffrey’s classic Formal Logic or my own Introduction to Formal Logic). There are number of options, but none are purpose-designed exactly for tableau proofs in the way that e.g. bussproofs is built for ND proofs. So often bits of trickery are needed to get nice-looking trees. Here are some options:

• The illustration was set using the pst-tree package which is part of the powerful pstricks family of packages. But this can be a little cumbersome to use, e.g. to fine-tune the placing of the diagonal lines.
• The qtree.sty package (Jeff Siskind and Alexis Dimitriadis) was written for typesetting linguists’ syntactic trees, and can also be adapted to logicians’ purposes. There is a useful tutorial for using qtree for logic here: LaTeX and tableaux (Charles Pence)
• Another package originally written for linguists is synttree, which has a pleasing simple syntax in use (Matijs van Zuijlen).
• pgf and TikZ (Till Tantau 2005-: a general TeX macro package for generating graphics, with a user-friendly syntax layer called TikZ). tikz-qtree provides a macro for drawing trees with TikZ using the easy syntax of qtree.
• Newest and possibly best, there is forest (Sašo Ži­vanović, 2012–2015). This is another package that  pro­vides PGF/TikZ-based apparatus for draw­ing trees, and looks very flexible. There is a nice worked example in the first answer here which shows how to fine-tune the output. (If you want to add line-numbers/commentary to the tree, then you should look here at the ‘new answer’ by Clea F. Rees).

Another possibility, I suppose, is to turn upside down buss proofs trees (the command \rootAtTop will specify that a proof has its root at the top, and \alwaysRootAtTop makes this behaviour persist). Of course, you won’t then get nicely sloping lines joining nodes at branch points!

For more advice on trees, see