A formal background to unify triples and triple terms

[franconi]

Added at the end of Section 5.3:

• semantic properties relating triple terms and asserted triples, together with a general definition of (simple) satisfiability.

The terminology defined here should be used to support the unification of the terminology of triples, as per issue #158 in Concepts.

This closes #87

---

Preview | Diff

[niklasl]

LGTM!

[franconi]

Ahah: https://letmegooglethat.com/?q=LGTM&l=1

[pfps]

It's a new initialism to get around the current political crackdown and still show that you are woke. I'll let you work out the expansion for yourself.

[TallTed]

Good forward motion!

[pfps]

Isn't it time to merge this PR?

[TallTed]

I see four open threads —

1. A formal background to unify triples and triple terms #91 (comment)
2. A formal background to unify triples and triple terms #91 (comment)
3. A formal background to unify triples and triple terms #91 (comment)
4. A formal background to unify triples and triple terms #91 (comment)

— raising issues with existing wording in this PR, so before it gets merged, I would expect to see four fresh issues starting from those open subthreads.

[doerthe]

I would like to have the wording for the equivalence fixed (see my comment).

[franconi]

Ready for merging - waiting for the OK by @doerthe.

[doerthe]

I am sorry, I accidentally directly changed the file instead of suggesting a change. But it was minor.

[niklasl]

I want to make sure that this is correct. Is IPR the domain of RE? Or are the propositions what RE maps into (the codomain)? Since triple terms denote propositions, is RE mapping propositions to other resources, or to propositions?

[pchampin]

@niklasl my understanding of those definitions is that both "propositions" and "facts" must be 3-uples of things, so yes, IPR is he domain of RE, not the co-domain. And you are right, the "propositions" here are not the instances of rdfs:Proposition, but their inverse images for RE.

I am not too bothered by this conflation, because:

• there are precedents anyway (rdfs:Literal and, in a way, rdf:Statement)
• while it is cleaner to define the co-domain of RE as a set of "opaque" elements of the domain, their intended meaning is (at least in my mental model) to represent the proposition itself (in a literal-ish way)
• introducing two different terms here would confuse anyone beyond those who commented on this PR...

[niklasl]

Yes, I certainly don't want two different terms here. I just wonder, if my reasoning is correct, that IPR(I) = { RE(x, y, z) | x ∈ IR, y ∈ IP, z ∈ IR } and F(I) = { RE(x, y, z)｜<x, z> ∈ IEXT(y) } might be the way to express that.

I've figured that the reason of keeping RE "opaque" rather than expanding its definition is because to do that, we'd need modal and/or higher order logic (and forsake completeness). My thinking is that it maps to a "delayed evaluation" of <x, z> ∈ IEXT(y) (which may even be parameterized in a modal logic). Of course, I suppose that makes F(I) a mapping from (all facts in) the interpretation to their image of propositions.

But if keeping the definitions of IPR and F as the preimages of (respectively) propositions and facts in the interpretation keeps things simpler (rather than obscuring by conflation), I can probably live with that. (I should, since I initially conflated them like that in an attempt to move further towards clarity. I much prefer some clarification to none. And yes, there are other conceptual conflations.)

[doerthe]

We have been discussing about that before. Currently, RE is an injective mapping from IRxIPxIR into IR. Wether or not it is the identity is a different question which we discussed before and we can certainly keep discussing (I already see some people objecting here, but we can even do that if don't change the semantics :) ), but for this PR the current form is correct.

[doerthe]

Yes, I certainly don't want two different terms here. I just wonder, if my reasoning is correct, that IPR(I) = { RE(x, y, z) | x ∈ IR, y ∈ IP, z ∈ IR } and F(I) = { RE(x, y, z)｜<x, z> ∈ IEXT(y) } might be the way to express that.

I think what would be in line with your idea would be to simply get rid of RE (that is, use the identity), that is

I(<s,p,o>)=<I(s), I(p), I(o)>.

[niklasl]

Using RE to define IPR, F and FEXT.