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.

Best, Jos

> 
> 
> 	--michael  

-- 
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
In heaven all the interesting people are
missing.
  - Friedrich Nietzsche