Re: A Single Foundational Logic for the Semantic Web

From: jos.deroo.jd@belgium.agfa.com
Subject: Re: A Single Foundational Logic for the Semantic Web
Date: Tue, 30 Apr 2002 21:47:27 +0200

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

[...]

I was being a bit brief in my reasoning.  Here is some more detail.


To more fully investigate the status of n3 with the log: vocabulary, we
need to look at what sorts of things have to exist in all models.

A simple analysis shows than every formula has to exist in every model.
Otherwise formulae like 

	_:a rdf:type rdf:Statement .
	_:a rdf:subject ex:s .
	_:a rdf:predicate ex:p .
	_:a rdf:object ex:o .
	_:a log:implies _:a .

are not valid, which goes against the intended meaning of log:implies.

[From this, and from the intended meaning of this to refer to documents as
a whole, every conceivable document has to exist in every model.  However,
let's try to produce a paradox without reference to documents.]

Even formulae like the following have to exist in all models

	_:b rdf:type rdf:Statement .
	_:b rdf:subject _:b .
	_:b rdf:predicate rdf:type .
	_:b rdf:object n3:falsehood .

this is, more-or-less, 

	{ this a n3:falsehood }

Now does this formula belong to log:Truth?  If it does, then it is a true
formula, and thus is a falsehood, because it belongs to n3:falsehood, and
thus it can't belong to log:Truth.  If it does not, then it is a non-true
formula, and thus is a truth, because it does not belong to n3:falsehood,
and thus it must belong to log:Truth.

Thus log:Truth is ill-defined (model theory) or self-inconsistent (truth
theory) everything falls apart.


Note that this line of reasoning requires lots of assumptions as to the
meaning of the various n3: and log: constructs.  Note also that it is not
necessary to use n3:falsehood---most any contradiction can be embedded in a
self-referential formula.


peter

Received on Tuesday, 30 April 2002 16:36:58 UTC