Uniqueness of Skolemization?

At 04:57 PM 3/16/01 -0600, pat hayes wrote:
>The skolem function f(x,y) is the (hopefully unique) parent of y who is 
>x's child.

I assume the "hopefully unique" was meant as a social rather than a logical 
comment?

Behind this flippant observation is a more serious question about 
Skolemization:  is there any expectation that a Skolem function is 
unique?  If so, then statements like:

(forall (?a ?c)( <=> (grandparent ?a ?c)
                              (and (parent ?a (f ?a ?c))(parent (f ?a ?c) ?c)))
))

would seem to be a little problematical.

#g


------------
Graham Klyne
GK@NineByNine.org