Re: A Single Foundational Logic for the Semantic Web

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

[ quiet curses at this medium, where the reply chains always come from
the parts of my e-mail which are the least well explained...  but I
guess that's why the reply chains come from there.... ]

I'm sorry for getting you interested and not giving you proper
information.   I really didn't expect anyone to take that part of my
message so seriously so quickly.  

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],
but more of the community seems comfortable with n3/cwm, so let's
stick to that.  I'm going to try to restrict their imprecises
semantics for quantification to something cleaner.  Alas, you seem to
have looked at an out-of-date version of cwm's logic (if Falsehood was
still there), not the one I linked from my first message in this chain
[2].  Can you tell me where you saw log:Falsehood?

So here's the deal:

  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
     rdf:subject rdf:predicate rdf:object
  to describe an n3 atomic Formula, and you can use
     log:conjunction, whose domain is a DAML list of 2+ formulas and
  range is the formula which is their conjunction; 
     log:implies whose domain and range are both formulas and means
  about what you think it does;
     log:forSome and log:forAll, each of whose domain is a formula and
  whose range is unlimitted.  These quantifiers act like this:
           _:formula1 log:forAll _:var

  is true if and only if the formula 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.  I'm forgetting at the moment why I think the name
is unkn) 

log:forSome has no expressive power except inside the consequent
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.





> 
> So, just what am I allowed to use?  What meaning am I to assign to the
> semi-logical constants (like log:implies)?
> 
> If I am allowed to use anything on
> http://www.w3.org/DesignIssues/Notation3.html, and I can use them in what
> appears to be their intended meanings, I get quite a bit more than
> log:forSome, log:forAll, and log:implies.  In particular I can create
> conjunctions of formulae (using { ... }) and I can even use negation
> (n3:falsehood).  It appears that I can even use self-referential structures
> (with ``this'', whose definition is in
> http://www.w3.org/2000/10/swap/Primer.html).  
> 
> 
> A theory for all this is not trivial.
> First of all there are lots of tautologies, like
> 	?x log:implies ?x .
> and even some unsatisfiable statements, like
> 	{ ?x log:implies ?x } a n3:falsehood .
> where ?x is any formula.
> 
> 
> Now what about a document that consists of the following single statement:
> 	this a n3:falsehood .
> Consider any interpretation for the document. Suppose the statement is
> true in the interpretation.  But then the statement is false, because the
> entire document belongs to n3:falsehood, and the statement is the only
> statement in the document.  Suppose the statement is false in the
> interpretation.  But then it is true, because the entire document does not
> belong to n3:falsehood and the statement is the only statement in the
> document.  Thus it is impossible to assign a truth value to this
> statement (and document), thinking model theoretically, or it is possible
> to derive both this formula and its negation, thinking proof
> theoretically.
> 
> (The document is, of course, just the liar's paradox in another guise. If
> anyone is uncomfortable with the use of an implicit scope for ``this'', the 
> statement  
> 	{ this a n3:falsehood } a log:Truth .
> under a reading that log:Truth is contingent truth would have done just as
> well.) 
> 
> Thus, depending on how you look at these things, either n3 has no models,
> and thus any reasoning in it is suspect, or any theory of n3 has a built-in
> contradiction, and thus any reasoning in it is suspect.
> 
> 
> 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.
> 
> 
> Peter F. Patel-Schneider
> Bell Labs Research
> 
> 
> 
> 

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

Received on Monday, 29 April 2002 22:25:54 UTC