2.3. Currying and tuples

Formalizing operations and relations

To formalize in set theory every notion of operation (resp. relation) with any fixed arity n>1, acting as n-ary structures between n sets, would involve the following symbols (generalizing the case n = 1 of functions which we took as primitive): Let us give to the operation definers, the following notation which will be later (2.7) justified as reflecting their definitions: in the binary case (n = 2), operations defined by a binary operator A with domains E and F will be written

E×F ∋ (x,y) ↦ A(x,y)

After seeing what operations and relations are (which role they play) let us discuss how they are reducible to something else.
One aspect is that relations are reducible to operations, and vice-versa: These constructions can be useful despite their circularity (they are not decreasing the arity). But for foundational purposes, we need a construction which reduces to lower arity cases, down to sets and functions. There are actually 2 such constructions.


The simplest constructions of the notions of n-ary operation from our primitive tools for functions, are their curried representations, defined as classes of functions by expressing the operation definer as n successive uses of the function definer (one for each bound variable); and thus the evaluator as n uses of the function evaluator. For n=2, this means a binary operation in curried form b with domains E and F, is defined from a binary operator B, and evaluated back as B, by the formulas

b = (Ex ↦ (FyB(x,y)))
Dom b = E ∧ ∀xE, Dom b(x) = F ∧ ∀yF, B(x,y) = b(x)(y)

whose equivalence, similar to the axiom 1. for functions, is deducible from it.
The first domain functor comes as Dom b = E, but the second one, given as common value of all Dom b(x), is only definite for E ≠ ∅. The intermediate function b(x) = (FyB(x,y)) represents the functor defined by B with parameter x (free) and argument y (bound).
This somehow makes each binary operation work as a function evaluator, by giving x the role of a function with argument y ; the curried function evaluator just gives back each function it takes : f ↦ ((Dom f) ∋ yf(y)).

Similarly, the notion of n-ary relation can be defined in curried form as a class, giving the role of definer to a succession of n−1 uses of the function definer and 1 use of the set-builder. The curried form r of a binary relation with domains E and F, is so defined from a binary predicate R, and evaluated back as R, by the equivalent formulas

r = (Ex ↦ {yF | R(x,y)})
Dom r = E ∧ (∀xE, r(x) ⊂ F ∧ ∀yF, R(x,y) ⇔ yr(x))

This leaves no way to define second domain functor (F cannot be restored from r).
These constructions have the defect of breaking the symmetry of role between arguments. The next construction method, by tuples, will preserve this symmetry, and will be usually preferred for this reason.


For any theory and any natural number n, a notion of n-tuple is a notion constructed for its variables to serve as abbreviations for a pack of n variables from previous notions. A 2-tuple is called an ordered pair, a 3-tuple is a triple, a 4-tuple is a quadruple and so on. So each tuple x (so constructed object) represents a meta-function of "interpretation" from this list (meta-set) of n variables, into the model.

The definer and evaluator symbols for tuples take a special form because, while tuples are meta-functions, the role they play in the theory differs from those of functors or functions.

An n-tuple definer is not a binder but an n-ary operator, packing its n variables into one by taking them as its arguments in a parenthesis and separated by commas: ( ,…, ).

Now, each structure (resp. operation, relation) can be re-formalized as a unary structure (resp. a function, a unary relation) with domain a type (resp. a class which is actually a set) of tuples, to be used with the relevant tuples definer. This can be implicitly done by re-interpreting the notation: S(x,y) can be read seeing S either as a binary structure (resp. operation, relation), or as a unary one taking as argument the ordered pair given by the term (x,y) formed by the ordered pair definer with arguments x and y.

The role of n-tuple evaluator is played by a list of n functors called projections which extract each variable from the given pack. This list plays the role of the function evaluator curried in the reverse way, by fixing its meta-argument whose range (the domain of tuples as meta-functions) is not seen by the theory as a set of objects but as a list of n symbols to be taken separately.

The formal details of this construction depend whether we take a generic theory or a set theory.

Tuples axiom

In generic theories, it must be a distinct constructed type for not only each n but also each choice of the type of each of these n variables (if starting from a theory with multiple types - this choice of a list of variables with their types amounts to the choice of a predicate symbol type), but this directly forms a legitimate construction (4.11).
For n=2 (other cases are similar), and a type P of ordered pairs (x,y) where x,y have types E and F, the projections π0 and π1 are related to the ordered pair definer, by the axiom

E x, ∀F y, ∀P z, (x = π0(z) ∧ y = π1(z)) ⇔ (x,y) = z

which implies

P z, (π0(z), π1(z)) = z
E x, ∀F y, π0(x,y) = x
E x, ∀F y, π1(x,y) = y
E x,x', ∀F y,y', (x,y) = (x',y') ⇔ (x = x'y = y')

Tuples in set theory

Set theory having no types only needs one notion of n-tuple for each n. But it faces one difficulty : in order to rigorously justify that all tools of set theory remain applicable to tuples in the same way as to the rest of elements, tuples need to be integrated among elements. Namely, set theory needs to develop its notions of tuples by defining them as classes of already existing elements, instead of simply accepting them by the above constructions, which would leave them as separate types.

For this, since tuples are meta-functions, they are naturally represented by functions. This involves copying their meta-domain, which is a list of symbols, into a set (of elements). Namely, let us represent the domain of considered n-tuples by the set Vn of n numbers from 0 to n−1 all named by constant symbols we shall simply conceive as digits. To justify this as a development of set theory, these digits can be defined by any ground terms with distinct values, such as ∅, {∅}, {∅, {∅}} and endlessly many more sets and functions expressed from there. The notion of n-tuple is then defined as the class of all functions with domain Vn.

Then, the projections are defined by the function evaluator applied to the respective digits, which can be read as disguised in their notations : for all n-tuples x,

iVn, πi(x) = x(i).

This index notation, making a pun of the equivalence between reading the index i as an argument or a meta-argument that means to take the i-th symbol from a list (here πi is the i-th projection), is also commonly used for tuples : xi can be either read as the i-th variable in the tuple x = (x0,…,xn−1), or as a third notation for the same evaluator after x(i) and πi(x).

More tools need to be introduced before defining in set theory the tuple definers (2.4) and the operation definers working with tuples (2.7).

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
2.4. Uniqueness quantifiers

2.5. Families, Boolean operators on sets
2.6. Graphs
2.7. Products and powerset
2.8. Injections, bijections
2.9. Properties of binary relations
2.10. Axiom of choice
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 2.3. Curryfication et uplets