2. Set theory (continued)

The first part of this exposition on the foundations of mathematics introduced both set theory and model theory; the second part continues developing set theory.

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=(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 x00(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).

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 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.

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 replacing tuples by families. 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 (continued)
2.1. Tuples, families
2.2. Boolean operators on families of sets
2.3. Products, graphs and composition
2.4. Uniqueness quantifiers, functional graphs
2.5. The powerset axiom
2.6. Injectivity and inversion
2.7. Binary relations ; orders
2.8. Canonical bijections
2.9. Equivalence relations and partitions
2.10. Axiom of choice
2.11. Notion of Galois connection
3. Model theory