Re: basic decisions underlying DAML-ONT (defined classes)

  Dan Connolly wrote:
> > [b] This also shows that DAML-ONT's is not similar to SHOE's 
><DEF-RENAME> element,
> > as Jeff Heflin suggested, since <DEF-RENAME> is a syntactic 
>operation concerning class names, not a relation between two classes?
>
>I don't think so. First, it's a little odd to say
>(as I did) that equivalentTo is a relation between *two* classes,
>since it asserts that the classes are identical; i.e.
>there's just one class.

In general, relations hold between two things which might be the same 
thing. There are two in the sense that there are two arguments to the 
relation. So its not really odd.

>Second, in formal systems, identity comes down to the
>sort of syntactic manipulations that Jeff H. is talking
>about, no? i.e. the semantics of
>	(= X Y)
>is nothing more and nothing less than saying that if
>we see
>	(P X)
>we can write
>	(P Y)
>and vice versa. (This is, of course, an informal
>paraphrase of the substitution-of-equals-for-equals
>inference rule that may, in particular formal
>systems, take pages and pages to state precisely.)

This isnt quite right. Identity really does not come down to 
syntactic manipulation. What identity means has to do with 
denotation, not rewriting. (X=Y) has the consequence that one can 
substitute (P X) for (P Y) (at least in any extensional context, but 
I guess DAML isnt likely to have modalitites in the near future), but 
its not quite the same thing. Making it the same (which is often 
called the identity of indiscernables) has been suggested as a 
logical rule (by Leibnitz, among others), ie if one can substitute (P 
X) for (P Y) and vice versa for any expression (P..) and it makes no 
difference, then X=Y.  But this rule is a lot more controversial and 
tricky to put into practice than a simple denotational meaning. 
First, it only works if that "any expression" really does mean ANY 
expression, and in a limited language like those in the OIL/CLASSIC 
tradition, it might well be impossible to provide enough kinds of 
expression to give intersubstitution the required semantic force. (It 
is pretty tricky even in first-order logic, and totally impractical 
in second-order logic.) Second, it is easy to slip into making the 
intersubstitution be trivial, since for example if the language 
itself contains equality then one can substitute X for one of the Y's 
in 'Y=Y' to get 'X=Y' (notice the power of 'any expression' again, 
where we have to allow substituting for just some of the Y's but not 
others), so the intersubstitution implies equality by sneaking in the 
back door; but then defining the meaning of equality by substitution 
becomes kind of circular. Third, the identity-of-indiscernables rule 
only works for a pure extensional logic, and definitional langauges 
are often given a dash of nonextensionality in their meanings, which 
completely wrecks intersubstitibility. For example, it usually 
wouldnt be OK to substitute Y for X in something which means (define 
X to be Y), since that would make all definitions vacuous: they would 
all be equivalent to (define X to be X). And finally, a lot of people 
object to the principle on just philosophical or pragmatic grounds. 
Maybe things seem to have all the same properties but we will find 
out later that they are distinct; it's happened before, God knows. If 
we accept the intersubstitution criteria then either we have to keep 
changing our minds about what equals what, or else we have to refuse 
to allow any new information to pollute the substitutivity. Neither 
of these seem like a sensible way to approach the Web.

Pat Hayes

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Monday, 16 October 2000 11:33:02 UTC