Layering LX (near-FOL) on RDF

I'm getting closer to a compelling demonstration of same-syntax
semantic extension for RDF.

Here is my approach:

  1.  I view RDF as a sublanguage of FOL.   I use Otter's FOL syntax,
      and a few straightforward syntactic conventions.  The N-Triples
      line
	  _:x <http://www.w3.org/1999/02/22-rdf-syntax-ns#type>
				     <http://example.com/animals#Dog> .
      translates to FOL/otter as
          exists x (rdf(x, rdf_type, '<http://example.com/animals#Dog>')).   

      RDF as a sublanguage of FOL has just conjunction, existential
      quantification, and a ternary predicate called "rdf".  I have
      not established a system for handling literals yet, because it 
      seems unneccesary for this exercise.

  2.  I define another sublanguage of FOL, called LX, which is a
      superlanguage of RDF including the other standard logical
      operations (disjunction, negation, conditional, biconditional,
      universal quantification, and existential quantification).  I
      have not yet included arbitrary predicates and function terms,
      but I see no significant problem with doing so.  I also write LX
      with otter syntax, but of course one could use any FOL syntax
      easily enough.

  3.  I define an RDF vocabulary/ontology [1] for describing LX
      sentences.  This is similar to Drew McDermott's vocabulary for
      describing FOL sentences [2][3], except that I include a
      limitted truth predicate, allowing one to describe particular LX
      sentences as being true.  As with wtr in KIF3[6], this truth
      predicate does not allow arbitrary nesting.  (See [5] for
      details.) 

  4.  To explore my understanding of this layering, I have written a
      set of axioms [4] for LX-described-as-true-in-RDF.  I use
      otter with these axioms to perform inference on reified-as-true
      LX; I also use otter to prove the axioms are satisfiable.
      
My axioms are still flawed.  After considerable effort I still have
not been able to use them to produce certain more-complicated proofs
involving quantification.  So I cannot claim that the axioms are
correct while being satisfiable, but I do think producing such axioms
is very probably possible.  I don't want to go that last mile (feeling
a little like a blind man in a maze -- I find this kind of thinking
very difficult) unless it's really necessary.

(After writing that I went another quarter mile, doing another set of
axioms to investigate the liar paradox more closely.  See [5].)

So my question is: is there a flaw in this kind of layering?  If so
where?   If you're sure there is, but can't say where, then what more
details and evidence do you need?

(Note that I was calling this work "Positive Triples Logic (PTL)" for
a while, until I decided negation was worth the problems it might
cause.  I see no major obstacle to extending LX up to full FOL.) 

   -- sandro
    
[1] http://www.w3.org/2002/08/LX/RDF/v1.n3   
[2] ftp://ftp.cs.yale.edu/pub/mcdermott/papers/noworry.ps.gz 
[3] http://link.springer.de/link/service/series/0558/bibs/2342/23420250.htm
[4] http://www.w3.org/2002/08/LX/RDF/ax3.20020822T1630.html
[5] http://www.w3.org/2002/08/LX/RDF/ax4.20020822T1630.html
[6] http://meta2.stanford.edu/kif/Hypertext/node35.html

Received on Thursday, 22 August 2002 17:12:23 UTC