Re: RDF Semantics: use of functions IEXT / ICEXT

>>  >
>>>First, the truth of the axiomatic triple
>>>
>>>rdfs:range rdfs:domain rdf:Property .
>>>
>>>and the semantic conditions on rdfs:domain together require that
>>>
>>><x,y> inIEXT(I(rdfs:range)) implies x in ICEXT(I(rdf:Property))
>>>
>>>which in turn, by applying the condition (definition if you like :)
>>>
>>>IP= ICEXT(I(rdf:Property))
>>>
>>>means that
>>>
>>><x,y> in IEXT(I(rdfs:range)) implies x in IP
>>>
>>>Similarly y is in IC, using a different axiomatic triple.
>>>
>>>Is this more convincing?
>>
>>No: you use in this reasoning the conditions which
>>I claimed are not complete in their statement.
>
>I do not think that I do use them. I will present the argument in more 
detail.
>
>1.    I |= rdfs:range rdfs:domain rdf:Property .         [axiomatic 
triple]
>2.    <I(rdfs:range), I(rdf:Property)> in IEXT(I(rdfs:domain)) 
>[1., basic RDF truthconditions]
>3.   <x,y> in I(rdfs:range)  implies  x in ICEXT(I(rdf:Property)) 
>[2., semantic conditions on rdfs:domain]
>4.  <x,y> in I(rdfs:range)  implies x in IP  [3., definition of IP]
>
>Note, step 3 does not depend on x being in any particular class; it 
>simply uses the semantic conditions in the form they have in the 
>document. None of this derivation implicitly assumes anything other 
>than what is stated, and it has as a conclusion the 'assumption' that 
>x is in IP. An exactly similar derivation (replace rdfs:domain by 
>rdfs:range, rdf:Property by rdfs:Class and IP by IC) shows that y is 
>in IC. So these assumptions are derivable, so are not needed.
>
>>The domain and range conditions as they are now formulated
>>implicitly assume that x is in IP and y is in IC,
>
>If you still maintain that these assumptions are used implicitly, 
>please give details of where the above derivation fails.

Your proof works, contrary to what I said earlier.
It is satisfactory that this can be proved.
I apologize that I did not look closely enough to your
previous version of the proof.

It still seems to me that the proof uses an implicit 
assumption.  To be precise, in Step 3.
The following description of the proof puts this step under 
the microscope.

Claim: If I is an rdfs-interpretation and <u,v> is in I(rdfs:range) 
then u is in IP and v is in IC
and similarly for rdfs:domain.

Proof:
>1.    I |= rdfs:range rdfs:domain rdf:Property .         [axiomatic 
triple]
>2.    <I(rdfs:range), I(rdf:Property)> in IEXT(I(rdfs:domain)) 
>[1., basic RDF truth conditions]
3a. If <x,y> is in IEXT(I(rdfs:domain)) [and x is in IP and y is in IC]
and <u,v> is in IEXT(x) then u is in ICEXT(y)
[full semantic condition on rdfs:domain]

(Note: such an addition is needed because otherwise it is not clear
that the function invocations IEXT(x) and ICEXT(y) are legal, as 
it is not yet proved that x is in IP (the domain of IEXT) and y 
is in IC (the domain of ICEXT). 
In my earlier mails I made the addition after 'then'. 
However, in the light of your proof this seems better.)

3b. x:=I(rdfs:range) is in IP  [semantic condition]
3c. y:=I(rdf:Property) is in IC [semantic condition]
3d. <u,v> in I(rdfs:range)  implies u in  ICEXT(I(rdf:Property))
[2.,3a.,3b.,3c.]
4.  <u,v> in I(rdfs:range)  implies u in IP  [3d., definition of IP]
And similarly for the rest of the claim.

So the addition "[and x is in IP and y is in IC]" to 3a seems to be
needed as a kind of bootstrap to arrive at the claim.
This bootstrap addition would not be needed if another proof of 
the claim can be given without the use of the domain and range 
conditions.

It seems natural to add a lemma to the text for the claim and
the proof.
If the "bootstrap additions" are left out of the domain and range
conditions in the table, then the full domain and range
conditions 3a (and similarly for rdfs:range) should be mentioned
with the lemma, in my view.
A disadvantage of leaving these bootstrap additions out of the
table would be that understanding a statement in the (normative)
table would require an (informative?) lemma.

>
>Best wishes

Same to you
(I am sorry that I could not reply earlier, as I was away from my 
email.  With this mail and the next I hope to finish our discussion
about the last call semantics document as quickly as possible.)

>
>Pat
>
>
>-- 
>---------------------------------------------------------------------
>IHMC  (850)434 8903 or (650)494 3973   home
>40 South Alcaniz St.                                            (850)202 
4416   office
>Pensacola               (850)202 4440   fax
>FL 32501             (850)291 0667    cell
>phayes@ai.uwf.edu                         http://www.coginst.uwf.edu/~phayes
>s.pam@ai.uwf.edu   for spam
>
>

Herman

Received on Tuesday, 11 March 2003 07:56:14 UTC