Keyboard graph navigation: press N for concepts or E for relations; use arrow keys, Home, and End to move; Enter selects; Shift plus Enter selects and centers; plus and minus zoom; zero fits; Escape clears the selection. Use the visible viewport buttons as alternatives to dragging, wheel, and pinch gestures.
Canonical static concept record
Open this concept in the interactive graphRead the Markdown equivalent
The assertion that every set-indexed family of nonempty sets has a choice function.
AC is independent of ZF, assuming ZF is consistent. Its standard equivalents are equivalent over ZF, not in arbitrary weak background theories.
wp-axiom-choicenlab-axiom-of-choicesep-axiom-choiceopenlogic-set-theoryEach relation below ends at this concept.
This is an authored directed relation from the source endpoint to the target endpoint.
Over ZF, well-order every member of a family and choose its least element; thus the well-ordering theorem implies AC.
Record a genuine theorem implication that is not part of the target definition; these edges may point toward a weaker structure.
sep-axiom-choiceopenlogic-set-theoryThis is an authored directed relation from the source endpoint to the target endpoint.
The axiom of choice is one of the axioms of ZFC.
Record a genuine theorem implication that is not part of the target definition; these edges may point toward a weaker structure.
wp-zfwp-axiom-choiceEach relation below starts at this concept.
This is an authored directed relation from the source endpoint to the target endpoint.
Over ZF, AC implies that every set can be well-ordered; conversely, the well-ordering theorem implies AC.
Record a genuine theorem implication that is not part of the target definition; these edges may point toward a weaker structure.
sep-axiom-choiceopenlogic-set-theory