The IFF Development

The IFF has been under development since 2001, and development will continue into the foreseeable future. There are two major developmental phases: experiment and implementation. The experimental phase of IFF development occurred during the years 2001–2005. This is documented in the web pages starting from the old main page (see, for example, the various ontologies and portals linked on the old site map page). The present and future development is mainly concerned with the final coding and the implementation of the IFF. This is represented by the web pages starting from the new main page. The IFF development is largely driven by the principles of conceptual warrant and categorical design. The main application of the IFF is institutional. For a discussion of the philosophy behind the IFF development, see the paper “The Information Flow Framework: A Descriptive Category Metatheory” (presentation: pdf, doc) (preprint: dvi) presented at the International Category Theory Conference (CT 2004), July 18–24, 2004, University of British Columbia, Vancouver, Canada. For an overview of the new architecture of the IFF, see the paper “The Information Flow Framework: New Architecture” (presentation: pdf) (preprint: pdf) presented at the International Category Theory Conference (CT 2006), White Point, Nova Scotia, June 25 – July 1, 2006.

Experimental Phase [2001–2005]

The slogan here was “the IFF is an experiment in foundations”. This phase has gone through many experiments of development. Several of the most important ones are mentioned here. These are listed approximately in chronological order.

Category Theory (meta) Ontology:

The IFF Category Theory (meta) Ontology IFF-CAT, presented at the SUO Workshop (2001) (see also the overview in the IFF Foundation Ontology), is distinguished by being the first meta-ontology axiomatized in the IFF development. It has axiomatizations for large categories, functors, natural transformations, adjunctions, monads, and limits/colimits. The IFF-CAT indicated necessary ingredients in the core axiomatization now known as the metastack. It is an entry-level axiomatization for the category of large categories.

A Topos Axiomatization and Conceptual Warrant:

A non-starter in the early stages of the experimental phase was a topos axiomatization. This received objections from the SUO working group, in part due to its lack of support by motivating examples. Rejection of the topos axiomatization at this time prompted the idea of conceptual warrant. Starting from this point in development, the IFF would be designed bottom-up, following conceptual warrant as its guideline.

Finite Limits:

The most important metalogic terminology incorporated in the initial experiments used various concepts related to finite limits. For example, the desire to axiomatize composition of large functions in the upper metalevel required the pullback concept at the top (very large) metalevel. As a result, at the top metalevel only specific limits were needed. These included binary and ternary products and powers, and pullbacks. Equalizers were added, because of their close connection to pullbacks. At lower (lower, upper) metalevels general finite limits could be axiomatized.

Adjunctive Style Axiomatization:

This experiment of development involved reorganization of the metastack using the “adjunctive style axiomatization” technique illustrated in Sets for Mathematics by Lawvere and Rosebrugh. The IFF is structured with category theory, and adjunctions are one of the central ideas in category theory. As Mac Lane points out, “adjunctions occur almost everywhere” in mathematics. Hence, adjunctions are very useful in the IFF and need to be axiomatized in its foundations. This foundational axiomatization is the adjunctive style axiomatization. From the top-down perspective, it is first encountered in the finite limit axiomatization.

Categorical Design and Composition:

A major goal in this experiment was to complete the categorical design of the lower (small) metalevel and to initiate categorical design at the upper (large) metalevel. An important derived idea of the categorical design principle is that the (in this case, lower metalevel) axiomatization should be atomic, having only set/relational declarations and equations. In order to accomplish this, we needed to extend composition to all levels of the metastack. We also introduced the important exponent metalogic concept in the upper metalevel core.

Generic Levels and Cantorian Expansion:

The idea behind this (partly gedanken) experiment was possibly suggested by the Cantorian expansion in the metastack. An example that illustrates this idea is the axiomatization of category theory for all sizes of categories (small, large, very large, ...). The idea was that this could be given as a generic and parametric axiomatization, where the parameter is the metalevel. Initially, a new architecture was considered and experimented with. This would have order type (ω+1)+4 and would consist of an infinite number of generic metalevels plus metashell: n < ∞ = ur < meta < type < kind < iff. The namespaces ∞ and meta would have the same content, with ∞ being a complete specialization of meta. The meta namespace would be expressed in first order logic, but the ∞ namespace would be expressed atomically.

New Architecture:

This (partly gedanken) experiment was to optimize the result of the experiment for generic levels. The result of this experiment can be approximately and concisely expressed by mapping the old architecture with order type 4 = 1+3, consisting of the four metalevels lower < upper < top < ur, into the new architecture with order type ω+3, consisting of an infinite number of generic metalevels plus metashell n < meta < type < iff.

old		new
lower	⇒	n
upper	⇒	meta
top,ur	⇒	type
ur	⇒	iff

Grammar:

This experiment‘s goal, which was initially realized in the late experimental phase, was to write an grammar for the IFF language (logical notation). The IFF language, which has a LISP-like format, is a vastly simplified and modified version of the Knowledge Interchange Format (KIF). KIF was created to serve as a syntax for first-order logic. In the IFF language, as in KIF, all logical code is written as parenthesized lists. The IFF language contains both logical code and comments. Both nested namespaces and metalevels are specified by prefixes. The IFF grammar, which specifies the syntax of the IFF language, is written in Extended Backus Naur Form (EBNF). It borrowed much from a Common Logic grammar being written around the same time; however, in comparison it is much simpler. A parser for the IFF grammar is the first step in the implementation of the IFF.

Now in use in the metashell, the supra-natural part of the IFF, is a slightly modified syntax with respect to quantification: instead of a quantification (inherited from KIF) such as

   (forall (?m (man ?m) ?w (woman ?w) (married-to ?m ?w))
       (married-to ?w ?m))

the following simpler quantification is used

   (forall ((man ?m) (woman ?w) (married-to ?m ?w))
       (married-to ?w ?m))

An update for the grammar to support this change has not yet been written. Any code linked off the old main IFF page uses the old syntax, whereas all code linked off the new main IFF page uses the new syntax.

Category-theoretic Foundation and Generalized Composition:

The aim of this experiment was to provide the IFF with a more category-theoretic foundation. Here we use “generalized elements” (morphisms in general, functions in particular), instead of the ordinary elements of set theory. Composition, the most basic idea in category theory, has two associated inverse operations, which can be called division. Division on the right defines the belonging relation. The dividend is the “proof” for the division. Proof uniqueness defines parthood. Belonging restricted to parts is the subobject relation (subset in particular). Belonging of elements in parts is called membership. Composition for generalized elements in called generalized composition. In this experiment, a thorough-going application of the principle of categorical design indicated the strong need for generalized composition and proof (parameterized composition).

Meta Object Facility and Model Driven Architecture (MOF/MDA):

The IFF representation of the Meta Object Facility (MOF) and the Model Driven Architecture (MDA) of the Object Management Group (OMG). The MOF Representation of the IFF: portions of the IFF lower metalevel, the notions of language and theory.

The Lattice of Theories (LOF):

The IFF approach, representation and axiomatization for the “lattice of theories”.

The Theory of Multitudes:

The IFF axiomatization of theory of multitudes as presented in the paper “Sets and Classes as Many”, by John L. Bell. In Journal of Philosophical Logic, Vol. 29, 2000.

Other Experiments:

In addition to the previously described experiments, a look at the old site map and old work in progress pages will reveal many other experiments that took place during the first phase of the IFF development. These are associated with the various meta-ontologies, namespaces and portals of the IFF.

Meta-ontologies:: core, category theory, 2-category theory, institutions, information flow, multitudes, model theory, algebraic theory, simple common logic, first order logic, ontologies, etc.
Namespaces:: sets and functions, hypergraphs and their morphisms, spangraphs and their morphisms, type languages and their morphisms and colimits, classifications and infomorphisms, existential graphs, etc.
Portals:: traditional logic and conceptual graphs.

Implementation Phase [2006 ⋯]

The IFF implementational phase began in 2006. The axiomatization for the IFF-IFF and IFF-TYPE namespaces was accomplished in 2006 and the first quarter of 2007. The second and third quarters of 2007 were taken up by work on a chapter entitled “The Institutional Approach” to ontologies for inclusion in the book TAO – Theory and Applications of Ontologies. This chapter gave a gentle and non-intimidating introduction to the architecture of the theory of institutions using standard English (no mathematical notation). In the fourth quarter of 2007 and the first half of 2008, work will resume on the IFF-META namespace axiomatization, where the following tasks need to be finished:

axiomatize the generalized (parametric) composition;
axiomatize the exponent namespace, defining the Cartesian closed category Set_meta;
axiomatize the IFF-META namespace kernel as the specialization of the IFF-TYPE namespace kernel;
axiomatize other things not possible to code at the type metalevel.

After the IFF-META namespace axiomatization is finished, the IFF implementational phase will continue with axiomatization of the generic level of the natural part of the IFF, and with axiomatization of a much more complete version of the IFF Institution meta-ontology (IFF-INS), where the following tasks need to be finished:

axiomatize the concepts of fibrations and indexed categories;
axiomatiz the Grothendieck construction for the 2-category of indexed categories;
define coalescence, which maps V-diagrams and V-indexed categories to indexed categories;
update the axiomatization for the category of classifications and its equivalents.

The pure aspect of the IFF is largely concerned with category-theoretic matters. The applied aspect of the IFF is largely governed by institution-theoretic matters. Initially, the plan of development was for IFF to use category theory to represent various aspects of knowledge engineering, but more recently this strategy was augmented and reversed, thus applying knowledge engineering to the representation of category theory. The theory of institutions is the main instrument used by the IFF to connect and integrate axiomatizations of various aspects of knowledge engineering. But what exactly is the relationship in the IFF between category theory and the theory of institutions?.

A semanticist models a domain by actively living in it. He only uses formalism to record his findings. He is mainly centered on the domain itself, rather than its formal presentation. From his experience, he conceives of the existence of a certain kind of mathematical object, such as the notion of a group or a topological space. Then by placing himself conceptually within that creation, he states succinctly the properties which that creation as a structure seems to have, and then rigorously develops the consequences of those properties taken as axioms (Lawvere).
A formalist is oriented more towards the representation of a domain as a system. The meaning of the symbols does not figure as important in his mind as the rules for manipulating the symbols in the system. The system is autonomous and somewhat indepedent of the meaning.
The connection between semantics and formalism is through interpretation. The theory of institutions is centered on interpretation and represents it as a parameterized relation of satisfaction. Given any signature (context) Σ, any model (semantics) for that signature M_Σ ∈ mod(Σ) and any sentence (formalism) for that signature φ_Σ ∈ sen(Σ), a satisfaction relationship between the model and the sentence is symbolized as
M_Σ ⊨ φ_Σ.
We express this as “the sentence φ_Σ is true in the given model M_Σ” or “the model M_Σ satisfies the sentence φ_Σ”. But in the theory of institutuions more is required. The theory of institutions can represent the notion of translation from one logic to another in such as way as to preserve truth; that is, satisfaction should express the invariance of truth under change of notation (context). Given any signature morphism (context morphism) σ : Σ₁ → Σ₂, any model (semantics) for the target signature M₂ ∈ mod(Σ₂) and any sentence (formalism) for the source signature φ₂ ∈ sen(Σ₁), satisfaction must satisfy the condition
mod(σ)(M₂) ⊨_Σ₁ φ₁ iff M₂ ⊨_Σ₂ sen(σ)(φ₁),
where mod(σ) : mod(Σ₂) → mod(Σ₁) and sen(σ) : sen(Σ₁) → sen(Σ₂) translate logic models and sentences. Although the formal side of the satisfaction relation is set-theoretically small, the semantical side ranges through the hierarchy (sml = 1, lrg = 2, vlrg = 3, … n, …), with lrg (large) being the common case (for example, the domain of topological spaces and the usual axioms formalizing topologies).

Hence, we think of the theory of institutions as existing at a higher level, with its domain including the triple (semantics, formalism, interpretation) and its formal system encoded in category-theoretic terms. However, it incorporates category theory also, with concepts such as categories and functors in a domain and the axiomatization of category theory (as done in the IFF) as its formal system. So category theory provides a formalism for the theory of institutions, and the theory of institutions provides a semantics for category theory.