Tree proofs
A non-closing tree
The task is to set proof-trees in the style of the tree alongside, i.e. tableaux of the sort that appear in e.g. Richard Jeffrey’s classic Formal Logic or the first edition of my own Introduction to Formal Logic.
A very flexible package, allowing you also to add line numbers (if you want) and line-by-line justifications is provided by
- Prooftrees (Clea Rees, 2016–24). Read the package documentation for many examples of its power and flexibility (example below, and also see my document Setting Tableaux using Prooftrees).
Because of issues with the complex packages that prooftrees.sty invokes, a document with many trees does become slow to typeset. However the 2024 version of prooftrees allows you to use the “memoize” package so that (unchanged) diagrams are not re-processed every time you re-typeset your document, considerably speeding things up.
Older options for setting tableaux often require bits of trickery to get nice-looking trees (and don’t supply the option of line numbers etc.). I’ll mention them, however, in case they may be enough for your purposes. Two first options are
The qtree.sty package (Jeff Siskind and Alexis Dimitriadis), written for typesetting linguists’ syntactic trees, can also be adapted to logicians’ purposes.
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.
For a document with some illustrations of trees set with these, see Proofs in LaTeX (Alex Kocurek, 2017).
Further options include
The pst-tree package, used for the illustration above. This package 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.
Another package originally written for linguists is synttree, which has a pleasing simple syntax in use (Matijs van Zuijlen).
Then there is forest (Sašo Živanović, 2012–2017). 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 annotated tree produced by this package:
See my document for more examples.
Links checked 8 October 2024