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

Well, lots to the general issue of skolem functions, but I havnt seen 
anything on the 'second-order' point.

There is some very interesting-looking recent work on 'game-theoretic 
semantics' which Google found for me what I asked it to check skolem 
function + second-order logic, but I havnt digested it yet:
http://www.hf.uio.no/filosofi/njpl/vol4no2/gamesem/index.html

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

Yes, the contrast between
(P is provable iff Q is provable)
and
( (P <=> Q) is provable)
is a nice way to emphasise the difference between provability and implication.
However, in second-order logic, an expression IS genuinely equivalent 
to its second-order skolemised form. Transcriptions of second-order 
into first-order cannot infer the *existence* of a function from what 
might be called a functional relationship (forall....exists....), but 
it does follow in real second-order logic. It's a pity that real 
second-order inference isn't r.e. :-).

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

Im not quite sure what the problem is. A functional term is still 
just a term; in LISP it would be a list starting with the function 
symbol. Encoding arbitrary term structures into RDF, admittedly, I do 
not know how to do.

I think the basic problem for RDF is to figure out how to indicate 
quantifer scopes. Once we have that, the rest will come out in the 
wash.

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 Friday, 9 March 2001 18:02:05 UTC