[ontolog-forum] Russell's Paradox, Updating an Open Theory, and Negation

["Adrian Walker" <adriandwalker@xxxxxxxxx>]

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

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (01)