W3C home > Mailing lists > Public > public-rdf-comments@w3.org > June 2013

Re: Are Skolem IRIs uninterpreted?

From: Pat Hayes <phayes@ihmc.us>
Date: Mon, 17 Jun 2013 12:10:32 -0500
Cc: public-rdf-comments <public-rdf-comments@w3.org>
Message-Id: <9BE6EA74-97AD-4B4B-8DF2-0A6F06AB0E30@ihmc.us>
To: Gregg Reynolds <dev@mobileink.com>

On Jun 17, 2013, at 7:23 AM, Gregg Reynolds wrote:

> Hi,
> Is it correct to say that there is an implicit requirement that Skolem
> IRIs be treated as uninterpreted?  


> RDF11-MT
> (https://dvcs.w3.org/hg/rdf/raw-file/default/rdf-mt/index.html#skolemization-1)
> just says that skolemization coins fresh IRIs.


> The reason I ask is that the technical definitions of e.g. Skolem
> Normal Form ([1]) and Skolem function ([2]) suggest that they should
> be interpreted.

They should, yes. Logically they are just names like any other name. 

>  But then RDF11-MT states:
> "G does not entail sk(G) (since sk(G) contains IRIs not in G.)" (where
> sk(G) is the skolemization of graph G).
> 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). 

>  But since G does
> not entail sk(G), I conclude that Skolem IRIs in RDF are to be treated
> as uninterpreted.

Wrong conclusion :-)

>  In other words "skolemization" in RDF does not
> refer to the logic concepts associated with skolem function, skolem
> normal form, etc.

Also a wrong conclusion. It is exactly the trivial case of skolem functions where the function has no arguments. 


> Is that correct?
> Thanks,
> Gregg Reynolds
> [1] "Mathematical Logic", Ebbinghaus, Flum, Thomas; page 132
> [2] "The Language of First Order Logic", Barwise & Etchemendy, page 269

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
Received on Monday, 17 June 2013 17:11:01 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 16:59:34 UTC