Core Concepts

The content of the IFF core is concentrated in a dozen or so core concepts. These are partitioned into basic collections, metastack partial orders and fundamental relations. For a mental image of the metastack architecture, picture a three-dimensional figure in the form of a right prism, with the vertices being the basic collections, the horizontal dimension being structured as the two-dimensional Figure 1 by the fundamental relations, and the vertical dimension being structured by the metastack orders.

Basic Collections

The basic collections in the metastack are set (set), function (ftn), span (spn), predicate (unary relation or part) (pred) and (binary) relation (rel). There are also endorelations (endo ⊆ rel) and partial orders (ord ⊆ endo), and more generally, endospans (endo ⊆ spn) and partially ordered endospans (ord ⊆ endo). These are organized in the metastack via subset chains. Relations can be thought of (and transform into) predicates on a binary product, and predicates can be thought of (and transform into) special functions (injections).

Subset Chains
⋯ ⊆	set_n	⊆	set_n+1	⊆ ⋯ ⊆	set_meta	⊆	set_type	⊆	set_iff
⋯ ⊆	ftn_n	⊆	ftn_n+1	⊆ ⋯ ⊆	ftn_meta	⊆	ftn_type	⊆	ftn_iff
⋯ ⊆	spn_n	⊆	spn_n+1	⊆ ⋯ ⊆	spn_meta	⊆	spn_type	⊆	spn_iff
⋯ ⊆	pred_n	⊆	pred_n+1	⊆ ⋯ ⊆	pred_meta	⊆	pred_type	⊆	pred_iff
⋯ ⊆	rel_n	⊆	rel_n+1	⊆ ⋯ ⊆	rel_meta	⊆	rel_type	⊆	rel_iff
⋯ ⊆	endo_n	⊆	endo_n+1	⊆ ⋯ ⊆	endo_meta	⊆	endo_type	⊆	endo_iff
⋯ ⊆	ord_n	⊆	ord_n+1	⊆ ⋯ ⊆	ord_meta	⊆	ord_type	⊆	ord_iff

Associated with the basic collections are various component functions. There are source and target component functions ∂₀, ∂₁ : ftn → set for the function collection, with pairing function (∂₀,∂₁) : ftn → set×set. There are genus and differentia component functions γ, δ : ftn → set for the predicate collection. There are domain and codomain component functions σ₀, σ₁ : rel → set for the relation collection, with pairing function (σ₀,σ₁) : rel → set×set. There is also an extent component function (injection) ε : rel → set×set for the relation collection. These are organized in the metastack via restriction and optimal-restriction chains.

⋯ ⊑	∂₀ⁿ	⊑	∂₀ⁿ⁺¹	⊑ ⋯ ⊑	∂₀^meta	⊑	∂₀^type	⊑	∂₀^iff
⋯ ⊑	∂₁ⁿ	⊑	∂₁ⁿ⁺¹	⊑ ⋯ ⊑	∂₁^meta	⊑	∂₁^type	⊑	∂₁^iff
⋯ ⊑	δ_n	⊑	δ_n+1	⊑ ⋯ ⊑	δ_meta	⊑	δ_type	⊑	δ_iff
⋯ ⊑	ε_n	⊑	ε_n+1	⊑ ⋯ ⊑	ε_meta	⊑	ε_type	⊑	ε_iff
⋯ ⊑	σ₀ⁿ	⊑	σ₀ⁿ⁺¹	⊑ ⋯ ⊑	σ₀^meta	⊑	σ₀^type	⊑	σ₀^iff
⋯ ⊑	σ₁ⁿ	⊑	σ₁ⁿ⁺¹	⊑ ⋯ ⊑	σ₁^meta	⊑	σ₁^type	⊑	σ₁^iff
⋯ ⊑̊	γ_n	⊑̊	γ_n+1	⊑̊ ⋯ ⊑̊	γ_meta	⊑̊	γ_type	⊑̊	γ_iff

(Optimal-)Restriction Chains
⋯ ⊑̊	(∂_iⁿ)	⊑̊	(∂_iⁿ⁺¹)	⊑̊ ⋯ ⊑̊	(∂_i^meta)	⊑̊	(∂_i^type)	⊑̊	(∂_i^iff)
⋯ ⊑̊	(σ_iⁿ)	⊑̊	(σ_iⁿ⁺¹)	⊑̊ ⋯ ⊑̊	(σ_i^meta)	⊑̊	(σ_i^type)	⊑̊	(σ_i^iff)

Metastack Orders

The partial orders in the metastack are subset (⊆), function restriction (⊑), function optimal-restriction (⊑̊), span abridgment, predicate delimitation (≤) and relation abridgment (≼). Just as (binary) relations are predicates (unary relations or parts) on a binary product and predicates are special functions (injections), so also abridgment is a special case of delimitation and delimitaton is a special case of optimal-restriction. These are organized in the metastack via abridgment chains.

Abridgement Chains
⋯ ≼	⊆_n	≼	⊆_n+1	≼ ⋯ ≼	⊆_meta	≼	⊆_type	≼	⊆_iff
⋯ ≼	⊑_n	≼	⊑_n+1	≼ ⋯ ≼	⊑_meta	≼	⊑_type	≼	⊑_iff
⋯ ≼	⊑̊_n	≼	⊑̊_n+1	≼ ⋯ ≼	⊑̊_meta	≼	⊑̊_type	≼	⊑̊_iff
⋯ ≼	≤_n	≼	≤_n+1	≼ ⋯ ≼	≤_meta	≼	≤_type	≼	≤_iff
⋯ ≼	≼_n	≼	≼_n+1	≼ ⋯ ≼	≼_meta	≼	≼_type	≼	≼_iff

Fundamental Relations

The fundamental relations in the metastack are function belonging (x ⇒ y), span belonging (u ⇒ v), predicate (subobject) inclusion (p ⊆ q), relation inclusion (r ⊆ s), function-predicate membership (x ∈ p) with associated proof operation (⊢(x, p) = x̂), span-relation membership (u ∈ r) with associated proof operation (⊢(u, r) = ȗ), function-set elementhood (x : X) and span-set-pair elementhood (u : (X,Y)). These are defined in terms of “generalized elements” (morphisms in general, functions between abstract sets here) and “generalized subsets” (aka subobjects, parts or predicates) (monomorphisms in general, injections between abstract sets here). The usual relationship holds between inclusion and membership; that is, inclusion is equivalent to universal implication of membership: p ⊆ q iff ∀_x ∈ X (x ∈ p implies x ∈ q) for any two X-predicates (subobjects) p, q : X, and r ⊆ s iff ∀_{u ∈ (X,Y)} (u ∈ r implies u ∈ s) for any two (X,Y)-relations r, s : (X,Y).

Figure 1: IFF Subobject Architecture

The IFF uses category theory, both in its applications and as a foundation for its architecture. Composition is the most fundamental concept in category theory. Generalized composition is composition extended to generalized elements (morphisms in general, functions between abstract sets here). The IFF represents, axiomatizes and uses generalized composition to ensure that the IFF natural part has an atomic expression. In the IFF, generalized composition is defined in terms of span-relation membership, plus the associated proof operation.

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.