modification to new semantics to permit entailment that every triple term is a proposition

[pfps]

The semantics for RDF has the empty graph RDFS-entailing

AAA rdf:type rdfs:Resource .

for AAA any IRI.

This happens because IS is total on IRIs. (Most semantics for other logics do this in a different way.)

But the proposed semantics would not have the empty graph RDFS-entailing

<<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

for AAA, BBB, CCC any IRIs. This happens because RE is partial so RE(IS(AAA), IS(BBB), IS(CCC)) might not exist.

I suggest making RE total on (IR v IP)^3 to regain this entailment.

[pfps]

Even if RE is total on IRxIPxIR, the problem persists.

[franconi]

I propose to drop the semantic condition

 <r, [I+A](rdfs:Proposition)> ∈ IEXT([I+A](rdf:type))
         if ∃ x,y,z . RE(x,z,y)=r

from the RDFS metamodelling requirements,
so that triple terms are not anymore of type rdfs:Proposition.

[pfps]

Markdown mangles semantic conditions so I protected the change above.

[pfps]

I am firmly against this change.

[franconi]

I am firmly against this change.

would you mind to argue your firm position?

[franconi]

@pfps: could this be a solution to keep rdfs:Proposition?
We can introduce in an interpretation the set IPR.
RE mapping from IR x IP x IR to IPR
\forall r. r \in IPR -> \exists xyz RE(xyz)= r

[doerthe]

What about making RE total on IRxIRxIR? I would still make the extra set IPR.

The reasoning:
With your semantics, @franconi, we would still not be able to derive

<<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

Mainly because the interpretation function is only defined on IRxIPxIR, so it could be that I(BBB) is not in IP.
We do not have that problem if RE is defined on IRxIRxIR because in RDFS, where we want the entailment to happen, IP is a subset of IR, so, we should not have a problem.

What we loose here, however, is the entailment that from

XXX YYY <<( AAA BBB CCC )>>.

follows that

BBB rdf:type rdf:Property.

But I think that could be a compromise. Of course, we could alternatively give up the entailment from the empty graph. So we would not always get that

<<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

I personally would favor giving up the entailment of rdf:Property, but am open for both.

[pfps]

I am firmly against this change.

would you mind to argue your firm position?

To have triple terms belong to the extension of rdfs:Proposition.

[franconi]

@doerthe, I can't compromise with the middle element of a triple term not being a property. I've argued about that, and this can not happen :-)
However, I realise now that RDF semantics says the following:
x is in IP if and only if <x, I(rdf:Property)> is in IEXT(I(rdf:type))
so that, together with
RE a mapping from IR x IP x IR into IR
we get
XXX YYY <<( AAA BBB CCC )>>. ⊨ BBB rdf:type rdf:Property.
just because of that.
So, we shouldn't change what it is written in the liberal baseline document - IF I AM NOT WRONG :-)
Moreover, just for elegance, we can introduce in an interpretation the set IPR, and RE as a mapping from IR x IP x IR to IPR, together with \forall r. r \in IPR -> \exists xyz RE(xyz)= r

[franconi]

I am firmly against this change.

would you mind to argue your firm position?

To have triple terms belong to the extension of rdfs:Proposition.

A classical case of a non-explaining tautology :-)

[doerthe]

@franconi
Unfortunately, that does not solve our problem. If we want for all triple terms (syntax level) that the empty graph entails

<<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

it does not help that we know that I(BBB) is in IR. It could still be that I(BBB) is in IR but not in IP. Then,<<( AAA BBB CCC )>> would also not be a proposition.

Coming from your point of view, one could of course argue that you also would NOT like to have that the empty graph entails:

<<(rdf:Property rdf:Property rdf:Property )>> rdf:type rdfs:Proposition .

So, before we continue here, it might be worth to first discuss whether we want that derivation or not. I am not a big fan of rdf:Property derivation for nested predicates in the first place (we had that discussion), but I am also not really against that.

So, if we can't have both derivations, which of the two would you want to give up? (all opinions welcome :) )

[doerthe]

we could (=would have to), however, make more complicated entailment patterns with the semantics as we have it:

If S contains
AAA BBB CCC.
Then for all IRIs XXX and YYY we have
<<( XXX BBB YYY )>> rdf:type rdfs:Proposition .
That is the in-between solution.

[doerthe]

and
If S contains
AAA rdf:type rdf:Property.
Then for all IRIs XXX and YYY we have
<<( XXX AAA YYY )>> rdf:type rdfs:Proposition .

[franconi]

I believe that the current liberal semantics:

RE a mapping from IR x IP x IR into IR
<r, [I+A](rdfs:Proposition)> ∈ IEXT([I+A](rdf:type)) if ∃ x,y,z . RE(x,z,y)=r

is the correct one, and unlike Doerthe, I start from there.
For me triple terms have to be 3-tuples of resource-property-resource - no question about that.
In this semantics the following RDFS entailment does NOT hold:

∅ ⊨ <<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

It seems that you are not happy about this missing entailment.
But I say that, if we accept the semantics, then we have to accept that only triple terms for which we are sure that the second element is a property are indeed of type rdfs:Proposition. If we are not sure that the second element is a property, it seems obvious that we can not make the entailment.
This seems absolutely reasonable to me.

[doerthe]

I believe that the current liberal semantics:

RE a mapping from IR x IP x IR into IR <r, [I+A](rdfs:Proposition)> ∈ IEXT([I+A](rdf:type)) if ∃ x,y,z . RE(x,z,y)=r

is the correct one, and unlike Doerthe, I start from there.

Just as a quick comment: I started from what this issue "wanted". so no strong opinions here (yet), I really just like to modify the semantics towards "what we want". I just realised in the last post that the "what we want" is what we should discuss in the first place (even though, playing with the semantics is far more fun ;) ).

[franconi]

That's our difference: I want to define first a reasonable semantics (since model theory tells you exactly the meaning of your language) and then I have to accept (and understand) its consequences.
You want to fix "entailments" first, and have a semantics which captures this, even if this misrepresents the world (e.g., triple terms being IR x IR x IR).
Anyway, from your "entailments first" approach: why do you find absolutely necessary to have the entailment:
∅ ⊨ <<( AAA BBB CCC )>> rdf:type rdfs:Proposition .
or even
BBB PPP OOO. ⊨ <<( AAA BBB CCC )>> rdf:type rdfs:Proposition .
?
On the other hand, I expect the following to hold:
SSS BBB OOO. ⊨ <<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

[doerthe]

Might be that I simply think that it is always impossible to model "the world" and that you will always have to make choices...

But to be more concrete: I am fine with keeping your IRxIPxIR. Then, the last entailment you mention above needs to hold and so does the other one we had
AAA rdf:type rdf:Property. entails <<( XXX AAA YYY )>> rdf:type rdfs:Proposition .

I would be very curious to hear other opinions. What do you think @pfps ?

[franconi]

But to be more concrete: I am fine with keeping your IRxIPxIR. Then, the last entailment you mention above needs to hold and so does the other one we had AAA rdf:type rdf:Property. entails <<( XXX AAA YYY )>> rdf:type rdfs:Proposition .

Perfect. Indeed, in the current semantics of the liberal baseline the following hold:

SSS BBB OOO. ⊨ <<( AAA BBB CCC )>> rdf:type rdfs:Proposition .

AAA rdf:type rdf:Property. ⊨ <<( XXX AAA YYY )>> rdf:type rdfs:Proposition .