From: pat hayes <phayes@ai.uwf.edu>

Date: Thu, 16 Nov 2000 17:18:49 +0000

Message-Id: <v0421010ab639b2f4df0c@[193.60.10.118]>

To: Dan Connolly <connolly@w3.org>

Cc: www-rdf-logic@w3.org

Date: Thu, 16 Nov 2000 17:18:49 +0000

Message-Id: <v0421010ab639b2f4df0c@[193.60.10.118]>

To: Dan Connolly <connolly@w3.org>

Cc: www-rdf-logic@w3.org

Dan Connolly wrote: >* How do we avoid Russel's paradox. > >It seems easy enough to run into; just define A >ala: > (<=> (A ?x) (not (holds ?x ?x)) > >then, assuming (holds P X) can be used >interchangeably with (P X), we have: > >(A A) => (not (holds A A)) => (not (A A)) ! >(not (A A)) => (not (holds A A)) => (A A) ! > >Is there some restriction which avoids >the above definition of A? No, there is no such restriction in KIF, I believe as a matter of policy. That is, the KIF attitude is that if you make a paradoxical definition then you must be prepared to reap the resulting whirlwind, as it were. (Caveat Orator, maybe?) The KIF semantics for 'holds' means that anything of the form (holds ?x ?x) must be false for any ?x (since no set of items can contain itself), so the definition as given makes A the universally false predicate. The paradox arises if you assume that if something satisfies a definition then the definition is true of it; because A satisfies the form of its own definition, and so then (A A) must be both false (because A is false of everything) and also true (since A satisfies the defining conditions for A to hold of it.) The real KIF sin here is the act of making a universally false definition. As Richard Fikes pointed out, one can always assert a contradiction in any logical language. If you were to just assert the biconditional (<=> (A ?x)(not (holds ?x ?x)) then you are asserting a contradiction (since if the second conjunct is true the first one must be false). So you have just asserted a contradiction, and the language can hardly be expected to prevent you doing that. The paradoxical nature of this definition therefore depends on its being a *definition* rather than just an assertion of a biconditional. One might object that it shouldnt be possible to create a paradox just by making a definition, since a definition isnt supposed to have a truthvalue. However, someone can create a paradox without using 'holds', since it is legal to use a name in its own definition (to allow recursive definitions), which means that one could simply define (B ?x) to mean (not (B ?x)), creating a paradoxical B more simply. (If you feel that such a definition shouldnt be allowed since it doesnt terminate, see three paragraphs later.) It seems hard to legislate things like this out of existence: its like insisting that everyone writes good code.. Note, this situation is not as bad as it might seem, since there is no way that such a definition of A or B could be generated *automatically*: nothing in KIF requires that all possible definitions must define something. (If KIF were higher-order - which, to emphasise, it isn't - then something like A or B might get generated during the course of performing an inference, and the language would be genuinely incoherent, unless the process of generating names were restricted somehow. ) If one wants to make KIF foolproof by making it impossible to create a paradoxical definition, there are several ways to do it, but they all have a cost. One would be to add a strong typing to the language and insist that all definitions and expressions were consistently typed, so that (holds ?x ?x) would simply be syntactically illegal. This would change the character of KIF quite a lot and make all the axioms much more complicated (compare C++ to ALGOL-60) but wouldnt really change its utility. Another way to go would be to impose some restrictions on the form of legal 'holds' expressions, eg to forbid self-application (actually one would need to restrict any 'loops' of application eg ruling out (and (holds ?x ?y) (holds ?y ?x)) ; this is basically what a strong typing convention does, in fact) or to impose some restrictions on scoping variables in definitions through negations. The trouble with most of these kinds of 'guaranteed safe' restrictions is that they also rule out some perfectly legal constructions which are sometimes useful. (Even self-application is sometimes useful and meaningful, though it shouldn't be by KIF standards.) Another strategy is to alter the semantics slightly to allow expressions to have no value at all. (This might have been what Mike Genesereth intended to be the case for KIF, though it isnt the way the current semantics actually works out.) This is the natural way to interpret programming languages and recursion, where paradoxes tend to be expressions which keep alternating their truthvalue when 'evaluated' (like B above), ie correspond to a certain kind of infinite loop. ('Evaluation' here corresponds to replacing the defined term by its definition, which ought to eventually succeed in eliminating the defined term entirely in finitely many steps.) One way to deal with this, therefore, would be to not allow the inference from the fact that B satisfies the definition of A to A being true of B, which would bring the notion of a 'definition' in KIF more into line with the definition of a procedure or function in a programming language (where just writing a definition doesnt guarantee that anything useful can be done with it: you have to show that the definition 'works'.) This is the 'fixedpoint semantics' which underlies LISP and other recursive languages. The cost here is that there is no way to state in the language itself that any of its expressions have a value, so we can never be sure that what we are saying is really true (though we might be able to be sure it is not false); but this is a familiar kind of limitation from programming languages, so maybe we can get used to it. (You can add such a way by fiat in the semantic specification; but as soon as you do, you can state a paradox. It's impossible to have it both ways.) Yet another strategy (which I myself prefer) is to simply remove the concept of 'definition' from KIF altogether, treat all definitions as simply assertions of biconditionals, and stick strictly to the Caveat Orator principle. But I can see that this might not be acceptable in B2B semantic-web kinds of application. Hope this helps. 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/~phayesReceived on Thursday, 16 November 2000 12:18:35 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:32 UTC
*