Re: function terms in Euler, n3, and RDF [was: gedcom-relati

> > [Sandro]
> > 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.

> [Pat]
> 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.

It is indeed of interest in that it has made my understanding
of skolemization much more precise. Thank you very much Pat!
(BTW are there any pointers to these matters?)
I also understand that the skolemized reformulation is not
logically equivalent with the original formulation, but if
the skolemized reformulation is provable, so is the original
formulation and that is quite interesting ...
My main practical concern now is how to build an internal
representation of this f(?x) or what kind of computational
mechanisms should be involved?

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Friday, 9 March 2001 08:06:17 UTC