5.5. The Undecidability of AC

As the powerset allows to write bounded formulas to mean what may otherwise in simple cases be understood as mere statements with open quantifiers (and even escape that altogether in more complex cases), the persisting relativity of their meaning explains how these formulas may remain undecidable.
A big success of mathematical logic has been the proof (much too difficult to be explained here) of the independence of AC in set theory: each universe where it is true includes another one where it is false, and vice versa. Both sides of this result were proven separately as follows.

In 1938, Gödel proved the relative consistency of AC by showing that any universe includes one where AC is true (with the same ∈ but a different powerset). It is defined as the class L of "constructible" sets, obtained by successively adding sets definable from previously defined ones, in such a way that it forms a universe. There, each nonempty set is only made of "constructed" objects, thus has a "first constructed element" that can be used as a choice. Any exception to AC in the external universe, in the form of a family of sets (Ai) with empty product, is absent from L because for some i, the whole set Ai is disjoint from L (it has no constructed element).

In 1966, Paul Cohen proved the relative unprovability of AC. The proof is even harder, so we cannot sketch it here. Let us only explain how, from a constructible universe, it is possible to produce different ones. Since Cantor's theorem holds in L while each construction step of "adding all definable sets" to a given countable part of universe can only add countably many sets, an uncountable infinity of steps is needed to fill uncountable sets; therefore, sub-universes with a non-standard countable model of this "uncountable" hierarchy of construction times, will interpret "constructibility" differently, regarding as "unconstructible" some objects whose time of construction is not represented in this model.

Well-ordering and the axiom of choice

We shall show later that the axiom of choice implies the existence of a well-ordering on all sets. This is a bit difficult to prove but the converse is simple:

If all sets can be well-ordered then the axiom of choice can be deduced in the following way. If ∀x∈E, ∃y∈F, xRy, then with a well-ordering on F we can define f from E to F by f(x) = the smallest y such that xRy.

Thus without the axiom of choice we cannot assume that ZF-ordinals which are cardinals represent all cardinals.

Rebuilding recursion

Let us work in a first-order theory just assumed to have 3 types ℕ, E and HE, the language and axioms of arithmetic for ℕ with the schema of induction over expressible subsets of ℕ, and the axiom that H provides "all finite sequences"

n∈ℕ, ∀uH, ∀yE, ∃vH, vn=y ∧ ∀k<n, vk = uk

The following existential result has a simple proof by induction making no use of uniqueness:

R⊂ℕ×E2, ∀n∈ℕ, (∀i<n, ∀xE, ∃yE, R(i,x,y)) ⇒ ∀aE, ∃uH, u0=a ∧ ∀i<n, R(i,ui,ui+1).

Its simplicity only goes for this case, only generalizable to conditions of the form R(n,(uk)k<n,un), while the case of algebraic terms is also true but more difficult to prove.
As a particular case, comes the finite choice theorem written as

R⊂ℕ×E, ∀n∈ℕ, (∀i<n, ∃yE, R(i,y)) ⇒ ∃uH, ∀i<n, R(i,ui).

With fEℕ×E the restriction of such u to numbers ≤ n is also unique by induction, from which the xE such that x0=a ∧ ∀n∈ℕ, xn+1 = f(n,xn), can be defined by its graph

{(n,un) | (n,u)∈ℕ×H, u0=a ∧ ∀i<n, ui+1 = f(i,ui)}

As H contains any finite sequence expressible in the theory, this definition of recursion turns out to be "the recursion which the theory can express" independently of the particular choice of H.

Axiom of dependent choice (DC)

The axiom of dependent choice is expressible by the following equivalent formulas over every nonempty set E
  1. R⊂ℕ×E2, (∀n∈ℕ, ∀xE, ∃yE, R(n,x,y)) ⇒ ∀aE, ∃uE, u0=a ∧ ∀n∈ℕ, R(n,un,un+1).
  2. RE2, Dom R = E ⇒ ∀aE, ∃uE, u0=a ∧ ∀n∈ℕ, un R un+1.
  3. RE2, Dom R = E ⇒ ∃uE, ∀n∈ℕ, un R un+1.
  4. Any relation not well-founded has a descending sequence (while the converse was already seen)
3. ⇒ 1. can be proven in the above context with H, by taking the set defined like the above graph, {(n,un) | (n,u)∈ℕ×H, u0=a ∧ ∀i<n, R(i,ui,ui+1)} with the relation between (n,x) and (p,y) defined as p=n+1 ∧ R(n,x,y)
Being not well founded, means ∃AX, A≠∅ ∧ Im(R∩(A×A))=A.
3. ⇒ 4. as any descending sequence of R∩(A×A) in A is a descending sequence of R in E
4. ⇒ 3. with A=E
DC implies AC (as clear on 1.), with no converse.
DC as expressed by 2. can be deduced from ACE that narrows R to a function (∃fEE, ∀xE, xRf(x)) which gives such a u by recursion.

Sometimes DC needs to be expressed in the generalized form ∀n∈ℕ, (uk)k<n R un. It can be obtained from the above version by replacing E by the set of finite sequences in E. This substitution would affect the first deduction of DC from AC: the change of Dom R no more lets ACE suffice as a justification. Still it keeps the second justification, from the choice function on Im R which remains a set of nonempty subsets of E.
DC is equivalent to a form of the Lowenheim Skolem theorem, stating that any system with countable language has a countable elementary subsystem. To deduce this statement from DC, the elementary countable subsystem comes as the union of a sequence of countable subsystems, each chosen to satisfy the truth of formulas with parameters in the previous one. The converse is quite easy. Reference : paper by Asaf Karagila - message and paper by Christian Espindola.
In practice, DC, or even AC, may resolve most practical mathematical questions which depend on AC. The full AC only becomes important for higher, more abstract questions of set theory beyond ordinary purposes. It is then usually accepted as true for the questions that depend on it, as it intuitively feels more true and usually leads to rather uniform and effective consequences. Any statement of its falsity would beg for details about which kind of exceptions may it have, so as to reduce the margin of undecidability which occurs in its absence. But as (unlike the powerset) the axiom of choice is unnecessary for the core (vital) constructions at the foundation of mathematics, we shall generally do without it in this work.

Injections of ℕ into infinite sets

The existence of an injection from ℕ to E (equivalent to that of a non-surjective injection from E to E) implies that E is infinite. But the converse involves AC either way:

Counter-examples to the axiom of choice

AC is valid for any family of sets (Ai) having a choice tool over "this kind of" sets Ai (that is a fixed formula which from Ai can pick one of its elements), for every i except possibly a finite set of them (for which the finite choice theorem applies). This limits the possible counterexamples to AC to the rest of cases, that is families of sets where an infinity of them are without choice tool. The simplest sets with no choice tool, are mainly
Indeed, in a finite set of subsets of ℕ, you may choose "the smallest one" for a total order roughly defined as the order between real numbers between 0 and 1, seeing subsets of ℕ as binary expressions of these numbers; but an infinite set of them needs not contain any smallest one for this order: if an infinity of them contain 0 while an infinity don't, you can select those which don't, then continue choosing between those which contain 1 and those which don't, but after an infinity of such exclusion steps you may end up with nothing at all.
Exceptions to AC may appear:

AC vs measurability

Here is an important example of negation of AC while DC is accepted. The Lebesgue measure of the sets of reals is a way to giving each set its "length" (a real number or infinity) with 2 properties: countable additivity (the measure of a countable union of pairwise disjoint sets is the sum of their measures) and translation invariance. Specialists found the relative consistency of set theory with DC and the statement that all sets of reals are Lebesgue measurable. But this statement contradicts AC for the following reason. AC gives the existence of a choice function of the partition of ℘(ℕ) defined by the equivalence relation of finiteness of difference (A,B ↦ (AB is finite)), which can be seen in [0,1] as the equivalence relation of differing by a dyadic rational number. (This use of AC is illustrated by this video in French).
But the image of this function, that is a set made of one representative per equivalence class, cannot be Lebesgue measurable (a candidate measure can neither be zero nor non-zero to fit both properties of Lebesgue measurability).
Actually, it is a very similar use of AC to this one that is used in the construction of the Banach Tarski paradox, where the non-mesurability of sets is just more spectacular.

Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Arithmetic and first-order foundations
5. Second-order foundations
5.1. Second-order structures and invariants
5.2. Second-order logic
5.3. Well-foundedness
5.4. Ordinals and cardinals
5.5. Undecidability of the axiom of choice
5.6. Second-order arithmetic
5.7. The Incompleteness Theorem
More philosophical notes :
Gödelian arguments against mechanism : what was wrong and how to do instead
Philosophical proof of consistency of the Zermelo-Fraenkel axiomatic system