Quantifiers in Tableaux More about first order logic

X,  t: ALLv A X,  t: ALLv A,  t: Atv * X,  t: SOMEv A X,  t: Atv † X,  f: ALLv A X,  f: Atv † X,  f: SOMEv A X,  f: SOMEv A,  f: Atv * *   In an open branch, must be instantiated to all t in X or A †   In a closed branch, t must be a name not in X or A.

:   ALL and SOME in tableaux

In an earlier chapter of these notes, we introduced semantic tableaux as a systematic way of reasoning about the truth conditions of formulae and consequently of deciding the validity or invalidity of sequents. The tableau method carries over to quantified logic, though with the extra complexity it no longer provides a decision procedure. The tableau editing tool provided with this notes allows for quantifiers as well as connectives.

As in the propositional case, tableau construction proceeds by drawing out the consequences of supposing that a set of truth value attributions to formulae all hold together. As in the propositional case, this can be used to construct models or to test sequents for validity, the latter by taking as the set to be modelled the premises of the sequent labelled as true together with its conclusion labelled false (see closed below). The rules for developing branches by analysing formulae with connectives as their main operators are taken over unchanged, as is the rule for closing a branch when it contains a contradiction.

New rules are needed to deal with formulae of the forms  ALLvA and  SOMEvA. Note that NOTALLvA has the same truth conditions as SOMEvNOTA, and dually NOTSOMEvA is equivalent to ALLvNOTA, so the rules for the cases with label f are analogous to the ones for the opposite cases with label t, as was the case for the connectives AND and ORtheRules. In addition to the special conditions on instances, of course every quantified formula must be instantiated to at least one term in every open branch.

Developing a true universally quantified formula is intuitively simple. ALLvA says that A is true of everything, so for every term t that occurs in a branch containing the universal formula there should also be the formula A^t_v. There is assumed to be a name a that occurs (virtually) in every branch if no other name does, so the rule for developing the universal has to be applied at least once before the branch can be regarded as finished: this corresponds to the fact that the domain of an interpretation cannot be empty. Since it always remains possible that further names may be introduced in the development of any open branch, we cannot simply check off the analysis of the universal and declare it done: we may have to revisit it and apply the rule again if another name arises. This is reflected in the formal statement of the rule in that the universal formula is still present below the line, in case it needed again.

Where an existential formula SOMEvA is labelled as false, the assumption is that nothing satisfies A. That is to say, everything fails to satisfy A, so the treatment of a false existential is just like that of a true universal except that the label is f instead of t. The last of the four rules in theRules reflects this reasoning.

:   Closed tableau: ALLx (Fx IMP Gx),  SOMEx (Fx AND Hx) ⊨   SOMEx (Gx AND Hx) Click here to do it yourself.

The existential SOMEvA with label t says that there is some object or other with property A. In the tableau, this means that there should be some name or other of which the description A is asserted. This name could be one of those already introduced in the branch being extended, or it could be a new one. Since a new one is guaranteed not to occur in any formula currently involved, it must be completely arbitrary, in the sense that nothing can depend on which name it is, so there is no point in introducing two such names for the same existential formula. Standardly, the analysis of t: SOMEvA consists in extending the branch by adding the labelled formula t: A^m_v, where m is a name which does not yet occur in the branch. When this happens, of course, any true universal or false existential formulae above it in the branch must be instantiated to the new name.

closed shows an example. The existential formula SOMEx (Fx AND Hx) is true (line 2), meaning that there exists at least one thing that is F and H, so we pick one arbitrarily and give it a name so that we can reason about it. That happens at line 4, where the name a is introduced. The new formula Fa AND Ha has a connective as its main operator, so it can be treated using the propositional logic rules.

An alternative version of the rule for the existential quantifier allows branching in the manner of disjunction, one of the branches containing t: A^m_vas above, and the others containing t: A^n′_vfor names n′ which do already occur in the branch. Such alternative branches cannot help to prove that a set of formulae is unsatisfiable, of course, but they can enable the tableau method to show satisfiability in some cases where it might otherwise not terminate. When we actually use tableaux to find finite models, for example to show the invalidity of sequents, we use this alternative, more permissive, form of the rule. Branches formed using the existing names are optional. If one of them remains open, that shows consistency and we can stop constructing the tableau; if they all close, that shows nothing, so in that case branching to a new name is obligatory. The tableau editor implements this idea in a dynamic way, by allowing you to backtrack on the choice of term used, so if a name that has previously been used leads to a contradiction, you can go back and try a different name.

Just as a false existential formula is treated like a true universal one except for the difference of label, so a false universal formula behaves like a true existential one. Again this is intuitively obvious: if it is false that everything is F, then there must be something that is not F. The second rule in theRules is therefore just like the third, with the quantifiers and labels flipped.

From some logical points of view, this is not so obvious, but from the standpoint of tableaux as a way of implementing the classical semantics of quantifiers, it clearly holds.

:   Open tableau refuting ALLx (Fx OR Gx),  ⊨   ALLxFx OR ALLxGx Click here to do it yourself.

The two tableaux in closed and open are the same shape, but whereas the former is closed, showing the associated sequent to be valid, the latter has an open branch. Following the open branch back from the leaf to the root of the tree, we may collect all the atomic formula with their labels:

t: Fb
t: Ga
f: Gb
f: Fa

By examination of this list, we see easily what is needed to model the atoms: there are two distinct names a and b which need different objects to refer to, so let the domain of the interpretation be {α, β} where I(a) = α and I(b) = β. In order to make Fa false and Fb true, set I(F) = {β} and similarly set I(G) = {α}. Because this interpretation was generated from the assignments of truth values to atoms required by the analysis, it must be the case that it suffices to give all formulae in the branch the truth values with which they are labelled, and so to refute the sequent – and so it does.

Consider, for example, the formula ALLxGx which occurs in the open branch with the label f. The modelling condition for the universal quantifier says that a formula ALLvA^v_mis false for I over a domain D iff A is false for some interpretation J over D which is an m-variant of I. We can let m in this case be, for instance, a. Then A is the formula Ga, which is true for I, but letting J be the interpretation just like I except that J(a) = β, we have immediately that Ga is false for J. That makes ALLx Ga^x_afalse for I as required.

For the walkthrough, click here.