2. Set theory (continued)

Having introduced both set theory and model theory in the first part, we continue developing set theory in second part.

2.3. Tuples, families

Formalization of operations and currying

The notion of n-ary operation, objects acting as n-ary operators between n sets, would be formalized by: The notion of operation can be represented as a class of functions, in the following way called currying. The role of operation definer (binding n variables) is played by the succession of n uses of the function definer (one for each bound variable); and similarly as an evaluator, n uses of the function evaluator. For example (n=2), the binary operation f defined by the term (binary predicate) t with arguments x in E and y in F, may be formalized by

f ≈ (Ex ↦ (Fyt(x,y))) = g
(x,y) = g(x)(y) = t(x,y)

The intermediate function g(x) = (Fyt(x,y)) with argument y, sees x as fixed and y as bound. But this breaks the symmetry between arguments, and loses the data of F when E is empty but not the other way round. A formalization without these flaws will be possible using tuples (2.1.).

The formalization of n-ary relations involves an (n+1)-ary predicate of evaluation, and a definer binding n variables on a formula. We may either see n-ary relations as particular cases of n-ary operations (representing Booleans as objects), or see n-ary operations as particular cases of (n+1)-ary relations (see 2.3). And just like operations, relations can be reduced to the unary case in 2 ways : by currying (with n−1 uses of the function definer and 1 use of the set-builder, as will be done in 2.3 with n=2), or using tuples (2.1).


A tuple (or n-tuple, for any natural number n) is an interpretation of a list of (n) variables. It is thus a meta-function from a finite meta-set, to the universe. Tuples of a given kind (list of variables with their types) can be added to any theory as a new type of objects. Variables of this type play the role of abbreviations of packs of n variables with old types (copies of the given list) x = (x0,…, xn−1). In practice, the domain of considered n-tuples will be the (meta-)set Vn of n digits from 0 to n−1. Set theory can represent its own n-tuples as functions, figuring Vn as a set of objects all named by constants. A 2-tuple is called an oriented pair, a 3-tuple is a triple, a 4-tuple is a quadruple...
The n-tuple definer is not a binder but an n-ary operator, placing its n arguments in a parenthesis and separated by commas: ( ,…, ). The evaluator appears, curried by fixing the meta-argument, as a list of n functors called projections: for each iVn, the i-th projection πi gives the value πi(x) = xi of each tuple x=(x0,…,xn−1) at i (value of the i-th variable inside x). They are subject to the following axioms (where the first sums up the next ones) : for any x0,…, xn−1 and any n-tuple x,

x = (x0,…,xn−1) ⇔ (π0(x)=x0 ∧ … ∧ πn−1(x)=xn−1)
xi= πi((x0,…, xn−1))    for each iVn
x = (π0(x),…, πn−1(x))

Oriented pairs suffice to build a representation of tuples of any arity n > 2, in the sense that we can define operators to play the roles of definer and projections, satisfying the same axioms. For example, triples t = (x,y,z) can be defined as t = ((x,y),z)) and evaluated by x = π00(t)), y10(t)), z1(t).

Conditional connective

The 3-ary connective «If A then B otherwise C», is written as follows (applying (C,B) to AV2):

(A ? B : C) ⇔ (¬CAB) ⇔ ((AB)∧(¬AC)) ⇔ (¬A ? C : B) ⇔ (C,B)(A)
⇔ ((AB)∨(¬AC)) ⇔ ((CA)⇒(AB)) ⇎ (A ? ¬B : ¬C)

Any n+1-ary connective K amounts to two n-ary ones: K(A) ⇔ (A ? K(1): K(0)). Thus,

¬A ⇔ (A ? 0 : 1)
(AB) ⇔ (A ? B : 1)
(AB) ⇔ (A ? 1: B)
(AB) ⇔ (A ? B : ¬B).


A family is a function intuitively seen as a generalized tuple: its domain (a set) is seen as simple, fixed, outside the main studied system, as if it was a set of meta-objects. A «family of... » is a family whose image is a «set of... » (included in the range of these things).

Families use the formalism of functions disguised in the style of tuples (whose tools cannot apply due to the finiteness of symbols). The evaluator (evaluating u at i), instead of u(i) or πi(u), is written ui (looking like a meta-variable symbol of variable). A family defined by a term t, is written (t(i))iI instead of (Iit(i)) or (t(0),…,t(n−1)). The argument i is called index, and the family is said indexed by its domain I.

As we described the content of a theory, a "list" basically means a family. But more precisely:

Structures and binders

Each n-ary structure can be seen as a unary structure with domain a class of n-tuples, like a binder can be seen as a unary structure on a class of functions or subsets of a given set: binders are the generalization of structures when families replace tuples. In particular, ∀ and ∃ generalize the chains of conjunctions and disjunctions:

(B0∧…∧Bn−1) ⇔ (∀iVn, Bi).

The equality condition between ordered pairs, (x,y)=(z,t) ⇔ (x=zy=t), is similar to the one for functions.

Let R a unary predicate definite on E, and C a boolean. We have distributivities

(C ∧ ∃xE, R(x))  ⇔  (∃xE, CR(x))
(C ∨ ∀xE, R(x))  ⇔  (∀xE, CR(x))
(C ⇒ ∀xE, R(x))  ⇔  (∀xE, CR(x))
((∃xE, R(x)) ⇒ C)  ⇔  (∀xE, R(x) ⇒ C)
(∃xE, C) ⇔ (CE≠∅) ⇒ C ⇒ (CE=∅) ⇔ (∀xE, C)

Extensional definitions of sets

The functor Im defines the binder

{T(x)| xE} = {T(x)}xE = Im(ExT(x))

As this notation looks similar to the set builder, we can combine both :

{T(x)| xER(x)} = {T(x)| x∈{yE|R(y)}}

Applying Im to tuples, defines the operator symbols of exensional definition of sets (listing their elements): Im(a,b,…) = {a,b,…}. Those of arity 0,1,2 were presented in 1.11: the empty set ∅, the singleton {a} and the pairing {a,b}. We defined Vn as {0,…,n−1}. Images of tuples are finite sets.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. Formalization of set theory
2.2. Set generation principle
2.3. Tuples, families
2.4. Boolean operators on sets
2.5. Products, graphs and composition
2.6. Uniqueness quantifiers, functional graphs
2.7. The powerset
2.8. Injectivity and inversion
2.9. Binary relations ; order
2.10. Canonical bijections
2.11. Equivalence relations, partitions
2.12. Axiom of choice
2.13. Galois connection
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations