Re: A Single Foundational Logic for the Semantic Web

** OOPS!  Previous draft of this e-mail sent mid-edit!  Please ignore it! **

Peter F. Patel-Schneider writes:
> [...]
> Sandro Hawke writes:
> > Perhaps I'm misreading it; if someone can present a
> > paradox using only log:forSome, log:forAll, and log:implies, then I
> > think I (and I'll venture TimBL and others) will be very interested.
> > [Hrm, I guess you'll have trouble until an n3->n-triples conversion is
> > written down.  It's in public e-mail between me and Tim; I'll dig it
> > up if anyone seriously wants to try.  The idea is to use
> > log:Conjunction and daml:List to assemble an n3 Formula.]
> 
> [...]
> 
> You have to be more precise here.  If *all* I can use is
> log:forSome, log:forAll, and log:implies then I can't even make any
> statement (because I don't have the . to finish the statement).

I'm sorry for getting you interested and not giving you proper
information.   I really didn't expect anyone to approach that part of
my message so suddenly.   Silly me.

I see several different styles of Horn logics for RDF.  I think the
kind I'm most comfortable with is typified by this example of mine
[1], where every logical expression is reified, but more of the
community seems comfortable with n3/cwm where many expressions (like
"<x> implies <y>.") occur directly as triples.  Let's stick to the
more popular form for now.

I'm going to try to restrict their imprecises semantics for
quantification to something simpler, though.  And leave out things
like Falsehood, which I believe Tim has also abandoned.   I'll check
with him on getting it removed from
http://www.w3.org/DesignIssues/Notation3.html.

> So, just what am I allowed to use?  What meaning am I to assign to the
> semi-logical constants (like log:implies)?

  You're allowed to use N-Triples with literals, bNodes, and URI-Refs
  which will just be logical constants to the reasoner.
  (Syntactically distinct literals denote distinct objects, as usual.)

  In addition, you can use the normal
   (1,2,3) rdf:subject rdf:predicate rdf:object
  to describe an n3 atomic Formula, and you can use
   (4) log:conjunction, whose domain is a DAML list of 2+ formulas and
  range is the formula which is their conjunction.  (Alternatively,
  we could allow log:and, which is true iff both its subject and
  object are true formulas.  Such an approach would be more in keeping
  with this less-reified style.)

  => So { <a> <b> <c>. } is equivalent to _:x where
        _:x rdf:subject <a>.
        _:x rdf:predicate <b>.
        _:x rdf:object <c>.
     and { <a> <b> <c>.  <d> <e> <f>. } is equivalent to _:y where
        _:y log:conjunction _:list.
	_:list daml:first _:x.     # as above
        _:list daml:rest _:list2.
        _:list2 daml:first _:z.
        _:list2 daml:rest daml:nil.
        _:z rdf:subject <d>.
        _:z rdf:predicate <e>.
        _:z rdf:object <f>.
      Feel free to use { } terms using this meaning.
      
   (5) log:implies, whose domain and range are both formulas and means
  about what you think it does.  (That is, the triple is known true iff its
  object (3rd element) is known true or its subject is not known
  true.  I hope that's phrased right; I don't want to really introduce
  negation here.  Maybe it would be better to phrase this as a rule
  than as material implication.
   (6,7): log:forSome and log:forAll, each of whose domain is a formula and
  whose range is unlimitted.  These quantifiers act like this:  the triple
           _:formula1 log:forAll _:var
  is true if and only if _:formula1 would be true for any
  consistant subsitution of _:var as an rdf:subject/predicate/object
  in the formula.  More accurately, the substitution is of the object
  denoted by _:var, not the identifier text itself, which is not
  properly knowable, being syntactic rather than in the domain of
  discourse.    (n3/cwm dithers about this, sometimes saying the
  quantifiers are syntax structures instead of plain triples; I
  believe the above is best, although somewhat non-traditional.  I've
  heard people call it "possible worlds" semantics, but I don't know if
  that's appropriate.)

log:forSome has no expressive power except inside the
consequent/conclusion formula of log:implies.

In much of the n3 written, people do things like "this log:forSome
<x>." which seems much trickier, so I'm leaving it out.  If we're safe
without it, then we can consider adding it back.

I think I need some clause about WFFs and self-reference, but I can't
think of the right language.   Something like: all the predicates
involving formulas are not defined for ill-formed or self-referencial
formulas.  If that's where you want to push on the system, I'll try to
be more precise.


> Of course, I had to make a number of assumptions as to the meaning of n3
> constructs in the above argument.  However, I feel that all my assumptions
> are reasonable, given the available documentation on n3.

Absolutely, and I have to apologize again for not being much more
clear in my challenge.  Even though TimBL has
removed/never-implemented log:Falsehood, he has implemented and often
uses log:notIncludes [2], which still supports forms of the liar
paradox given its current documentation.  It might possible to define
it in some form that disallows loops, as I imagine the actual
implementation does.   

My focus here is on something closer to propert Horn clauses.  I'm
using existentially quantified variables and allowing conjunctions in
the consequent, instead of function terms and only an atomic sentence
in the consequent, but I believe the forms are equivalent.

     -- sandro



[1] http://www.w3.org/2001/12/semrun/test-conditional.rdf
[2] midway down http://www.w3.org/2000/10/swap/log.n3

Received on Tuesday, 30 April 2002 07:07:03 UTC