Re: Grist for layering discussion

From: "Tim Berners-Lee" <timbl@w3.org>
Subject: Re: Grist for layering discussion 
Date: Fri, 11 Jan 2002 20:04:27 -0500

> ----- Original Message -----
> From: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

[...]

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

If it doesn't break the formalism, then it isn't really a paradox.

[..]

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

And why not?  RDF and DAML+OIL (and OWL) have the Law of the Excluded Middle.

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

Well, it is possible to move to a logic with a gap truth value, i.e., that
does not have the Law of the Excluded Middle, and in which Russel's paradox
is no longer a paradox.

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

HUH?  Who said anything about noun phrases?
Please, let's stick to things that make logical sense.

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

Sure, these are implications that carry some of the import of the
paradoxical set.

> (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.)

Well if this is the case (that the semantic web can't talk about the
definition of anything, then we might as well quit and go home!
We can't talk about the class of people with two children, the class of
employees that manage employees that manage employees, etc., etc.


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

Yes, you certainly don't want these implications.

> 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"]

Yes, that set of contradictory statements does not have a priviledged
status.  However, the restriction construction that I have noted does.

> [[[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 :-/  )
> ]]]

Well if you can state these, which, of course, depends on how powerful your
logic is, then you get problems.


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

The WHOLE point of this debate is NOT that the above implications are
contradictory.  The point is, instead, that making DAML+OIL comply with the
new RDF model theory ends up requiring the presence of many restrictions (and
other syntactic constructs) in all interpretations.  Among these
restrictions are ones that embody Russel's paradox.

So it's not garbage-in-garbage-out, it's nothing-in-garbarge-out, or
anything-in-anything-out.

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

Yes, and the whole thrust of formal representation theory is to come up
with specifications of such systems (at least ones that are supposed to be
doing things that relate to representation).  The formal theory embodies a
collection of basic principles (like ``anything implies itself'') and
specifies the implications of the principles.

peter

Received on Saturday, 12 January 2002 17:47:58 UTC