Re: A Single Foundational Logic for the Semantic Web

From: Sandro Hawke <sandro@w3.org>
Subject: Re: A Single Foundational Logic for the Semantic Web 
Date: Mon, 29 Apr 2002 14:39:11 -0400

[...]

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


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

Received on Monday, 29 April 2002 17:10:32 UTC