Posted on 05 Nov 2009
For my PHI 340 at Princeton, I found myself needing to typeset lots of tableaux-style proofs in the style of our textbook, Possibilities and Paradox, An Introduction to Modal and Many-Valued Logic by Beall and van Fraassen. The same sorts of tableaux proofs appear in Tomassi’s Logic. Here’s a tutorial teaching you how to typeset them in LaTeX, using a couple of freely-available packages.
First of all, it’s assumed that the reader is already familiar with the LaTeX typesetting system and its various and sundry intricacies. It’s a fairly difficult thing to learn, but once you’ve got it, it’s incredibly useful. For those looking to get started, I just happen to have a tutorial right over here.
Qtree, the tree-making package I’m using in this document, is part of TeX Live. If you aren’t using TeX Live, however, you’ll need to download qtree from the author’s site. For *nix users, drop this file into your texmf tree, usually located at /usr/share/texmf, in the tex/latex/qtree folder, and do whatever you need to do to make your TeX distribution update its filename cache. For MiKTeX on Windows, assuming you took the default install location of the texmf folder (c:\texmf), make a new directory at c:\texmf\tex\latex\qtree and drop qtree.sty there. Then, go to Start -> Programs -> MiKTeX -> MiKTeX Options and click “Refresh Now” under “File name database” on the first screen.
With that out of the way, we’re ready to actually start creating some documents. The qtree syntax takes a bit of getting used to at first, but all in all, the structure of the LaTeX document pretty effectively mirrors the final structure of the tree.
To begin, create a basic LaTeX document in your normal manner. I’d recommend 12pt in the document type, or you’ll run into some readability problems.
In case you’ve never typeset any sort of formal logic in LaTeX before, here’s the full set of logical connectives and symbols that you should be concerned with:
UPDATE 2/4/08: I’ve added a formatted symbol (using the custom math symbol commands) thanks to Kevin Klement that provides a proper “tilde” unary-not symbol, in addition to the “hook” unary-not symbol that was already listed. Thanks!
Two more notes I almost forgot: to get this full set of symbols, you’ll need to be sure to include the amssymb, latexsym, and amsmath packages. Also, qtree uses PostScript specials, which means PDFLaTeX refuses to process such documents. You’ll need to do standard LaTeX and then run dvi2pdf or ps2pdf to get PDF files (both those programs should come with any reasonably decent TeX implementation).
With the preliminaries now fully out of the way, let’s start creating some trees. First a big, relatively daunting example from my latest problem set:
Which is generated by the following block of LaTeX:
As I said above, this is meant to look relatively daunting. The actual construction of trees such as this is relatively simple. Let’s walk through writing the tree given as an example on p. 40 of B&vF, which tests the following argument: is the following set satisfiable (in a language with no restrictions on the world-relationship R)?
So, to begin, we start by writing the following code, which sets out our premises on the trunk of the tree:
A few things to be careful of here: Note that the entire contents of a tree node must be surrounded by curly braces (a convention not entirely unfamiliar to LaTeX users), and also note the period before the starting curly brace. The best way to continue the explanation is by example. Now, following standard tableaux rules for CPL, we box the first formula and create the two branches at the lowest level of the tree:
Notice that we simply start two new branches after the closing brace of the contents of the current node. Both of these branches look exactly the same as the trunk, beginning with a period and with their contents surrounded by curly braces. Also note the \framebox command to box the first formula, and the fact that even in nodes with only one formula, I go ahead and return/indent the closing bracket of the node, which makes it easier to add subnodes later on. Now, box the second formula, and add those new branches to the two lowest levels of the tree in exactly the same manner as before:
Of course, at this point, branches one, three, and four are closed off, with branch two remaining open (and thus this set is satisfiable). The tree is finished like so:
Not too terribly hard, no? For the sake of examples, I’m going to provide the TeX files both for a basic introduction that is essetially a LaTeX form of this document.
If you have any questions, feel free to e-mail me. Happy typesetting!
