Consequences for Model Generation

We did not start our tableaux with a (negated) theorem in the example before. This means what we hoped for was to arrive at a saturated tableaux, containing a model for our input. But we obviously never will.

We did not start our tableaux with a (negated) theorem in the example before. This means what we hoped for was to arrive at a saturated tableaux, containing a model for our input. But we obviously never will.

Infinite Model

Nonetheless there is of course a model for our input. To convince ourselves of this, let us just take the set of natural numbers as the domain and choose as the set of natural numbers , and to be the set of pairs , where is a natural number. Then ``Every man has a father'' just means ``Every natural number has a successor'', which is of course true in the natural numbers. The set of natural numbers is infinite and this is why our tableaux couldn't generate it. But the fact that our model generation procedure couldn't find a model based on the natural numbers does not contradict the claim that it would have found a finite model if there was one.

Finite Model Property

In essence, we have just shown by an example that full first-order logic no longer has the finite model property (in contrast to PLNQ). Up to now, models have always been finite. With rule-like formulae such as the one we have been looking at, it is now possible to force models to be infinite. Of course the finite model property has now become highly desirable for our application of model generation in discourse interpretation - losing it is a considerable disadvantage.

Model Human Behaviour

But this consideration is largely theoretical, since we humans also face the same infiniteness problems; We could derive infinite chains of ancestors with the same world knowledge as well, yet we stop short of this in practice. To model this behaviour the model generation procedure would have to be equipped with a criterion when to stop saturation, even if it is not (theoretically) complete. Defining such a criterion is a current topic in research. In our implementation (as in most other implementations), we tackle the problem of infiniteness by simply fixing the maximal number of instantiations of an existential quantifier. If you allow 10 instantiations, our system will generate exactly 10 fathers for the example above and halt.