Re: SUO: Re: Peirce's MS 514
> >The common example of the need for care over the choice of namespace
> >is that of Skolem functions, which are 'new' function symbols are
> >introduced to replace existential quantifiers, so that one can replace
> >(forall (?x) (exists (?y) (R ?x ?y))
> >with
> >(forall (?x)(R ?x (fun ?x)))
> >These are almost the same in meaning, if you think about it, but the
> >first does not entail the second because the second one uses a symbol
> >which isnt in the namespace of the first one.
>
>Yes, but you could (in a second-order notation) add another
>quantifier that ranges over functions:
>
> (forall (?x) (exists (?fun) (R ?x (?fun ?x))))
Or, better: (exists (?fun) (forall (?x) (R ?x (?fun ?x))))
I.e. skolemization is really a process of bringing existentials to
the front of the expression. My point above is illustrated here by
the fact that in second order, ?fun is a variable, so there isn't a
new name, so the vocabularies are the same, and indeed the inference
is then (second-order) valid.
Pat
---------------------------------------------------------------------
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