Setting tableaux / downward-branching trees

The task is to set proof-trees in the style of the illustrated tree (which proves the invalidity of the inference-- cf. e.g. Jeffrey's Formal Logic or my own Introduction to Formal Logic). [Oops, excuse missing negation sign!]

The illustration was set using the pst-tree package which is part of the pstricks family of packages. This was recommended as the best option in a recent exchange on comp.text.tex (see below).

This is a little cumbersome to use but produces quite nice results -- and it shouldn't be too difficult to define commands to wrap up some of the trickery. (However, at the moment, I couldn't easily get the sort of control over the angle of branching that I'd ideally like.)

The following package written for typesetting linguists' syntactic trees can be adapted to logicians' purposes, though my attempts weren't terrifically successful.

• qtree.sty (Jeff Siskind and Alexis Dimitriadis)

However, I've now found two useful pages

• LaTeX and tableau in logic (Charles Pence)
• Tableau using qtree (Ang Tong)

which show what can be done with qtree.

There is also an "unreleased" package which tweaks proof.sty (described here) to turn things upside down, which therefore produces a tableau proof with inferences marked by horizontal lines rather than sloping lines.

As noted above, the question of how to set Jeffrey-style treeswas recently asked on the usenet newsgroup comp.text.tex (22 June 2004). Replies include:

Home