Metamath Proof Explorer


In this section we add the Axiom of Choice ax-ac, as well as weaker forms such as the axiom of countable choice ax-cc and dependent choice ax-dc. We introduce these weaker forms so that theorems that do not need the full power of the axiom of choice, but need more than simple ZF, can use these intermediate axioms instead.

The combination of the Zermelo-Fraenkel axioms and the axiom of choice is often abbreviated as ZFC. The axiom of choice is widely accepted, and ZFC is the most commonly-accepted fundamental set of axioms for mathematics.

However, there have been and still are some lingering controversies about the Axiom of Choice. The axiom of choice does not satisfy those who wish to have a constructive proof (e.g., it will not satisfy intuitionistic logic). Thus, we make it easy to identify which proofs depend on the axiom of choice or its weaker forms.

  1. ZFC Set Theory - add Countable Choice and Dependent Choice
    1. Introduce the Axiom of Countable Choice
    2. Introduce the Axiom of Dependent Choice
  2. ZFC Set Theory - add the Axiom of Choice
    1. Introduce the Axiom of Choice
    2. AC equivalents: well-ordering, Zorn's lemma
    3. Cardinal number theorems using Axiom of Choice
    4. Cardinal number arithmetic using Axiom of Choice
    5. Cofinality using the Axiom of Choice
  3. ZFC Axioms with no distinct variable requirements
    1. nd1
    2. nd2
    3. nd3
    4. nd4
    5. axextnd
    6. axrepndlem1
    7. axrepndlem2
    8. axrepnd
    9. axunndlem1
    10. axunnd
    11. axpowndlem1
    12. axpowndlem2
    13. axpowndlem3
    14. axpowndlem4
    15. axpownd
    16. axregndlem1
    17. axregndlem2
    18. axregnd
    19. axinfndlem1
    20. axinfnd
    21. axacndlem1
    22. axacndlem2
    23. axacndlem3
    24. axacndlem4
    25. axacndlem5
    26. axacnd
    27. zfcndext
    28. zfcndrep
    29. zfcndun
    30. zfcndpow
    31. zfcndreg
    32. zfcndinf
    33. zfcndac
  4. The Generalized Continuum Hypothesis
    1. Sets satisfying the Generalized Continuum Hypothesis
    2. Derivation of the Axiom of Choice