-
Notifications
You must be signed in to change notification settings - Fork 6
No connection between propositions and facts in model-theoretic semantics #144
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
@@ -710,7 +710,7 @@ <h3>Properties of simple entailment and satisfiability</h3> | |||||||||||||||||||||||||
<p class="fact"> If E contains an IRI which does not occur anywhere in S, | ||||||||||||||||||||||||||
then S does not simply entail E.</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p>The following semantic properties relate triple terms and triples asserted in a graph, and they introduce a general definition of satisfiability.</p> | ||||||||||||||||||||||||||
<p>The following semantic properties relate triple terms, triples asserted in a graph and reified triples, and they introduce a general definition of satisfiability.</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p>We define the <dfn>set of propositions</dfn> in an interpretation as follows:</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
|
@@ -720,10 +720,20 @@ <h3>Properties of simple entailment and satisfiability</h3> | |||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p class="fact"> The set F of facts in an interpretation I is F(I) = { RE(x, y, z)|<x, z> is in IEXT(y) }. The set of facts is the set of propositions which are true in the interpretation. </p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p>We define the <dfn>set of reifications</dfn> in an interpretation as follows:</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p class="fact"> The set R of reifications in an interpretation I is R(I) = { RE(x, y, z)| | ||||||||||||||||||||||||||
x is in IR, | ||||||||||||||||||||||||||
y is rdf:reifies, | ||||||||||||||||||||||||||
z is a triple term and | ||||||||||||||||||||||||||
<x, z> is in IEXT(y) }. | ||||||||||||||||||||||||||
The set of reifications is the multi-set of propositions which are reified in an interpretation. </p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p>Given a blank node mapping, we define the <dfn>set of facts asserted by a graph</dfn> in an interpretation as follows:</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p class="fact">Given a blank node mapping A, the set of all facts asserted by a graph G in an interpretation I is FEXT(G, I, A) = { RE( [I+A](s), I(p), [I+A](o) )|`s p o.` is in G }. We then observe that given a blank node mapping, the asserted facts of a graph with respect to an interpretation may not necessarily be among the facts of the interpretation.</p> | ||||||||||||||||||||||||||
<p>We introduce a <dfn>general definition of satisfiability</dfn> of a graph in an interpretation as follows:</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<p class="fact">An interpretation (simply) satisfies a graph if and only if there exists a blank node mapping such that the facts asserted by the graph in the interpretation are among the facts of the interpretation.</p> | ||||||||||||||||||||||||||
|
@@ -1959,8 +1969,52 @@ <h2 id="non_semantics">RDF reification, containers and collections</h2> | |||||||||||||||||||||||||
processes to check formal RDF entailment. For example, implementations may decide | ||||||||||||||||||||||||||
to use special procedural techniques to implement the RDF collection vocabulary.</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<section id="TTerms"> | ||||||||||||||||||||||||||
<h3>RDF 1.2 reification - triple terms and reifiers</h3> | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
<p> | ||||||||||||||||||||||||||
To repeat nomenclatura: | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
<ul> | ||||||||||||||||||||||||||
<li>an `rdfs:Proposition` subsumes multiple kinds of triples: | ||||||||||||||||||||||||||
abstract triples, asserted triples and reified triples | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
</li> | ||||||||||||||||||||||||||
<li>an abstract triple is encoded as a triple term</li> | ||||||||||||||||||||||||||
<li>an asserted triple is also called a fact, | ||||||||||||||||||||||||||
and also known as an RDF statement | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
or simply as a triple in the graph</li> | ||||||||||||||||||||||||||
<li>a reified triple is represented by a reifier and defined by | ||||||||||||||||||||||||||
a fact with `rdf:reifies` as the predicate, | ||||||||||||||||||||||||||
the reified triple term as the object | ||||||||||||||||||||||||||
Comment on lines
+1985
to
+1987
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
and a reifier, denoting the reification, as the subject.</li> | ||||||||||||||||||||||||||
</ul>. | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
Reifying an abstract proposition, encoded as a triple term, | ||||||||||||||||||||||||||
never entails that triple as a fact. | ||||||||||||||||||||||||||
Neither does a fact entail a reification of that triple. | ||||||||||||||||||||||||||
Comment on lines
+1992
to
+1993
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
From that follows that in a strict interpretation of the model-theoretic semantics of RDF 1.2 | ||||||||||||||||||||||||||
an assertion on a reified triple (denoted by a reifier) | ||||||||||||||||||||||||||
can never be an assertion on a fact asserting that same triple. | ||||||||||||||||||||||||||
Comment on lines
+1995
to
+1997
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
The connection between a reification and an assertion of the same triple, | ||||||||||||||||||||||||||
even if they occur in the same graph, | ||||||||||||||||||||||||||
can only be understood as being merely coincidental. | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
A looser interpretation of that connection | ||||||||||||||||||||||||||
as one of <a href="https://w3c.github.io/rdf-semantics/spec/#dfn-identify">identification</a>, | ||||||||||||||||||||||||||
not <a href="https://www.w3.org/TR/rdf12-concepts/#dfn-denote">denotation</a>, | ||||||||||||||||||||||||||
as applied in RDF 1.2 Concepts, RDF 1.2 Primer and the RDF 1.2 note on triple terms (tbd), | ||||||||||||||||||||||||||
establishes an operational semantics of such a connection between reification and fact | ||||||||||||||||||||||||||
as convention and best practice. | ||||||||||||||||||||||||||
Comment on lines
+2002
to
+2007
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
The semantics of RDF 1.2's triple term-based reification mechanism thus diverges | ||||||||||||||||||||||||||
from RDF 1.0/1.1 reification which strictly upholds the model-theoretic interpretation | ||||||||||||||||||||||||||
that reified and asserted triple have no connection beyond mere coincidence. | ||||||||||||||||||||||||||
This design was chosen to facilitate assertions on asserted triples, a.k.a. "statements about statements", | ||||||||||||||||||||||||||
while keeping the model-theoretic semantics of RDF 1.2 simple | ||||||||||||||||||||||||||
and upholding a safe distance from modal logic complications. | ||||||||||||||||||||||||||
Comment on lines
+2011
to
+2013
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
</p> | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<section id="Reif"> | ||||||||||||||||||||||||||
<h3>Reification</h3> | ||||||||||||||||||||||||||
<h3>RDF 1.0/1.1 reification - statement quad reification </h3> | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
<div class="c1"> | ||||||||||||||||||||||||||
<table> | ||||||||||||||||||||||||||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.