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 16:11, Aidan Hogan wrote:
> 
> 
> 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.

For posterity ... to complete the proof (since it's neater).

In order to prove the RDFS_{xsd:boolean}-unsatisfiability of the following:

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

we wish to show that it RDFS_{xsd:boolean}-entails:

     xsd:boolean rdf:type xsd:boolean .          # goal

Which will be inconsistent, per the previous mail (see above).

------------------------------------------------------------------------

We note that the following hold:

     "true"^^xsd:boolean rdf:type xsd:boolean .     #1
     xsd:boolean a rdfs:Class                       #2
     xsd:boolean rdfs:subClassOf xsd:boolean .      #3

------------------------------------------------------------------------

Given #AZ, we know that there can exist at most two properties in IP. 
Hence, by the pigeonhole principle, at least two of the following terms 
must refer to the same property.

    rdf:type
    rdfs:subClassOf
    rdfs:subPropertyOf

------------------------------------------------------------------------

Case 1: rdf:type and rdfs:subClassOf refer to the same property

     xsd:boolean rdf:type xsd:boolean .  #goal [Case 1, #3]

------------------------------------------------------------------------

Case 2: rdf:type and rdfs:subPropertyOf refer to the same property

     "true"^^xsd:boolean rdfs:subPropertyOf xsd:boolean . #4
     xsd:boolean rdf:type rdf:Property . #5 [#4, range of sPO]
     xsd:boolean rdf:type xsd:boolean .  #6 [#5, #AZ, rdfs9]

------------------------------------------------------------------------

Case 3: rdfs:subClassOf and rdfs:subPropertyOf refer to the same property

     xsd:boolean rdfs:subPropertyOf xsd:boolean . #7 [Case 3, #3]
     xsd:boolean rdf:type rdf:Property . #8 [#7, range of sPO]
     xsd:boolean rdf:type xsd:boolean .  #9 [#8, #AZ, rdfs9]

------------------------------------------------------------------------

Q.E.D.

>> 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 Thursday, 23 January 2020 16:51:38 UTC