# 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

#### Tuples

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*
= (*x*_{0},…, *x*_{n−1}).
In practice, the domain of considered *n*-tuples will be the
(meta-)set V_{n} of *n*
digits from 0 to *n*−1. Set theory can represent its own *n*-tuples
as functions, figuring V_{n}
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 *i*∈V_{n}, the *i*-th
projection π_{i} gives the value π_{i}(*x*)
= *x*_{i} of each tuple
*x*=(*x*_{0},…,*x*_{n−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 *x*_{0},…, *x*_{n−1}
and any *n*-tuple *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 3-ary 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*+1-ary connective *K* amounts to two *n*-ary
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 meta-objects. A «family of...
» is a family whose image is a «set of... ».

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 meta-variable 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*.
#### 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: (*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*∈*E*|*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 V_{n}
as {0,…,*n*−1}. Images of tuples are finite sets.