- From: Pat Hayes <phayes@ai.uwf.edu>
- Date: Mon, 14 Jan 2002 16:11:52 -0600
- To: "Tim Berners-Lee" <timbl@w3.org>
- Cc: <sandro@w3.org>, "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, <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. How does it prevent such an implicit introduction? One moral of the 30-odd years of discussion after Goedel's proof was published is that the ways one can *implicitly* introduce contradictions are much more subtle than almost anyone can imagine, and 'anyone' here includes the likes of Alonzo Church, WVO Quine and Richard Montague, all of whom got their fingers burned at one time or another. Sorry, I won't be convinced by inability to think of a way of encoding an implicit contradiction: I want to see a proof that it is impossible. (Such proofs can be done, eg there is one for KIF.) Allowing reification into the formalism is like dancing on the edge of a cliff, BTW. >----- 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. Careful to distinguish a paradox from a contradiction. A contradiction is provably false, and so when asserted can be used to infer anything. A paradox is worse: it is provably both true and false (or, if you prefer, if true, then false, and if false, then true.). A paradox doesn't need to be asserted to cause trouble: it causes it all by itself. Just by existing it makes truth indistinguishable from falsity, and there is in general no way to prevent it from making inferences happen. As Peter says, a formalism with a paradox (in its semantics) is fundamentally broken. > > 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. What do you mean, it doesnt 'work'? It is valid (true in all interpretations) in most logics. What logic are you using, that makes it invalid? (If you move to multi-valued logics, one can easily restate all the standard paradoxes in multi-valued form: instead of 'p or not p' you simply use 'p or not p or (undefined p)' ; if you want to move to intuitionistic logic, the paradoxes are harder to construct but one still gets them; the proofs are a lot longer, is all. That is what Turing showed, basically: the paradoxes recur in a computational context as non-termination results. If you want to use relevance logics, then I'm not sure what the status of the paradoxes is; but there are other reasons to not use relevance logics.) >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. Nonsense. Sorry, but it is nonsense. One can define sets in intuitionistic logic, for example. What I suspect you want to say is that this cannot be allowed (as a general rule) as you don't want all formulae to define sets. Fair enough. This rule - that every formula with one free variable defines a set of things that it is true of - (usually called comprehension) isn't valid in most first-order logics, however, so there's no need to worry about your reasoner being forced to use it. >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. So what? Comprehension only refers to the truths. The non-truths can do what they like, and be anything they want to be, and that is irrelevant to the set. This has nothing to do with PEM. >We admit to the >existence of >paradoxes and tautologies. Good for you, but what has that got to do with what we are discussing? (And do you really mean paradoxes, or only contradictions?) > >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. Yes it is. Just as a matter of English grammar, it is a noun clause. The paradox arises from taking this observation more seriously than one ought to, perhaps. But Russell wasn't just doing a parlor trick; he showed that there are indeed some sets that are not members of themselves (and some that are). Using Frege's reasoning, there ought to be a set of all of them. Its not just a trick; if you think there shouldn't be such a set, you need to give some rationale for what distinguishes the collections that are sets from the collections which aren't. (The current best guess in FOM is sheer size: very, very 'large' collections may not be sets.) > 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) DAML 'classes' are sets in this sense. > { :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. Don't worry, you can't in FOL either. That's a familiar point. The Russell paradox doesn't depend on this at root, though, since you can get the effect of a definition by asserting an IFF. > 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". Right. But that isn't the point. Look, logic doesn't assume set theory; set theories are axiomatized in logics. (And very few axiomatic set theories can be stated in FOL (or, therefore, in N3 or DAML) since they - the set theories - use non-FO constructions like the 'all formulae with one free variable' used in the comprehension principle. Zermelo-Fraenkel ST isn't FO expressible, for example.) So of course the set-theoretic contradictions only show up when one formalizes the set theory in axioms, just as you point out. Russell's paradox isn't a *logical* paradox, its a paradox in naive set theory. The point at issue is what happens when one *language* construction - not an axiom supplied by a user, but a construction with a meaning fixed by the model theory, part of the language spec. - in language B (eg DAML) is mapped into another construction in language A (eg RDF) in such a way that there is a contradiction between the language specifications. If we insist that both specifications are correct, then just by doing that we have *created* a paradox. The language specs are not just user axioms: they are supposed to be the rules under which *all* axioms are interpreted. > :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 :-/ ) Just an aside, but this isn't really correct, since what causes the trouble here is the self-reference implicit in the use of 'precedes' and the (meta-)observation that the act of preceding produces that very sentence itself, not the 'such that' part. And the real point is that can be true, but not provable in the system; and then this only shows that the system is incomplete, not that it is paradoxical or contradictory. (This is in fact a kind of pop version of Goedel's own proof.) General moral: words like 'true' don't have a single, global, meaning. They are only precise when understood relative to a particular language or notation. Change that, and the notion of truth changes. >]]] > >> 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. Wrong, see above. Or, if you prefer, the GI was done by the writers of the W3C specs, not by the users. With paradoxes in the semantics, the formalism is built on garbage. It would be better called AIGO - anything in, garbage 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. Well, KIF has almost full abilities to describe its own formulae, is stronger than FOL and is provably consistent, and has been around for about a decade. You might take a look at it, just for a start :-) 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 Monday, 14 January 2002 17:10:56 UTC