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.


In conclusion, I no longer have a concern about the overlapping sorts,
and I do not object to having overlapping sorts in RIF.



Best, Jos

-- 
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