- From: pat hayes <phayes@ai.uwf.edu>
- Date: Thu, 8 Mar 2001 19:36:21 -0600
- To: Sandro Hawke <sandro@w3.org>, "Tim Berners-Lee" <timbl@w3.org>
- Cc: www-rdf-logic@w3.org
>And you can remove an existentially quantified variable in an asserted >context by replacing it with a new term (that is, by skolemization), >right? > >In another context, like a negated context or a query, I agree >skolemization would be wrong. I guess I should have been more explicit. If you think about skolemization in second-order logic it is much clearer what is going on. (It also happens to be valid in second-order logic.) The usual way of describing skolemization is that an existential inside a universal, ie (informal logical syntax:) (forall ?x )[(exists ?y) R(?x ?y)] can be replaced by a 'new' function name f, ie one not used anywhere else: (forall ?x) R(?x f(?x) ) But that phrase 'new' is really first-order-logicspeak for 'there exists', and in second-order syntax the *real* skolemised form is: (exists ?f)[(forall ?x) R(?x ?f(?x))] ie the existential hasn't been eliminated, only brought to the front. So this is really only a quantifier-swap, like changing (forall ?y forall ?y...) into (forall ?y forall ?x...), but it just has this extra complication that when you do it with quantifiers of different kinds, you have to keep track of what depends on what, which is why the simple existential becomes a functional existential. In any order logic, a simple existential at the top (ie not inside a universal) can always be exchanged for a name (of the appropriate kind, and as long as you don't use a name already in use, of course), so you can get the usual kind of skolem function by doing that next. But that is just existential instantiation, which is kind of trivial. There really isnt much logical difference between a top-level existentially quantified variable and an 'anonymous' name. Sorry if this is old hat to y'all, I just thought it might be of interest. 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 Thursday, 8 March 2001 20:34:54 UTC