ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Russell's shoes and socks

Example

Russell's illustration separates an explicit selection rule from a bare request for simultaneous choices. For a family of pairs of shoes, suppose the data includes a set $L$ meeting each pair in exactly one member—the left shoe. Then ZF constructs a choice function. For a family of pairs of indistinguishable socks, no such distinguisher is supplied; asking for a selection from every pair is an instance of choice for pairs. This example proves the first claim and identifies the second statement without asserting any model-theoretic nonimplication.

Facts & Assumptions

Given: A family $F$ of two-element sets and a set $L$ such that $S \cap L$ has exactly one element for every $S \in F$ .

[L1]

A choice function for $F$ is a function $g$ with domain $F$ such that $g (S) \in S$ for every $S \in F$ (Choice function).

[L2]

The Axiom of Choice asserts that every family of nonempty sets has a choice function (The Axiom of Choice).

Verification

technique · direct

1.1

For each $S \in F$ , the phrase “the unique element of $S \cap L$ ” defines one element of $S$ from the supplied data.

given

2.1

By Separation, $g = {(S, x) \in F \times ⋃ F : S \cap L = {x}}$ is a set; the uniqueness hypothesis makes it single-valued and total on $F$ .

step 1.1construct

3.1

For every $S \in F$ , $g (S)$ is the unique member of $S \cap L$ , so $g (S) \in S$ . Thus $g$ is a choice function constructed in ZF from $F$ and $L$ .

step 2.1L1

4.1

If the distinguisher $L$ is omitted, step 2.1 has no defining predicate to use. The assertion that an arbitrary family of pairs nevertheless has a choice function is precisely the corresponding restricted instance of [L2]. This identifies the sock question but neither assumes nor proves an independence result.

step 2.1L1L2∎

Remarks

Boundedly many indexed pairs require no choice principle: if the family is listed as $F (0), \dots, F (n - 1)$ , Every natural-number-indexed list of nonempty sets has a choice function on its family of values builds a selection one value at a time. The definition of an arbitrary finite set appears later in Finite, countably infinite, countable, uncountable ↗, so this remark uses only the indexed-family form.
The argument never uses pairwise disjointness or cardinality two. It uses only the supplied predicate selecting exactly one member of every set.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

I. Khatchatourian, The Axiom of Choice (University of Toronto MAT327 notes) (standard reference, not scraped)
B. Russell, Introduction to Mathematical Philosophy (1919), Ch. 12 (standard reference, not scraped)