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

Though this be madness, yet there is method in’t.

Pat


> On Jan 22, 2020, at 2:46 AM, Antoine Zimmermann <antoine.zimmermann@emse.fr> 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?
> 
> 
> --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!
> 
> -- 
> Antoine Zimmermann
> Institut Henri Fayol
> École des Mines de Saint-Étienne
> 158 cours Fauriel
> CS 62362
> 42023 Saint-Étienne Cedex 2
> France
> Tél:+33(0)4 77 42 66 03
> Fax:+33(0)4 77 42 66 66
> http://www.emse.fr/~zimmermann/
> Member of team Connected Intelligence, Laboratoire Hubert Curien