- From: pat hayes <phayes@ai.uwf.edu>
- Date: Sat, 23 Jun 2001 23:22:15 -0500
- To: Graham Klyne <Graham.Klyne@Baltimore.com>
- Cc: w3c-rdfcore-wg@w3.org
>At 02:53 PM 6/21/01 -0500, pat hayes wrote:
>>Existentially quantified variables do not bind to multiple values either.
Ah, I see that this may have been misleading, and apologise for being
too quick. (It depends what 'bind to' means...) Please read on.
>
>Hmmm, there's something I'd like to better understand here.
>
>Consider something like:
>
> child(fred) & ( exists(Y): parentOf(Y,fred) )
>
>Now, as I understand, Skolemizing this would yield something like:
>
> child(fred) & parentOf(Y,fred)
Well, the existential variable Y would become a (new) constant name,
say sk2356, and this would become
child(fred) & parentOf(sk2356,fred)
The fact that this name is 'new' means that there are no other
assertions about it, ie all that you know about sk2356 is that it
exists (since all FOL names refer to something) and that the above
axiom is true of it, which is exactly what you knew about Y. Now,
there could logically have been several Y's that might have existed
and would have satisfied the orginal existential axiom (so in this
sense the existential variable might be said to 'bind to' more than
one thing, though this sense of 'bind' is not that used in
programming language semantics); the existential quantifer doesn't
guaranteee uniqueness. The skolemised formula in effect 'picks out'
one of them and says something about it, since every logical name
only denotes one thing in a given interpretation. But there isnt
really any difference in content, since you don't know which of them
it picks out (denotes), and in fact it could denote any of them (if
there was more than one) and still be correct.
>I guess that you're saying that in this expression Y binds to a
>single instance of fred's parent, even though we expect there to be
>two possible such bindings. So the logical expression does not, of
>itself, uniquely define the binding, even though there may be only
>one in any instance of the expression.
Once Y has been made into a constant it has a unique referent
(binding) in any given interpretation, yes. And the logical
expression does not define the binding, indeed. (An existential
assertion says a(tleast one) binding makes the sentence true, a
universal says it is true for any binding, and a name just assumes a
single binding, but does not specify it directly, only by whatever
the axioms say about it.)
>Some problems, it seems to me, call for enumeration of all the
>possible bindings (including problems of the kind RDF is likely to
>be used with). E.g. Who are fred's parents? Should I conclude that
>such problems cannot be fully specified within the framework of FOL?
No, they can be, but you need to say more than just 'parents exist'
if you want to talk about all the parents. There are all sorts of
ways to do this, eg you might say something like
parentOf(?x,fred) implies .....?x....
where the ?x is univerally quantified, or you might introduce sets
and talk about the set of freds parents, or you might introduce
explicit Mother and Father relations.
BTW, notice that 'who are fred's parents' is logically an open-ended
query; you and I know it isn't open-ended because we know that people
only have two parents, but theres no *logical* reason why someone
might not have, say, infinitely many parents.
The two-parent rule could be axiomatised by saying (sorry, I will
revert to SKIF notation)
(forall (?x)
(exists (?y1 ?y2)
(& (parentOf ?y1, ?x)
(parentOf ?y2, ?x)
(not (= y1 y2))
(forall (?z)(implies (parentOf ?z ?x) (or (= ?z ?y1)(= ?z ?y2))))
)))
If you skolemise the inner existentials y1 and y2, by the way, the
natural names to use for the skolem functions would be 'motherOf' and
'fatherOf'
Pat Hayes
---------------------------------------------------------------------
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 Monday, 25 June 2001 10:43:03 UTC