SUO: Composing Ontologies using morphisms and colimits
John F. Sowa
sowa at bestweb.net
Wed Jan 17 10:20:56 CST 2001
Mike,
The comments by Mike Healy raise some important points that
we should take into account when developing ontologies. But
I don't believe that they create any immediate problems for
the KIF standard. Following is my summary of the issues:
1. Category theory (CT) is a general, powerful, and fundamental
approach, which can be used as an alternative to set theory
(ST) as a foundation for mathematics in general and the
model theories for logic(s) in particular.
2. For Ontolingua, there have been some issues concerning
classes and subclasses that can be put on a sounder
foundation with CT than with ST.
3. However, KIF is a simpler system than Ontolingua (which
just happens to use KIF as its notation for logic). The
kernel of KIF assumes only classical first-order logic
with equality. For that kernel, an ST-based model theory
and a CT-based model theory provide logically equivalent
foundations -- i.e., the truth value of any statement in
KIF would be identical if determined by a CT model or an
ST model.
4. Healy mentions the von Neumann, Goedel, Bernays (VNGB)
version of set theory as one that is more compatible
with a CT foundation than the more commonly used
Zermelo-Fraenkel version (ZF). As a matter of fact,
VNGB was the recommended version of set theory that
was included in the original KIF 3.0 specification.
For the draft ANSI standard, however, all versions of
set theory were removed from KIF and relegated to the
ontologies that might be defined on top of KIF (such
as, for example, Ontolingua).
Bottom line: Nothing in the KIF kernel, as it is currently
being developed, is incompatible with either a CT or an ST
foundation. But when extensions to the kernel are being
contemplated or developed, we should confer with the CT
experts about how such extensions might be defined in a way
that does not create incompatibilities with a CT approach.
John
______________________________________________________________
>John,
>
>Here are some comments from Mike Healy, a colleague at Boeing who worked with
>me on converting the Engineering math ontology into Specware. The punch line
>is that:
>
>
>CATEGORICAL MODEL THEORY IS DISTINCTLY DIFFERENT FROM SET-THEORETIC MODEL
>THEORY, AND THAT IS WHY I [Mike Healy] SAY THAT THE DISTINCTION MUST BE
>CAREFULLY MADE WITHIN LOGIC AS WELL AS WITHIN MATHEMATICS IN GENERAL.
>
>MODELING PREDICATE LOGIC IN SETS CAN LEAD TO INCONSISTENCIES IN THE METATHEORY,
>WHEREAS MODELING THEM AS MORPHISMS IN AN APPROPRIATE CATEGORY DOES NOT.
>
>THE PROBLEMS WE WERE HAVING WITH ONTOLINGUA SEEMED TO ME TO BE PRETTY
>FUNDAMENTAL. THE NOTION OF CLASSES AND SUB-CLASSES DID NOT SEEM TO WORK WELL
>AS A MEANS OF REPRESENTING HIERARCHIES OF THEORIES [Read Ontologies] OR THEIR
>MODELS.
>========
>
>These were the points I was concerned about, but unable to articulate clealy.
>
>What follows is a shortened version of Mike's remarks, followed by the full
>text, which includes a nice pico-tutorial explaining some of the basic ideas
>of of category theory, for the uninitiated.
>
>I have put into CAPITAL LETTERS those remarks that are most pertinent to this
>discussion.
>
>> You are correct in stating that THE UNDERLYING SEMANTICS OF CATEGORY THEORY
>> (CT) IS NOT SET THEORY (CS), and John is correct in stating that THEY ARE
>> COMPATIBLE. That said, WE HAVE TO MAKE A CAREFUL DISTINCTION ABOUT WHAT
>> KIND OF SEMANTICS WE ARE TALKING ABOUT---what metamathematical viewpoint
>> we are taking with each of the two. Also, I agree that FIRST-ORDER LOGIC
>> IS NEUTRAL WITH RESPECT TO CT AND ST as it is commonly understood, but
>> logic in general is not---so we also have to distinguish metalogical
>> viewpoints.
>>
>> In the first few pages of Mac Lane's "Categories for the Working Mathemtician",
>> the co-discoverer of CT makes the point that CT DOES NOT DEPEND ON ST---it
is
>> an INDEPENDENT AND ALTERNATIVE FOUNDATIONAL MATHEMATICAL THEORY. In contrast
>> to ST, which is based upon the notion of membership in a collection, CT is
>> based upon the notion of arrows, or morphisms....
>>
>> ... On the subject of logic, there are are many categorical logics. These
and
>> their models are studied in topos theory and categorical type theory and
>> model theory. CATEGORICAL MODEL THEORY IS DISTINCTLY DIFFERENT FROM
>> SET-THEORETIC MODEL THEORY, AND THAT IS WHY I SAY THAT THE DISTINCTION
>> MUST BE CAREFULLY MADE WITHIN LOGIC AS WELL AS WITHIN MATHEMATICS IN GENERAL.
>> Roy Crole's book "Categories for Types" has a very readable account of this
>> distinction in the third chapter. HE GIVES AN EXAMPLE TO SHOW THAT MODELING
>> PREDICATE LOGIC IN SETS CAN LEAD TO INCONSISTENCIES IN THE METATHEORY, WHEREAS
>> MODELING THEM AS MORPHISMS IN AN APPROPRIATE CATEGORY DOES NOT.
>>
>> Many CT people have the idea that the most natural kind of logic associated
>> with CT is intuitionistic in nature ... I do know that
>> in categorical logic, classical, intuitionistic and other kinds of logic
>> are special cases. These can be represented in ST, but some of them can
>> only be represented in ST by implementing CT within it (geometric logic,
>> for example).
>>
>> THE PROBLEMS WE WERE HAVING WITH ONTOLINGUA SEEMED TO ME TO BE PRETTY
>> FUNDAMENTAL. THE NOTION OF CLASSES AND SUB-CLASSES DID NOT SEEM TO WORK
WELL
>> AS A MEANS OF REPRESENTING HIERARCHIES OF THEORIES [Read Ontologies] OR THEIR
>> MODELS. I'VE BEEN WORKING SOME MORE WITH THE CATEGORICAL APPROACH IN SPECWARE.
>> I've made a couple breakthroughs that seem to greatly simplify what we were
>> doing, and I just wish we had time to carry this to completion (actually
use
>> the categorical Engmath ontology in deriving engineering software).
>>
>> ... So, most people just assume that "the
>> category Set" of classical ZF sets and functions is already available and
>> go from there. Realize, though, that there can be different categories of
>> sets depending upon the assumptions about set membership one makes!
>>
>> IT'S ALSO POSSIBLE TO IMPLEMENT CT IN ST by using sets to represent the
>> collections of objects and morphisms in a category, the set of morphisms
>> for a category being closed under composition. Here, ZF ST won't do, though,
>> because we need sets that are not "sets"---in fact, we need the hierarchy
>> of sets, classes, conglomerates, ... of VNBG (I may have the letters permuted
>> from the usual usage) ST. This is because ...
>>
>> From mjhealy at redwood.rt.cs.boeing.com Tue Jan 16 13:58:58 2001
>> To: mfu at redwood.rt.cs.boeing.com
>> Subject: Re: SUO: Composing Ontologies using morphisms and colimits
>> Cc: mjhealy at redwood.rt.cs.boeing.com
>>
>> Mike,
>>
>> Thanks for cc-ing me on the message. I will respond to you directly and
then
>> you can send my response on to the others if you wish. I would have to
>> defer to an actual category theorist for an authoritative answer, and I'll
>> ask a few and let you know the result. Meanwhile, I'll give you my answer
>> as a mathematician who is applying CT but is not qualified to do research
>> in the subject.
>>
>> You are correct in stating that the underlying semantics of category theory
>> (CT) is not set theory (CS), and John is correct in stating that they are
>> compatible. That said, we have to make a careful distinction about what
>> kind of semantics we are talking about---what metamathematical viewpoint
>> we are taking with each of the two. Also, I agree that first-order logic
>> is neutral with respect to CT and ST as it is commonly understood, but
>> logic in general is not---so we also have to distinguish metalogical
>> viewpoints.
>>
>> In the first few pages of Mac Lane's "Categories for the Working Mathemtician",
>> the co-discoverer of CT makes the point that CT does not depend on ST---it
is
>> an independent and alternative foundational mathematical theory. In contrast
>> to ST, which is based upon the notion of membership in a collection, CT is
>> based upon the notion of arrows, or morphisms. In contrast to set membership,
>> which is not transitive, two arrows are composable when they match head-to-
>> tail, their composition being a third arrow. Composition being associative,
>> and there being identity arrows, the notion of objects arises naturally as
>> representatives of "the places where arrows meet", each object being associated
>> with an identity arrow. From this viewpoint, a category is a system of arrows
>> and their associated objects that is closed under composition. So, categories
>> can be as abstract as you like and other things can be built up from them.
>> This yields mathemtical objects defined from purely structural relationships.
>> On the other hand, one obtains concrete categories by assigning certain
>> mathematical objects to the objects in a category and relationships between
>> them to the arrows, as long as the concrete items do in fact obey the rules
>> for a category. The category of sets and functions can be obtained in this
>> way. This may sound like cheating, grabbing mathemtical objects out of thin
>> air, but F. William Lawvere showed long ago that categories of sets can be
>> derived from abstract categories. So, most people just assume that "the
>> category Set" of classical ZF sets and functions is already available and
>> go from there. Realize, though, that there can be different categories of
>> sets depending upon the assumptions about set membership one makes!
>>
>> It's also possible to implement CT in ST by using sets to represent the
>> collections of objects and morphisms in a category, the set of morphisms
>> for a category being closed under composition. Here, ZF ST won't do, though,
>> because we need sets that are not "sets"---in fact, we need the hierarchy
>> of sets, classes, conglomerates, ... of VNBG (I may have the letters permuted
>> from the usual usage) ST. This is because there are categories of categories
>> with functors---mappings that preserve compositon---as arrows, categories
>> of categories whose class of morphisms (functors) is not a "set", etc. Also,
>> there are categories of functors with natural transformations as arrows,
etc.
>> In fact, most categories are derived in this way. In fact, categories of
>> theories in logic can be derived in this way, whether with CT implemented
>> in set theory or not. Joseph Goguen did groundbreaking work on this approach
>> to logic.
>>
>> On the subject of logic, there are are many categorical logics. These and
>> their models are studied in topos theory and categorical type theory and
>> model theory. Categorical model theory is distinctly different from
>> set-theoretic model theory, and that is why I say that the distinction
>> must be carefully made within logic as well as within mathematics in general.
>> Roy Crole's book "Categories for Types" has a very readable account of this
>> distinction in the third chapter. He gives an example to show that modeling
>> predicate logic in sets can lead to inconsistencies in the metatheory, whereas
>> modeling them as morphisms in an appropriate category does not.
>>
>> Many CT people have the idea that the most natural kind of logic associated
>> with CT is intuitionistic in nature (including intuitionistic logics) as
>> distinguished from classical logic. This idea arises from topos theory.
>> A Boolean topos (I'm out of my element here so ask a CT person) would be
>> aspecial case that corresponds to classical logic (I think). I do know that
>> in categorical logic, classical, intuitionistic and other kinds of logic
>> are special cases. These can be represented in ST, but some of them can
>> only be represented in ST by implementing CT within it (geometric logic,
>> for example).
>>
>> The problems we were having with Ontolingua seemed to me to be pretty
>> fundamental. The notion of classes and sub-classes did not seem to work
>> well as a means of representing hierarchies of theories or their models.
>> I've been working some more with the categorical approach in Specware.
>> I've made a couple breakthroughs that seem to greatly simplify what we
>> were doing, and I just wish we had time to carry this to completion
>> (actually use the categorical Engmath ontology in deriving engineering
>> software).
>>
>> This is a rather lengthy reply. I hope you find it worth your while.
>>
>> Mike
>>
>> F. William Lawvere (SUNY at
>> Buffalo) made the fundamental discoveries
>> fundamental discoveries
>> --
>>
>> ===========================================================================
>> e
>> Michael J. Healy A
>> FA ----------> GA
>> (425)865-3123 | |
>> FAX(425)865-2964 | |
>> Ff | | Gf
>> c/o The Boeing Company | |
>> PO Box 3707 MS 7L-66 \|/ \|/
>> Seattle, WA 98124-2207 ' '
>> USA FB ----------> GB
>> -or for priority mail- e "I'm a natural man."
>> 2760 160th Ave SE MS 7L-66 B
>> Bellevue, WA 98008
>> USA
>>
>> michael.j.healy at boeing.com -or- mjhealy at u.washington.edu
>>
More information about the Kif
mailing list