re:RE: SUO: RE: First piece of 4D ontology
On Sun, 11 Mar 2001 18:41:50 +0100 West, Matthew MR SSI-GREA-UK <Matthew.R.West@is.shell.com> wrote:
>
>Dear Robert,
### Matthew, reply below--
--Robert Meersman
>
>> ### Ian, Matthew,
>>
>> ### am traveling in US so replies may be a bit slower. I had
>> also noticed the relationship between in Matthew's axioms #3
>> and #4 but in fact, why does the comment of #3 talk about
>> classes while the code is expressed using collection? Is that
>> accidental or intentional.
>
>MW: Just an editiing accident. I'm having troubles picking and using terms
>consistently for the meanings I have.
>
>> Similarly, is "member of" the same
>> as "is a"?
>
>MW: Well I don't like to use "is a" because it can be ambiguous in natural
>language, being commonly used both for subclass-of and member-of.
### The reason I asked is that you used it in the comments of your axioms #1 and #3.
>>
>> ### BTW these 4 axioms don't tell me a whole lot... not to
>> mention the serious agreement one needs about the "exists"
>> predicate and the implicit membership/is_a semantics. I
>> wonder how to use them.
>
>MW: Please elaborate on the "serious agreement" that is needed.
### You and others use KIF to specify axioms, rather than an
"accepted" syntax such as mathematics ("accepted" = "universally"
semantically agreed, at least since Hilbert and consorts --and
pardon the many quotes) in which, incidentally, the 4 axioms could
be written much more concisely. Clearly this is done with a certain
form of future computer processing in mind, i.e. interpretation by
a program for purposes of storage, validation, reasoning, ... by
computers. This requires a formal definition of the syntax used --in
the case at hand this likely involves an (the!) ontology itself we
are trying to define. So, in order to avoid infinite regress, we
have no alternative but to axiomatically define (= agree on) the
basic predicates such as "exists ?x ?y". E.g. if this merely involves
finite sets, one "only" has to agree on the definition of the extension
of ?x and on the lookup of ?y in this extension --but one assumes there
is more at play here, otherwise the whole SUO becomes an exercise
in triviality. I believe thick volumes of logic have been written on
this subject of "exists" alone (cfr. the Intuitionists, ...) so a
proper initial agreement seems required. Of course I don't doubt that
[the interpreter for] KIF++ has/will "prescribe" this; my point is
that it will be required at every step and needs to be performed
explicitly.
### Hope this helps for the time being. Apologies should replies
from me be even slower in the coming days, will be on the road
>
>> Is there more to come?
>
>MW: Well the title does say "First piece", so I hope so, as time permits.
>>
>> --Robert Meersman
>>
>>
>> >
>> >Matthew,
>> >
>> > Please see my comments below.
>> >
>> >-Ian
>> >
>> >> -----Original Message-----
>> >> From: West, Matthew MR SSI-GREA-UK
>> >> [mailto:Matthew.R.West@is.shell.com]
>> >> Sent: Thursday, March 08, 2001 1:22 AM
>> >> To: Standard-Upper-Ontology (E-mail)
>> >> Subject: First piece of 4D ontology
>> >>
>> >>
>> >> Dear Colleagues,
>> >>
>> >> Please find below a first piece of a 4D ontology.
>> >>
>> >> I'd like to thank Pat Hayes for reviewing some early drafts.
>> >>
>> >> Comment text is of two types:
>> >> 1. Translations into English of the KIF below. I assume that
>> >> eventually automatic translation from KIF into e.g. ACE
>> >> will be possible for human interaction.
>> >> 2. Structuring information, e.g. Subject Area, Theory,
>> Statement No.
>> >> These are things that I think we need to support engineering
>> >> an ontology (vs. saying what we mean) which I hope will be
>> >> supported by KIF before long.
>> >>
>> >> Comments are welcomed.
>> >>
>> >> ; Subject Area: Thing
>> >> ;
>> >> ; theory: individual and collection
>> >> ; uses:
>> >> ;
>> >> ; #1:
>> >> ;
>> >> ; For all X, X is a thing.
>> >> ;
>> >> ; i.e. that which everything is a member of.
>> >> ;
>> >> ; Note 1: In First Order Logic there is no need to make any
>> >> declaration,
>> >> ; (forall ?x ...) is sufficient.
>> >> ; Note 2: This means that all collections will be a
>> subclass of thing.
>> >
>> >This axiom also appears in the merged ontology. There it
>> has the following
>> >form: (forall (?X) (instance-of ?X Entity))
>> >
>> >> ;
>> >> ; #2:
>> >> ;
>> >> ; for all X, if there exists a Y and Y is a member of X,
>> then X is a
>> >> ; member of collection.
>> >> ;
>> >> ; i.e. any thing that has a member is a collection.
>> >> ;
>> >> (forall ?x
>> >> (=> (exists ?y
>> >> (?x ?y)
>> >> )
>> >> (collection ?x)
>> >> )
>> >> )
>> >> ; Note: This (?x ?y) is not valid SUO-KIF today, but I
>> understand it
>> >> ; will be in the near future.
>> >
>> >You could express (?x ?y) as (instance-of ?y ?x), which is
>> syntactically
>> >well-formed SUO-KIF. However, it is also not a first-order
>> sentence.
>> >
>> >I'm wondering what you mean by "collection" in your axiom.
>> I thought we
>> >were using this term to denote things like wolf packs,
>> football teams, etc.,
>> >which are set-like, in that they have members, but, unlike
>> sets, they have a
>> >spatio-temporal location. However, if this is what you
>> mean, then you
>> >exclude sets and classes, which have members but are not
>> collections in the
>> >sense just explained.
>> >
>> >> ;
>> >> ; #3:
>> >> ;
>> >> ; For all X, X is an individual, or X is a class.
>> >> ;
>> >> ; i.e. everything is either an individual or a class
>> >> ;
>> >> (forall ?x
>> >> (or (individual ?x)
>> >> (collection ?x)
>> >> )
>> >> )
>> >
>> >Note that axiom #3 is redundant, since it is logically
>> entailed by axiom #4.
>> >
>> >> ;
>> >> ; #4:
>> >> ;
>> >> ; For all X, if X is a member of collection then X is not a
>> >> ; member of individual and vice versa.
>> >> ;
>> >> ; i.e. any thing that is not a collection is an individual, and
>> >> ; vice-versa.
>> >> ;
>> >> (forall ?x
>> >> (<=> (collection ?x)
>> >> (not (individual ?x))
>> >> )
>> >> )
>> >
>> >My earlier comment about "collection" applies here as well,
>> since this axiom
>> >appears to rule out sets and classes.
>> >
>> >> ;
>> >> ; end theory
>> >> ;
>> >> ; end subject area
>> >>
>> >> Regards
>> >> Matthew
>> >> ============================================================
>> >> Matthew West
>> >> Operations & Asset Management - Shell Services International
>> >> Shell Visiting Professor, The Keyworth Institute
>> >>
>> >> H3229, Shell Centre, London, SE1 7NA, UK.
>> >> Tel: +44 207 934 4490 Fax: 7929 Mobile: +44 7796 336538
>> >>
>> >> http://www.shellservices.com/
>> >> http://www.keyworth.leeds.ac.uk/
>> >> http://www.matthew-west.org.uk/
>> >> ============================================================
>> >>
>> >
>> >
>>
>>
>
>Regards
> Matthew
>============================================================
>Matthew West
>Operations & Asset Management - Shell Services International
>Shell Visiting Professor, The Keyworth Institute
>
>H3229, Shell Centre, London, SE1 7NA, UK.
>Tel: +44 207 934 4490 Fax: 7929 Mobile: +44 7796 336538
>
>http://www.shellservices.com/
>http://www.keyworth.leeds.ac.uk/
>http://www.matthew-west.org.uk/
>============================================================
>
>