| Last
updated June 10th. |
|||
| New as of Jun 25th. Follows the adjunctive axiomatization! | |||
| Partial
axiomatization - contains exponents as of July 2nd. |
|||
|
|
Diagram 1: The IFF Metastack
| Ur |
⊃ | Col |
⊃ | Cls |
⊃ | Set |
|
| category theory → | |||||||
| finite limits → | |||||||
| exponents + finite colimits → | |||||||
| general limits/colimits | |||||||
The IFF Category Theory (meta) Ontology (IFF-CAT) was the first ontology axiomatized. This was the beginning of the first phase of the IFF. A non-starter for the remaining part of the first phase was a topos axiomatization that followed some suggestions of Colin McLarty. This received objections from the SUO working group, in part due to its lack of support by motivating examples.
The terminology appearing in any standardization meta-ontology will exert authority. This will be especially true for the SUO and the IFF standardizations. Because of this, in selecting which terminology to specify in the IFF, we utilize the notion of conceptual warrant, an adaptation of the librarianship notion of literary warrant, where warrant means evidence for or token of authorization. All IFF terminology should require conceptual warrant for their existence: any term that appears and is axiomatized in the IFF metalanguage should reference a concept needed in lower metalevel or object level axiomatizations. Following the idea of conceptual warrant, the second phase of the IFF was designed bottom-up, and follows conceptual warrant as its guideline. The current (early 2004) version of the IFF represents the second phase. As seen in the current IFF Top Core (aka Basic KIF) (meta) Ontology (IFF-TCO), the most important metalogic terminology incorporated in the second phase references the various concepts related to finite limits. For example, the desire to axiomatize composition of class functions requires the pullback concept.
Now the IFF is at the beginning of a new reorganization effort. This will be the third phase of IFF development. One important metalogic concept to be incorporated in the third phase is exponents. Also, a central task in this third phase is the reorganization of the IFF metastack (core hierarchy). This reorganization, which uses an "adjunctive axiomatization", will follow the conceptual lines expressed in the book Sets for Mathematics by Lawvere & Rosebrugh. The adjunctive aximatization in the new IFF metastack, which is based upon the adjunctive nature of the central concepts of finite limits/colimits and exponents, (1) will provide the metastack with better structure, and (2) will simplify the IFF-KIF metalanguage core by not requiring the definite descriptive operator.
Looking further in the future, it is anticipated that fibrations and indexed categories will be central to the fourth phase of the IFF construction.
The IEEE P1600.1 Standard Upper Ontology (SUO) project aims to specify an upper ontology
| An ontology is a formal, explicit specification of a shared conceptualization. It is an abstract model of some phenomena in the world, explicitly represented as concepts, relationships and constraints, that is machine-readable and incorporates the consensual knowledge of some community. |
that will provide a structure and a
set of general concepts upon which
object-level domain ontologies can be constructed. These object-level
domain ontologies will utilize the SUO for
applications such as data interoperability, information search and
retrieval, automated inferencing, and natural language processing. The
Information Flow Framework (IFF) is being developed to represent
the structural aspect of the SUO. The categorical approach of the IFF
provides a principled framework for
the modular design of object-level ontologies via a structural
metatheory. The IFF takes a building blocks approach towards the
development of
object-level ontological structure, using insights and ideas from the
theory of information flow Barwise
and Seligman, 1997 and the theory of formal concept analysis Ganter
and Wille, 1999. The IFF provides an important practical
application for category theory. It is an experiment in foundations,
which follows a bottom-up approach to the logical description. The IFF
represents metalogic, and as such operates at the structural
level of ontologies. In the IFF, there is a precise boundary between
the metalevel and the
object level. The modular architecture of the IFF consists of
metalevels, namespaces
and meta-ontologies. There are four metalevels, Ur,
Top,
Upper
and Lower,
with the last three corresponding to the set-theoretic distinctions
between generic, large and small collections, respectively.Each
metalevel services the levels below by providing a metalanguage
used to declare and axiomatize those levels. Corresponding to the four
metalevels are the four metalanguages: IFF-Ur,
IFF-Top,
IFF-Upper
and IFF-Lower,
with each metalanguage including those above it. Within each metalevel,
the terminology is partitioned into namespaces, and various namespaces
are collected together into meaningful
composites called meta-ontologies. Currently, the IFF contains
meta-ontologies representing category
theory, information flow, formal concept analysis, first order logic,
the semantic integration of ontologies,
institutions, multitudes, simple common logic, etc. All the various
meta-ontologies in the IFF are anchored to the IFF core
hierarchy (aka, the IFF metastack)
Ur
⊃ Col ⊃ Cls ⊃ Set.
axiomatized in the ur (IFF-UR), top core (IFF-TCO), upper core (IFF-UCO) and lower core (IFF-LCO) meta-ontologies, respectively, where all inclusions preserve composition and identities (are functorial), the last two preserve finite limits, and the last preserves the Cartesian closed structure. These preservation properties require use of the three fundamental relations of subcollection, (function) restriction and (relation) abridgment. The IFF structure is driven largely by the IFF categorical design principle (a goal), which states that the axiomatization of any non-core lower metalevel namespace should be categorical (only use category-theoretic operators; but not use quantifiers and logical connectives).
Diagram 2: The IFF Metalanguages
| Ur |
Top |
Upper | Lower
|
|
IFF-Ur |
|||||
|
|
IFF-Top | |||||||||
|
|
IFF-Upper | |||||||||
|
|
IFF-Lower |
|||||||||
The IFF metalevel hierarchy has grown bottom-up. From the start, one major design criteria was that terminology be introduced and axiomatized on a basis of need by lower level ontologies. The current hierarchy has one object-level and four metalevels (Lower, Upper, Top and Ur). Ordinary (large) categories are specified in the Lower metalevel and discussed in the Upper metalevel, where classes and class functions are axiomatized. A major design decision is where to allow axiomatization for notions related to the exponent YX = hom[X, Y] and power 2X = ℘X constructions. In practice (and particularly, in order to abide by the categorical design principle), it was decided early on that these were needed in the Upper metalevel. However, in order to avoid Russell’s paradox, these need at least one higher metalevel above their level of axiomatization. Hence, the need for the top metalevel was clear; and this, of course, should not have such constructions. Finally, the Ur metalevel abstracts the category-theoretic orientation of the Top metalevel.
Each metalevel has an associated metalanguage, which is defined by the various meta-ontologies at that metalevel and is used by the meta-ontologies and ontologies at all lower levels. We have associated a primary color with each metalevel: black with the Ur metalevel, red with the Top metalevel, blue with the Upper metalevel, and green with the Lower metalevel. Each metalanguage includes the ones above it in the hierarchy, and each metalanguage inherits those colors. For example, the specification of the IFF-Top metalanguage will involve only two primary bolded colors, black and red, since it includes (and axiomatizes) Top level terminology (red) and uses Ur level terminology (black); plus logical gray. Hence, we envision a hierarchy of IFF metalanguages (Figure 11), where each lower level metalanguage includes the ones above it. In order to define the metalanguage for a particular metalevel n, the IFF-KIF language is used in two ways.
First, the typing (of the terminology in the various meta-ontologies) for the metalanguage at any level uses the metalanguages at higher metalevels, where the IFF-KIF expression is restricted to membership in sets, application for functions, and holds for unary and binary relations.
Second, the meaning (of the terminology in the various meta-ontologies) for the metalanguage at any level uses the metalanguages at the higher levels plus unrestricted IFF-KIF (quantifiers, connectives, etc.).
Table 1 charts the major analogous concepts throughout the IFF hierarchy - each row presents a group of analogous concepts with the leftmost being the most generic and the rightmost the most specific. This illustrates the claim that Ur-Top-Upper-Lower chain corresponds to the chain of categorical concepts: category, finitely complete category, Cartesian closed category, and topos. Table 2 gives the complete set of Top terms that are axiomatically linked to their Ur superiors, where the bolded and colored ones are in Table 1.
Table 1: Major Analogous
Concepts
|
IFF-Ur |
IFF-Top |
IFF-Upper |
IFF-Lower |
| object subobject morphism source/target composition/identity relation object0/object1 extent |
collection subcollection function source/target composition/identity relation collection0/collection1 extent |
class subclass function source/target composition/identity relation class0/class1 extent |
set subset function source/target composition/identity relation set0/set1 extent |
| restriction abridgment unit/unique collection-pair binary-product opspan pullback |
restriction abridgment unit/unique class-pair binary-product opspan pullback |
restriction abridgment unit/unique set-pair binary-product opspan pullback |
|
| exponent application curry power constant element |
exponent application curry power constant element |
||
Table 2: All Ur-Top Analogs
| thing |
thing |
| object
subobject subordinate lesser greater inclusion reflex disjoint isomorphic |
collection
subcollection subordinate lesser greater inclusion reflex disjoint isomorphic |
| relation
object0 object1 extent projection0 projection1 abridgment |
relation
collection0 collection1 extent projection0 projection1 abridgment |
| morphism
source target mor2rel monomorphism epimorphism isomorphism morphism-morphism morphism0 morphism1 composition identity restriction |
function
source target ftn2rel injection surjection bijection function-function function0 function1 composition identity restriction |
For more on this see the CT04 presentation (pdf, doc) or the preprint "The Information Flow Framework: A Descriptive Category Metatheory" (dvi).
| Note: The IFF documents contain many unicode characters and require a recent browser. But even some recent browsers fail to render these documents properly (notably, Internet Explorer). You can test your browser here. |