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>

Cc: www-rdf-logic@w3.org

Date: Sun, 18 Mar 2001 23:19:54 -0600

Message-Id: <v04210115b6db4265f65f@[205.160.76.171]>

To: Graham Klyne <GK@ninebynine.org>

Cc: www-rdf-logic@w3.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 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/~phayesReceived on Monday, 19 March 2001 00:18:18 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:34 UTC
*