Some Links to Notes on the Axiom of Choice

Zermelo identified the axiom of choice in 1904 when he used it to proved the well-ordering principle. Later, in 1908, he defended the use of choice in the original 1904 proof as well as in a newer proof of the well-ordering principle.

The axiom of choice was also an involved in the proofs of the Lowenheim-Skolem theorem. Lowenheim's original proof contained gaps that could be filled using versions of the axiom of choice. Skolem filled in these gaps in two different ways (yeilding two slightly different results). One way used choice; the other did not.

Fraenkel proved the independence of the axiom of choice using the idea of Russell's socks. This technique of involves constructing permutation models (requiring the existence of urelements) known as Fraenkel-Mostowski models. Andrews (General Models, Descriptions, and Choice in Type Theory, Journal of Symbolic Logic 37, 385-394, 1972) used an FM-model of simple type theory to prove independence of choice over a formulation of higher-order logic. Godel's constructible universe showed the consistency of the axiom of choice. Cohen later proved the independence of the axiom of choice and the continuum hypothesis using forcing.

Church included a version of the axiom of choice in his type theory.

Leivant notes the axiom of choice can be formulated in different ways in higher order logic.

Andrews showed how to formulate choice in his equality-based version of Church's type theory.