comments on RDF MT

Better late then never, I hope.

Yesterday I saw the "Nondraft" at [1] of the new version of the RDF model 
theory document that is underway.
I have some comments which are hopefully considered useful.
The first two comments question the correctness of proofs; the other 
comments are small corrections/editorial suggestions.
(Section numbers refer to [1].)

- RDF closure lemma: since the definition of the set IP has been
changed (it is now part of the definition of a simple interpretation),
the last part of the proof of this lemma does not apply anymore:
the set IEXT(I(aaa)) can no longer be assumed to be nonempty.
(I fully support the change of the definition of IP, and considered
the old version of this definition to be a "weak spot" in the document.)

- There seems to be a problem with the proof of the second anonymity 
lemma.
Consider the sentence "Since E is lean, it contains no other triples
of the form S1 P1 O' or S2 P2 O'." This is true, when O' is assumed
to be a name.  However, E may contain two other triples S1 P1 _:x3
and S2 P2 _:x3.  In this case, the last part of the proof does not
apply.

- 1.5: paragraph starting with "For example,": replace <1,2> by <1,1>

- 3.1: example: it should be IR = {1,2,T,P} instead of {1,2,T}

- 3.3: The introduction of the set IC looks a little circular, and
can be made smoother (when I first read this, I had to stop for some time 
at this point).
Namely: the mapping ICEXT is defined from classes to extensions
(so the set of classes IC is assumed to be already there, although it is 
not
explicitly specified) and subsequently, in the table, IC is described in 
terms
of ICEXT.

In my view, the going would become smoother when the explicit definition 
of IC,
IC := {x in IR : <x, I(rdfs:Class)> in IEXT(I(rdf:type))},
is given before the definition of 
ICEXT : IC -> P(IR)
given in the text.

-2: definition of entailment. The central case of the document
(S entails E where S is a set of RDF graphs and E is an RDF graph)
could be understood quicker by saying [I satisfies S => I satisfies E]
and by adding one line to the table of 1.6:
[If S is a set of RDF graphs, then I(S) = I(Merge S).]
This definition case could be added to the first paragraph of 2; it is 
convenient to use this when following the proofs, for example.
With the original text, the reader can deduce this from the first 
paragraph 
of 2, but it takes more unwinding (the word expression has to be matched 
with 
the word RDF graph, etc.)

- I suggest to add to the merging lemma: S entails E iff Merge S entails 
E.
At several places where the merging lemma is used (for example, in the 
proof
of the interpolation lemma), this addition would make the use of this 
lemma 
instantaneous.

- Just before the minimality lemma: "It is clear that if I satisfies E 
then
a minimal satisfying [add: sub]interpretation exists with a vocabulary 
precisely..."  (I guess this is what is meant. Without this addition, 
the assumption is not needed.)

- proof of anonymity lemma 1: "otherwise" suggests that now the negation
of the preceding will be used, but this is not the case.
It would be better to say: Since..., E' contains a triple [add: s'p'o' 
obtained by replacing a blank node by a name in the triple spo from E, 
while s'p'o'] has no instances in E; otherwise, the triple spo would 
have had a proper instance in E.

- Interpolation lemma. It would be helpful to add the following corollary
explicitly: E does not entail E' iff E' is separable from E.
In addition to the two lemmas mentioned, the if direction also uses the
subgraph lemma.

- RDF entailment lemma: second paragraph: it should be rdf-interpretation 
instead of rdfs-interpretation

Herman ter Horst
Philips Research

[1] http://www.coginst.uwf.edu/~phayes/RDF%20Model%20Theory_Oct_draft.html