Re: A Model Theoretic Semantics for DAML-ONT

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/~phayes

Received on Thursday, 16 November 2000 12:18:35 UTC