Membership is one of the more important relations in the IFF. Here we follow the category-theoretic approach of Lawvere and Rosebrugh in Sets for Mathematics, 2003 and Lawvere’s three email messages Why are we concerned? I, II and III sent earlier this year to the CAT list. In the IFF syntax and in the IFF-IFF namespace, membership is treated in the traditional set-theoretic fashion. For example, if the symbols ‘X’ and ‘x’ represent the two IFF things X and x, then the IFF code ‘(set X)’ declares X to be a set, and the IFF code ‘(X x)’ makes the assertion that object x is a member of set X, x ∈ X. However, in the natural part of the IFF, in order to represent and use “generalized composition”, it is important that membership be treated in a category-theoretic fashion. This categorical treatment of membership actually starts near the top of the metashell in the IFF-TYPE namespace.

Elements

From the category theoretic point of view, the statement x ∈ X that object x is a member of set X is represented by the mapping x : 1 → X from source indexing set 1 = {0} to target set X. We can think of the image x(0) ∈ X as being the actual object with the map x pointing to it. In category theory, such a mapping is called an element. For example, if set X represents all ancient Greek philosophers, then the map x might represent Socrates. However, we can change the indexing set to be something larger. For example, if X represents this same set, a mapping x : 2 → X from indexing set 2 = {0,1} to set X might represent the two philosophers Socrates and Plato with x(0) ∈ X being the actual object Socrates and x(1) ∈ X being the actual object Plato; that is, the map x represents the subset {Socrates, Plato} ⊆ X. In this case the mapping is injective, meaning that different indices map to different things in X. Hence, maps can represent subsets, and in this case they are injective. In the IFF, a generalized element is a function x : Y → X from source indexing set Y to target set X. Category theory abstracts these definitions. In category theory, a morphism x : 1 → X in a category represents an element, and a morphism x : Y → X in a category represents a generalized element. In summary, both “element in a set” and “subset of a set” are represented by morphisms in category theory and functions in the metashell and pure aspect of the IFF.

Belonging, Inclusion and Membership

Here we follow the approach of Lawvere and Rosebrugh to membership and inclusion, and we quote and paraphrase from Lawvere’s second email message cited above. Composition in a category is a kind of non-commutative multiplication, hence there are two kinds of division problems. For example, when x is the composition of y and z, x = y · z, then y divides x on the left and z divides x on the right. (Note: we use diagrammatic order throughout the IFF documentation and axiomatization; thus, y · z means apply y first and z second.) We could say that y is a left divisor of x and z is a right divisor of x. If the emphasis is on left division, then z might be called the quotient of the left division of x by y. However, we actually use different terminology.

In any category, given any two morphisms a and b, we can ask whether there exists a left divisor p of (the dividend) a returning the quotient b, a = p · b; if so, we say that a belongs to b and that p is a proof (there may be several) of that belonging. This forces a and b to have the same object X as target (Figure 1), and this object serves as their common “context” or “universe of discourse”. (The dual relation, f determines g, defined by ‘there exists m with f · m = g’, is also important in mathematics.)

There are two special cases of this belonging relation which are of interest. First we say that b is a part (or subset in the case of a category of sets) of its target, if for all a belonging to b, the proof p of that belonging is unique; this is immediately seen to be equivalent to the usual notion of monomorphism (or injection in a category of sets). Then, if a and b are parts of the same object X, we say a is included in b, symbolized a ⊆ b, when a belongs to b. Any arbitrary morphism (generalized element) x with target X may be considered an element of (figure in) X in the sense of Volterra, symbolized x : X. If x is an element of X and b is a part of X, then x is a member of b, symbolized x ∈ b, when x belongs to b. The following equivalence holds between inclusion and universal implication of membership. Hence, the usual connection between these two relations is maintained. This equivalence holds even with x restricted to special elements (those with source 1).

Fact 1.

a ⊆ b iff (∀x) if x ∈ a then x ∈ b.

 

Some IFF documents such as this one contain a lot of unicode characters, and so require a recent browser. But even some recent browsers fail to render it properly. Two browsers that do render these documents correctly are Firefox and Opera.

Author: Robert E. Kent