Classical Semantic Tableaus
We now move to a discussion of semantic tableaus. Sequent proofs start with axioms and work forward to the formula being proved. They are often used for proof discovery, in which case they are run backwards, starting with the formula to be proved and working upward to axioms.
Tableaus take that feature and make it primary. As the name suggests, their origins were semantic—they can be thought of as searches for countermodels. Soundness and completeness have direct proofs, but because tableaus have a strong connection with sequents, we will simply use this connection to transfer these results that were already proved for sequents in Section 5.4.Tableaus are refutation systems; we will say what this means later. For those logics having tableau systems, machinery can vary quite a bit. At the heart of these systems, most commonly, is classical logic, and we sketch the ideas for that here.
For starters, let us assume formulas are built up from propositional letters using just
connectives will be added later. We introduce two
special symbols, T and F, and specify that T X and FX are signed formulas if X is a formula. The intended reading is that X is true, or false, respectively, but this might mean classically, or constructively, or at some possible world, depending on the logic in question. Because this is classical logic for now, Boolean truth and falsehood are the motivating intuitions behind T and F. For intuitionistic logic, signs are essential; for classical logic they could be dispensed with, but for our purposes it is much more convenient to have them.
A tableau proof is a labeled binary tree, where the labels are signed formulas meeting special conditions. A proof of X begins with a tree having only a root node, labeled F X. We noted earlier that tableaus are refutation systems—we want to show FX is impossible.
To this end a tree is “grown” using branch extension rules, one for each propositional connective and each sign (though we only discuss → for the time being). The initial tree and each subsequent tree is a tableau. The goal is to produce a tableau in which each branch contains an obvious contradiction. If we achieve this goal we conclude that F X cannot happen, X cannot be false, and so must be a tautology.Figure 5.1 shows the very simple branch extension rules for implication— the rule for T → is branching, the F → rule is not.
Figure 5.1 TableauRulesfor →
Tableaus are displayed as downward branching trees. Think of a tree as representing the disjunction of its branches, and a branch as representing the conjunction of the signed formulas on it. Because a node may be common to several branches, a formula labeling it, in effect, can occur as a constituent of several conjunctions, while being written only once. This amounts to a kind of structure sharing.
A tableau expansion is often discussed temporally—one talks about the stages of constructing a tableau, meaning the stages of growing a tree. The rules in Figure 5.1 are thought of as branch-lengthening rules. Thus, a branch
Figure 5.2 A Classical Tableau Example
Tableau rules are understood to be nondeterministic. At each stage we are allowed to choose a signed formula occurrence on a branch and apply a rule to it. Because the order of choice is arbitrary, there can be many tableaus for a single signed formula. Sometimes a prescribed order of rule application is imposed, but this is not basic to a tableau system. For example, Figure 5.3
Figure 5.3 A Classical Tableau Example Revisited
For all logics we consider, closure can be taken to be atomic.
That is, a branch is closed if it contains T P and F P where P is atomic, or it contains T ?. This corresponds to Atomic Axiomatization for sequents, see Theorem 5.5. We will always require atomic closure.Branch extension rules for classical connectives can be restricted to single use. That is, a tableau rule need never be applied to a signed formula occurrence on a branch more than once. The tableau rules allow for multiple usage, but it is never necessary. (This is not true for all logics, however, and modal logics are an example.) The tableau examples in Figures 5.2 and 5.3, in fact, follows a single use convention. All classical tableau rule applications here will follow this single use convention.
We now have the basics of classical tableaus. Other connectives can easily be added, either as primitive or as defined connectives. Figure 5.4 shows the rules for negation, conjunction, and disjunction. If the connectives are taken as defined, these rules are derivable rules. It is possible, and often very useful, to combine rules that appear similar into general conjunctive and disjunctive classes called a and β cases respectively. This is called uniform notation. It can be applied here as well, but we thought it would be information overload and have decided not to follow this route. More can be found about uniform notation in Smullyan (1963) where it was introduced, and in Smullyan (1968) and Fitting (1996).
To illustrate the full set of connectives, a classical tableau proof of :(X ^
Figure 5.4 Tableau Rules for :, Λ, and V
Figure 5.5 A Classical Tableau Example with Multiple Connectives
We have said nothing about how soundness and completeness are proved for tableaus.
This is an extensive topic in itself and is not the subject of this book. However, there is room for a few illustrative remarks.Soundness of tableau systems is usually given a direct proof, making use of the semantics for the logic. It also follows from the soundness of the sequent calculus, once a translation is defined in Section 5.9. There is also a proof-theoretic way of understanding tableaus that has relevance to the tableau quasi-realization algorithm that will be presented in Chapter 7. It has already been seen, for the sequent calculus, in Definition 5.2. The following is for classical logic, but the same ideas apply directly to the modal tableaus that will be discussed starting in the next section.
Pick your favorite axiomatic presentation of classical logic—details don't matter. If a tableau branch is closed, or can be continued to closure, the formula translation for that branch will be provable in that axiom system. Here is how to show this. If a branch is closed it is obvious; because both T P and F P will be on the branch the formula translation for the branch will be 
which is obviously a tautology and hence axiomatically provable. With a modest amount of work, one can show the following. If branch B extends in one step to a branch or branches having axiomatically provable formula translations, then B itself has an axiomatically provable formula translation. Then a kind of backward induction establishes the result for all closable branches.
As to completeness, we briefly sketch the ideas that were used for the sequent calculus, but applied to tableaus. If a tableau is constructed so that every signed formula has a rule applied to it on every branch on which it appears, the result will either be a proof or will yield a counterexample. This makes concrete the idea that tableaus are a search for a countermodel, and if none is 
left branch is not closed—this is not a proof. Furthermore, every nonatomic formula on the left branch has had a rule applied to it on that branch. Given our single use restriction, there is nothing more to do. And in fact, the open branch tells us why we failed to find a proof. If we set X to be false (5 or 7) and Y to be false (6), every formula on the branch will have the truth value corresponding its sign, so
will be false, and hence is
not a tautology.
Figure 5.6 An Unclosed Classical Tableau
5.6