From: <jos.deroo.jd@belgium.agfa.com>

Date: Tue, 30 Apr 2002 21:47:27 +0200

To: pfps@research.bell-labs.com

Cc: sandro@w3.org, phayes@ai.uwf.edu, www-rdf-logic@w3.org

Message-Id: <OFCBB60AED.53261F74-ONC1256BAB.00686C6E@bayer-ag.com>

Date: Tue, 30 Apr 2002 21:47:27 +0200

To: pfps@research.bell-labs.com

Cc: sandro@w3.org, phayes@ai.uwf.edu, www-rdf-logic@w3.org

Message-Id: <OFCBB60AED.53261F74-ONC1256BAB.00686C6E@bayer-ag.com>

[...] > 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. Well I didn't follow completely. I can follow the trouble you get with a *builtin* contradiction but not when you write a paradox *in* a language. As I indicated in www-webont-wg "the decision stuff requirement" -> http://lists.w3.org/Archives/Public/www-webont-wg/2002Jan/0091.html the latter one just gives rise to incompleteness and I would say proof theoretically it is *im*possible to derive *either* the formula *or* its negation (which could indeed be like saying that there are no models for a paradox). E.g. if I write *in* N3 { ?x a :R } log:implies { ?x a [ owl:complementOf ?x ] } . { ?x a [ owl:complementOf ?x ] } log:implies { ?x a :R } . and asking :R a :R . we match with the consequent of the 2nd implication so we try to prove it's antecedent and that one matches with the consequent of the 1st implication so we try to prove it's antecedent but that is what we were already trying to prove... That is of course assuming that triples in antecedents and consequents are unasserted. -- Jos PS indeed a Horn clause is a disjunction with at most one positive literal but we never assert clauses with no positive literal (which is a query)Received on Tuesday, 30 April 2002 15:48:54 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:38:23 UTC
*