same-syntax extensions to RDF

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
          _:x rdf:type lx:UniversalQuantification.    # implied
          _:x lx:univar _:y.
          _:y rdf:type lx:UniVar.                     # implied
          _:x lx:negated _:z.
          _:z rdf:type lx:Sentence.                   # implied
          _:z rdf:type lx:Triple.                     # 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.

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.   
 
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.

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.)

      -- sandro

Received on Wednesday, 15 December 2004 23:28:54 UTC