- From: Sandro Hawke <sandro@w3.org>
- Date: Mon, 29 Apr 2002 22:22:16 -0400
- To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
- cc: phayes@ai.uwf.edu, www-rdf-logic@w3.org
> > [...] > > > 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