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."

That's a universal sentence of you write it out. It has the form
(forall (?x)(implies (meets-criteria ?x) (will-pay-for me you $35 ?x)))

>
> > (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?

No, its a universal, since it is an assertion you are making.

>
>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.

Substitutions of universally quantified variables, right.

>
>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?

Yes, it is traditional and accurate *in FOL*, where the language  has 
full Boolean expressivity (in particular, has negation), but RDF 
isn't FOL, so its not at all clear what an RDF query is supposed to 
be. With the interpretation you are giving, an RDF query has the 
logical force of a universal quantification, which goes beyond what 
is usually (?) taken to be the expressive power of RDF, as I 
understand it.

Look, heres a way to put it. Divide variables into U-variables and 
E-variables. U-variables are:
1. Universally quantified in positive contexts (ie inside an even 
number of negations in an assertion or an odd number in a query) 
(where the LHS of an implication counts as a negation)
2. Existentially quantified in negative contexts (ie inside an odd 
number of negations in an assertion or an even number in a query)
and E-variables are the others. Then U-variables are 'effectively 
universal' and E-variables are 'effectively existential', where 
'effectively' indicates that the semantics and proof theory don't 
really distinguish between these cases. Skolemisation applies to 
E-variables, and U-variables are bound to new values during inference 
processing: they are the variables that it is valid to freely 
substitute terms for.

>[[[
>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

Yeh, and that is potentialy misleading. In this sense, a conjunction 
in a query is really a disjunction and vice versa, and skolemisation 
has to be done backwards. The point is that queries are essentially 
*negated*, but when you negate something with free variables, the 
free variables stay free. So to keep the intepretation of free 
variables (which are universal in assertions) consistent, they have 
to be thought of as existential in queries. But if you check out the 
actual semantics of KIF, there is no notion of 'query' defined. The 
way that traditional theorem-provers work is basically by negating 
the 'query' and then testing the combination for inconsistency. 
During the actual reasoning process, all U-variables are treated 
similarly.

In a Gentzen sequent logic, 'queries' are on the RHS of the sequent 
and assertions on the LHS. All the inference rules apply to both 
sides but are exactly dual, so that conjunctions on the RHS are like 
disjunctions on the LH, universals on one side like existentials on 
the other, and so on.

> > 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.

No, if YOU describe your book using an existential, then the 
existential is not in the goal to be proved by the bookseller. Your 
example used an existential in the goal to be proved, which is like 
the use of a universal in an assertion. If he has an asserted 
existential he isnt in a position to infer that he's got a book you 
want, either. He isnt allowed to validly instantiate any of your 
existential variables (unless he knows enough to infer that they are 
unique, but then he could also infer that about your skolem name, 
since he knows exactly asmuch about that as he does about the possble 
values of your existentials.)

> > >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.

No, it has to have it an all interpretations that satisfy the 
antecedents, if we are talking about sentences that contain the name. 
If I assert
(exists (?x)(foo ?x))
and if I assert
(foo genid3452)
knowing that nobody, including me, can possibly know anything else 
about genid3452 (because I just made the name up out of thin air and 
it is guranteed to be unique), then I have said the same thing, and 
you can infer the same things from it (apart from the completely 
useless fact that whatever it is, I am calling it 'genid3452' in the 
second case.)

>
> > >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.

In the strict logical sense, I think that isnt actually true. When a 
new name is generated, the logical langauge changes. Its a fine 
point, but this is one place where we may need to be rather careful.

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

Well, all that means is using a new name. There isnt any doubt that 
THAT is what is happening, right?

>
>[...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.

OK.
BTW, I think that Frank Manola said it all right, as well.

Pat

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Tuesday, 3 July 2001 13:27:20 UTC