4. 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 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:

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 Ži­vanović, 2012–2017). 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.

Clea Rees’s prooftrees package is based on forest. Here’s a fully annotated tree produced by this package:

Screengrab copy

See my document for more examples.

Links checked 12 February 2017

7 Responses to 4. Tree proofs

  1. Clea F. Rees says:

    Note that prooftrees CAN now be used with bussproofs. Either load bussproofs first. Or load prooftrees with option ‘tableaux’: ‘\usepackage[tableaux]{prooftrees}’. Either way, you can then use ‘prooftree’ for bussproofs trees and ‘tableau’ for prooftrees trees. Take care not to load the tableaux package instead which, as far as I can tell, does something completely different. The tableaux package is loaded with ‘\usepackage{tableau}`. However, should you need bussproofs, tableaux and prooftrees in the same document, I *think* it should still all play nicely together, as tableaux does not seem to define a ‘tableau’ environment, but only provides a ‘tableau’ .sty file. It would help a bit if package authors didn’t commandeer not one, but multiple names – if bussproofs provided ‘bussproof’, say! In the beginning, package authors believed names would always be plentiful and life simple and good. By now, of course, life is no longer so simple.

  2. Clea F. Rees says:

    You don’t need to hard code the line references, by the way.

  3. Jan von Plato says:

    Rather than “illustrated tree” one could write “annotated tree,” that’s the linguists’ term for syntax trees with nodes annotated by expressions.

  4. Simon says:

    Is anybody else able to get prooftrees to compile on the 2016 tex distribution? I was able to get it to work once I updated to the 2017 distribution but unfortunately I’m having difficulties submitting the paper to ArXiv as they’re still running the 2016 distribution. Is there any fix for this? Otherwise, great package!

    • Peter Smith says:

      At a guess, some compatibility issues may be inherited from changes in forest.sty which prooftrees.sty depends on.

    • Clea F. Rees says:

      As Peter Smith indicates, this is probably due to changes in prooftrees and/or forest, though it is just possible it could be pgf/tikz related. In general, forest and prooftrees have been updated together or only a few days apart, at most, so an updated TeX Live should (hopefully) include a version of prooftrees compatible with the installed version of forest. However, if you try to combine a newer prooftrees with an older forest, it probably won’t work. Assuming that ArXiv has prooftrees and forest installed, they should be compatible. But you might need to adjust the code for your trees to avoid syntax not supported by older versions. But without knowing the error and without any idea what’s in your code, it is hard to give more specific advice.

Leave a Reply to Jan von Plato Cancel reply

Your email address will not be published. Required fields are marked *