Re: same-syntax extensions to RDF

In general this is much to vague.  You don't need to (at this stage) dot
all the i's and cross all the t's, but this is much more like waving a
magic wand.  Specific comments are embedded below.



From: Sandro Hawke <sandro@w3.org>
Subject: same-syntax extensions to RDF
Date: Wed, 15 Dec 2004 18:31:53 -0500

> Here's an approach to extending RDF to FOL, while staying within the
> RDF syntax.  You've talked about this being difficult or impossible.
> Do you see a fatal flaw in the approach I sketch below?
> 
> There are three parts to this: reification, connection, and assertion.
> 
> 1. Reification 
> 
>      The first part of this approach is to put the non-RDF formulas
>      into the domain of discourse.  This "pollutes" the domain of
>      discourse and means the semantics of this approach can't be
>      exactly the same as with vanilla FOL, but I don't think this
>      pollution causes any difficulty in Semantic Web uses cases.
> 
>      Syntactically, reification is quite straightforward in vanilla
>      FOL if the syntax of logical formulas is not distinguished from
>      that of logical functions.   For instance:
> 
>          (and (color car red) (wheels car 4))
> 
>      is a sentence in a KIF-like language, but the same text is a term
>      in this atomic sentence:
> 
>          (requirements purchase342 (and (color car red) (wheels car 4)))
> 
>      In the second example, "and" is the name of a logic function, not
>      a logical connective.  One presumably does this because someone
>      down the line will treat it as a logical connective, but at this
>      point the second argument to "requirements" is something in the
>      domain of discourse, perhaps an instance of a Sentence or Formula
>      class.
> 
>      No surprises so far, right?  This is a lot like what Pat calls
>      "punning", although for a different purpose.  He does it in
>      Common Logic to allow function and predicate names to be used to
>      also name individuals; I'm using it to allow predicate names and
>      logical connectives to be parsed as logical function names.
> 
>      This is all syntactic sugar we don't have in RDF triples anyway,
>      so let's get dirty here and look at some triples.
> 
>      Image we want to say that everything is an rdf:Resource.  We're
>      in part 1 (reification) so we'll just say "there exists a
>      sentence which says that everything is an rdf:Resource". 
> 
>      Something like this:
>   
>           @prefix lx: <http://www.w3.org/2004/12/LX>
>           _:x rdf:type lx:Sentence.                   # implied
Why implied?
>           _:x rdf:type lx:UniversalQuantification.    # implied
Why implied?
>           _:x lx:univar _:y.
>           _:y rdf:type lx:UniVar.                     # implied
Why implied?
>           _:x lx:negated _:z.
>           _:z rdf:type lx:Sentence.                   # implied
Why implied?
>           _:z rdf:type lx:Triple.                     # implied
Why implied?
>           _:z lx:subjectTerm _:y.
>           _:z lx:predicateTerm _:rdftypeTerm.
>           _:z lx:objectTerm _:rdfResourceTerm.
>           _:rdftypeTerm rdf:type lx:Constant.    
>           _:rdfResourceTerm rdf:type lx:Constant. 
> 
> 
>     I don't think there are any surprises here.  I'm just saying that
>     a universal quantification exists of some triple; the universally
>     quantified variable is the subject of the triple, and the predicate
>     and object are constants.   I have neither asserted this sentence
>     nor connected those constants with rdf:type and rdf:Resource yet.

No surprise, but that is only because there is nothing here to criticize.

What counts as a formula?  What counts as a variable? (Any RDF name??)  

You need to at least give a sketch of the comprehension principles.  (There
are lots of examples in the OWL S&AS document.)

> 2.  Connection
> 
>     I see two approaches to connecting those constant symbols
>     (_:rdftypeTerm and _:rdfResourceTerm) to RDF.  The one that I've
>     had the most success implementing looks like this:
> 
> 	  _:rdftypeTerm lx:denotation rdf:type.
>        	  _:rdftypeTerm lx:denotation rdf:Resource.
> 
>     This says that reified terms map to the given individuals in all
>     models.  It's trivial to axiomatize.
> 
>     Another approach (which TimBL's reification vocabulary uses) would
>     use triples like this:
> 
> 	  _:rdftypeTerm lx:text 
>                       "http://www.w3.org/1999/02/22-rdf-syntax-ns#type".
>           _:rdfResourceTerm rdf:type lx:Constant.
>                       "http://www.w3.org/1999/02/22-rdf-syntax-ns#Resource".
> 
>     which is appealing in keeping RDF and the described logic
>     separate, but then they need some extra-logically machinery to be
>     re-combined.   

I'm not sure why you need this at all.  Why not just do it directly, i.e.,
have 
	_:z lx:objectTerm rdf:Resource.
above?

> 2.  Assertions 
> 
>     So how do we assert this sentence, _:x ?
> 
>     The obvious approach is to say 
> 
>           _:x rdf:type log:Truth
> 
>     which might work for cwm/n3's reification which lacks negation
>     (it's roughly positive Horn), but for FOL (which I'm proposing
>     here) it becomes trivial to construct a Liar paradox.  So that's
>     no good.
> 
>     The alternative I propose is to say, instead:
> 
>          _:x rdf:type lx:Usable
> 
>     The definition of Usable is merely this: for a sentence to be
>     lx:Usable, it must be true.  There may be true sentences which are
>     not lx:Usable.  Nothing follows from knowing that a sentence is
>     not lx:Usable.
> 
>     The sentence S1 which says "S1 is not Usable" is true.  (If S1 were
>     false, S1 would be Usable, which would mean (since Usable implies
>     true) S1 would be true, which contradicts the premise.  If S1 were
>     true, ... no problem.)   
> 
>     The sentence S2 which says "S2 is Usable" isn't a problem either.
>     If it's true, then S2 is Usable, which is consistent with S2 being
>     true.  If it's false, then it's not Usable, which is also
>     consistent with S2 being False.
> 
>     My intuition here is that some class of sentences is
>     "problematic", and we don't want to talk about whether those
>     sentences are true or false.  So Usable is basically: true and not
>     problematic.  But by not separating those in the language not
>     naming True, False, and Problematic in the language, we keep the
>     language itself (and the reasoners) clear of the problematic zone.

I don't think that this works at all.

One thing that you *need* to come out of this is that the theorems of FOL
are true in all interpretations (roughly, see below).  So, for example, you
need to have the encoding of
	Axy Pxy v ~Pxy
be true in all interpretations.  How are you going to get this to do
through?

(It might be the case that the above is only true provided that P is
stated to be a predicate somehow, but then you need to have a mechanism for
so stating, and you have only pushed the problem back a bit because then
you need 
	Axy Pxy v ~Pxy
to be true in all interpretations where P is a predicate.)

> There you have it.  Go ahead and throw your rocks now.  :-)
> 
> (Or, if I haven't given you any solid enough targets, let me know
> where you'd like it made more solid.)

Not only is this not solid, its not even vapour yet.  (No joke.)

>       -- sandro

peter