Re: Disjoint vs. overlapping sorts

>> Regarding my action:
>>
>> "talk to Michael Kifer and have one of your post the results to the
>> list" about the resolution of
>> issue 31 (the question was about translating from OS to DS) (action 287).
>>
>>
>> My original concern was that, when translating from the situation of
>> disjoint sorts to a situation of overlapping sorts, and entailment would
>> not be preserved, e.g.:
>>
>> forall x,y (x=y)
>> p(a)
>> q(b)
>>
>> entails q(a) in the case of overlapping sorts (since p and q are
>> interpreted as the same object), but not in the case of disjoint sorts
>> (because the variables x and y are interpreted in the individual domain,
>> and p, q are interpreted in the unary predicate domain).
>>
>> When talking to Michael, we came to the conclusion that the above
>> formulas are actually not proper RIF formulas for the case of disjoint
>> sorts, since the symbols do not have an associated sort.
>> The formulas would be represented in the following way:
>>
>> forall x^I,y^I (x^I=y^I)
>> p^P1(a^I)
>> q^P1(b^I)
>>
>> where I is the sort of individuals, and P1 is the sort of unary
>> predicates.
>>
>> In the case of disjoint sorts, the following formulas are theorems:
>>
>> forall x^I,y^P1 (x^I != y^P1)
>> forall x^I,y^P2 (x^I != y^P2)
>> forall x^P1,y^P2 (x^P1 != y^P2)
>> ......
>>
>> We can thus axiomatize disjoint sorts in the overlapping sorts example.
>>  This is, however, not necessary if we restrict ourselves to formulas
>> which are allowed to be written in the disjoint sorts case (i.e. no
>> equality statements involving different sorts).
>>
>> The following can be easily shown (and would need be to be part of some
>> RIF document which describes how languages with disjoint sorts
>> interoperate with RIF):
>>
>> Let phi and psi be two disjoint-sort formulas, then
>>
>> phi |=ds psi    iff     phi |=os psi
>>
>> where |=ds is entailment in the case of disjoint sorts, and |=os is
>> entailment in the case of overlapping sorts.
> 
> I'm not quite sort how this addresses the issue you raised but if you
> are convinced then fine.
> 
> However, I'm also not instantly convinced it is correct for all
> plausible interpretations of "overlapping sorts".
> 
> Consider OWL/full, map class extensions to unary predicates, then:
> 
>    C^I = D^I  |=os  C^P1 = D^P1
> 
> but
> 
>    NOT   C^I = D^I  |=ds  C^P1 = D^P1
> 
> Are (C^I = D^I) and (C^P1 = D^P1) not "disjoint-sort formulae"?

Sorry, I should have defined "disjoint-sort formula" more clearly. I
meant to restrict the formulas to textbook-style FOL, which means that
it is only possible to write equality between terms which are
interpreted in the individual domain (i.e. have the sort I).

So,
C^P1 = D^P1 is not a disjoint-sort formula.

> Or does the proposed model theory for RIF with overlapping sorts differ
> from the OWL approach sufficiently to invalidate the first entailment?

The first entailment is perfectly valid in RIF.


Best, Jos


> 
> Dave

-- 
Please note my new email address:
                         debruijn@inf.unibz.it

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