2.6. Graphs

A graph is a set of ordered pairs. Let us denote the class of graphs as gr:

gr R ⇔ (Set R ∧ ∀x∈R, Fnc x ∧ Dom x = V2).

For any binder Q and any graph G, the formula Qz∈G, A(z0,z1) that binds the variable z = (z0, z1) on a binary structure A definite on G, can be seen as binding 2 variables z0, z1 on A(z0, z1), and thus be denoted with a pair of variables: Q(x,y)∈G, A(x,y).

The transpose of an ordered pair is

t(x,y) = (y,x)

The transpose of a graph R is the image of transposition over it:

tR = {(y,x)|(x,y) ∈ R}

We define the domain and the image of a graph as the respective images of π0 and π1 over it:

Dom R = {x|(x,y) ∈ R}
Im R = {y|(x,y) ∈ R} = Dom tR

Currying notation

Graphs R can be expressed in curried forms as functors R⃗ and R⃖:

∀x,  R⃗(x) = {y | (z,y)∈R ∧ z=x}.
∀y,  R⃖(y) = {x | (x,z)∈R ∧ z=y} = tR⃗ (y).
∀x,y,   y ∈ R⃗ (x) ⇔ (x,y) ∈ R ⇔ x ∈ R⃖ (y)
∀x,  x ∈ Dom R ⇔ R⃗ (x) ≠ ∅
Dom R ⊂ E ⇒ Im R = ⋃x∈E R⃗(x) ∧ ∀y, R⃖(y) = {x∈E | (x,y) ∈ R}

They can also appear as functions

R⃗E = (E∋x ↦ R⃗(x))
R⃖F = (F∋y ↦ R⃖(y))
(R⃗) = R⃗Dom R
(R⃖) = R⃖Im R.

Functional graphs

The graph of a function f is defined by

Gr f = {(x,f(x)) | x ∈ Dom f}
∀x,y, (x,y) ∈ Gr f ⇔ (x ∈ Dom f ∧ y = f(x))
Dom f = Dom Gr f
Im f = Im Gr f

For any function f and any graph R,

Gr f ⊂ R ⇔ ∀x∈Dom f, f(x) ∈ R⃗(x)
R ⊂ Gr f
 ⇔ (Dom R ⊂ Dom f ∧ ∀(x,y)∈R, y = f(x))
R = Gr f
 ⇔ (Dom R ⊂ Dom f ∧ ∀x∈Dom f, R⃗(x) = {f(x)} )

A graph R is functional if it is the graph of a function. This condition is equivalently written in either way

∀x∈ Dom R, !: R⃗(x)
∀x,y∈R, x0 = y0 ⇒ x1 = y1.

It is then the graph of the unique function ℩R⃗ = ((Dom R) ∋ x ↦ ℩(R⃗(x))).

For any set E we shall denote 𝛿E = Gr IdE.

Indexed partitions

Two sets E and F are called disjoint when E∩F = ∅, or equivalently ∀x∈E, x∉F.
A family of sets (Ai)i∈I is called pairwise disjoint when ∀i≠j∈I, Ai∩Aj = ∅
For any graph R with Im R ⊂ F, the family (R⃖(y))y∈F is pairwise disjoint if and only if R is functional:

(∀y≠z∈F, ¬∃x∈R⃖(y), x ∈ R⃖(z)) ⇔ (∀(x,y)∈R, ∀z∈F, xRz ⇒ y = z)

For any function f and any y we define the fiber of y under f as

f•(y) = {x∈Dom f | f(x) = y} = (Gr⃖ f)(y)

When f : E → F this defines a family f•F = (f•(y))y∈F of pairwise disjoint subsets of E:

∀y,z∈F, f•(y) ∩ f•(z) ≠ ∅ ⇒ ∃x∈ f•(y) ∩ f•(z), y = f(x) = z
⋃y∈F f•(y) = E
Im f = {y∈F | f•(y) ≠ ∅}.

An indexed partition of a set E is a family of nonempty, pairwise disjoint subsets of E, whose union is E.
In other words it is any family of the form f• = f•Im f for any function f with domain E.

Sum or disjoint union

The binder ∐ of sum of any family of sets (Ei)i∈I, gives a graph ∐i∈I Ei defined as
∐
i∈I Ei = ⋃
i∈I {(i,x) | x∈Ei}
∀i,x, (i,x) ∈ ∐
i∈I Ei ⇔ (i∈I ∧ x∈Ei)
(∀(i,x)∈∐
i∈I Ei, A(i,x)) ⇔ (∀i∈I, ∀x∈Ei, A(i,x))
(∀i∈I, Ei ⊂ E′i) ⇔ ∐i∈I Ei ⊂ ∐i∈I E′i
E0⊔…⊔En−1 = ∐i∈Vn Ei
This binder serves as inverse of currying : R = ∐i∈I Ei ⇔ (Dom R ⊂ I ∧ ∀i∈I, R⃗(i) = Ei).
It is also called disjoint union as the family of copies {(i,x) | x∈Ei} of each Ei is pairwise disjoint, with the function from R to I given by π0.

Direct and inverse images by a graph

The restriction of a graph R to a set A is defined as

R|A = {(x,y)∈R | x∈A} = ∐x∈A R⃗(x)

The direct image of a set A by a graph R is
R⋆(A) = Im R|A = ⋃x∈A R⃗(x) = {y |(x,y)∈R∧x∈A} ⊂ Im R.
Dom R ⊂ A ⇔ R|A = R ⇒ R⋆(A) = Im R
R⋆(⋃
i ∈ I Ai) = ⋃
i ∈ I R⋆(Ai)
R⋆(⋂
i ∈ I Ai) ⊂ ⋂
i ∈ I R⋆(Ai)

A ⊂ B ⇒ R⋆(A) ⊂ R⋆(B)
Similarly, the inverse image or preimage of a set B by a graph R is

R⋆(B) = tR⋆(B) = ⋃y∈B R⃖(y) = {x | (x,y)∈R∧ y ∈ B} ⊂ Dom R.

Direct image and preimage by a function

The direct image of a subset A ⊂ Dom f by a function f, denoted f[A] or f⋆(A), is
f[A] = (Gr f)⋆(A) = {f(x) | x∈A} ⊂ Im f
For any f : E → F and B ⊂ F, the preimage of B by f, written f⋆(B), is defined by

f⋆(B) = (Gr f)⋆(B) = {x∈E | f(x) ∈ B} = ⋃
y∈B f•(y)
f•(y) = f⋆({y})

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

For any family (Bi)i ∈ I of subsets of F, f⋆(⋂i∈I Bi) = ⋂i∈I f⋆(Bi) where intersections are respectively interpreted as subsets of F and E.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. Formalization of set theory
2.2. Set generation principle
2.3. Tuples
2.4. Uniqueness quantifiers
2.5. Families, Boolean operators on sets⇦
2.6. Graphs
⇨ 2.7. Products and powerset 		2.8. Injections, bijections
2.9. Properties of binary relations
2.10. Axiom of choice
2.A. Time in set theory
2.B. Interpretation of classes
2.C. Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 2.6. Graphes