The IFF Metastack



Last updated June 10th.


New as of Jun 25th. Follows the adjunctive axiomatization!


Partial axiomatization - contains exponents as of July 2nd.

  • IFF-LCO



Diagram 1: The IFF Metastack

Ur
Col
Cls
Set

     category theory


     finite limits




     exponents + finite colimits






    general limits/colimits

IFF Development Phases

  1. 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.

  2. 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.

  3. 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.

  4. Looking further in the future, it is anticipated that fibrations and indexed categories will be central to the fourth phase of the IFF construction.

Introduction

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)

UrColClsSet.

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).

Metalanguages

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[XY] 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.).

Hierarchical Structure

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

CT04 Presentation/Preprint

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.

Valid HTML 4.01!