Re: Layering LX (or FOL) on RDF

> > I'm proposing that the logical formula
> > 
> >     % there exists a triple whose subject is itself
> >     exists t subjTerm predTerm objTerm pred obj (
> >       rdf(t, lx_subjectTerm, subjTerm) &
> >       rdf(subjTerm, lx_denotation, t) &
> >       rdf(t, lx_predicateTerm, predTerm) &
> >       rdf(predTerm, lx_denotation, pred) &
> >       rdf(t, lx_objectTerm, objTerm) &
> >       rdf(objTerm, lx_denotation, obj)       
> >     )
> 
> This does not look like a logical formula to me.  What is it supposed to mean?

Would you prefer it as
 
  Eabcdeg (rdf(a, lx_subjectTerm, b) ^ rdf( ... ) ... )
or
  (exists (?t ?subjTerm ?predTerm ?objTerm ?pred ?obj)
          (and (rdf ?t lx_subjectTerm ?subjTerm)
               (...)
          )
  )
?

There doesn't seem to be any standard for ASCII transmission of FOL
formulas.  Of the leading contenders, I use OTTER's syntax because it
has a nice suite of software that uses it.  I mentioned that in
earlier e-mail.  (I haven't found any KIF software I'm comfortable
with yet, but perhaps I haven't looked hard enough.)

> > has the same meaning as any other formula which contradicts the
> > layering axioms or contradicts itself, such as
> > 
> >      % there exists some triple which is both true and false
> >      exist a b c (
> >        rdf(a,b,c) & -rdf(a,b,c)
> >      )
> 
> Again, what logical formula is this supposed to be?

It's a way of saying (p & -p), but I'm restricting myself to the LX
subset of FOL where at the moment I'm only allowing one predicate, the
ternary "rdf".  I don't think this restriction has any serious
utility, it just made defining the language's relationship to RDF
easier.


> > You sound concerned that the triple (self,x,y) doesn't have a truth
> > value, but in my proposal the triples one would have to use to
> > construct such a triple essentially contradict each other, so one
> > can't even phrase the problematic triple to notice that you have no
> > truth value for it.  This seems very like FOL, which disallows
> > self-referencial terms, although it manages such a restriction in a
> > purely-syntactic manner.
> 
> Suppose that I want a theory of entailment in this LX.  I need to be able
> to do things like
> 	p  entails  p v q
> To do that in RDF, I need comprehension principles, which essentially
> require all formulae to exist, including the false ones, because
> 	p  entails  p v ( q & -q )
> and for   p v ( q & -q )  to exist,  q & -q also needs to exist.
> So, every formula needs to exist, and has to be given a truth value.
> 
> So far, so good.  But now how can the self-referential formulae be handled?
> Some of the self-referential formulae are easy, such as x : x (the formula
> that references itself positively) but others are impossible, such as x :
> -x
> 
> So the problem is not that such formulae are false, but that not matter
> what truth value they are given, no model can be constructed for them.
> 
> If you have disallowed self-referential formulae, then you don't have this
> problem.

Good.   I think disallowing them is a reasonable compromise.

> [...]
> 
> > My question is a fairly narrow technical one, not a political one.
> > Can one precisely define a way to reach out from the RDF sublanguage
> > of FOL to full FOL by means of a pre-arranged vocabulary and
> > associated semantics?  
> > 
> > If you think the answer is "No", then please point out the weak link
> > in my demonstration [1].  (If it's in the handling of self-reference
> > in the axioms, then please say so (no need to try to find a flaw in
> > the axioms), and let me polish that area first.  It'll be tricky, and
> > I'd like to avoid the work if it's not necessary.)
> 
> The answer, of course, is yes, as long as?
> 1/ You are allowed to extended the semantics of RDF.

Even if I'm extending them while keeping the syntax the same?  (Or am
I claiming some URIRefs as keywords in my language, no longer letting
them be logical constant symbols as in RDF?  But that's how you use
RDF....)

LX itself is a normal syntactic extension, but the RDF LX layering
vocabulary, which lets one describe and assert LX sentences in RDF is
a same-syntax extension.   I should go reread your Tower of Babel
paper; it seemed like you were saying such things were unworkable.

> 2/ You forbid self-referential statements.

Done.

     -- sandro

Received on Monday, 26 August 2002 21:26:11 UTC