Tableaus and Annotated Formulas
When we come to Realization Theorems, starting in Chapter 6, we will need to know about the polarity of subformulas, that is, which subformulas occur positively and which negatively.
We will also need to keep track of occurrences of necessity operators as formulas are decomposed. For many purposes this does not need anything elaborate, but as things get more complicated, good machinery will prove useful. Signed formulas themselves provide an appropriate device for the first of these problems. Annotated tableaus help to address the second issue. We discuss this machinery now, though it will not be employed until Chapter 7.If a formula contains only ë and : as propositional connectives, a subformula occurrence is positive if it is in the scope of an even number of negation signs, and it is negative if the number is odd. If other connectives are present, translate them into ë, : and use the previous definition. This is the idea, though we will make it more formal. (Actually, we will only be interested in the polarity of occurrences of necessitated formulas.) In Fitting (2009) annotated formulas were introduced to track the occurrences of necessitated formulas manipulated in the course of proofs, and in Fitting (2013a, b) a simpler version was used. It is the simpler version that we present now.
Definition 5.16 (Annotated Formula) An annotated modal formula is like a standard modal formula except for the following.
(1) Instead of a single necessity symbol ? there is an infinite family, ?1, ?2,..., called annotated modal operators. Formulas are built up as usual, but using annotated modal operators instead of ?. The important condition is that in an annotated formula, no annotation may occur twice.
(2) If A is an annotated formula, and A' is the result of replacing all annotated modal operators, ?n, with ?, regardless of annotation, then A' is a conventional modal formula.
We say A is an annotated version of A', and A' is an unannotated version of A.Annotations are purely for bookkeeping purposes. Semantically they are ignored. Thus ?n and ? are understood to behave alike in Kripke models, so that a modal formula and an annotated version of it evaluate the same at each possible world. In tableaus the propositional rules function the same way whether or not annotations are present. Thus for instance, if
occurs on a branch we can add
and
to the branch end, and similarly for the other rules. The definition of,
for S4 becomes the following.
, and similarly for other modal logics. And because we require atomic closure, closure conditions are not affected by annotations.
Given all this, Figure 5.12 shows an annotated version of the S4 proof given in Figure 5.11. Every modal tableau proof can be turned into an annotated proof simply by annotating the modal operators appearing in the root, and then propagating these annotations downward through the tree. And similarly for other modal logics as well, of course.
Signed formulas are useful for keeping track of the polarity of subformulas. We do need to make a somewhat arbitrary decision about whether, in F X, say, the occurrence of X should be counted as positive or as negative. Because a tableau proof of X will start with F X, it is most convenient for us to consider such an occurrence as a positive one, and an occurrence of X in T X as negative, though this may be thought backwards for some other purposes.
Once this decision has been, the key observation is that the conjunctive and disjunctive classical tableau rules from Section 5.5 respect polarity. For instance, suppose we use the F → tableau rule to conclude T X and F Y from FX → Y. Well, if X → Y is positive according to our earlier informal characterization, the occurrence of X will be negative and the occurrence of Y will be positive, matching the way we said we would be understanding the signs.In fact, it is only necessitated formulas whose polarity we will be interested in, and annotated versions at that. Below is a recursive characterization of polarity for this case. It will be used extensively in Chapter 7. In the definition we talk about a formula X being a subformula of a signed formula, say TZ or F Z, by which we mean it is a subformula of Z. Recall that an annotation can occur at most once in an annotated formula so, for instance,
occurs as a subformula of a conjunction, it must occur in exactly one of the conjuncts, and similarly for disjunctions and implications.
Definition 5.17 (Polarity) We define the polarity of necessitated subformulas of an annotated signed formula.
5.9