Re: Grist for layering discussion

----- Original Message -----
From: "Pat Hayes" <phayes@ai.uwf.edu>
To: "Tim Berners-Lee" <timbl@w3.org>
Cc: <pfps@research.bell-labs.com>; <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: Tuesday, January 15, 2002 5:06 PM
Subject: 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".
>
> Right, exactly. The 'weak' 3-valued logics do this, but they are then
> so weak that you can hardly do anything with them. They act like
> 2-valued logics but if anything is undefined then all assertions just
> vanish into undefinedness. (They actually model computation quite
> faithfully in a sense, if you interpret 'undefined' as 'no value gets
> returned', ie 'wanders into weeds', in Sandro's phrase.Then if
> anything subexpression wanders into the weeds, you never get a value.
> But what you can't ever do is *conclude* that something is in the
> weeds.)
>
> >  >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.
>
> Yes, but that is what 'truth' means in logic as well. Don't think
> that not knowing whether something is 'really' true implies that one
> has to abandon 2-valued logic. The logic only says, in effect: IF
> these are true, THEN this other stuff Ive deduced from it must be
> true as well.

We are agreed about that.

> >>  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 by *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 problems about 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?")
>
> Good example. Its a bad idea to even allow things like that to be
> said, because the task of telling whether some larger DB implies one
> of them isn't computable, in general, so you can never be sure you
> have filtered them out.

Unfortunately, for the web, we have to insist that it can be said.
Basically, while a databse can be seen as a tree-lie expression,
the web isn't.   A document A can assert that  [the formula one
gets by parsing a representation of] document B is false.
Document B, under separate authorship and control, can
indpendently assert that document A is true.

I maintain, as I can't see any other way, that the language
must have the power to make each of these two important stataments.
And the language must have the power to be able to express the
conjunction of two documents.  So I don't see any way to prohibit,
in the expressive power of the language, a paradox from
being written.  So we are stuck with tackling the problem
on the other side - by limiting the infernce.  Which does look like
Intuitionalistic logic as you say.

> If paradoxes - not contradictions like (p and
> not p), which are always false, but *paradoxes* - which can't
> rationally be either true or false - can be stated in the language,
> then all reasoning from any source is suspect.

In classic logic, but not all logics.

> And (again unlike a
> contradiction) the problem might not show up in any way you can
> detect. You just have incompatible conclusions where each of them
> might have impeccable and checkable derivations, both warranted
> correct, but disagreeing. Not a good thing to have.

Absolutely.  However, there must be a set of formulae which you can
show do not have this problem, where I am including inference rule
as a formula.

And you will probably tell me that to determine whether a given
formula (for example, set of semantic web pages) is in this set of
safe formulae is just unscalable- it takes a very long time for
a set of any size.  And then i would suggest that this is life,
but there may be ways of simplifying the problem.  This is why
we design modular systems.  When I figure out whether I should
get mony out of the ATM, I  don't absorb all the internal formulae
in the ATM.  There is an interface which hides them.
By absorbing only certain sorts of information from certain sources
I can made  a limited and safe system.   It means that for any real system,
the actual complexity of the information actually belived is limited.

(So for example, when I write rules to check whether a document is
schema-valid,
the system only looks at the the document and reads it like a bunch
of data without believeing it, and the same with the schema.
Then in a separate operation it creates a new formula which is
the dedcutive closure of the document and the schema and the axioms
and looks for inconsistencies in that formula.  But it never belives it.
In fact it deliberately trying to make a contradiction within  that sandbox)


> >
> >>  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.
>
> Sure, but a paradox is worse than a contradiction. Contradictions are
> orcs, but a paradox is a balrog.

Beliveing neither is good.  Hearing someone mutter either should not hurt
you.

> >  >  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.
>
> That sounds very like intuitionist logic, or maybe some other
> constructive logic. The key idea for the intuitionists was that to
> prove not-P, it wasn't enough to just demonstrate that assuming P
> produces a contradiction. You had to actually prove the negation
> *directly*. It amounts to a restriction on kinds of proofs that are
> allowed.

Yes... in a previosu message I said how I see therebeing some Properties
with
converses, and some Classes with complements.   When working with those
then you have limited ways of shifting the "not" around.  When working with
others
you don't.  In n3 (ish) one can infer

forSome n2, n3
    p2 log:converse n2.
    p3 log:converse n3.
    {x2  p2 y2}   ->  { x3  p3 y3}
    {x3  n3  y3}
___________________
{x2 n2 y2}

which is much more limiting than being able to infer

forSome n3
    p3 log:converse n3.
    {x2  p2 y2}   ->  { x3  p3 y3}
    {x3  n3  y3}
___________________
forSome n2
    p2 log:converse n2.
    {x2 n2 y2}

Guess I should look up this Intuitionalistic stuff - it hard enough to
pronounce.


Tim

PS:
intuitionist logic
<spelling> Incorrect term for "intuitionistic logic".
http://burks.brighton.ac.uk/burks/foldoc/82/59.htm
whcih makes it even harder...

> Pat
> --
> ---------------------------------------------------------------------
> IHMC (850)434 8903   home
> 40 South Alcaniz St. (850)202 4416   office
> Pensacola,  FL 32501 (850)202 4440   fax
> phayes@ai.uwf.edu
> http://www.coginst.uwf.edu/~phayes
>

Received on Thursday, 17 January 2002 11:02:14 UTC