# Re: Uniqueness of Skolemization?

From: pat hayes <phayes@ai.uwf.edu>
Date: Sun, 18 Mar 2001 23:19:54 -0600
Message-Id: <v04210115b6db4265f65f@[205.160.76.171]>
To: Graham Klyne <GK@ninebynine.org>

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

Yes.  I live very close to Alabama.

>Behind this flippant observation is a more serious question about
>Skolemization:  is there any expectation that a Skolem function is
>unique?

Er.. what do you mean? Certainly the value (for a given collection of
arguments) of a particular skolem function, like any other function,
will be unique. But that doesnt mean that the skolem function itself
is unique. In an earlier message I pointed out that a skolem function
is like an existentially quantified function variable (in 2nd order
logic it actually is that), so there could be more than one function
that would do the work of the skolem function, and you have no
function, at which point it isnt really a *skolem* function any more)
that your skolem function symbol denotes any particular one of the
possible functions. For example, suppose you have the axiom that
everyone has a parent:
(forall (?x)( => (person ?x)
(exists (?y)(parent ?y ?x))))
and you skolemise it:
(forall (?x)(=> (person ?x)
(parent (f ?x) ?x)))
then certainly (f ?x) is unique, given ?x - since f is a function it
must be - but it could be x's mother or x's father, and you have no
way of knowing which unique person it is.  So it is unique in a sense
- it is one or the other - but not in another sense; it is not
uniquely specified; you have no way of knowing (from the axiom alone)
what its value is.

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

No, they are always logically correct. Even if there are several
things that would satisfy the existential quantifier and so would
count as possible values of the function, the function itself just
delivers one of them. It always chooses the same one, but you have no
way of knowing which one it is.

In logical axioms, functions arent procedures; they don't get called.
They are just things you know something about, and sometimes you
don't know much at all. Functional programming languages are based on
a definitional style which is guaranteed to provide enough
information to enable you to call a function with argument values and
always get a partial result back, but logic provides no such
guarantees.

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, 19 March 2001 00:18:18 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:38 GMT