- From: Tim Berners-Lee <timbl@w3.org>
- Date: Mon, 14 Jan 2002 15:49:02 -0500
- To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
- 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>
----- 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