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:
- 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 n-ary 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 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).
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... » (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 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.
As we described the content
of a theory, a "list" basically means a family. But more precisely:
- The list of types is best seen as a set of urelements, usable as indexing
set of possible families
- The list of symbols can be formalized as a family of tuples
of types
- Of the list of axioms, only its image matters, which is a subset of the set of all
expressible statements.
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.