2.10. Axiom of choice

Properties of curried composition

Proposition. ∀Set E,F,G, ∀f ∈ FE,
  1. Im f = F ⇒ Inj(GF ∋ g ↦ g⚬f)
  2. (Inj(GF ∋ g ↦ g⚬f) ∧ ∃≥2:G) ⇒ Im f = F
  3. (Inj f ∧ G ≠ ∅) ⇒ {g⚬f | g∈GF} = GE
  4. ({g⚬f | g∈GF} = GE ∧ ∃≥2:G) ⇒ Inj f
  5. (E ⊂ F ∧ G ≠ ∅) ⇒ {g|E | g∈GF} = GE
  6. (Inj f ∧ E ≠ ∅) ⇒ ∃g∈EF, g⚬f = IdE
Proofs :
1. done in 2.9 ; simpler proof: ∀g,h∈GF, (∀x∈E, g(f(x)) = h(f(x))) ⇔ (∀y∈F, g(y) = h(y)) ⇔ g=h
2. ( ) ⇒ ∃z≠z′∈G, (F∋y ↦ z)⚬f = (F∋y ↦ (y ∈ Im f ? z : z′))⚬f ∴ (∀y∈F, y ∈ Im f ∨ z = z′) ∴ Im f = F
3. Inj f ⇒ ∀z∈G, ∀h∈GE, h = (F ∋ y ↦ (y ∈ Im f ? h(f -1(y)) : z))⚬f
4. ∀z≠z′∈G, ∀x∈E, ∀g∈GF, g⚬f = (E∋y↦ (y = x ? z : z′)) ⇒ ∀y∈E, f(y) = f(x) ⇒ g(f(y)) = g(f(x)) = z ⇒ y = x.
5. and 6. are particular cases of 3.∎

The case G = V2 gives the following properties of h = (℘(F)∋B↦ f⋆(B)) :

Im f = F ⇔ Inj h
Inj f ⇔ Im h = ℘(E)

Moreover {f[A]|A ⊂ E} = ℘(Im f) because ∀B ⊂ Im f, f[f⋆(B)] = B.

Proposition. For any sets E, F and any function g with domain F,

  1. Inj g ⇒ Inj(FE ∋ f ↦ g⚬f)
  2. (Inj(FE ∋ f ↦ g⚬f) ∧ E ≠ ∅) ⇒ Inj g
  3. ∀SetG, ({g⚬f | f∈FE} = GE ∧ E ≠ ∅) ⇒ Im g = G.
Proofs:
1. ∀f,f'∈FE, (Inj g ∧ ∀x∈E, g(f(x)) = g(f'(x))) ⇒ (∀x∈E, f(x) = f'(x)).
2. ∀y,z∈F, g(y) = g(z) ⇒ g⚬(E ∋ x ↦ y) = g⚬(E ∋ x ↦ z) ⇒ (∀x∈E, y = z) ⇒ (E ≠ ∅ ⇒ y = z).
3. (left as an exercise to the reader).∎

Axiom of choice over a set (ACX)

The axiom of choice (AC) is a statement expressible in any set theory with powerset, which «feels true» and is convenient to accept as an axiom; but we will actually not need it in the rest of this work.

It has several equivalent formulations (in clear, it is the common name of these equivalent statements). The main ones fit the common format (∀SetX, ACX) where ACX means any of the following equivalent formulas with the free variable X in the class of sets:

(AC3X) and (AC4X) are more often used in cases of equality (respectively X = Im g and X = Dom R) which are equivalent to the general cases, as the proofs of equivalence work the same : Other easy deductions are

Dependencies between diverse ACX

A big achievement of mathematical logic was to prove the independence of AC from the rest of set theory: even the very strong ZF system, if consistent, can neither prove nor refute it, as each universe where AC is true includes another one where it is false, and vice versa. This will be further commented in 5.5 (without the details of the proofs which are much too difficult).
The diverse ways in which AC may fail in different universes, can be partly sorted out by specifying for which X does ACX hold. The different ACX depend on each other as follows: The proofs of these implications are easy and left as an exercise to the reader.

Finite choice theorem. If X is finite then ACX.

This will be easily deducible from the case of singletons AC{x} (which is trivial) and the preservation by binary union (ACX ∧ ACY) ⇒ ACX∪Y once finiteness will be formalized (4.6).
Now let us just suggest a schema of proofs, namely one for each number of elements of X. For example the case of X with 3 elements comes down to (AC2V3) whose proof can be written

∀SetX,Y,Z, (X ≠ ∅ ∧ Y ≠ ∅ ∧ Z ≠ ∅) ⇒ (∃x∈X, ∃y∈Y, ∃z∈Z, (x,y,z) ∈ X×Y×Z) ⇒ X×Y×Z ≠ ∅.∎

More statements simply equivalent to AC

Theorem. The following statements are equivalent to the axiom of choice:
(AC5) Any set E of nonempty sets has a choice function: ∅ ∉ E ⊂ Set ⇒ ∏ IdE ≠ ∅.
(AC6) For any partition P of a set E, ∃K⊂E, ∀A∈P, ∃!: K∩A.
(AC7) For any sets E,F,G and any g: F ↠ G, {g⚬f | f ∈ FE} = GE.

Proofs:
(AC2)⇒(AC5) is obvious ;
(AC5)⇒(AC6) : (x∈ ∏ IdP ∧ K = Im x) ⇒ (K⊂E ∧ ∀A∈P, xA ∈ K∩A ∧ ∀B∈P, xB ∈ A ⇒ A∩B ≠ ∅ ⇒ A = B)
(AC6)⇒(AC3) : ∀Fnc g, X ⊂ Im g ⇒ ∃K⊂Dom g, (∀A∈ Im(g•), ∃! : K∩A) ∴ ∃f ∈ (Dom g)X, (∀x∈X, {f(x)} = K∩g•(x)) ∴ g⚬f = IdX.
(AC1E)⇒(AC7) : ∀h∈GE, (∀x∈E, ∃y∈F, g(y) = h(x)) ⇒ (∃f∈FE, ∀x∈E, g(f(x)) = h(x))
(AC3G)⇒(AC7) : ∃j∈FG, g⚬j = IdG ∴ ∀h∈GE, j⚬h ∈ FE ∧ g⚬j⚬h = h.
(AC7)⇒(AC3) : ∀SetX, ∀Fncg, X = Im g ⇒ IdX ∈ XX = {g⚬f | f ∈ (Dom g)X}. ∎

Note: (AC5)⇒(AC2) is also easy : ∅ ∉ Im A ⊂ Set ⇒ ∃f ∈ ∏ IdIm A, f⚬A ∈ ∏ A.

There are many more statements equivalent to AC, which will not be of any use in this work, and for which the proofs of equivalence are much harder. Interested readers can find about them elsewhere.

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
⇨ Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra ⇨ 3.1. Galois connection
4. Arithmetic - 5. Second-order foundations

Other languages:
FR : 2.10. Axiome du choix