diff --git a/spec/index.html b/spec/index.html
index 0634ddd..3c83678 100644
--- a/spec/index.html
+++ b/spec/index.html
@@ -710,7 +710,7 @@
Properties of simple entailment and satisfiability
If E contains an IRI which does not occur anywhere in S,
then S does not simply entail E.
- The following semantic properties relate triple terms and triples asserted in a graph, and they introduce a general definition of satisfiability.
+ The following semantic properties relate triple terms, triples asserted in a graph and reified triples, and they introduce a general definition of satisfiability.
We define the set of propositions in an interpretation as follows:
@@ -720,10 +720,20 @@ Properties of simple entailment and satisfiability
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.
+ We define the set of reifications in an interpretation as follows:
+
+ 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.
+
+
Given a blank node mapping, we define the set of facts asserted by a graph in an interpretation as follows:
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.
-
+
We introduce a general definition of satisfiability of a graph in an interpretation as follows:
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.
@@ -1959,8 +1969,52 @@ RDF reification, containers and collections
processes to check formal RDF entailment. For example, implementations may decide
to use special procedural techniques to implement the RDF collection vocabulary.
+
+
+ RDF 1.2 reification - triple terms and reifiers
+
+ To repeat nomenclatura:
+
+ - an `rdfs:Proposition` subsumes multiple kinds of triples:
+ abstract triples, asserted triples and reified triples
+
+ - an abstract triple is encoded as a triple term
+ - an asserted triple is also called a fact,
+ and also known as an RDF statement
+ or simply as a triple in the graph
+ - 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
+ and a reifier, denoting the reification, as the subject.
+
.
+
+ 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.
+
+ 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.
+ 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 identification,
+ not denotation,
+ 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.
+ 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.
+
+
- Reification
+ RDF 1.0/1.1 reification - statement quad reification