The IFF Namespace

Table 1: Terminology
	Set	Function
	thing
	set
	function	source target
	Technical and Recommended Prefix:iff

Namespace Prefix: Technical: iff; Recommended: iff

The IFF namespace is a tiny namespace at the very top of the IFF architecture. The terminology of the IFF namespace, which is used to specify the concepts in the IFF type namespace and hence the entire IFF, is listed in Table 1. There are only five primitive terms and two primitive syntactic constructs. There is a collection of all IFF things. Conceptually, all IFF things are morphisms; morphisms combine via an associative composition operation, and objects are special identity morphisms satisfying two unit laws. Since we are within a universe of Cantorian featureless sets (a graph at the iff level, a finitely-complete category with subobjects at the type level, and a well-pointed topos from the meta level down), we use the terminology ‘set’ and ‘function’ for objects and morphisms, respectively. Practically, we take several shortcuts: (1) at this level we ignore composition and identity; (2) for our primitive syntactic constructs of set membership (declaration) and function application, we use ordinary set-theoretic elements rather than generalized category-theoretic elements, and (3) in order to distinguish the two syntactic constructs during parsing, we separate IFF things into the two disjoint collections of IFF sets and IFF functions, with source and target maps from functions to sets.

Like other parts of the IFF metashell, the IFF namespace is closely related to the IFF grammar, which specifies the correct form for IFF expressions. The IFF grammar can be used for type correctness in set membership and function application: an error should be signaled, (1) if a set symbol is being used as a function (in a term), or (2) if a function symbol is being used as a set (in a declaration) or a set component for functions. As is explained below, the IFF grammar can and should be used to check for well-formedness of set membership and function application.

IFF Things

Things exist. There is a collection of all IFF things. The symbol ‘thing’ is used to declare an IFF thing. Any IFF thing is an IFF set or an IFF function. But no thing can be both set and function.

(forall ((thing ?x))
    (and (or (set ?x) (function ?x))
         (not (and (set ?x) (function ?x)))))

IFF Sets

Sets exist. There is a collection set of all IFF sets. The symbol ‘set’ is used to declare an IFF set. Any IFF set is an IFF thing. Any element of an IFF set is an IFF thing.

(forall ((set ?X)) (thing ?X))
(forall ((set ?X) (?X ?x)) (thing ?x))

If the symbols ‘X’ and ‘x’ represent the two IFF things X and x, then the code

(set X)

declares X to be an IFF set, X ∈ set, and the code

(X x)

which expresses the primitive syntactic construct of set membership (declaration) that “x ∈ X”, is a well-formed statement of IFF. However, the following nullary, binary, ternary and higher arity expressions are ill-formed:

(X)
(X x0 x1)
(X x0 x1 x2)
...

Two sets are equal precisely when they have the same elements: for any two sets X, Y ∈ set, X = Y iff ∀_x ∈ X x ∈ Y and vice-versa.

(forall ((set ?X) (set ?Y))
    (<=> (= ?X ?Y)
         (and (forall ({?X ?x)) (?Y ?x))
              (forall ({?Y ?y)) (?X ?y)))))

IFF Functions

Functions exist. There is a collection ftn of all IFF functions. The symbol ‘function’ is used to declare an IFF function. Any IFF function is an IFF thing.

(forall ((function ?f)) (thing ?f))

Each IFF function has a unique source IFF set and a unique target IFF set. The function notation f : X → Y shows an IFF function f ∈ ftn with source IFF set X ∈ set and target IFF set Y ∈ set. The notation ∂₀(f) = X and ∂₁(f) = Y is also used to assert the source and target. Hence, the IFF namespace represents a graph of abstract sets and functions (Figure 1)

Figure 1: Graph

with the collection ftn of IFF functions as the edges of the graph, the collection set of IFF sets as the nodes of the graph, and the source and target operations ∂₀, ∂₁ : ftn → set mapping functions to sets. The symbols ‘source’ and ‘target’ are used to express application of the source and target (total, functional) operations.

(forall ((thing ?f) (thing ?X) (= ?X (source ?f)))
    (and (function ?f) (set ?X)))

(forall ((function ?f))
    (and (exists ((set ?X))
             (= (source ?f) ?X))
         (forall ((set ?X0) (set ?X1) (= (source ?f) ?X0) (= (source ?f) ?X1))
             (= ?X0 ?X1))))

(forall ((thing ?f) (thing ?Y) (= ?Y (target ?f)))
    (and (function ?f) (set ?Y)))

(forall ((function ?f))
    (and (exists ((set ?Y))
             (= (target ?f) ?Y))
         (forall ((set ?Y0) (set ?Y1) (= (target ?f) ?Y0) (= (target ?f) ?Y1))
             (= ?Y0 ?Y1))))

Any IFF function is required to be total (defined on all source elements) and functional (have only one value).

Note: This axiom uses quantification over variables in function position.

(forall ((function ?f) ((source ?f) ?x))
    (and (exists (((target ?f) ?y))
             (= (?f ?x) ?y))
         (forall (((target ?f) ?y0) ((target ?f) ?y1) (= (?f ?x) ?y0) (= (?f ?x) ?y1))
             (= ?y0 ?y1))))

If the symbols ‘f’, ‘X’ and ‘Y’ represent the three IFF things f, X and Y, then

(function f)
(set X) (= (source f) X) 
(set Y) (= (target f) Y)

makes the declaration “f ∈ ftn ” and “f : X → Y” (or “∂₀(f) = X” and “∂₁(f) = Y”), and

(X x) (X y) 
(= y (f x))

expresses the equality statement that “ y = f(x)”. Hence, the primitive syntactic construct ‘(f x)’ of function application is a well-formed term, which follows the prescription: all IFF functions are unary. Hence, the following nullary, binary, ternary and higher arity expressions are iff-formed

(= y (f))
(= y (f x0 x1))
(= y (f x0 x1 x2))
...

The IFF tuple notation can be used to express n-ary functions

(= y (f [x0 x1 ...]))

Two functions are equal precisely when they have the same source and target sets and the same image on all source elements: for any two functions f, g ∈ ftn, f = g iff ∂₀(f) = ∂₀(g), ∂₁(f) = ∂₁(g), and ∀_{x ∈ ∂₀(f)} f(x) = g(x).

(forall ((function ?f) (function ?g))
    (<=> (= ?f ?g)
         (and (= (source ?f) (source ?g)) 
              (= (target ?f) (target ?g))
              (forall ({(source ?f) x)) 
                  (= (?f ?x) (?g ?x))))))

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.