Re: Grist for layering discussion

>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