Skip to content
No description, website, or topics provided.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
images
README.md
qtree-examples.pdf
qtree-examples.tex

README.md

LaTeX and Tableaux

Charles H. Pence

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, you should be.

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.

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:

A completed tree

Which is generated by the following block of LaTeX:

\vspace{\baselineskip}
\Tree
[.{\framebox{$\neg(\lozenge(p \lor q) \supset (\lozenge p \lor \lozenge q)), w_0$}}
[.{\framebox{$\lozenge(p \lor q), w_0$} \\
\framebox{$\neg(\lozenge p \lor \lozenge q), w_0$}}
[.{$w_0 R w_1$ \\
\framebox{$p \lor q, w_1$}}
[.{\framebox{$\neg \lozenge p, w_0$} \\
\framebox{$\neg \lozenge q, w_0$}}
[.{$\square \neg p, w_0$ \\
$\square \neg q, w_0$}
[.{$\neg p, w_1$ \\
$\neg q, w_1$}
[.{$p, w_1$} [.$\otimes$ ] ]
[.{$q, w_1$} [.$\otimes$ ] ]
]
]
]
]
]
]
\vspace{\baselineskip}

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

The set to satisfy

So, to begin, we start by writing the following code, which sets out our premises on the trunk of the tree:

Tree containing only premises

\Tree
[ .{$(p \supset q)$ \\
$(r \lor \neg q)$ \\
$\neg r$ \\
$\neg p$}
]

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:

First formula boxed, branches added

\Tree
[ .{\framebox{$(p \supset q)$} \\
$(r \lor \neg q)$ \\
$\neg r$ \\
$\neg p$}
[.{$\neg p$}
]
[.{$q$}
]
]

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:

First two formulas boxed, work complete

\Tree
[.{\framebox{$(p \supset q)$} \\
\framebox{$(r \lor \neg q)$} \\
$\neg r$ \\
$\neg p$}
[.{$\neg p$}
[.{$r$}
]
[.{$\neg q$}
]
]
[.{$q$}
[.{$r$}
]
[.{$\neg q$}
]
]
]

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:

Unsatisfiable branches closed, tree finished

\Tree
[.{\framebox{$(p \supset q)$} \\
\framebox{$(r \lor \neg q)$} \\
$\neg r$ \\
$\neg p$}
[.{$\neg p$}
[.{$r$}
[.$\otimes$ ]
]
[.{$\neg q$}
]
]
[.{$q$}
[.{$r$}
[.$\otimes$ ]
]
[.{$\neg q$}
[.$\otimes$ ]
]
]
]

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 essentially a LaTeX form of this document.

TeX source
PDF output

If you have any questions, feel free to e-mail me. Happy typesetting!

Update Nov. 2014: Simon Tommerup wrote me to report a funny incompatibility between these tableaux and the LaTeXiT TeX editing environment. Since these tableaux can get so large, there's a tendency for them to be cut off on the right-hand side when you insert them as equations. The fix, as offered by LaTeXiT's author, Pierre Chatelier, is to use the geometry package: add something like

\usepackage[paperwidth=40cm]{geometry}

to the preamble, and everything should work.

You can’t perform that action at this time.