Re: D-entailment games... [Was: Re: is rdf a regular logic? RIF? was: Coherent Logic (a.k.a Geometric Logic) and RDF?]

On 2020-01-22 5:46, Antoine Zimmermann wrote:
> [I changed the topic, as this is irrelevant to the original thread.]
> 
> 
> Very good, Aidan, I don't see any error in the reasoning.
> 
> Note that you do not need to appeal to RDFS recognising xsd:string. If 
> we assume "proto-RDFS entailment", which I define exactly as RDFS 
> entailment except that it does not impose that xsd:string and 
> rdf:langString are recognised, then how can the inconsistency be proved?

Hmm, interesting.

Without using known disjointness of value spaces, the only 
"inconsistency hook" that I can find (based on what you said previously) 
is to show that:

   rdf:Property rdfs:subClassOf xsd:boolean .  #AZ

entails:

   xsd:boolean rdf:type xsd:boolean .     #otherGoal

which I believe leads to inconsistency. Specifically ...

Under D-entailment, we have that:
- I(xsd:boolean) = (L,L2V,V)

Under RDFS semanatics, we have that:
- ICEXT(I(xsd:boolean)) = { true, false }

So #otherGoal suggests that I(xsd:boolean) ∈ ICEXT(I(xsd:boolean)), 
which it clearly ain't.

As for showing the entailment, my (slightly lazy :P) guess is that more 
or less the same pigeons as before *should* be up to the task.

> --AZ
> 
> 
> 
> Le 22/01/2020 à 08:45, Aidan Hogan a écrit :
>> off topic ...
>>
>> On 2020-01-21 5:48, Antoine Zimmermann wrote:
>> [snip]
>>> D-entailment can be horribly complicated. Consider this example:
>>>
>>> rdf:Property rdfs:subClassOf xsd:boolean .
>>>
>>> Is this RDFS-recognising {xsd:boolean}-consistent?
>>
>>
>> No. (If I'm not mistaken.)
>>
>> First D-entailment (which must recognise xsd:string) will give us:
>>
>>    xsd:string rdf:type rdfs:Datatype .        #1 [rdfs1]
>>    "a" rdf:type xsd:string .                  #2 [semantic conditions]
>>    "b" rdf:type xsd:string .
>>    ...
>>
>> I will use generalised RDF to make (my) life easier.
>>
>> What we'll try to prove is that given:
>>
>>    rdf:Property rdfs:subClassOf xsd:boolean . #AZ
>>
>> the following triple must hold:
>>
>>    "a" rdf:type rdf:Property .                #goal
>>
>> since when it is combined with #AZ and rdfs9, it gives:
>>
>>    "a" rdf:type xsd:boolean .
>>
>> which should be D recognising-xsd:boolean-unsatisfiable.
>>
>> ================================================================
>>
>> We'll need some RDFS axiomatic triples:
>>
>>    rdfs:domain rdfs:domain rdf:Property .        #A1
>>    rdfs:range rdfs:domain rdf:Property .         #A2
>>    rdfs:subPropertyOf rdfs:domain rdf:Property . #A3
>>    rdf:type rdfs:range rdfs:Class .              #A4
>>    rdf:type rdf:type rdf:Property .              #A5
>>
>> ================================================================
>>
>> Given:
>>
>>    rdf:Property rdfs:subClassOf xsd:boolean .
>>
>> We now have (at most) two possible "relations" in IP.
>>
>> Per the pigeonhole principle, at least one pair here must refer to the 
>> same property:
>>
>>    rdf:type
>>    rdfs:domain
>>    rdfs:range
>>
>> This leaves the following three cases.
>>
>> ================================================================
>>
>> Case 1: rdf:type and rdfs:domain refer to the same property.
>>
>>    "a" rdfs:domain xsd:string .           #3 [#2 and Case 1]
>>    "a" rdf:type rdf:Property .            #goal [#3, #A1 and rdfs2]
>>
>> ================================================================
>>
>> Case 2: rdf:type and rdfs:range refer to the same property.
>>
>>    "a" rdfs:range xsd:string .            #4 [#2 and Case 2]
>>    "a" rdf:type rdf:Property .            #goal [#4, #A2 and rdfs2]
>>
>> ================================================================
>>
>> Case 3: rdfs:domain and rdfs:range refer to the same property.
>>
>>    rdf:type rdfs:domain rdfs:Class .      #5 [#A4 and Case 3]
>>    "a" rdf:type rdf:Class .               #6 [#2, #5 and rdfs2]
>>    "a" rdfs:subClassOf rdfs:Resource .    #7 [#6 and rdfs8]
>>
>>   I don't see a good way to make direct progress from here, but within 
>> Case 3, we can always invoke the pigeonhole principle again. At least 
>> one pair here must refer to the same property:
>>
>>    rdfs:domain/rdfs:range (already equivalent under Case 3)
>>    rdfs:subClassOf
>>    rdfs:subPropertyOf
>>
>> This leaves three sub-cases.
>>
>> ----------------------------------------------------------------
>>
>> Case 3.1: rdfs:domain, rdfs:range and rdfs:subClassOf all refer to the 
>> same property.
>>
>>    "a" rdf:domain rdfs:Resource .         #8 [#7 and Case 3.1]
>>    "a" rdf:type rdf:Property .            #goal [#8, #A1 and rdfs2]
>>
>> ----------------------------------------------------------------
>>
>> Case 3.2: rdfs:subClassOf and rdfs:subPropertyOf refer to the same 
>> property.
>>
>>    "a" rdfs:subPropertyOf rdfs:Resource . #9 [#7 and Case 3.2]
>>    "a" rdf:type rdf:Property .            #goal [#9, #A3 and rdfs2]
>>
>> ----------------------------------------------------------------
>>
>> Case 3.3: rdfs:domain, rdfs:range and rdfs:subPropertyOf all refer to 
>> the same property.
>>
>> It will make (my) life easier to observe that within Case 3.3, either:
>>
>> - Case 3.3.1: rdfs:subClassOf refers to the same property as 
>> rdfs:domain, rdfs:range and rdfs:subPropertyOf, or
>> - Case 3.3.2: rdfs:subClassOf refers to the same property as rdf:type.
>>
>> Since Case 3.3.1 is covered by Case 3.2, we assume Case 3.3.2.
>>
>>    rdf:type rdfs:subClassOf rdf:Property . #10 [#A5 and Case 3.3.2]
>>    rdf:type rdfs:subPropertyOf rdf:type .  #11 [#A5 and rdfs6]
>>    rdf:type rdfs:domain rdf:type .         #12 [#11 and Case 3.3]
>>    "a" rdf:type rdf:type .                 #13 [#2, #12 and rdfs2]
>>    "a" rdf:type rdf:Property .             #goal [#10, #13 and rdfs9]
>>
>> ================================================================
>>
>> In all cases given to us by the pigeons we infer the goal:
>>
>>    "a" rdf:type rdf:Property .
>>
>> Hence
>>
>>    rdf:Property rdfs:subClassOf xsd:boolean .
>>
>> ... is not RDFS-recognising {xsd:boolean}-consistent.
>>
>>
>> So what's horribly complicated about that? :)
>>
>> ================================================================
>>
>> Disclaimer:
>>
>> Possibly I made a mistake somewhere.
>>
>> Possibly there is a much simpler argument.
>>
>> Fun question for an exam!
>>
>

Received on Wednesday, 22 January 2020 19:11:31 UTC