|
KIF Expression of the Information Flow Framework |
|
||
|
|
|
||
|
|||
|
|||
|
|||
|
|||
|
|||
|
Algebraic Theory Ontology |
|
||
|
Ontology Ontology |
|
||
|
|
|
||
|
The mission of the Information Flow
Framework (IFF) is to further development the theory of Information Flow and
to apply Information Flow to distributed logic, ontologies, and knowledge
representation. IFF provides mechanisms for a principled foundation for an
ontological framework – a framework for sharing ontologies, manipulating
ontologies as objects, partitioning ontologies, composing ontologies,
discussing ontological structure, noting dependencies between ontologies,
declaring the use of other ontologies, etc. |
||
|
IFF is primarily based upon the theory of Information Flow initiated by Barwise (Barwise and Seligman 1997), which is centered on the notion of a classification. Information Flow itself based upon the theory of the Chu construction of *-autonomous categories (Barr 1996), thus giving it a connection to concurrency and Linear Logic. IFF is secondarily based upon the theory of Formal Concept Analysis initiated by Wille (Ganter & Wille 1999) , which is centered on the notion of a concept lattice. |
||
|
IFF represents metalogic, and as such operates at the metalevel and structural level of ontologies. In IFF there is a precise boundary between the metalevel and the object level. The structure of IFF is illustrated in Figure 1. This consists of a collection of metalevel ontologies, each centered on a category-theory category of IFF. |
||
|
o At the upper metalevel is a Basic (bootstrap) KIF Ontology, whose function is to represent a core aspect of set theory. This Basic KIF Ontology should provide an adequate foundation for representing ontologies in general and for defining the other metalevel IFF ontologies of Figure 1 in particular. One approach for doing this would be to require the Basic KIF Ontology to represent the foundation assumptions (restricted comprehension principle) made by Mac Lane on pages 21–24 in (Mac Lane 1971): existence of a universe (the set of all KIF objects), and formation of doubletons, pairs, Cartesian product, power set, union, etc. All KIF categories use the basic KIF ontology. The basic needs of the Category Theory Ontology are modest – the base must include the following predicates and functions: ‘Class’, which is a synonym for ‘UnaryRelation’; ‘subclass’, which is the subtype relation between classes; ‘BinaryRelation’, which is used only once in a theorem; ‘UnaryFunction’; and ‘BinaryFunction’. These are all prefixed with the ‘KIF’ namespace in what follows. The Core Ontology also needs ‘Set’ and ‘Function’ predicates corresponding to Mac Lane’s small sets and small functions. The Ontologies in the middle and lower levels primarily represent categories, and secondarily represent functors, natural transformation and adjunctions. All these ontologies use the Basic KIF Ontology. |
||
|
○ At the middle metalevel are two generic ontologies – a Category Theory Ontology (partially presented in this paper) that allows us to make claims about bottom-level ontologies such as “the Classification Ontology represents a category” or “the classification functor is left adjoint to the theory functor” (Kent 2000), and a Core Ontology on which is based other set-theoretically defined ontologies, such as the Classification Ontology. The Category Theory Ontology is a KIF formalism for category theory in one of its normal presentations. Other presentations, such as home-set or arrows-only, may also have value. The Category Theory Ontology helps to structure other aspects of metalogic, in particular the lower-level IFF ontologies. |
||
|
○ At the lower (and main) metalevel, ontologies are organized in two dimensions, the instantiation-predication dimension and the entity-relation dimension. These two precise mathematical dimensions loosely correspond to the Heraclitus distinction and the Peirce distinction, respectively. |
||
|
□ In IFF the type-token distinction looms large. In the instantiation-predication dimension are a Classification Ontology that directly represents the type-token distinction, an IF Theory Ontology that is adjoint to the Classification Ontology, and a combining IF Logic Ontology. The Classification Ontology declares and axiomatizes the central ‘Classification’ construction. The IF Theory Ontology, which is based upon a sequent calculus, declares and axiomatizes the standard predicates of ‘subclass’, ‘disjoint’ and ‘partition’. Representing Formal Concept Analysis is a Concept Lattice Ontology. In addition to formal concepts and their lattices, this also includes collective concepts. |
||
|
□ In the entity-relation dimension are a Hypergraph Ontology that represents multivalent relations and a Language Ontology (whose presentation is a little delicate) that represents expressions. |
||
|
□ Also at the lower level are a combining Model Ontology and a derivative Ontology Ontology. The latter two ontologies are related to the fundamental truth meta-classification1 between models and expressions. In addition, the lower-level ontologies have sufficient morphism and colimit structure to build things. |
||
|
|
||
|
1 The truth classification of a first-order language L is the meta-classification, whose instances are L-structures (models), whose types are L-sentences, and whose classification relation is satisfaction. In IFF the concept lattice of the truth meta-classification functions as the appropriate “lattice of ontological theories.” A formal concept in this lattice has an intent that is a closed theory (set of sentences) and an extent that is the collection of all models for that theory. The theory (intent) of the join or supremum of two concepts is the closure of the intersection of the theories (conceptual intents), and the theory (intent) of the meet or infimum of two concepts is the theory of the common models. |
||
|
|
||
|
Many
links on this page point to documents in PDF (Portable Document Format). The
free Adobe® Acrobat® Reader™ necessary for reading these documents can be
obtained from the following link.
|
||
|
|||
|
Please send questions, comments and suggestions about this page to: Robert E. Kent rekent@ontologos.org |
||
|
|||
