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).

The illustration was set using the pst-tree package which is part of the powerful pstricks family of packages. This is a little cumbersome to use; and to produce nice results you sometimes need to resort to trickery (e.g. to get the apex of a branching pair to sit a little below the formula above, you have to put an empty node just below the formula and branch from there).

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:

Another package written for linguists is synttree, which has a pleasing simple syntax in use (Matijs van Zuijlen).

Another powerful graphics package which can be used for trees has also been recommended:

  • pgf and TikZ (Till Tantau 2005-: a general TeX macro package for generating graphics, with a user-friendly syntax layer called TikZ). See §17 of the manual.
  • tikz-qtree provides a macro for drawing trees with TikZ using the easy syntax of qtree.

Another possibility, I suppose, is to turn upside down trees as used for setting Gentzen-style natural deduction proofs. Thus, if you use the recommended bussproofs, 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

Links checked 11 July 2013

Leave a Reply

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

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>