Pairs: any two sets fit in a set together¶

Level: 201 · for anyone reading the axiom ∀v₀∀v₁∃v₂∀v₃(v₃ ∈ v₂ ⇔ (v₃ ≃ v₀ ∨ v₃ ≃ v₁)) and asking why it needs saying

One line: The axiom of pairs is the first axiom that makes a set, {a, b}, and with a = b it makes {a}; it needs saying because a universe can run out, as every finite V_n does at its top rank, and it is enough, used three times, to build the ordered pair that the whole of coordinate geometry stands on.

The axiom, read aloud¶

∀v₀ ∀v₁ ∃v₂ ∀v₃ (v₃ ∈ v₂ ⇔ (v₃ ≃ v₀ ∨ v₃ ≃ v₁))

For any a and b there is a set c such that a set is a member of c exactly when it is a or it is b. That c is the pair {a, b}, "the" by extensionality. Read the quantifiers in order: the outer two loops pick a and b, any two sets at all, and the search for c must then succeed; the innermost ∀ says who c's members are.

Nothing says a and b must differ. With a = b the members of c are "a or a", that is, a alone, and c is the singleton {a}. The book notes it in one line; the program shows it in section 3.

What it is for¶

It is the first set-maker. Extensionality judges sets; pairs builds one. From ∅, which comprehension provides, pairs gives {∅}, then {∅, {∅}} and {{∅}}, and the universe starts to fill. Every set in V₂, V₃ and V₄ is reached by pairs and unions alone.

Order comes from it. A pair forgets order: section 4 checks the book's remark that {a, b} = {a′, b′} exactly when the two lists agree or are swapped. Kuratowski's trick (1921) recovers order with nothing but pairs: (a, b) := {{a}, {a, b}}, three applications of the axiom, and section 5 checks that (a, b) = (c, d) forces a = c and b = d. The inner singleton marks which entry is first. Cori and Lascar's Definition 7.3 is this set, and their Proposition 7.4 is this check as a proof; the Cartesian product builds ℝ² from it.

Finite sets follow. {a, b, c} is {a, b} ∪ {c}, a pair, a singleton and a union; any finite list of sets becomes a set the same way, which is page 112 of the book.

What goes wrong without it¶

A universe with a top rank. The sets of V₄ have rank at most 3, where the rank is the depth of the braces, and the pair of two sets of rank 3 has rank 4: it is a set in the sense that we can write it, and it is not a point of V₄. Section 2 counts: of the 256 ways to pick a and b in V₄, only 16 have their pair inside. So the axiom fails in every finite stage V_n, and in any universe that stops somewhere. A universe that satisfies it has no last rank, which is the first hint that the axioms are demands for size.

What the program prints¶

Verified output of pairs.py — regenerated by tools/run_examples.py, never hand-typed.

1. THE AXIOM, AND WHAT IT BUILDS
   ∀v0 ∀v1 ∃v2 ∀v3 (v3 ∈ v2 ⇔ (v3 ≃ v0 ∨ v3 ≃ v1))
   for any a and b there is a c whose members are exactly a and b: {a, b}.
   a = ∅          b = {∅}        {a, b} = {∅, {∅}}
   a = {∅}        b = {{∅}}      {a, b} = {{∅}, {{∅}}}
   a = {∅, {∅}}   b = ∅          {a, b} = {∅, {∅, {∅}}}

2. WHERE V_4 RUNS OUT: PAIRS OF SETS FROM THE TOP RANK
   of the 256 pairs (a, b) of sets in V_4, 16 have their {a, b} in V_4
   and 240 do not, e.g. a = ∅, b = {{{∅}}}:
   rank(a) = 0, rank(b) = 3, rank({a, b}) = 4, and V_4 stops at rank 3.
   So the axiom fails in every V_n: it asks for a set one rank up.
   A universe that satisfies it has no top rank.

3. a = b GIVES THE SINGLETON {a}
   {a, a} with a = ∅          is {∅}, one member, not two
   {a, a} with a = {∅}        is {{∅}}, one member, not two
   {a, a} with a = {{∅}}      is {{{∅}}}, one member, not two

4. WHEN ARE TWO PAIRS EQUAL? THE BOOK'S REMARK, CHECKED
   {a, b} = {a', b'}  iff  (a = a' and b = b') or (a = b' and b = a')
   for every a, b, a', b' in V_3 (256 cases): True
   so a pair forgets order: {a, b} = {b, a} always.

5. THREE PAIRS MAKE AN ORDERED PAIR (KURATOWSKI 1921)
   (a, b) := {{a}, {a, b}}, so (a, b) = (c, d) iff a = c and b = d:
   for every a, b, c, d in V_3: True
   (∅, {∅}) = {{∅}, {∅, {∅}}}
   ({∅}, ∅) = {{{∅}}, {∅, {∅}}}   different sets, so order is kept
   (∅, ∅)   = {{∅}}   the pair collapses, and still decodes
   Pairs, then, are enough for order; the Cartesian product page
   builds the plane from them.

6. HAUSDORFF'S PAIR WORKS TOO: (a, b) := {{a, ∅}, {b, {∅}}}
   (a, b) = (c, d) iff a = c and b = d, for every a, b, c, d in V_3: True
   Kuratowski (∅, {∅}) = {{∅}, {∅, {∅}}}   Hausdorff (∅, {∅}) = {{∅}, {{∅}}}
   Different sets with the same property; any set with the property will do,
   and nobody ever unpacks one. The ∅ and {∅} are tags for 'first' and 'second'.

7. PAIRS WITHOUT THE AXIOM: REPLACEMENT OVER 𝒫(𝒫(∅)) (SUPPES, ISABELLE/ZF)
   𝒫(∅) = {∅}, and 𝒫(𝒫(∅)) = {∅, {∅}}: a set with exactly two members.
   The rule 'send ∅ to a and {∅} to b' is a function on it, so replacement gives
   its image, and the image is {a, b}: it agrees with the axiom for every a, b in V_3: True
   So pairing is a theorem once power set and replacement are axioms. Suppes
   and Isabelle/ZF take it that way; Isabelle's definition is exactly this rule:
     Upair(a,b) ≡ {y . x ∈ Pow(Pow(0)), (x = 0 ∧ y = a) ∨ (x = Pow(0) ∧ y = b)}

Section 2 is the row of the chapter's table for this axiom, with the counterexample written out: a = ∅ and b = {{{∅}}} are both in V₄, and {a, b} is not. Sections 4 and 5 are the two facts about pairs that the rest of the book uses, checked over every choice of four sets from V₃. Section 6 checks Hausdorff's alternative pair, {{a, ∅}, {b, {∅}}}, which Robert André's book presents beside Kuratowski's: ∅ and {∅} tag the first and second entries, the defining property holds just the same, and the two constructions give different sets, which is the point: any set with the property will serve, and nobody ever looks inside one.

Pairs without the axiom¶

Section 7 is a remark from Paulson's manual for Isabelle/ZF, placed in the proof assistants guide: pairing need not be an axiom at all. The power set of ∅ is {∅}, and the power set of that is {∅, {∅}}, a set with exactly two members that power set alone provides. The rule "send ∅ to a and {∅} to b" is a function on it, so replacement yields its image, and the image is {a, b}. The program checks that this agrees with the axiom for every a and b in V₃. Suppes's Axiomatic Set Theory derives pairing this way, and Isabelle/ZF defines it so, as Upair(a,b), with six axioms and a constant 0 in place of the chapter's seven; the axiom is kept on this page because every book the chapter reads states it, and because a universe that lacks it is the clearest way to see what it demands.

Po polsku, w skrócie¶

Aksjomat pary mówi: dla dowolnych zbiorów a i b istnieje zbiór, którego elementami są dokładnie a i b, czyli para {a, b}; dla a = b dostajemy singleton {a}. To pierwszy aksjomat, który coś buduje: z ∅ daje {∅}, potem {∅, {∅}} i tak dalej. Para nie pamięta kolejności ({a, b} = {b, a}), ale trzy pary dają parę uporządkowaną Kuratowskiego (a, b) = {{a}, {a, b}}, z której (a, b) = (c, d) wynika a = c i b = d; na niej stoi cała geometria współrzędnych. Aksjomat trzeba wypowiedzieć, bo uniwersum może się skończyć: w V₄, gdzie zbiory mają rangę najwyżej 3, para dwóch zbiorów rangi 3 ma rangę 4 i w V₄ jej nie ma. Program liczy, że z 256 par elementów V₄ tylko 16 ma swoją parę w środku. Sekcja 7 pokazuje uwagę z podręcznika Isabelle/ZF: para nie musi być aksjomatem, bo 𝒫(𝒫(∅)) = {∅, {∅}} ma dokładnie dwa elementy, a zastępowanie (∅ ↦ a, {∅} ↦ b) daje z niego obraz {a, b}.

Auf Deutsch: Stichwörter¶

Paarmengenaxiom: je zwei Mengen passen zusammen in eine Menge; daraus Einermenge und geordnetes Paar.

Stichwörter: Paarmengenaxiom, ungeordnetes Paar {a, b}, Einermenge {a}, geordnetes Paar (Kuratowski), Ersetzung über 𝒫(𝒫(∅)).

Run it yourself¶

From the root of your clone of this repository:

python3 13_Axioms_of_Set_Theory/pairs/examples/pairs.py