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

2.2. Boolean operators on sets

Union of a family of sets

For any family of unary predicates Ai with index iI, all definite in (at least) a common class C, their application to the same variable x with range C reduces this to a family of Boolean variables depending on x (their parameter, see 1.5). This way, any operation Q on these variables (a quantifier with range I, which becomes a connective when I is finite) defines a meta-operation between unary predicates, with result a unary predicate ℛ, defined for x in C as Qi, Ai(x). When C is a set E, this operates between subsets of E (through ∈ and the set builder).
For example, the existential quantifier (Q=∃) defines the union of a family of sets:

x
iI
Fi ⇔ ∃iI, xFi

This class is a set independent of E, as it can also be defined from the union of a set of sets (1.11):

iI
Fi ={Fi | iI}
(x
iI
Fi, B(x)) ⇔ ∀iI, ∀xFi, B(x)
xXY ⇔ (xXxY)
XXY = YX

All extensional definition operators (except ∅) are definable from pairing and binary union.

Intersection

Any family of sets (Fi)iI can be seen as a family of subsets of some common set, such as their union U=⋃iI Fi , or any other set E such that UE. Then for any operation (quantifier) Q between Booleans indexed by I, the predicate ℛ(x) defined as (Qi, xFi) takes value (Qi, 0) for all xU. Thus Q needs to satisfy ¬(Qi,0) (to be false when all entries are false) for the class ℛ to be a set {xE| ℛ(x)}={xU| ℛ(x)}. This was the case for Q=∃, including on the empty family (⋃∅ =∅), but for ∀ (that defines the intersection) it requires a non-empty family of sets (I ≠ ∅):
 ∀jI,
iI
Fi = {xFj | ∀iI, xFi}
  x
iI
Fi ⇔ ∀iI, xFi
xXY ⇔ (xXxY)
XY = YX = {xX | xY} ⊂ X
X = XYYXY = XY

Two sets A and B are called disjoint when AB=∅, which is equivalent to ∀xA, xB.
Union and intersection have the same associativity and distributivity properties as ∧ and ∨ :

ABC = (AB)∪C = A∪(BC) ={A,B,C}
(
iI
Ai)C =

iI
(AiC) (
iI
Ai)C =

iI
(AiC)
(AB)⋂C = (AC)∪(BC) (AB)∪C =
(AC)⋂(BC)

Other operators

The difference is defined by A\B = {xA| xB} so that xA\B ⇔ xAxB.
Finally the connective ⇎ gives the symmetric difference: AB = (AB)\(AB).
When (Qi,0) is true, we must choose a set E to define operations between subsets of E:

iI
Fi = {Fi|iI} = {xE | ∀iI, xFi} = ∁E
iI
E Fi

2.3. Products, graphs and composition

Finite product

For any two sets E and F, the product E×F is the set of (x,y) where xE and yF. Similarly, the product of n sets E0×…×En−1 is the set of n-tuples (x0,…,xn−1) where ∀iVn, xiEi.
An n-ary operation is a function with domain a product of n sets.
A relation between any two sets E and F is formalized as a set of oriented pairs GE×F (the domains E and F might be specified by taking the triple (E,F,G)). A set of oriented pairs (such as G) is called a graph.
For any binder Q and any graph G, the formula QxG, A(x0, x1) that binds x = (x0, x1) on a binary structure A with domain G, can be seen as binding 2 variables x0, x1 on A(x0, x1), and thus be denoted with an oriented pair of variables: Q(y,z) ∈ G, A(y,z).
The existence of the product (in all arity) is justified by the set generation principle:

(∃(x,y) ∈ E×F, A(x,y)) ⇔ (∃xE, ∃yF, A(x,y)) ⇔ (∃yF,∃xE, A(x,y))
(∀(x,y) ∈ E×F, A(x,y)) ⇔ (∀xE, ∀yF, A(x,y)) ⇔ (∀yF,∀xE, A(x,y))

The quantifier ∀(x,y) ∈ E×E will be abbreviated as ∀x,yE, and the same for ∃.
With F=V2,
(∃xE, A(x)∨B(x)) ⇔ ((∃xE, A(x))∨(∃xE,B(x))
(∀xE, A(x)∧B(x)) ⇔ ((∀xE, A(x))∧(∀xE,B(x))
(∃xE, CA(x)) ⇔ ((C∧(E ≠ ∅))∨∃xE, A(x))
(∀xE, CA(x)) ⇔ ((C∨(E=∅))∧∀xE, A(x))

Sum or disjoint union

The transpose of an ordered pair is
t(x,y)=(y,x)
That of a graph R is
tR={(y,x)|(x,y) ∈ R}
Graphs can be expressed in curried forms R andR :
yR (x) ⇔ (x,y) ∈ R ⇔ xR (y) = tR (y)
justified by defining the functor R as
R(x) = {y | (z,y)∈Rz=x}.

Inversely, any family of sets (Ei)II defines a graph called their sum (or disjoint union) ∐iI Ei:

(iIxEi)  ⇔ (i,x) ∈
iI
Ei =
iI
{iEi=
iI
={(i,x)|xEi} ⊂ I×
iI
Ei

(∀x ∈ ∐iIEi, A(x)) ⇔ (∀iI,∀yEi, A(i,y))
E0⊔…⊔En−1 = ∐iVn Ei
E×F = ∐xE F     E×∅ = ∅ = ∅×E
(EE′∧FF′) ⇒E×FE′×F
(∀iI, EiEi) ⇔ ∐iI Ei ⊂ ∐iI Ei

Composition, restriction, graph of a function

For any set E, the function identity on E is defined by IdE = (Exx).
For any functions f,g with ImfDomg (namely, f : E → F and g : F → G), their composite is

gf = ((Dom f) ∋ xg(f(x))): E → G

The same with h:G →H, hgf = (hg)০f = h০(gf) = (Exh(g(f(x)))) and so on.
The restriction of f to ADomf is f|A= (Axf(x)) = fIdA.
The graph of a function f is defined by
Gr f = {(x,f(x)) | x ∈ Dom f} = ∐xDomf {f(x)}
(x,y) ∈ Gr f ⇔ (x ∈ Dom fy=f(x))
We can define domains, images and restrictions for graphs, generalizing those for functions (i.e. Dom f = Dom(Grf), Imf = Im(Grf) and Gr(f|A)=(Grf)|A):

Dom R={x|(x,y) ∈ R}= Im tR
xx ∈ Dom R ⇔ R (x) ≠ ∅
RE×F ⇔ (Dom RE ∧ Im RF)
R|A=R∩(A× Im R) = {(x,y) ∈ R | xA} = ∐xA R (x)

Then we have R = ∐iI Ei ⇔ (Dom RI ∧ ∀iI, R(i)=Ei) ⇒ Im R = iI Ei.
For any functions f,g, any graph R, and E= Dom f,

Gr fR ⇔ ∀xE, f(x) ∈ R(x)
R ⊂ Gr f
⇔ (∀(x,y) ∈ R, xEy=f(x)) ⇔ (Dom RE∧∀(x,y)∈R, y=f(x))
Gr f ⊂ Gr g ⇔ ((E ⊂ Dom g)∧ f=g|E)

Direct image, inverse image

The direct image of a set A by a graph R is R*(A) = Im R|A= xA R(x).
Dom RA ⇔ R|A=RR*(A)= Im R
R*(
iI
Ai) =
iI
R*(Ai)
R*(
iI
Ai) ⊂
iI
R*(Ai)

ABR*(A) ⊂ R*(B)
The direct image of A ⊂ Dom f by a function f is
f[A] = f*(A) = (Gr f)*(A) = Im(f|A) = {f(x)|xA} ⊂ Im f
For any f : E → F and BF, the inverse image of B by f, written f*(B), is defined by

f*(B)= (tGr f)*(B) = {xE|f(x) ∈ B}=
yB
f(y)
f(y)= (Gr f)(y) = f*({y}) = {xE|f(x) = y}

 f*(∁F B) = ∁Ef*(B)

For any family (Bi)iI of subsets of F, f*(iI Bi)=iI f*(Bi) where intersections are respectively interpreted as subsets of F and E.

2.4. Uniqueness quantifiers, functional graphs

For all sets FE, all unary predicate A definite on E, and all xE,

xF ⇔ {x} ⊂ F ⇔ (∃yE, x=yyF) ⇔ (∀yE, x=yyF)
xF ⇒ ((∀yF, A(y))⇒A(x)⇒∃yF, A(y))
F ⊂ {x} ⇔ (∀yF, x=y) ⇒ ((∃yF, A(y))⇒A(x)⇒(∀yF, A(y)))
F={x} ⇔ (xF∧∀yF, x=y) ⇔ (∀yE, yFx=y)

Here are 3 new quantifiers: ∃2 (plurality), ! (uniqueness), and ∃! (existence and uniqueness), whose results when applied to A in E only depend on F={xE | A(x)} (like ∃ and unlike ∀) :
(∃xE, A(x)) ⇔ (F ≠ ∅) ⇔ (∃xF, 1) ⇔ (∃xE, {x} ⊂ F)
(∃2xE, A(x)) ⇔ (∃2: F) ⇔ (∃x,yF, xy) ⇔ (∃x,yE, A(x)∧A(y)∧xy)
(!xE, A(x)) ⇔ (!:F) ⇔ ¬(∃2: F) ⇔ (∀x,yF, x=y) ⇔ ∀xF, F ⊂ {x}
(∃!xE, A(x)) ⇔ (∃!: F) ⇔ (∃xF, F ⊂ {x}) ⇔ (∃xE, F={x})
F ⊂ {x} ⇒∀yF, F ⊂ {y} ⇔ (!:F)
(∃!:F) ⇔ (F ≠ ∅∧!: F)
F ≠ ∅ ⇒ ((∀yF, B(y)) ⇒ (∃yF, B(y)))
( !: F) ⇒ ((∃yF, B(y)) ⇒ (∀yF, B(y)))
F={x} ⇒ ((∃yF, B(y)) ⇔ B(x) ⇔ ∀yF, B(y))

A function f is said constant when !:Imf. The constancy of a tuple is the chain of equalities:
x=y=z ⇔ !:{x,y,z} ⇔ ((x=y)∧(y=z))⇒x=z

Translating operators into predicates

In a generic theory, any functor symbol T can be replaced by a binary predicate symbol  R  (where x R y ⇔ (y=T(x))) with the axiom ∀x,∃!y, x R y, replacing any formula A(T(x)) (where x is a term) by (∃y, xRyA(y)), or by (∀y, xRyA(y)) (while terms cannot be translated). This way, any predicate R such that ∀x,∃! y, x R y implicitly defines an operator symbol T. We can extend this to other arities by replacing x by a tuple.
But the use of open quantifiers in this construction makes it unacceptable in our set theory. Instead, let us introduce a new operator ϵ on the class (Set(E)∧∃!:E) of singletons, giving their element according to the axiom (∀x) ϵ{x}=x, or equivalently (Set E∧ ∃!:E) ⇒ ϵEE. Then for every unary predicate A and every singleton E, AE) ⇔ (∃xE, A(x)) ⇔ (∀xE, A(x)).

Conditional operator

Like the conditional connective, it chooses between two objects x,y depending on the boolean B:

(B? x:y) = (y,x)B = ϵ{z∈{x,y}|B ? z=x : z=y}

so that for any predicate A we have A(B? x:y) ⇔ (B? A(x):A(y)). All para-operators other than connectives but with at least a Boolean argument, are naturally expressed as composed of the conditional operator with operators, or the conditional connective with predicates, which is why they did not need an explicit presence in the language of a theory.

Functional graphs

A graph R is said functional if ∀x ∈ Dom R, !: R(x), or equivalently ∀x,yR, x0=y0x1=y1. This is the condition for it to be the graph of a function. Namely, R = GrR) where
ϵR = ((Dom R) ∋ x ↦ ϵ(R(x)))

2.5. The powerset axiom

Let us extend set theory by 3 new symbols (powerset, exponentiation, product) with axioms, that will declare given classes C to be sets K. These extensions are similar to those provided by the set generation principle (1.11), but no more satisfy its requirement.
In the traditional ZF formalization of set theory only accepting ∈ as primitive stucture, such a declaration is done purely by the axiom (or theorem) (∀ parameters), ∃K, ∀x, xK ⇔ C(x). Then, the operator symbol K taking the parameters of C as its arguments, represents the following abbreviations: ∀xK means ∀x, C(x)⇒ ; the equality X=K means (∀x, xX ⇔ C(x)), and any other A(K) means ∃X, (X=K)∧A(X). But these formulas use open quantifiers, forbidden in our framework.
For what the set generation principle justified, ∀C could be replaced by formulas, while the above ∃X could be treated by existential elimination (1.9). But otherwise without open quantifiers, even a given set K identical to a class C, would not be recognizable as such, so that the very claim that C coincides with a set remains practically meaningless.
Thus, our set theoretical framework requires the operator symbol K to be regarded as primitive in the language (instead of a defined abbreviation), with argument the tuple y of parameters of C, and the axiom
(∀y…), Set(K(y))∧(∀x, xK(y) ⇔ Cy(x))

Powerset. Set E, Set(℘(E)) ∧ (∀F, F∈℘(E) ⇔ (Set(F) ∧ FE)).
We shall also shorten ∈ ℘ into ⊂ in binders: (∀AE,…) ⇔ (∀A∈℘(E),…).

Exponentiation.Set E,F, Set(FE)∧(∀f, fFE ⇔ f : EF).

Product of a family of sets. This binder generalizes the finite product operators (2.3):

x, x
iI
Ei ⇔ (Fnc(x) ∧ Dom x = I ∧ ∀iI, xiEi).
For all iI, the i-th projection is the function πi from ∏jI Ej to Ei evaluating every family x at i : πi(x)=xi. This is the function evaluator curried in the unnatural order.
These operators are «equivalent» in the sense that they are definable from each other:

℘(E)={f(1) | fV2E}
FE= ∏xE F = {(ϵ R(x))xE | RE×F ∧∀xE, ∃!: R(x)}
  {x(
iI
 Ei)I|∀iI, xiEi} = {(ϵ R(i))iI | R
iI
Ei ∧∀xE, ∃!: R(x)}
Even some cases are expressible from previous tools:

F{a}= {{a}∋xy | yF}
 F= {∅}
℘({a}) = {∅,{a}}
   ∏
iIJ
Ei={(iI ? xi : yi)iIJ | (x,y) ∈
iI
Ei×
iJ
Ei}
(∃iI, Ei=∅) ⇒
iI
Ei =∅ 
(∀iI, ∃!:Ei) ⇒
iI
Ei = {(ϵEi)iI}

If FF′ then ℘(F) ⊂ ℘(F′), FEFE, and (∀iI, EiEi) ⇒ ∏iI Ei ⊂ ∏iI Ei .

Cantor Theorem. Set E, ∀Fnc f, Dom f = E ⇒ ℘(E) ⊄ Im f.
Proof: F = {xE| xf(x)} ⇒ (∀xE, xFxf(x)) ⇒ (∀xE, Ff(x)) ⇒ FIm f.∎
(The Russell paradox may be seen as a particular case)

2.6. Injectivity and inversion

A function f : EF is injective (or : an injection ) if tGr f is a functional graph:

Inj f
⇔ (∀yF,!:f(y))

⇔ (∀x,x′∈E, f(x)=f(x′) ⇒ x=x′)

⇔ (∀x,x′∈E, xx′ ⇒ f(x) ≠ f(x′))
Then its inverse is defined by f−1f=(Imfy ↦ ϵf(y)) so that Gr(f−1)=tGr f.
A function f : E → F is said bijective (or a bijection) from E onto F, and we write f : EF, if it is injective and surjective: ∀yF, ∃!: f(y), in which case f−1: FE.
A permutation (or transformation) of a set E is a bijection f : EE.

Proposition. Let f:E → F and g:F → G.
1. (Inj f ∧ Inj g) ⇒ Inj(gf)
2. Inj(gf) ⇒ Inj f
3. Im(gf) = g[Im f] ⊂ Img.
4. Im(gf) = G ⇒ Img=G.
5. Im f = F ⇒ Im(gf) = Im g, so that ((f:EF)∧(g:FG)) ⇒ (gf:EG)

Proofs:
1. (Inj f ∧ Inj g)⇒∀x,yE, g(f(x))=g(f(y)) ⇒ f(x)=f(y) ⇒ x=y.
2. ∀x,yE, f(x)=f(y) ⇒ g(f(x)) = (g(f(y)) ⇒ x=y.
3. ∀zG, z ∈ Im(gf) ⇔ (∃xE, g(f(x))=z) ⇔ (∃y ∈ Imf, g(y)=z) ⇔ zg[Imf].
3.⇒ 4. and 3.⇒5. are obvious.∎
Proposition. For any sets E,F,G and any fFE,
Im f=F ⇒ Inj(GFggf) ⇒ (Im f = F∨ !:G)
(Inj fG ≠ ∅) ⇒{gf| gGF}=GE ⇒(Inj f∨ !: G)
(EFG ≠ ∅) ⇒{g|E|gGF}=GE
(Inj fE ≠ ∅) ⇒∃gEF, gf=IdE
Proofs :
Imf=F⇒∀g,hGF, ((∀xE, g(f(x)) = h(f(x))) ⇔ (∀yF, g(y)=h(y) ⇔ g=h)).
z,z′∈G, (yz)০f = (y ↦ (y ∈ Imf ? z : z′))০f ∴ (Inj(ggf) ⇒ (z=z′∨Imf=F))
zG,∀hGE, Injf ⇒ (Fy ↦ (y ∈ Imf? hf−1(y):z))০f=h.
z,z′ ∈ G,∀xE, if gGF is such that ∀yE,g(f(y)) = (y=x ? z : z′), then
yE, f(y)=f(x) ⇒ g(f(y)) = g(f(x)) = z ⇒ (y=xz=z′).
The last formulas are particular cases of the second one.∎

Let f:E →  F and f*F: ℘(F) →  ℘(E) defined by f*. Then (by G=V2 and ∀BImf, f[f*(B)]=B),

Inj f ⇔ Im f*F = ℘(E)
Im f = F⇔Inj f*F
Im f*={f[A]|AE}=℘(Im f)

Proposition. Let F=Dom g. Then Inj gInj(FEfgf) ⇒ (Inj gE=∅).

Proofs: ∀f,f′ ∈ FE, (Inj g∧∀xE, g(f(x))=g(f′(x))) ⇒ (∀xE,f(x)=f′(x)).
Then from the middle formula, ∀y,zF,
g(y)=g(z) ⇒ g০(Exy) = g০(Exz) ⇒ (∀xE, y=z) ⇒ (y=zE = ∅).∎

Proposition. Let f: E → F and Dom g=F. Then
gf = IdE ⇔ (∀xE, ∀yF, f(x)=yg(y)=x)

⇔ (Gr ftGr g) ⇔ (∀yF, f(y)⊂{g(y)})

⇔ (∀xE, f(x)∈g(x)) ⇔(Inj fg|Imf=f−1)

E ⊂ Im g
(g:FEgf= IdE) ⇒ (Im f = F ⇔ Inj g ⇔ fg = IdF ⇔ g=f−1).
Proof of the last formula: (Inj ggfg = gIdF) ⇒ fg=IdF. ∎

Proposition. 1) If f,g are injective and Im f = Dom g, then (gf)−1= f−1g−1.
2) If
f,h : E → F and g : F →E then (gf= IdEhg = IdF) ⇔ ((g:FE)∧f=h=g−1).

Proofs:
1) ∀x ∈ Dom f, ∀y ∈ Im g, (gf)(x)=y ⇔ f(x)=g−1(y) ⇔ x = (f−1g−1)(y).
Other method: (gf)−1= (gf)−1gg−1= (gf)−1gff−1g−1 = f−1g−1.
2) We deduce f=h from f = hgf = h, or from Gr ftGr g ⊂ Gr h. The rest is obvious.∎

2.7. Binary relations, ordered sets

A binary relation on E is a graph RE×E. Denoting x R y ⇔ (x,y) ∈ R and letting the domain E of quantifiers implicit, it will be said
reflexive  ⇔   ∀xx R x
irreflexive  ⇔   ∀x, ¬(x R x)
symmetric  ⇔   RtRR = tRR =R
antisymmetric  ⇔   ∀x,y, (x R yy R x)⇒x=y
transitive  ⇔   ∀x,y,z, (x R yy R z)⇒x R z

For any transitive binary relation R we denote x R y R z ⇔ ((x R y)∧(y R z))⇒x R z.
Example. Let AEE and R=fA Gr f. Then
(IdEA) ⇒ R is reflexive
(∀f,gA, gfA) ⇒ R is transitive
(∀fA, f:EEf−1A) ⇒ R is symmetric

Preorder. A preorder R on a set E is a reflexive and transitive binary relation on E. Equivalently,
x,yEx R y ⇔R(x) ⊂R(y)
Proof: ∀x,yExR(x) ⊂ R(y) ⇒ x R y ;
transitivity says x R yR(x) ⊂R(y). ∎

Then tR is also a preorder: x R yR(y) ⊂ R(x).

Ordered set. An order is an antisymmetric preorder. A preordered set is a set E with a chosen preorder R. An ordered set is a set with an order, usually written as .

For x,y in an ordered set E, the formula xy can be read «x is less than y», or «y is greater than x». The elements x and y are said incomparable when ¬(xyyx). (This implies xy).

Any subset F of a set E with an order (resp. a preorder) RE×E, is also ordered (resp. preordered) by its restriction R∩(F×F) (which is an order, resp. preorder, on F).

Strict order. It is a binary relation both transitive and irreflexive; and thus also antisymmetric.

Strict orders < bijectively correspond to orders ≤ by
x < y ⇔ (xyxy).
The inverse correspondence is defined by xy ⇔ (x < yx = y).

Total order. A total order on a set E is an order R on E without any pair of incomparable elements : x,yE, xyyx, i.e. RtR = E×E.

Equivalent definitions:
A strict order associated with a total order, called a strict total order, is any transitive relation < on E such that
x,yE, x < y ⇎ (y < xx=y)
or equivalently ∀x,yE, x=y ⇎ (y < xx < y)).

Monotone, antitone, strictly monotone functions

Between ordered sets E and F, a function f : EF will be said :
Any composite of a chain of monotone or antitone functions, is monotone if the number of antitone functions in the chain is even, or antitone if it is odd. Any strictly monotone or strictly antitone function is injective. If fFE and gEF are both monotone (resp. both antitone) and gf=IdE, then f is strictly monotone (resp. strictly antitone).

Order on sets of functions

For all sets E, F where F is ordered, the set FE (and thus any subset of FE) is ordered by

fg ⇔ (∀xE, f(x) ≤ g(x))

Then, ∀f,gFE, ∀hEG, fgfhgh, i.e. ffh is always monotone.
The particular case F=V2 is that ℘(E) (and thus any set of sets) is naturally ordered by ⊂ , and that h* is monotone from ℘(E) to ℘(G).
If F and G are ordered and uGF is monotone (resp. antitone) then FEfufGE is monotone (resp. antitone).
In an ordered set E, a function fEE is said extensive if
xE, xf(x)
i.e. IdEf. The composite of two extensive functions is extensive.

2.8. Canonical bijections

For all objects x,y we shall say that x determines y if there is an invariant functor T such that T(x) = y. Then the role of y as free variable can be played by the term T(x), thus by the use of x. This is a meta-preorder on the universe, but not a predicate of set theory as it involves a meta-concept. Rather, it is meant to abbreviate the use of T.
Similarly, a function f : EF will be said canonical if it is defined as Ex → T(x) for some invariant functor T. A bijection f will be said bicanonical if both f and f−1 are canonical. When a bijection f : E ↔  F is canonical (resp. bicanonical), we write f : EF (resp. f : EF); or, with its defining functor, T : EF which means that (ExT(x)) is injective with image F. We shall write EF (resp. EF) to mean the existence of a canonical (resp. bicanonical) bijection, that is kept implicit.
Canonical bijections can fail to be bicanonical especially when their defining functor is not injective:
V
2E ≅ ℘(E), {x}E ≅ {x} and E×{x} ≅ E, whereas {xEE{x} and E ≡ {0}×E.
This is a meta-preorder on the class of sets, preserved by constructions: for example if EE′ and FF′ then E×FE′×F′ and FEFE using the direct image of the graph (while we may not have FEFE when E′ does not determine E). It will often look like a property of numbers as the existence of a bijection between finite sets implies the equality of their numbers of elements.
The transposition of oriented pairs (E×FF×E) extends to graphs (℘(E×F) ≡ ℘(F×E)) and to operations: GE×FGF×E where fGE×F is transposed by tf(x,y)=f(y,x).

Sums of sets, sums of functions

If S=∐iI Ei then ∐: ∏iI ℘(Ei) ≅ ℘(S), whose inverse SRRI = (IiR(i)) depends on I. In particular for two sets E and F we have (℘(F))E ≅ ℘(E×F).
The sum over I of functions fi where ∀iI, Ei = Domfi is defined by
iI fi = (S ∋ (i,x) ↦ fi(x))
f=∐iI fi⇔ (Dom f=S∧∀iI, fi= f(i)=fji)    where ji=(Eix ↦ (i,x))
Thus the canonical bijections (bicanonical if I= Dom S, thus if E ≠ ∅ in the case I×E)


iI
FiEFS
(FE)IFI×E

iI
 
xEi
F(i,x)
cS
Fc
  (E×FGE×F×G
(fi)iI ∈ (FE)I⇒ 
iI
Gr fi ⊂ ℘(I×(E×F)) ≡ ℘((I×EF) ⊃ Gr
iI
fi

Product of functions or recurrying

Transposing a relation R exchanges its curried forms R andR, by a bijection (℘(F))E  ↔  (℘(E))F with parameter F. Similarly we have a bijection (FE)I ↔ (FI)E, canonical if I ≠ ∅ (to let (FE)I determine E), defined by a binder ∏ called the product of the functions fiFE for iI:

(fi)iI
iI
FiE ≅ (
iI
Fi)E
iI
fi = (Ex ↦ (fi(x))iI)
  ∀g, g =
iI
fi  ⇔ (g : E →
iI
Im fi ∧∀iI, fi = πig)
Dom f = Dom g = Ef×g = (Ex ↦ (f(x),g(x)))
 IE×FE ≡ (I×F)E

ϕ∈IE
 
xE
Fϕ(x) (
iI
Fi)E.

2.9. Equivalence relations and partitions

Indexed partitions

A family of sets (Ai)iI is called pairwise disjoint when any pair of them is disjoint : ∀i,jI, ijAiAj=∅
Equivalently, (∀(i,x),(j,y) ∈ ∐kI Ak, x=yi=j), thus ∃f, Grf = tiI Ai with
Dom f = Im ∐iI Ai = ⋃iIAi
Im f ={iI| Ai ≠ ∅}
Inversely, any fFE defines a family fF = (f(y))yF ∈ ℘(E)F of pairwise disjoint sets :
y,zF, f(y)⋂f(z) ≠ ∅⇒∃xf(y)⋂f(z), y=f(x)=z
An indexed partition of a set E is a family of nonempty, pairwise disjoint subsets of E, whose union is E. It is always injective :
i,jI, Ai = AjAiAj=Ai≠∅ ⇒ i=j.

Equivalence relation defined by a function

An equivalence relation is a symmetric preorder. Any f : E → F defines an equivalence relation on E by
f ={(x,y) ∈ E| f(x)=f(y)}=∐(ff)
Its composite g = hf with any hGF satisfies ∼f ⊂ ∼g, with
f  = ∼g ⇔ Inj h|Imff= (h|Imf)−1g
In particular, ∼f coincides with the equality relation Gr IdE on E when f is injective. As  f = ff, the injectivity of the indexed partition fImf (that we will abusively denote as f) gives the characteristic identity of equivalence relations : xf y ⇔ f(x)= f(y).
If F = Im f, the injection (2.6) GFhhf has image {gGE | ∼f ⊂ ∼g}: letting H=Im(f×g),
f ⊂  ∼g ⇔ ∀(y,z), (y′,z′) ∈ H, y=y′⇒ z=z
Dom H = F
hGF, g=hf ⇔ HGr h.
For any functions f,g such that Dom f = Dom g∧ ∼f ⊂ ∼g, the function with graph Im(f×g) is called the quotient g/f: ImfImg, and is the only function h such that
Dom
h = Im fg = hf.
Inversion comes as a particular case: Inj ff−1 = IdDomf/f.

Remark. if R is reflexive and x,y,z, (x R yz R y)⇒z R x then R is an equivalence relation.
Proof : symmetry is verified as: ∀x,y, (x R yy R y)⇒y R x. Then comes transitivity.∎

Partition, canonical surjection

A partition of E is a set of nonempty, pairwise disjoint sets whose union is E, thus the image of any indexed partition f of E (where f is any function with domain E): P=Imf=Im(ff).
RE×E, ∀P ⊂ ℘(E), if P = Im RE then
(∀x,yE, xR(y) ⇔ R(x)=R(y)) ⇔ (∀xE, ∀AP, xAR(x)=A) ⇔ IdP=(RE)
Thus if R is an equivalence relation then P is a partition.
Conversely for any partition P of E, ∃! gPE, IdP=g thus P=Domg=Img and
R=∐gE×E⇒ IdP= (RE)
thus R is an equivalence relation, where
x R y ⇔ (∃AP, xAyA) ⇔ (∀AP, xAyA).
The partition Im R associated with an equivalence relation R on E is called the quotient of E by R and denoted E/R; the function R is the canonical surjection from E to E/R. For all xE, R(x) is the only element of E/R containing x, and called the class of x by R.

Order quotient of a preorder

Any preordered set (E,R) is reflected through R by the ordered set (Im R, ⊂ ), with

R(x) = R(y) ⇔ (R(x) ⊂R(y)∧R(y) ⊂R(x)) ⇔ (xRyyRx)

so that R is injective if and only if R is an order. Through R, the preorder R is reduced to the order relation ⊂ in Im R, which plays the role of the quotient of R in the quotient set E/(RtR).
On each (ordered) set E, only one order will usually be considered, denoted ≤E, or abusively ≤ . This may be justified by defining ordered sets as sets of sets, ordered by ⊂ , ignoring their elements.

2.10. Axiom of choice

The axiom of choice is a claim with several equivalent formulations, named as an «axiom» because it cannot be deduced from other axioms of set theory but it «feels true» and, when taken as an axiom, it does not increase the risk of contradictions but has convenient consequences. But we will actually not need it in the rest of this work.

Axiom of choice (AC). It says SetX, ACX, where ACX names the following equivalent claims
(1) ∀SetE,∀RX×E, (∀xX, ∃yE, xRy) ⇒ (∃fEX, ∀xX, xRf(x)).
Or in short : for any graph R
, X = Dom R ⇒ ∃f ∈ (Im R)X, Gr fR.
(2) Any product over X of nonempty sets is nonempty : (∀xX, Ax ≠ ∅) ⇒ ∏xX Ax ≠ ∅.
(3) ∀Fnc g, Im g = X ⇒ ∃f ∈ (Dom g)X, gf=IdX.

Proof of equivalence :
(1)⇒(2) by R = ∐xX Ax ;
(2)⇒(3) by Ax=g(x) ;
(3)⇒(1) Im π0|R = DomR = X ⇒ ∃(h×f) ∈ RX, h=IdX ∧Gr fR. ∎
(We also have (2)⇒(1) by Ax = R(x), and (1)⇒(3) by R = tGr g)

Finite choice theorem. If X is finite then ACX.

A rigorous proof for the general case will need a formal definition of finiteness. Now let us only give a schema of proofs, one for each explicit number of elements of X, using expression (2): for example with 3 elements, for each triple of sets (A,B,C),
(A≠∅∧B≠∅∧C≠∅) ⇒ (∃xA, ∃yB, ∃zC, (x,y,z)∈A×B×C) ⇒ A×B×C ≠ ∅.
The general case might be written (∀i<n, Ai ≠ ∅) ⇒ (∃u0A0,..., ∃un-1An-1, (u0,...,un-1)∈ ∏i<n Ai) ⇒ ∏i<n Ai ≠ ∅. ∎

The different claims ACX are related by the following implications:

The proofs are easy and left as an exercise to the reader.

Theorem. The following claims are equivalent to the axiom of choice:
(4) Any set E of nonempty sets has a choice function: ∅ ∉ E ⇒ ∏AE A ≠ ∅.
(5) For any partition P of a set E, ∃KE, ∀AP, ∃! : KA
(6) For any sets E,F,G and any g: FG, {gf | fFE}=GE.

Proofs:
(2)⇒(4) is obvious ;
(4)⇒(5) (x∈∏AP AK = Im x) ⇒ (KE ∧∀AP, xAA ∧ ∀BP, xBABA=B)
(5)⇒(3) Let P = Im g. Then f = (Xx ↦ ϵ(Kg(x))) = g|K−1gf = IdX.
(ACE 1)⇒(6) ∀hGE, (∀xE, ∃yF, g(y)=h(x)) ⇒ (∃fFE, ∀xE, g(f(x))=h(x))
(ACG 3)⇒(6) : ∃iFG, gi=IdG ∧ ∀hGE, ihFEgih=h.
(6)⇒(3) : E=GIdE ∈ {gf | fFE}. ∎

Remarks:

2.11. Notion of Galois connection

The set of fixed points of a function f is written

Fix f ={x∈Dom f | f(x)=x} ⊂ Im f
Then,
Im f ⊂ Fix g ⇔ ((Im f ⊂ Dom g)∧(gf=f))
Im f= Fix f ⇔ ((Im f ⊂ Dom f)∧(ff=f)) : such a function f is called idempotent.

Definition. For any ordered sets E, F, denoting F the set F with the transposed order, the sets of (antitone) Galois connections between E and F, and monotone Galois connections from E to F, are defined by
Gal(E,F) = {(⊥,⊤) ∈ FE×EF|∀xE, ∀yF, xE⊤(y) ⇔ yF ⊥(x)} = tGal(F,E)
Gal+(E,F) = {(u,v) ∈ FE×EF|∀xE, ∀yF, xE v(y) ⇔ u(x) ≤F y} = Gal(E,F)

Fundamental example. Any relation RX×Y defines a (⊥, ⊤) ∈ Gal(℘(X),℘(Y)) by
AX, ⊥(A) ={yY |∀xA, x R y}= xAR(x)
BY, ⊤(B) ={xX |∀yB, x R y}={xX | BR(x)}
Then, ⊥(∅)=Y and ⊤(∅)=X

Proof :
AX, ∀BFA ⊂ ⊤(B) ⇔ (∀xA, ∀yB, x R y) ⇔ B ⊂ ⊥(A).∎
This will later be shown to be a bijection : Gal(℘(X),℘(Y)) ≅ ℘(X×Y).

Lemma. ∀⊥ ∈ FE, !⊤ ∈ EF,(⊥,⊤) ∈ Gal(E,F).
Proof: ∀⊤ ∈ EF, (⊥,⊤) ∈ Gal(E,F) ⇔ E০⊤ =⊥*F, but E is injective.∎

Properties. For all (⊥,⊤) ∈ Gal(E,F), the closures Cl =⊤০⊥ ∈ EE and Cl′=⊥০⊤ ∈ FF satisfy
1) Cl and Cl′ are extensive.
2) ⊥ and ⊤ are antitone
3) Cl and Cl′ are monotone
4) ⊥০⊤০⊥ = ⊥, and similarly ⊤০⊥০⊤ = ⊤
5) Im ⊤ = Im Cl = Fix Cl, called the set of closed elements of E
6) Cl০Cl = Cl
7) (⊥ strictly antitone) ⇔ Inj⊥ ⇔ Cl = IdE ⇔ Im⊤ =E
8) ∀x,x′ ∈ E, ⊥(x) ≤ ⊥(x′) ⇔ (Im⊤∩ ≤(x) ⊂ ≤(x′)).
9) Denoting K=Im⊤, ⊤০⊥|K= IdK thus ⊥|K is strictly antitone and ⊥|K−1 = ⊤|Im⊥.

Proofs:
1) ⊥(x) ≤ ⊥(x) ∴ x(⊥(x)).
1) ⇒2) ∀x,yE, xy ≤ ⊤(⊥(y))⇒⊥(y) ≤ ⊥(x).
1)∧2) ⇒4) IdE ≤ Cl ⇒⊥০Cl ≤ ⊥ ≤ Cl′০⊥ = ⊥০⊤০⊥.
4)⇒5) Cl = ⊤০⊥ ∴ Im Cl ⊂ Im⊤ ;
Cl০⊤ = ⊤ ∴ Im⊤ ⊂ Fix Cl ⊂ Im Cl.
2)⇒3) and 4)⇒6) are obvious.
7) (Inj⊥∧⊥০Cl =⊥) ⇔ Cl = IdE ⇔ (Im⊤ =E∧Cl০⊤ = ⊤);
Cl = IdE ⇒ ⊥ strictly antitone ⇒ Inj ⊥.
8) ⊥(x) ≤ ⊥(x′) ⇔ (∀yF, x≤⊤(y) ⇒ x′≤ ⊤(y)).
9) K= Fix(⊤০⊥) ⇒ ⊤০⊥০IdK=IdK.
Other proof : (⊥|K,⊤) ∈ Gal(K,F) with ⊤ surjective.
In ⊤|Im⊥০⊥|K=IdK the roles of ⊤ and ⊥ are symmetrical. ∎

Remark. Properties 1) and 2) conversely imply that (⊥,⊤) ∈ Gal(E,F).
Proof: ∀xE, ∀yF, x ≤ ⊤(y) ⇒ y ≤ ⊥(⊤(y)) ≤ ⊥(x).∎
Analogues of the above properties for monotone Galois connections are obtained by reversing the order in F: if (u,v) ∈ Gal+(E,F) then u and v are monotone, vu is extensive and uv ≤ IdF.

Closure. A closure of an ordered set E is an fEE such that, equivalently:
1) There exists a set F and an (u,v) ∈ Gal(E,F) or Gal+(E,F) such that vu=f
2) f is monotone, idempotent and extensive
3) ∀xE,∀y∈ Im f, xyf(x) ≤ y, i.e. (f, IdK) ∈ Gal+(E,K) where K=Im f

Proof of equivalence:

3)⇒1) ⇒2);
for 2) ⇒3), ∀xE,∀yK, xf(x) ≤ yxyf(x) ≤ f(y) = y. ∎

Notes:

To go further on Galois connections