Re: Grist for layering discussion

Butting into Peter and Sandro's discussion... and making a point different
from Sandro's.

Abstract: The n3 logic system does not fall for Russel's paradox because it
doens't allow
  an implicit introduction of contradictory statemnts in the definition of a
set.

----- Original Message -----
From: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
To: <sandro@w3.org>
Cc: <phayes@ai.uwf.edu>; <hendler@cs.umd.edu>; <timbl@w3.org>;
<las@olin.edu>; <connolly@w3.org>; <w3c-semweb-ad@w3.org>;
<www-archive@w3.org>
Sent: Friday, January 11, 2002 11:28 AM
Subject: Re: Grist for layering discussion


> From: Sandro Hawke <sandro@w3.org>
> Subject: Re: Grist for layering discussion
> Date: Fri, 11 Jan 2002 10:42:06 -0500
>
> [...]
>
> > > The third price is that we have introduced a form of reification and a
> > > construct that can assert the truth of reification constructs.  This
> > > (probably) doesn't cause any problems here because the extension is so
> > > expressively limited.  However, for more powerful extensions
reification
> > > produces paradoxes, and thus cannot be used.
> >
> > Two answers here.
> >
> > 1.  I've heard some people say, "Who Cares?"  Operationally, what's
> > the problem with a paradox?  My guess is it will show up as infinite
> > loops and/or bottomless recursion, which is unpleasant but can be
> > managed as a resource-management problem.  That is, in theory there's
> > a huge difference between a paradox and a problem that will simply
> > take 4 hours to terminate, but operationally they're both just systems
> > that go off into the weeds.  The user presses "stop" and everything's
> > fine again.
>
> Who cares?  Just the people that matter, that's all.  By the ``people that
> matter'', I don't mean just Pat and myself, I mean anyone who wants to
> implement or work with the formalism.
>
>
> A formalism with a paradox is fundamentally broken.

We need to be specific here.  A formalism which allows the expression of
a paradox is OK, so long as you can't use it to deduce that it is snowing.
So we have to be clear what "with" means here.

>  The breakage can
> appear in several ways.  For standard logics the breakage will often show
> up as a breakdown in the retrieval specification.
>
> For example, consider initial versions of set theory that allowed the
> creation of { x : x not in x }.  In a formalism that includes this paradox
> it is generally possible to reason as follows:
>
> Assume that John is in { x : x not in x }
> Then John is not in { x : x not in x }.
> Contradiction, so John is in { x : x not in x }
> implies that it is snowing.
> Assume that John is not in { x : x not in x }
> Then John is in { x : x not in x }.
> Contradiction, so John is not in { x : x not in x }
> implies that it is snowing.
> Thus it is snowing.

You are using the Principle of Excluded Middle (PEM) here - forall p, p or
not p.
That doesn't work.

Simply the construction    "S is the set of x such that F(x)"  { x: F(x)}
cannot be allowed as such in our system, as it carries a PEM assumption
in its core.  The concept of set is a well-defined partitioning of all
things
into two, and this is done, in the "such that" construction, by mapping
between things and the truth of formulae about things. However, in general
formulae are not necessarily either true or not true. We admit to the
existence of
paradoxes and tautologies.

The parlour trick in Russel's paradox is that the constraint "x is not a
member of itself"
is specified in a clause which makes "the set of all sets which are not
members
of themselves" look like a noun clause.  It isn't.   Breaking it down into
the
sort of logic we have in DAML with N3 rules, we have to say

There exists some c:such that:
  For all x:
    :c  rdf:type rdfs:Class.               # There is some class (we don't
have sets)
    {   :x rdf:type [ daml:complementOf :c]  } log:implies { :x rdf:type
:c }.  # if
    { :x rdf:type :c } log:implies {   :x rdf:type [ daml:complementOf
c]  }   # and only if.


(There is a philosophical difference that on the semantic web we can't
really
talk about a "definition" of something.  A document can introduce a concept
and
assert things about it.  But those things have no logical status above any
other
statements [[[apart from socially their authorship by the owner of the
concept
which is what mean by their being definitive]]].  Most programming langauges
allow you to define a function as that which, and separately say things
about it.)

These are a set of assertions.  They are not a set which I would accept in
my
/etc/rc.n3 file, as they clearly lead to a contradiction because if we
subsitute :c for :x
we get something which is a member of both a class and its complement, which
we know
is false. So we could use it to prove that it is snowing.

However, this set of contradictory statements have no more status than any
other
set such as "There is something equiavlant to "1" and to "2".

    :joe rdf:type :f, [ is :complementOf  :x ].

or for that matter

       [ = "1", "2"]

[[[If we allow the "such that" construction then we are sunk anyway, we can
stick any old paradox in, not even a function of x:

{x:   "preceded by itself in quotes is a false statement" preceded by itself
in quotes is a false statement.}

{ x:  {this  a log:Falsehood} }                       #(mixing braces a bit
there :-/  )
]]]

> So the operational result of this paradox is not an infinite regress, but
> instead the production of any consequence whatsoever (and very quickly).
>
> A reasoner based on model theory could be even faster.
>
> There are no models for KBwhatever.
> Therefore it is snowing is true in all models for KBwhatever.
> Reply that it is snowing.
>
> Again, no long computation, just strange results.

But looked at as above just bad results coming from bad data - gigo.

However, it seems to me one could make a functional system of any size which
to do real work and which does not have a built-in contradiction
and in which an agent cannot use the logic to generate one out of thin air.
But I don't have a theory for it.

tim

> peter
>

Received on Saturday, 12 January 2002 14:27:17 UTC