Changing the Tableau Representation
So far tableaus have been trees with nodes labeled by signed formulas, and these formula occurrences could be common to multiple branches. While this has advantages for some purposes, it does not when our quasi-realization construction is introduced in Chapter 7.
We will be associating a set of quasi- realizers with each signed formula occurrence in a tableau. How that is done will depend on the history of the branch below a given occurrence. If an occurrence is common to more than one branch it has more than one history, and things become ambiguous. Our simple solution is to change the way tableaus are represented so that a certain amount of that history is explicitly present. The result is, essentially, the block tableaus of (Smullyan, 1968, chapter XI)—our version differs only in that we impose a single-use restriction where Smullyan did not. This is of no deep significance for present purposes.Definition 5.19 (Block Tableau) A block tableau is similar to a tableau except that each node in the tree is labeled with a finite set of signed formulas (such a set is called a block). A block tableau proof of X begins with a root node labeled with {FX). For classical logic, branches are grown using the rules in Figure 5.13, and these rules are only applied to the lowest blocks on branches. A block is closed if it contains T P and F P for some atomic P, or if it contains T ? (we require atomic closure). A block tableau branch is closed if it contains a closed block, and a block tableau is closed if each of its branches is closed. A classical block tableau proof of X is a closed block tableau beginning with {F X).
Notationally we often (but not always) display a block without using the enclosing curly brackets customary with sets. Also, when we write a block as B, Z we mean it is the set whose members are those of B, together with signed formula Z.
This notation generally assumes that Z is not part of B. Single use conditions are ensured by our deleting from a block the signed formula to which we have applied a rule. For example, the T → rule in Figure 5.13 is to be read as follows. If a block tableau has block B, TX → Y at a node, then we can branch and add two new blocks, B, F X and B, T Y, and these do not contain the occurrence of TX → Y. Similarly for the other rules.There is one misleading aspect to the notation in Figure 5.13. In the rule for T :, for instance, it may happen that F X already occurs in B, in which case the display of B, F X below the line is not correct—it should be simply B. We allow this mild abuse, rather than complicating notation.
Figure 5.13 Classical Block Branch Extension Rules
An ordinary classical tableau can easily be converted into a block tableau.
Simply replace each signed formula occurrence Z on a branch by the set of all signed formulas on the branch that have not had a rule applied to them at the point when Z was added to the branch. Informally, a block is a snapshot of a tableau branch at a particular stage of the construction. For instance, Figure 5.5 shows a standard tableau proof. Figure 5.14 shows the same proof, converted to a block tableau.
Figure 5.14 Tableau from Figure 5.5 as a Block Tableau
Next we reformulate the S4 tableau rules in this style, building in the notion of single usage for tableau rules. Of course rules for other modal logics could also be presented in a similar fashion, but S4 will be sufficiently representative. Single usage is a bit tricky for S4 block modal rules, which are shown in Figure 5.15. Single usage for the F ? rule is automatic because the
Figure 5.15 S4 Modal Block Branch Extension Rules
Block tableaus provide the easiest to describe link between tableaus and
Figure 5.16 A Longer Block Tableau Proof than Necessary
sequents.
Here is a brief description of a translation from block tableau proofs to sequent proofs; the other direction is similar and a description is omitted. Start with a block tableau. Replace each block B with the sequent
where
are as in Definition 5.14 (ignore the distinction between crossed out and uncrossed out formulas). Finally, turn the tree over. Figure 5.17 shows an example of an S4 block tableau conversion to sequents.
Finally, block annotated tableaus will be needed. They have a similar structure to the block tableaus discussed earlier, and we can safely omit the obvious details in our presentation here.
Figure 5.17 Block Tableau to Sequent Conversion: (a) An S4 Block Tableau Proof, (b) Intermediate Conversion Stage, (c) A Sequent Proof