Re: comments on current version BLD document: symbols, datatypes, semantics

> Michael Kifer wrote:
> > Just wanted to infuse a healthy doze of a reality check regarding the
> > following:
> > 
> > Jos wrote:
> >>>>    g- the value space is required to be a subset of the domain.  This
> >>>> means that every interpretation includes all value spaces of all data
> >>>> types.  This is unnecessary.
> >>> So what? It makes the definition simple and uniform.
> >> It makes every domain infinite. For most kinds of rules (especially
> >> those without equality in the head) this is not really a problem.
> >> However, as soon as we have full use of equality, or deal with
> >> extensions in the direction of FOL, then one often wants to talk about
> >> finite models.
> >>
> >>
> >> It also makes rule sets which only contain rules such as Forall ?x,?y
> >> (?x=?y)  inconsistent. I claim that this is undesirable.
> > 
> > Apart from everything that was said about it, you should remember that we
> > have function symbols. So, the domain is infinite whether you have data
> > types or not.
> 
> This would be the case if you use a Herbrand universe.  Otherwise, it is
> not necessarily the case that the domain is infinite.

Recall that unsatisfiability reduces to unsatisfiability problem over
Herbrand models.  Only "uninteresting" models would have finite domains.

I hope that you realize that your argument about finite models in the
presence of function symbols is a red herring.


	--michael