The task is to set proof-trees in the style of the illustrated tree, the sort of tableaux that appears in e.g. Richard Jeffrey’s classic Formal Logic or my own Introduction to Formal Logic). Despite the very wide use of such tableaux, there has only lately appeared a purpose-designed package which looks excellent and very flexible, allowing you also to add line numbers (if you want) and line-by-line justifications:
- Prooftrees by Clea Rees. Read the package documentation for many examples of its power and flexibility (example below).
Older options for setting tableaux often required bits of trickery to get nice-looking trees (and didn’t supply the option of line numbers etc.). I’ll mention them, however, in case they may be enough for your purposes.
- The illustration above was set using the pst-tree package which is part of the powerful pstricks family of packages which you may already know. 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.
- Then there is forest (Sašo Živanović, 2012–2015). This is another package that provides PGF/TikZ-based apparatus for drawing trees, and looks very flexible. There is a nice worked example in the first answer here which shows how to fine-tune the output.
Clea Rees’s prooftrees package is based on forest. Here’s a fully documented tree produced by this package:
Links checked 3 April 2016