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

Formalization of operations and currying

The notion of n-ary operation, objects acting as n-ary operators between n sets, would be formalized by: 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 ≈ (Ex ↦ (Fyt(x,y))) = g
f
(x,y) = g(x)(y) = t(x,y)

The intermediate function g(x) = (Fyt(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 = (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 x = π00(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... » (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 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.

As we described the content of a theory, a "list" basically means a family. But more precisely:

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:

(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 any set E that includes their union U = ⋃iI FiE. 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))

Quantifiers Q(x,y)∈E×E will be written Qx,yE, and those with domain {(x,y)∈E×E | xy} will be written QxyE.
Thus ∀xyE,... means ∀x,yE, xy⇒..., that is ∀xE,∀yE, xy⇒...
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)) ⇔ ((CE≠∅) ∨ ∃xE, A(x))
(∀xE, CA(x)) ⇔ ((CE=∅) ∧ ∀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∈∐iI Ei, 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 Im f ⊂ Dom g (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 A ⊂ Dom f is f|A = (Axf(x)) = f০IdA.
The graph of a function f is defined by

Gr f = {(x,f(x)) | x ∈ Dom f} = ∐x∈Dom f {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(Gr f), Im f = Im(Gr f) and Gr(f|A) = (Gr f)|A):

Dom R = {x|(x,y) ∈ R} = Im tR
xx ∈ Dom RR (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 or preimage 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) ⇔ (∃xyE, A(x) ∧ A(y))
(!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 !: Im f. 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 = Gr(ϵR) where
ϵR = ((Dom R) ∋ x ↦ ϵ(R(x)))

2.5. The powerset

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 statement 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's Theorem. Set E, ∀Fnc f, Dom f = E ⇒ ℘(E) ⊄ Im f.
Proof: F = {xE| xf(x)} ⇒ (∀xE, xFxf(x)) ⇒ (∀xE, Ff(x)) ⇒ FIm f.∎
(Russell's paradox may be seen as a particular case)

2.6. Injectivity and inversion

A function f : EF is called injective (or : an injection ), which we write Inj f or f : EF, if tGr f is a functional graph:

Inj f
(∀yF, !:f(y))
(∀x,x′∈E, f(x)=f(x′) ⇒ x=x′)
(∀xx′∈E, f(x) ≠ f(x′))

Then its inverse is defined by f -1 = ϵf = (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.

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] ⊂ Im g.
4. Im(gf) = G ⇒ Im g = 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 :
Im f = F ⇒ ∀g,hGF, ((∀xE, g(f(x)) = h(f(x))) ⇔ (∀yF, g(y) = h(y) ⇔ g=h)).
z,z′∈G, (yz)০f = (y ↦ (y ∈ Im f ? z : z′))০f ∴ (Inj(ggf) ⇒ (z=z′ ∨ Im f=F))
zG,∀hGE, Inj f ⇒ (Fy ↦ (y ∈ Im f ? hf-1(y):z))০f=h.
z,z′∈G, ∀xE, ∀gGF, gf = (Ey↦ (y=x ? z : z′)) ⇒ ∀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 : EF 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 g ⇒ Inj(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 : EF and g : FE then (gf = IdEhg = IdF) ⇔ ((g:FE) ∧ f=h=g−1).

Proofs:
1) ∀x∈ Dom f, ∀y∈ Im g, (gf)(x)=yf(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  ⇔   ∀xxRx
irreflexive  ⇔   ∀x, ¬(xRx)
symmetric  ⇔   RtRR = tRR =R
antisymmetric  ⇔   ∀x,y, (xRyyRx) ⇒ x=y
transitive  ⇔   ∀x,y,z, (xRyyRz) ⇒ xRz

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 where all elements are comparable : ∀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 IdEf i.e. xE, xf(x).
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 ExT(x) for some invariant functor T. In particular for EF we have the canonical injection IdE : EF, and any set E has a canonical injection to ℘(E) defined by x ↦ {x}.
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.
More generally we shall write Ex F to mean a bijection defined using the parameter x.
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 the sum ∐ defines a canonical bijection ∏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 = Dom fi is defined, using the canonical injections ji = (Eix ↦ (i,x)) by
iI fi = (S ∋ (i,x) ↦ fi(x))
f = ∐iI fi ⇔ (Dom f = S ∧ ∀iI, fi = f(i) = fji)
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, Gr f = 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 : EF 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|Im ff= (h|Im f)−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 fIm f (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 = hfH ⊂ Gr 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: Im f ↠ Im g, and is the only function h such that
Dom h = Im fg = hf.
Inversion comes as a particular case: Inj ff−1 = IdDom f /f.

Remark. If R is reflexive and ∀x,y,z, (xRyzRy) ⇒ zRx then R is an equivalence relation.
Proof : symmetry is verified as: ∀x,y, (xRyyRy) ⇒ yRx. 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 P of any indexed partition f of E (where f is any function with domain E):

P = Im f = 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 = Dom g = Im g and
R=∐gE×E⇒ IdP= (RE)
thus R is an equivalence relation, where
x R y ⇔ (∃AP, xAyA) ⇔ (∀AP, xAyA).
For any equivalence relation R on E, the partition Im R is called the quotient of E by R, written 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.
For any function f such that Dom f = ER ⊂ ∼f, we can also write f/R for the function f / 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 statement 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 statements
(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 different statements ACX are related by the following implications:

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

Theorem. The following statements 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 ggf=f)
Im f = Fix f ⇔ (Im f ⊂ Dom fff=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)

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

Proof : ∀AX, ∀BFA ⊂ ⊤(B) ⇔ A×BRB ⊂ ⊥(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:

More on Galois connections