Description: Axiom of Choice using
abbreviations. The logical equivalence to ax-ac 9024
can be established by chaining aceq0 8684 and aceq2 8685. A standard
textbook version of AC is derived from this one in dfac2a 8695, and this
version of AC is derived from the textbook version in dfac2 8696.
The following sketch will help you understand this version of the
axiom. Given any set 𝑥, the axiom says that there exists a
𝑦
that is a collection of unordered pairs, one pair for each nonempty
member of 𝑥. One entry in the pair is the member
of 𝑥, and
the other entry is some arbitrary member of that member of 𝑥.
Using the Axiom of Regularity, we can show that 𝑦 is really a set of
ordered pairs, very similar to the ordered pair construction
opthreg 8258. The key theorem for this (used in the proof
of dfac2 8696) is
preleq 8257. With this modified definition of ordered
pair, it can be
seen that 𝑦 is actually a choice function on the
members of 𝑥.
For example, suppose
𝑥 =
{{1, 2}, {1, 3}, {2, 3, 4}}. Let us try
𝑦 =
{{{1, 2}, 1}, {{1, 3}, 1},
{{2, 3, 4}, 2}}. For the member (of 𝑥)
𝑧 =
{1, 2}, the only assignment to 𝑤 and 𝑣 that
satisfies the axiom is 𝑤 = 1 and 𝑣 = {{1, 2}, 1}, so
there is exactly one 𝑤 as required. We verify the other two
members
of 𝑥 similarly. Thus, 𝑦
satisfies the axiom. Using our
modified ordered pair definition, we can say that 𝑦 corresponds to
the choice function {⟨{1, 2}, 1⟩, ⟨{1,
3}, 1⟩,
⟨{2, 3, 4}, 2⟩}. Of course other
choices for 𝑦 will
also satisfy the axiom, for example
𝑦 =
{{{1, 2}, 2}, {{1, 3}, 1},
{{2, 3, 4}, 4}}. What AC tells us is that there
exists at
least one such 𝑦, but it doesn't tell us which one.
(New usage is discouraged.) (Contributed by NM,
19-Jul-1996.) |