Re: A Single Foundational Logic for the Semantic Web

[...]

> 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