# Re: A Model Theoretic Semantics for DAML-ONT

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>

```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

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:45:35 UTC