Re: Grist for layering discussion

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


> I have been guilty of misrepresenting the law of the excluded middle.
>
> The Law of the Excluded Middle states that any proposition is either true
> or false, i.e., no other possibilities exist.  There are several logical
> systems that do not have the Law of the Excluded Middle.  These logics, in
> essense, add one, or more, other possible situations for a proposition.
> Some such logics add an ``undefined''; some add a ``contradictory''; some
> add both; some add even more.

I understand from Lynn that basically any finite number of states
leaves you with the same problem. In other words, if the "undefined"
is a state you can deduce something must be in by a process of
elimination then it allows you to construct a paradox.  These seem to be
systems in which the middle is still excluded there are just more things
outside it.  To not not have the PEM at all, you have to limit the
inference so that there are things which, while in fact are not true
or false, you don't have a label for what they are, or axioms for
that label which allow you to hang yourself.

"This statement has truth-value undefined".

>Some logics even abandon the whole idea of
> propositions have a truth value.

Well, I am sure ... though without knowing what replaces it
i don't know how to react.   But for example on the sweb there  is
no absolute truth, there is just the starting place a process takes
for its reasoning.

> From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
> Subject: Re: Grist for layering discussion
> Date: Fri, 11 Jan 2002 20:14:08 -0500
>
> > > The normal way you do it relies on the Princple of the Excluded
middle,
> > > which of course cannot be part of the semantic web.
> >
> > Why not?  Well, of course, I don't want to deduce anything just because
> > some web page says X and some other web page says not X, but there are
lots of
> > formalisms that don't have this property and that have the Law of the
> > Excluded Middle.

Why not? Because you don't want to deduce anything be *contemplating*
a paradox.  If you start off with a paradox in your inital data (stuff taken
as
true for this run) then you will of course run amok, as you would had you
started
simply with a falsehood. But I had rules aout the law of the excluded middle
in that I want a system which can't be crashed by asking it to consider
a hypothetical paradox.  ("Consider "this is false" - it must either be true
or
false, right?")

> I should have gone on and said:
>
> There are logics (including most of the first group above) that don't have
> the Law of the Excluded Middle but nonetheless would be able to deduce
> anything from an explicit contradiction.

I don't see a problem with being able to deduce anything from
an explicit contradiction in what one belives as true.

>  There are other logics (including
> most of the second group above) where even explicit contradictions don't
> enable the inference of all propositions.
>
> You can't claim that abandoning the Law of the Excluded Middle solves a
> particular problem without saying what you are going to replace it by.

What we seem to be using, as Dan mentioned, is a form of not in which
certain
properties have converses, and some (most normal ones) don't.   Basically,
you have to show how to something does before anyone can assume so.

Examples:
  string:lessThan   log:converse  string notLessThan .

     This is straightforward: in a formula with all arithmetic operators i
can
     do "not" manipulation happily.

  log:includes log:converse log:notIncludes.

     Here log:incldues is the query operator as to whether one set of
statments
     contains another set.   becasue that is also a calculation, a logical
operator,
     it has a converse, so we can check that a document doesn't say
something
     by  just looking.  This allows us to make defaults, and o define
documents
    as being definitive in the sense that for any x,y  if the doc doesn't
say   x p y
     then x [is converse of p] y.

So you can use LEM with formulae whose predicates all have converses.
I haven't done much with this in terms of manipulating nots in
inference.

In general, rtf$type does not have a converse.  But rdf$type is not so much
to be thought of as a binary operator as a way of writing a unary operator.
So taking the same idea (he noodles) to unary operators, classes, one would
assume that some classes have complements but you can't assume they
do unless you have been told.

Would that work, do you think?



Tim BL

> Peter F. Patel-Schneider
> Bell Labs Research
>

Received on Monday, 14 January 2002 15:49:31 UTC