Re: Are Skolem IRIs uninterpreted?

On Mon, Jun 17, 2013 at 12:10 PM, Pat Hayes <phayes@ihmc.us> wrote:
>
> On Jun 17, 2013, at 7:23 AM, Gregg Reynolds wrote:
>
>> If I've understood skolemization (the logical concept, not just
>> generation of unique IRIs) then G should entail sk(G)
>
> No. G never entails sk(G) in FOL.
>
>> since each
>> Skolem IRI in sk(G) picks out a witness that makes its triples true,
>> which would only be the case where G is satisfied.
>
> No. I am not sure what you mean by "picking out a witness". The point is that one can create an interpretation which (perversely, if you like) interprets the skolem IRIs to refer to different things, and then choose those things to make the triples false, even though the bnode versions of them are true because the "right" things are still lying around in the universe. That is why G does not entail sk(G), because such an interpretation will satisfy G but not sk(G).

Thanks.  I believe the scales have fallen from my eyes.  My mistake
was thinking that skolemization imposes a constraint on
interpretation, e.g. in skolemizing from %Ex.Px to Pc, c is to be
taken as assigned to a value that makes Pc true (hence "picks a
witness").  The trick is to see how skolemization is purely syntactic,
and that Pc is about whatever individual happens to be assigned to c,
whereas %Ex.Px is about the world.  So you can have a model of %Ex.Px
that assigns c to a value that makes Pc false, which is ok since Pc
isn't a claim about the world.  (E.g. Even(c) always entails that
there is an even number in the world, but that an even number exists
does not entail that Even(c) is true when e.g. c=3.)

Incidentally, doesn't skolemization involve extending the symbol set?
The explanations I've seen say something like "use a fresh constant",
which I originally took to mean one not used in a formula; but it
looks like it must mean "add a new symbol to the symbol set of the
language".  For example, if we have only the digit symbols and our
domain is the integers, then to skolemize %Ex.Even(x) we need to add
'c' or something like that to our symbol set.  But if that's the case,
then technically skolem IRIs would have to be non-IRIs, at least if we
take the symbol set of RDF to include all possible IRIs.  So in
practice blank node skolemization cheats a little and just says "use
an IRI that is highly unlikely to be in use anywhere".  Correct?

Thanks,

Gregg

Received on Tuesday, 18 June 2013 04:10:15 UTC