Extensionality: a set is its members¶

Level: 201 · for anyone who has met the axiom as ∀v₀∀v₁(∀v₂(v₂ ∈ v₀ ⇔ v₂ ∈ v₁) ⇒ v₀ ≃ v₁) and wondered what it is for

One line: Extensionality is the only axiom that says when two sets are equal, so it is the one that makes {2, 5} = {5, 2}, that turns "prove a = b" into "prove a ⊆ b and b ⊆ a", and that lets every other axiom say "the" set it promises; a universe with two memberless points is exactly a universe where it fails.

The axiom, read aloud¶

∀v₀ ∀v₁ (∀v₂ (v₂ ∈ v₀ ⇔ v₂ ∈ v₁) ⇒ v₀ ≃ v₁)

For every a and every b: if every set is a member of a exactly when it is a member of b, then a and b are the same set. In four words, same members, same set. The converse, that the same set has the same members, needs no axiom; it is what "same" means in logic. So the axiom is the one direction that is not free: having the same members is enough to be equal.

It is the only axiom in Cori and Lascar's list that does not assert that a set exists. Every other one says "there is a set whose members are …"; this one says what counts as the same set, and the book uses it after each of the others in the same sentence: by extensionality, there is only one such set.

What it is for¶

It defines what a set remembers. A set remembers which things are in it and nothing else: not the order they were listed in, not how many times, not the rule that produced them. {2, 5} and {5, 2} have the same members, so they are one set; {1, 1, 1} and {1} are one set; the set of divisors of 12 and the set {1, 2, 3, 4, 6, 12} are one set, though one was given by a rule and the other by a list. This is the point what is a set? makes at length, and this page is the same point in the formal language.

It is the proof method for equality. To prove a = b, show a ⊆ b, that every member of a is in b, and b ⊆ a. Section 2 of the program does it for the divisors of 12. Nearly every equality in a set theory book is proved this way, and the two halves are often different arguments: Cori and Lascar's Theorem 7.20 and Proposition 7.21 are pages of showing inclusions both ways.

It makes "the" possible. The axiom of pairs says a set with members a and b exists. Could there be two? Not by extensionality: two sets with exactly the members a and b have the same members and are therefore equal. So the book may write {a, b}, "the pair", and the same reasoning licenses ∪a, 𝒫(a), {x ∈ a : F} and every other name in the chapter. Section 3 counts the candidates in a small universe and finds one each time.

What goes wrong without it¶

A universe can satisfy every other axiom and have two different sets with no members, as long as nothing in it ever asks for their members. Section 4 builds the smallest such universe: three points a, b, c with a and b memberless and c = {a}. The formula fails at the pair (a, b): same members, different points. Such points are called atoms or urelements, and Zermelo's original 1908 axioms allowed them. ZF does not: with extensionality there is exactly one memberless set, ∅, and since every set is built from ∅ by the other axioms, the whole universe is sets of sets of sets of nothing. That is why the universes V₁, V₂, V₃, V₄ of this chapter start from ∅ alone.

What the program prints¶

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

1. THE AXIOM ON V_4
   ∀v0 ∀v1 (∀v2 (v2 ∈ v0 ⇔ v2 ∈ v1) ⇒ v0 ≃ v1)
   for every a and b: if every set is in a exactly when it is in b,
   then a and b are the same set.
   16 sets, 256 pairs (a, b) checked: True

2. HOW IT IS USED: TO PROVE a = b, PROVE a ⊆ b AND b ⊆ a
   a = {1, 2, 3, 4, 6, 12}, written out;  b = {d : 1 ≤ d ≤ 12 and d divides 12}
   every member of a is in b: True
   every member of b is in a: True
   so a = b: True   (Python's == on sets is the axiom)
   Order and repetition are not members, so they do not count:
   {2, 5} == {5, 2}: True   {1, 1, 1} == {1}: True

3. 'UNIQUE BY EXTENSIONALITY': EACH AXIOM'S SET HAS EXACTLY ONE CANDIDATE
   for every a, b in V_3, the number of sets in V_4 whose members are
   exactly a and b: [1].  The pair exists (the axiom of pairs),
   and extensionality says two candidates would have to be equal,
   so 'the pair {a, b}' names one set. The same sentence follows
   every other axiom in the book.

4. A UNIVERSE WHERE IT FAILS: TWO POINTS WITH NO MEMBERS
   points a, b, c with a, b memberless and c = {a}
   extensionality: False
   witness: a and b have the same members (True), and a ≃ b is False
   Such points are called atoms or urelements. ZF has none: by
   extensionality there is exactly one memberless set, ∅, and every
   other set is built from it.

Section 1 evaluates the formula literally on V₄: two nested loops over the sixteen sets, an inner loop over the members. Section 2 is the proof method, and the last two lines are the part a programmer already knows: Python's == on sets is extensionality, which is why a set literal with a repeated element shrinks. Section 3 is the sentence "unique by extensionality" made countable. Section 4 is the failing universe, and the witness is the pair of atoms.

Po polsku, w skrócie¶

Aksjomat ekstensjonalności mówi, kiedy dwa zbiory są równe: gdy mają te same elementy. Czyta się go tak: dla każdych a i b, jeśli każdy zbiór należy do a dokładnie wtedy, gdy należy do b, to a i b są tym samym zbiorem. To jedyny aksjomat, który nie mówi, że jakiś zbiór istnieje; mówi, co to znaczy „ten sam". Z niego wynika, że zbiór pamięta tylko swoje elementy, nie kolejność ani powtórzenia ({2, 5} = {5, 2}), że równość a = b dowodzi się przez dwa zawierania a ⊆ b i b ⊆ a, i że zbiór obiecany przez każdy inny aksjomat jest jedyny, więc wolno mówić „para {a, b}". Program sprawdza formułę na szesnastu zbiorach uniwersum V₄ i buduje uniwersum z dwoma punktami bez elementów, w którym aksjomat nie zachodzi; takie punkty to atomy, których ZF nie ma.

Auf Deutsch: Stichwörter¶

Extensionalität: eine Menge ist ihre Elemente, zwei Mengen mit denselben Elementen sind gleich.

Stichwörter: Extensionalitätsaxiom, Gleichheit von Mengen, Elemente, Teilmenge in beide Richtungen, intensional vs. extensional.

Run it yourself¶

From the root of your clone of this repository:

python3 13_Axioms_of_Set_Theory/extensionality/examples/extensionality.py