Re: D-entailment games... [Was: Re: is rdf a regular logic? RIF? was: Coherent Logic (a.k.a Geometric Logic) and RDF?]
Aidan Hogan <[email protected]>
| Newsgroups | gmane.org.w3c.semantic-web |
|---|---|
| Message-ID | <[email protected]> |
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!
>>>
>>