100 years of Zermelo’s
axiom of choice:
What was the problem with it? Per Martin-Löf 2006 WORK IN PROGRESS
Cantor conceived set theory in a sequence of six papers published in the Mathematische Annalen during the five year period 1879–1884. In the fifth of these papers, published in 1883, he stated as a law of thought (Denkgesetz) that every set can be well-ordered or, more precisely, that it is always possible to bring any well-defined set into the form of a well-ordered set. Now to call it a law of thought was implicitly to claim self-evidence for it, but he must have given up that claim at some point, because in the 1890s he made an unsuccessful attempt at demonstrating the well-ordering principle.
The first to succeed in doing so was Zermelo, although, as a prerequisite of the demonstration, he had to introduce a new principle, which came to be called the principle of choice (Prinzip der Auswahl) respectively the axiom of choice (Axiom der Auswahl) in his two papers from 1908. His first paper on the subject, published in 1904, consists of merely three pages, excerpted by Hilbert from a letter which he had received from Zermelo. The letter is dated 24 September 1904, and the excerpt begins by saying that the demonstration came out of discussions with Erhard Schmidt during the preceding week, which means that we can safely date the appearance of the axiom of choice and the demonstration of the well-ordering theorem to September 1904.
Brief as it was, Zermelo’s paper gave rise to what is presumably the most lively discussion among mathematicians on the validity, or acceptability, of a mathematical axiom that has ever taken place. Within a couple of years, written contributions to this discussion were published by Felix Bernstein, Schoenflies, Hamel, Hessenberg, and Hausdorff in Germany; Baire, Borel, Hadamard, Lebesgue, Richard, and Poincaré in France; Hobson, Hardy, Jourdain, and Russell in England; Julius König in Hungary; Peano in Italy, and Brouwer in the Netherlands. Zermelo responded to those of these contributions that were critical, which was a majority, in a second paper from 1908. This second paper also contains a new proof of the well-ordering theorem, less intuitive or less perspicuous, it has to be admitted, than the original proof, as well as a new formulation of the axiom of choice, a formulation which will play a crucial role in the following considerations.
Despite the strength of the initial opposition against it, Zermelo’s axiom of choice gradually came to be accepted, mainly because it was needed at an early stage in the development of several branches of mathematics, not only set theory, but also topology, algebra and functional analysis, for example. Towards the end of the thirties, it had become firmly established and was made part of the standard mathematical curriculum in the form of Zorn’s lemma.
The intuitionists, on the other hand, rejected the axiom of choice from the very beginning. Baire, Borel, and Lebesgue were all critical of it in their contributions to the correspondence, which was published under the title Cinq lettres sur la théorie des ensembles in 1905. Brouwer’s thesis from 1907 contains a section on the well-ordering principle in which it is treated in a dismissive fashion (‘of course there is no motivation for this at all’) and in which, following Borel, he belittles Zermelo’s proof of it from the axiom of choice. No further discussion of the axiom of choice seems to be found in either Brouwer’s or Heyting’s writings. Presumably, it was regarded by them as a prime example of a nonconstructive principle.
It therefore came as a surprise when, as late as in 1967, Bishop stated, A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence, although, in the terminology that he himself introduced in the subsequent chapter, he ought to have said ‘choice operation’ rather than ‘choice function’. What he had in mind was clearly that the truth of (∀i : I)(∃x : S)A(i, x) → (∃f : I → S)(∀i : I)A(i, f(i)) and even, more generally, (∀i : I)(∃x : S_i)A(i, x) → (∃f : Π_{i : I} S_i)(∀i : I)A(i, f(i)) becomes evident almost immediately upon remembering the Brouwer-Heyting-Kolmogorov interpretation of the logical constants, which means that it might as well have been observed already in the early thirties. And it is this intuitive justification that was turned into a formal proof in constructive type theory, a proof that effectively uses the strong rule of ∃-elimination that became possible to formulate as a result of having made the proof objects appear in the system itself and not only in its interpretation. AC : ∀ ℓ → Set _ AC ℓ = ∀ {I S : Set ℓ} {A : I → Subset S ℓ} → (∀ i → ∃[ x ⦂ S ] A i x) → ∃[ f ⦂ (I → S) ] ∀ i → A i (f i) GAC : ∀ ℓ → Set _ GAC ℓ = ∀ {I : Set ℓ} {S : I → Set ℓ} {A : ∀ i → Subset (S i) ℓ} → (∀ i → ∃[ x ⦂ S i ] A i x) → ∃[ f ⦂ (∀ i → S i) ] ∀ i → A i (f i) gac : ∀ {ℓ} → GAC ℓ gac h = fst ∘ h , snd ∘ h ac : ∀ {ℓ} → AC ℓ ac = gac
In 1975, soon after Bishop’s vindication of the constructive axiom of choice, Diaconescu proved that, in topos theory, the law of excluded middle follows from the axiom of choice. Now, topos theory being an intuitionistic theory, albeit impredicative, this is on the surface of it incompatible with Bishop’s observation because of the constructive unacceptability of the law of excluded middle. There is therefore a need to investigate how the constructive axiom of choice, validated by the Brouwer-Heyting-Kolmogorov interpretation, is related to Zermelo’s axiom of choice on the one hand and to the topos-theoretic axiom of choice on the other.
... continue reading