Re: SUO: RE: KIF syntax and semantics and a basic ontology
Hi Matthew, thanks for your comments.
> 1. I feel rather like someone who has just been given the answer
> (which we all know is 42) but not the question.
Do you have the same feeling about every other proposed ontology? If
not, why not?
> It would help greatly if you could document the requirements you are
> trying to satisfy. This would mean we could check both that we could
> check whether the requirements match our (individually and
> collectively) requirements, and whether what you propose satisfies
> them.
Not sure what you're asking for, Matthew. The notions of class,
relation, number, and sequence are fundamental to ontology. If they are
to be useful, they have to be axiomatized. Here are some axioms for
review -- use them, criticize them, refine them, etc. Isn't that just
what we do in ontology? What more are you looking for?
> 2. You start by saying that instance-of is not required, and then in
> the set theory bit go on to use it. Is this habit? Or are we to have
> two ways to denote classification?
A lot of folks like to use "instance-of". It's there if you want it,
but it's dispensable.
> 3. You have classes as non-extensional,
No, I just don't declare them to be extensional. That's very different
from saying that the axioms assert them to be non-extensional. If you
want extensionality, add it as an axiom.
> i.e. two classes can have the same membership but not be identical.
Yes, in the sense that one could also posit this as an axiom.
> I'm afraid this does not compute with me. I was also not aware of a
> demand for this (whose requirement is this? what are the benefits?)
Suppose one wants to develop an ontology that embodies a conception of
time on which the future is not determinate, and hence on which there
are past and present objects, but no determinate future objects. (Such
a conception might be useful, say, in a manufacturing system that has
to calculate on the fly the number of kind of objects it is going to
produce during any given run depending on demand.) On such a
conception, the class of humans grows moment by moment with each birth
(or conception, or whatever your criterion is for being human). But if
classes are extensional, they don't "grow"; `human' picks out a
different class with each birth. Now, maybe that's ok with you; maybe
it's the way it should be. But there are, it seems to me, intuitions
that warrant saying that membership in the class of humans can change
over time. Extensionality is omitted simply to for allow such a
conception of class. Add extensionality if you don't like it.
Also, note that I identify classes with unary relations, i.e.,
properties, and properties are not typically taken to be extensional.
Maybe that's not a good idea. An option here would be distinguish
classes and properties, and take classes to be the extensions of
properties. But I wonder if this is an unnecessary multiplication of
entities.
> However, I don't mind as long as I can have classes that are
> extensional - which are presumably a subset of the ones that aren't.
> Could you explain how I can get there?
Add an extensionality axiom for classes.
> If classes are non-extensional then I presume membership can also
> change over time. There needs to be something that explains how you
> get to the membership at some point in time.
I'm not sure I understand the question, but it's irrelevant until you
add a temporality to the axioms somehow, either by introducing temporal
operators and an appropriate extension to the semantics or an explicit
theory of time. If you do, then presumably you'd have to add something
like a temporal parameter to all predicates, including instance-of, so
that talks instead of being an instance-of class C *at some time* t. Is
that what you're talking about?
> If classes are non-extensional then I don't see what point there is in
> having null.
Nothing in the axioms entails that there is a null class. Null gives
us one with a name. If you want, change the axiom to "There is an empty
class" and then when you add extensionality you can prove the existence
of null.
> Since any class that had no members would have to be declared as such,
Why? You mean you have to identify all the null classes in your domain?
> 4. There are a number of relations that appear to be undefined. These
> include: - documentation
The status of `documentation' is sort of funny. I'm following
convention here by using it, but it really functions as a comment
mechanism. But comments proper are not really what you want, because
you don't want it to be ignored by an ontology browser. I admit I am
fuzzy on the status of `documentation'.
> - instance-of
Think of it as "defined" by the axiom that says it is dispensable, i.e.,
(<=> (instance-of ?x ?cls) (?cls ?x)).
> 5. Please can you give a bit more explanation about functional
> relations?
I don't know what more I can say beyond the repeating the documentation
and the axiom for the "functional" predicate.
> 6. I don't understand what unary is really about. Do you mean
> singular, i.e. there is only one member? Do you mean just one placed
> relations (classes?) (though you say for n-tuples where n>2, rather
> than n>=2)?
Yes, that is an unfortunate typo. That should be "n>1" (equivalently,
of course, "n>=2"). Unary relations are classes -- but not all classes
are unary relations the way things are defined, as null classes are not
unary.
> (please don't expect me to decifer the KIF).
Whatever. Though I don't understand why you wouldn't *want* to be able
to read it.
> 7. You documentation for ternary says it is documentation for binary.
Thanks.
> 8. You have used the word sequence in a restrictive sense. There are
> other sorts of sequence than number sequence. I suggest changing
> sequence to number-sequence.
Sequences are *functions* on numbers, but the numbers simply index the
elements of the sequence; they are what provide a notion of order. To
be an element of a sequence s is to be the value of s on some positive
integer n. But *anything* can be an element of a sequence. This is the
standard way of understanding sequences in set theory, and it is quite
elegant, so I nicked it.
> 9. Signature looks much better than nth-domain, though I notice that
> with the earlier changes you have made to KIF you can define even
> Nth-domain,
No, nth-domain was never definable. Rather, a metatheoretic *schema*
was given that defines infinitely many *instances* all at once. But the
schema itself was not KIF. To define it in KIF proper, you need
sequences and integers.
> where it not being definable was my principal objection. Why have
> both?
No reason other than that nth-domain is fairly entrenched, so it was
important to show that it could be expressed. I think the following
should fall out as a theorem that relates the two relations (WARNING!!
KIF AHEAD!! ;-) :
(forall (?rel ?n @args (= (arity ?rel) ?n))
(<=> (signature ?rel @args)
(forall (?m (posint ?m) (=< ?m ?n))
(nth-domain ?rel ?m ([@args] ?m)))))
> 10. I don't understand the last theorem about nth domain.
It is a special case of the general axiom for nth-domain that
corresponds to its usual manifestation as a 3-place relation.
> I haven't read all the stuff on arithmetic. I'll try to read that
> later.
Just a simple integer arithmetic for addition and subtraction. That's
all that's needed for the rest of the ontology.
-chris
--
Christopher Menzel # web: philebus.tamu.edu/~cmenzel
Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
College Station, TX 77843-4237 # vox: (979) 845-8764