Russell's Paradox, Updating an Open Theory, and Negation as Failure

Hi All --

The notion of assuming something is false if you cannot prove it is often
deprecated as 'nonmonotonic' in Semantic Web circles, even though it is
widely used in practice in SQL databases.

The notion is often implemented under the name Negation as Failure (NAF).

Besides its use with SQL databases, NAF also used in some deductive rule
systems, such as Internet Business Logic [1] (IBL).

If we use NAF, a statement such as "P is true if we cannot prove P" is
intuitively wrong.  So, programming languages such as Prolog misbehave when
asked to compute with this kind of thing, and there is a notion of layering,
or stratification, which can be enforced syntactically to avoid this kind of
statement.  The IBL system has such a syntax check.

Curiously, Russell's Paradox in set theory [2] is also intuitively
problematic, and it led mathematicians to develop are related notion of
stratification.

There's a version of the paradox that is often used to explain it in
concrete terms.  It goes like this.

*In a certain village, the barber shaves all (and only) the men who do not
shave themselves.
Who shaves the barber?

If it's the barber there's a contradiction -- he is shaving himself, but
he's only supposed
to shave those who do not shave themselves.

If someone else shaves the barber, there is also a contradiction -- the
barber is
supposed to shave those who do not shave themselves.*

In the IBL system [1], one can state the barber version of Russell's Paradox
like this [3].

*some-person lives in the village
not : that-person shaves himself
----------------------------------------------
B shaves that-person


this-person shaves this-other-person
==========================


this-person lives in the village
=====================
 A
 B
 C


this-person is a barber
=================
 B*

However, the IBL also has a notion of stratification, and it checks and
finds that the above rule is not meaningful.  It produces a "Check" page
explaining why.

To see this working, you could point a browser to [1], click on "Internet
Business Logic", then on "GO", and select RussellParadox.

As previously discussed on the Ontolog Forum, there's an interesting
correspondence between what happens when one updates a theory using NAF, and
what happens when doing the same thing using classical "open" negation.
Briefly, adding a missing fact P under NAF corresponds to starting with an
"open" theory containing ~P, adding P, then noting that there is a
contradiction that must be removed before a respectable theorem prover will
process this, and therefore removing  ~P.

I hope this may be of interest, and thanks for comments,

                                       -- Adrian

Adrian Walker
Reengineering


[1]  Internet Business Logic
A Wiki and SOA Endpoint for Executable Open Vocabulary English over SQL and
RDF
Online at www.reengineeringllc.com    Shared use is free

[2]  http://en.wikipedia.org/wiki/Russell's_paradox

[3]  www.reengineeringllc.com/demo_agents/RussellParadox.agent