Re: Are Skolem IRIs uninterpreted?

* Pat Hayes <phayes@ihmc.us> [2013-06-19 02:40-0500]
> 
> On Jun 17, 2013, at 11:09 PM, Gregg Reynolds wrote:
> 
> > 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?
> 
> Yes. Which is why its not strictly valid, by the way :-)

Does "not strictly valid" mean it violates some type constraints
because you're robbing from one symbol set to create another?


> > 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".
> 
> Well, you can always say that your language contains an infinite stock of symbols waiting to be used for this purpose. Which is what the current RDF sematnics does, in effect. 
> 
> >  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.  
> 
> Right, if you are already using all the names in your vocabulary then when you need a new one you have to grow the vocabulary.
> 
> > 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.
> 
> No, it just has to be an IRI that hasnt been used before. People coin new IRIs all the time.
> 
> >  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?
> 
> It depends how you do it. You might for example put a timestamp and a unique local identifier into it to make it unique.
> 
> Pat
> 
> > 
> > Thanks,
> > 
> > Gregg
> > 
> > 
> 
> ------------------------------------------------------------
> IHMC                                     (850)434 8903 or (650)494 3973   
> 40 South Alcaniz St.           (850)202 4416   office
> Pensacola                            (850)202 4440   fax
> FL 32502                              (850)291 0667   mobile
> phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes
> 
> 
> 
> 
> 
> 

-- 
-ericP

Received on Wednesday, 19 June 2013 12:08:01 UTC