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

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 
guarantee (unless you add some other axioms about the skolem 
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 UTC