Re: log:forSome/#rdfms-identity-anon-resources

[oops... I saw your message later in this thread
before I saw this one...]

pat hayes wrote:
[...tangent about definite descripitons...]
> >This information from the inventory database clearly
> >provides a match (i.e. a proof, or the interesting
> >bits of one, anyway) for the
> >description of the book stated as a formula involving
> >an existentially quantified variable, ?x0.
> 
> No, not a description; it just proves that a book exists which
> satisfies the existential. But since there might be several things
> that satisfy an existential,

That's beside the point...

> nothing follows about whether the
> bookseller's item#342323 actually IS the particular thing that you
> had in mind when writing your order.

I don't have any particular thing in mind when I place such
an order. That's how orders work: "if you have any things
that meet these criteria, I'll pay you $35 for one of them."

> (Not without some uniqueness
> assumption from somewhere.) So the bookseller is in the same position
> in either case. If he knows the thing is unique, he can figure out
> what you want; if he doesn't, he can't.


> Of course, if you had phrased your order not as an existential but as
> a universal , so that you say: "if it is a book and has author...and
> title ...., then I want it",

Er... that's an existential, not a universal, right?

A prolog query
	author(X, "b"), title(X, "f e")
is a request to prove the theorem

	(exists (?x) (author ?x "b") (title ?x "f e))
right? and the query results are proofs; i.e. substitutions
of the variables that show that it's satisfyable.

That's how queries work, right? They're existential formulas,
and the job of a query engine is to give proofs, by
example, of the theorem. This is completely traditional, no?

[[[
Free variables in a query
are assumed to be existentially quantified.
]]]

--        Knowledge Interchange Format
http://logic.stanford.edu/kif/dpans.html
Thu, 25 Jun 1998 22:31:37 GMT

> then the bookseller can figure out what
> you want. However, you might now get several books, unless you give
> enough of a description to pin down one uniquely.

Several books might match my query, but I specify how many
I want in the order.


> >But it doesn't match/prove the formula where _:g0
> >is replaced by the skolem constant
> ><http://skolem.example#432oj34oij2o3ijo23j> .
> 
> Right. And it might not be it. On the other hand it is possible that
> those names corefer, ie
> (=  http\:\/\/booksRus\.example\/inv2001\-06\-25\#item342323
>       <http://skolem.example#432oj34oij2o3ijo23j>)
> and if the bookseller could somehow conclude this (eg by knowing that
> only one thing satisfied the description) then he could get you the
> book you want from your order, skolemised or not.
> 
> >So an RDF document with anonymous nodes is *not*
> >interchangeable with a skolemized version of that document.
> >Q.E.D.
> 
> It is if everyone is using valid logical reasoning.

No, I disagree.

The bookseller can conclude that he has a book that
matches your description iff your description is stated
as an existential. If your description is skolemized,
there's no valid inference that allows him to conclude
that he's got a book that you want.


> >I think this is the important part of Pat's message
> >that I disagree with is:
> >
> > > RDF is supposed to
> > > consist of assertions, not equations, and they are pretty simple
> > > assertions of the logical form (V s o) . Those s's and o's are
> > > logical names = logical constants, ie they denote things, one thing
> > > each in a given interpretation. Now, logical names are *just* like
> > > existentially quantified variables where the quantifers are at the
> > > top level (the only level there is in RDF), ie not inside any
> > > universal quantifiers.
> >
> >The s's and o's would be just logical constants if we
> >left out anonymous/existentially-quantified terms.
> >But RDF does have such terms, as demonstrated above.
> >And the semantics of such terms is non-trivially
> >different from the semantics of constants:
> >an existentially quantified formula is satisfied
> >by an interpretation if there's *some* thing
> >you can bind the existential term to that makes
> >it work out.
> 
> Yes, and that is exactly the truth conditions for a logical name, as
> well; it has to have a denotation that makes the sentences containing
> the name work out true.

But it only has that denotation in *some* interpretations;
valid inference requires that *all* interpretations work.

> >Skolemizing the formula reduces
> >the number of interpretations that satisify the
> >formula.
> 
> No, it doesnt. Technically, if E is an existential sentence and E' is
> a skolemisation of it, then E and E' are actually in different
> logical languages,

But what's going on in the implementations of RDF that
do this (i.e. emit generated URIs for anonymous terms,
as if these generated URIs were in the
document in the first place) is all happening in the
same language.

So perhaps it's a misnomer to say that they're doing skolemization.

[...model theory stuff that I sorta followed...]

I don't think I want to go into that E/E' stuff until
I've seen your response to my clarification about
orders/queries being existentials.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Thursday, 28 June 2001 14:03:52 UTC