10.4.2 A special Rule for Model Generation

A special Rule for Model Generation.

Still there's one thing that we can do to exploit the information in an existential quantification also with respect to the individuals that we already know of: We can enumerate all the individuals we know of, plus a new one, disjunctively. In terms of tableaux this means we will continue on a branch of its own with each of the constants that are already there, and on yet another one with a newly invented constant. This is done by the following rule, which we will use instead of when generating models:

A new rule...

The rule makes a case distinction between the cases that the scope holds for one of the already known individuals (those in the Herbrand base) or a currently unknown one (for which it introduces a witness constant ).

Let us look at our example again, this time with the -rule applied:

...fixes our problem

On the rightmost branch we get the model we could already generate with our old -rule. The middle branch, where we instantiated the quantified formula with , closes because we know that . But on the leftmost one we get a model that we couldn't generate before: Mutz purrs.

As an exercise, convince yourself that the rule is admissible!