- From: Tim Berners-Lee <timbl@w3.org>
- Date: Fri, 11 Jan 2002 20:04:27 -0500
- To: <sandro@w3.org>, "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
- Cc: <phayes@ai.uwf.edu>, <hendler@cs.umd.edu>, <las@olin.edu>, <connolly@w3.org>, <w3c-semweb-ad@w3.org>, <www-archive@w3.org>

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