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.1. Tuples, families
Formalization of operations and currying
The notion of nary operation, objects acting as nary
operators between n sets, would be formalized by:
 n domain functors (of little practical use);
 an (n+1)ary operator of evaluation (evaluator) written in filled form as
f(x_{1},…,x_{n}),
with arguments an nary operation f and its
n arguments x_{1},…,x_{n};
 an operation definer, binding n variables to their respective
ranges on a term.
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 ≈ (E ∋ x ↦
(F ∋ y ↦ t(x,y))) = g
f(x,y) = g(x)(y) = t(x,y)
The intermediate function g(x) = (F ∋ y
↦ t(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 nary relations involves an (n+1)ary
predicate of evaluation, and a definer binding n variables
on a formula. We may either see nary relations as
particular cases of nary operations (representing
Booleans as objects), or see nary 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 setbuilder, as will be done in 2.3 with n=2),
or using tuples (2.1).
Tuples
A tuple (or ntuple, for any natural number n) is an
interpretation of a list of (n) variables. It is thus a metafunction
from a finite metaset, 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
= (x_{0},…, x_{n−1}).
In practice, the domain of considered ntuples will be the
(meta)set V_{n} of n
digits from 0 to n−1. Set theory can represent its own ntuples
as functions, figuring V_{n}
as a set of objects all named by constants. A 2tuple is called an oriented
pair, a 3tuple is a triple, a 4tuple is a quadruple...
The ntuple definer is not a binder but an nary
operator, placing its n arguments in a parenthesis and
separated by commas: ( ,…, ). The evaluator appears,
curried by fixing the metaargument, as a list of n functors
called projections: for each i∈V_{n}, the ith
projection π_{i} gives the value π_{i}(x)
= x_{i} of each tuple
x=(x_{0},…,x_{n−1})
at i (value of the ith variable inside x).
They are subject to the following axioms (where the first sums up
the next ones) : for any x_{0},…, x_{n−1}
and any ntuple x,
x = (x_{0},…,x_{n−1})
⇔ (π_{0}(x)=x_{0} ∧ …
∧ π_{n−1}(x)=x_{n−1})
x_{i}= π_{i}((x_{0},…,
x_{n−1})) for each i
∈ V_{n}
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 = π_{0}(π_{0}(t)),
y=π_{1}(π_{0}(t)),
z=π_{1}(t).
Conditional connective
The 3ary connective «If A then B otherwise C», is written as
follows (applying (C,B) to A ∈ V_{2}): (A ? B : C) ⇔
(¬C⇒A⇒B) ⇔ ((A⇒B)∧(¬A⇒C))
⇔ (¬A ? C : B) ⇔ (C,B)(A)
⇔ ((A∧B)∨(¬A∧C)) ⇔
((C⇒A)⇒(A∧B))
⇎ (A ? ¬B : ¬C)
Any n+1ary connective K amounts to two nary
ones: K(A) ⇔ (A ? K(1): K(0)).
Thus, ¬A ⇔ (A ? 0 : 1)
(A⇒B) ⇔ (A
? B : 1)
(A∨B) ⇔ (A ? 1: B)
(A ⇔ B) ⇔ (A ? B : ¬B).
Families
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 metaobjects. 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 u_{i}
(looking like a metavariable symbol of variable). A family defined
by a term t, is written (t(i))_{i∈I}
instead of (I ∋ i ↦ t(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. However each of these 3 lists
is rather conceived as a set but for different reasons:
 Those of types and symbols are best seen as sets of pure elements
serving as indexing sets of possible families

Of the list of axioms, only its image matters, which is a subset of the set of all
expressible ground formulas.
Structures and binders
Each nary structure can be seen as a unary structure with
domain a class of ntuples, 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: (B_{0}∧…∧B_{n−1}) ⇔
(∀i∈V_{n}, B_{i}).
The equality condition between ordered pairs,
(x,y)=(z,t) ⇔ (x=z
∧ y=t), is similar to the one for functions.
Let R a unary predicate definite on E, and C
a boolean. We have distributivities
(C ∧ ∃x∈E, R(x))
⇔ (∃x∈E, C ∧ R(x))
(C ∨ ∀x∈E, R(x))
⇔ (∀x∈E, C ∨ R(x))
(C ⇒ ∀x∈E, R(x)) ⇔ (∀x∈E,
C ⇒ R(x))
((∃x∈E, R(x)) ⇒ C) ⇔
(∀x∈E, R(x) ⇒ C)
(∃x∈E, C) ⇔ (C ∧ E≠∅) ⇒
C ⇒ (C ∨ E=∅) ⇔ (∀x∈E, C)
Extensional definitions of sets
The functor Im defines the binder
{T(x) x∈E} =
{T(x)}_{x∈E} = Im(E ∋ x
↦ T(x))
As this notation looks similar to the set builder, we can combine both :
{T(x) x∈E ∧ R(x)}
= {T(x) x∈{y∈ER(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 V_{n}
as {0,…,n−1}. Images of tuples are finite sets.