Formal knowledge
Axiom of choice
A principle that selects an element from each set in a family of nonempty sets.
Definition
Axiom of choice
The axiom of choice permits a selection function for a family of nonempty sets without requiring an explicit rule for each selection.
Choice is standard in much classical mathematics and appears in many formal developments. Dependency reporting can show whether a declaration reaches it.
01
Example
Given a family of inhabited sets, choice supplies one selected member from each set.
02
Important distinction
Finite choices with explicit witnesses do not require the unrestricted axiom of choice.
After reading this article, you should be able to
- Define Axiom of choice in the sense used on this site.
- Recognize when a proof selects witnesses without constructing a selection rule.