The IFF Metastack

The core meta-ontology IFF-CORE axiomatization contains many terms, partitioned according to whether the term is a basic term (sets, predicates, functions or relations), a diagram term, a (co)limit term or an exponent term. The IFF-CORE axiomatizates finite limits of specific shapes at the type level and general finite limits at all lower levels. Finite limits are connected with Dedekind’s abstract definition of finiteness (Lawvere and Rosebrugh, 2003). Following the principle of conceptual warrant, terminology has been placed in the IFF-CORE only when it is needed in the lower or more peripheral namespaces. All metalevel ontologies import and use, either directly or indirectly, the core meta-ontology. This includes the all meta-ontologies in the structural component of the IFF axiomatization.

The IFF-CORE axiomatization is in adjunctive form. The generic level of the core plays a central role in the IFF axiomatization — this is the most referenced namespace in the natural part of the IFF. The kernel and finite limits namespace axiomatizations of the core rely heavily upon the subset, (optimal-)restriction and abridgment relations for sets, (unary) functions and (binary) relations, respectively. The finite colimits namespace is a categorical dual to the finite limits namespace. The axiomatization for exponents and curry begins at the meta level of the metashell.

Figure 1: Metastack Structural Framework

The collection of kernel namespaces in the IFF-CORE is called the IFF metastack (Figure 1). This represents a chain of toposes

Set₁ ⊆ Set₂ ⊆ Set₃ ⊆ … ⊆ Set_n ⊆ … ⊆ Set_ur

which anchors the entire IFF architecture. The argument for the metastack structure is based upon Cantor’s Diagonal Argument, as presented in the book Sets for Mathematics (2003) by Lawvere and Rosebrugh. As stated by Saunders Mac Lane in a section on foundations in his book Categories for the Working Mathematician (1971), “One of the main objectives of category theory is to discuss properties of totalities of Mathematical objects such as the ‘set’ of all groups or the ‘set’ of all homomorphisms between any two groups.” Since the IFF not only uses but also axiomatizes category theory, it too must consider such totalities of Mathematical objects. These include, following Mac Lane, the set of all groups grp, the set of all topological spaces top, and the set of all vector spaces vect. Of course, each group, topological or vector space has an underlying set. Let set denote the collection of all sets, as used in everyday mathematics. We assume available some of the usual operations of set theory. In particular, we assume available the power set operator

which maps a set X to its set of all subsets {Y ∈ set | Y ⊆ X}, and the union operator

of sets of sets, which takes any set X ∈ set where X ⊂ set, this gives the meaning of the collection Pset, to the set ∪X = {y ∈ Y | some Y ∈ X} ∈ set. As Cantor’s diagonal argument implies, the collection set is not an ordinary, everyday, garden-variety set; that is, it is not true that set ∈ set. But of course set is some kind of set. So, let set₁ = set denote the collection of all ordinary garden-variety sets and let set₂ denote a larger notion of set (kind of collection): set₁ ⊆ set₂ and set₁ ∈ set₂ (thus, we have the strict inequality set₁ ⊂ set₂). We call set₁ the collection of all small sets, and we call set₂ the collection of all large sets. Hence, the collection of all small sets is a large set, and any small set is itself a large set. Of course, we also note that the collection of all groups is a large set grp ∈ set₂, the collection of all topological spaces is a large set top ∈ set₂, and the collection of all vector spaces is a large set vect ∈ set₂.

One consequence of Cantor’s diagonal argument (Lawvere and Rosebrugh, Mac Lane) is that this is not a set. In working practice, mathematicians distinguish between ordinary collections, such as the collection of all the current occupants of Paris or the collection of all of the stars in the Milky Way galaxy, from “larger” collections such as set₁. The latter kind of set is called a large set or a proper class, while the ordinary kind of set is called a small set or just set. Let set₂ denote the collection of all classes. All small sets are classes set₁ ⊂ set₂, and the collection of all small sets is a class set₁ ∈ set₂, but there are some classes that are not small sets, such as set₁ (that is, it is not the case that set₁ ∈ set₁). As noted before, typical categories such as the category Grp of (small) groups and group morphisms, the category Top of (small) topological spaces and continuous maps, the category Vect of (small) vector spaces and linear transformations, and the category Set = Set₁ of (small) sets and functions between small sets, are large categories in the sense that their sets of objects and morphisms are large.

In practice, in particular in the application of category theory, mathematicians sometimes need to distinguish an even “larger” kind of collection, called a very large set. Specifically, the category CAT of large categories and functors has very large object and morphism sets. Let set₃ denote this even larger notion of set (kind of collection): set₂ ⊆ set₃ and set₂ ∈ set₃ (thus, we have the strict inequality set₂ ⊂ set₃), and let Set₂ denote the category of (large) sets and functions between large sets. Then Set₂ is a very large category — a category whose collection of objects (morphisms) is very large. This initiates the chain:

This chain is at the heart of the IFF metastack, and results in the architecture visualized above in Figure 1, which includes not only a chain of different kinds of sets, but also (using pullbacks, in particular optimal restriction on functions and abridgment on relations) corresponding chains of (unary) functions and (binary) relations. The supremum of all three chains are the cumulated collection of generic sets, functions and relations axiomatized in the Ur meta-ontology. The necessary ingredients for describing the terms of the Ur meta-ontology is axiomatized in the meta namespace of the metashell.