Comprehension: a property picks a subset of a set you already have¶

Level: 201 · for anyone reading the scheme ∀v₁ … ∀vₙ₊₁ ∃vₙ₊₂ ∀v₀ (v₀ ∈ vₙ₊₂ ⇔ (v₀ ∈ vₙ₊₁ ∧ F)) and wondering why it is so long, and why the book insists on the "v₀ ∈ vₙ₊₁"

One line: Comprehension is not one axiom but one for every formula F, and each says only that {x ∈ a : F[x]} exists, a subset of a set already in hand; drop the "x ∈ a" and the obvious-looking rule contradicts itself in two lines, which is Russell's paradox and the reason the whole list of axioms exists.

The axiom, read aloud¶

∀v₁ ∀v₂ … ∀vₙ₊₁ ∃vₙ₊₂ ∀v₀ (v₀ ∈ vₙ₊₂ ⇔ (v₀ ∈ vₙ₊₁ ∧ F[v₀, v₁, …, vₙ]))

Strip the parameters first. The variables v₁ … vₙ are sets that F may mention, such as the b in "x ∈ b"; they are quantified at the front so that the axiom holds whatever they are. What remains is: for every set a (that is vₙ₊₁) there is a set s (vₙ₊₂) such that x is a member of s exactly when x is a member of a and F holds of x. The book writes it {x ∈ a : F[x]}; Cunningham calls the same axiom the subset axiom and writes ∀A ∃S ∀x (x ∈ S ↔ (x ∈ A ∧ φ(x))), the book's page 24; other books say separation or, in Zermelo's German, Aussonderung. Python writes it {x for x in a if F(x)}, with the for x in a doing exactly the work of the "x ∈ a".

It is a scheme: a different axiom for each formula F, infinitely many in all, since the language has infinitely many formulas. A program can check some of them, never all; section 1 checks four.

What it is for¶

Every set defined by a rule. The even numbers {n ∈ ℕ : 2 divides n}, the interval {x ∈ ℝ : 0 < x < 1}, the solutions {x ∈ ℝ : x² = 2}: each is a comprehension inside a set that already exists. This is Cunningham's "method of separation" on page 3 and his truth sets, and the set-builder notation of every mathematics book.

The empty set, ∩, ∖. Page 114 of Cori and Lascar derives them: ∅ is {x ∈ a : x ≠ x} for any a; a ∩ b is {x ∈ a : x ∈ b}; a ∖ b is {x ∈ a : x ∉ b}; the intersection of a family is a comprehension inside any one of its members, which is why the family must be non-empty. Section 4 computes each. Cunningham instead has a separate empty set axiom; Cori and Lascar get ∅ for free because a first-order universe is never empty, so some a exists to comprehend inside.

Classes. The sets satisfying a formula do not always form a set, and page 113 gives such collections the name class: the class of all sets, the class of ordinals (their Proposition 7.25). Comprehension says a class cut down to a set is a set, and nothing more.

What goes wrong without the "x ∈ a"¶

The tempting rule is Cantor's comprehension principle (Cunningham, page 20): for every property there is a set of all the things with that property, ∃s ∀x (x ∈ s ⇔ F[x]). Two things go wrong, and section 2 and 3 of the program show them in turn.

First, the universe is not big enough. Take F to be x ∉ x. In V₄ no set is a member of itself, so {x : x ∉ x} would be all of V₄, a set of rank 4 that V₄ does not contain. Unrestricted comprehension demands a set the universe lacks, as pairs and power set do, and no universe could ever catch up, since the demand is for the set of all sets.

Second, it contradicts itself. Suppose r = {x : x ∉ x} exists and ask whether r ∈ r. If it is, then by its own definition it is not; if it is not, then it qualifies, so it is. Section 3 writes the sentence r ∈ r ⇔ r ∉ r as a truth table with two rows and no true row. This is Russell's paradox, which what is a set? tells at length; here it is the reason the axiom carries its "x ∈ a". With it, {x ∈ a : x ∉ x} is just a, since nothing is its own member, and the question "is a a member of itself?" has the harmless answer no.

One qualification, which the books mostly omit: "there is no set of all sets" is a theorem of ZF, a consequence of this way of restricting comprehension, not a fact about sets as such. Quine's New Foundations (1937) restricts comprehension differently, to stratified formulas, ones whose variables can be given levels so that x ∈ y always has y one level above x; x ∉ x cannot be stratified, so Russell's set is not asked for, while x = x can be, so a universal set V with V ∈ V exists. The reading guide places NF among the other systems.

What the program prints¶

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

1. ONE AXIOM PER FORMULA
   ∀v1 ∀v2 ... ∀v(n+1) ∃v(n+2) ∀v0 (v0 ∈ v(n+2) ⇔ (v0 ∈ v(n+1) ∧ F[v0, v1, ..., vn]))
   for every set a there is a set b whose members are the members x of a
   that satisfy F. The book writes {x ∈ a : F[x]}; Python writes
   {x for x in a if F(x)}. There is one axiom for each formula F:
   a = V_3 = {∅, {∅}, {{∅}}, {∅, {∅}}}
     {x ∈ a : x is empty}              = {∅}
     {x ∈ a : x has exactly one member} = {{∅}, {{∅}}}
     {x ∈ a : x ∉ x}                   = {∅, {∅}, {{∅}}, {∅, {∅}}}
     {x ∈ a : ∅ ∈ x}                   = {{∅}, {∅, {∅}}}
   each such set is in V_4, for every a in V_4 and these four F: True
   A subset never has higher rank than the set, so no V_n lacks one.

2. WHAT 'x ∈ a' BUYS: DROP IT AND THE UNIVERSE IS NOT ENOUGH
   {x : x ∉ x} over all of V_4 has 16 members (no set here is its own member),
   and that set is in V_4: False.  It has rank 4; V_4 stops at 3.
   Unrestricted comprehension demands a set the universe does not have.

3. AND WORSE: RUSSELL'S CONTRADICTION, AS A TRUTH TABLE
   Suppose a set r with  ∀x (x ∈ r ⇔ x ∉ x).  Put x = r:  r ∈ r ⇔ r ∉ r.
     r ∈ r    r ∉ r    r ∈ r ⇔ r ∉ r
     True     False    False
     False    True     False
   No row makes it true, so no such r exists in any universe. The
   scheme with 'x ∈ a' only ever gives {x ∈ a : x ∉ x} = a, and a ∉ a.
   for every a in V_4, {x ∈ a : x ∉ x} == a: True

4. WHAT THE BOOK DERIVES FROM IT (PAGE 114)
   ∅     = {x ∈ a : x ≠ x}             = ∅   (any a will do)
   a ∩ b = {x ∈ a : x ∈ b}             = [3, 4]
   a − b = {x ∈ a : x ∉ b}             = [1, 2]
   ∩fam  = {x ∈ c : x ∈ every m ∈ fam} = [2, 3]   for any one member c of fam
   Each is a comprehension inside a set already in hand, which is why
   a ∩ b and a − b never need an axiom of their own, and why ∩fam needs
   fam ≠ ∅: there must be a c to comprehend inside.

Po polsku, w skrócie¶

Aksjomat wyróżniania (u Coriego i Lascara: schemat comprehension, u Cunninghama: subset axiom, po polsku też aksjomat podzbiorów) mówi: dla każdego zbioru a i każdej własności F istnieje zbiór {x ∈ a : F[x]} tych elementów a, które mają własność F. Python pisze to {x for x in a if F(x)}. To nie jeden aksjomat, lecz schemat: osobny aksjomat dla każdej formuły, nieskończenie wiele. Z niego wynikają ∅, a ∩ b, a ∖ b i przekrój rodziny (który wymaga rodziny niepustej). Kluczowe jest „x ∈ a": bez niego reguła „każda własność wyznacza zbiór" (zasada Cantora) żąda zbioru, którego uniwersum nie ma, i sama sobie przeczy: r = {x : x ∉ x} należy do siebie dokładnie wtedy, gdy nie należy, a tabela prawdy tego zdania nie ma żadnego prawdziwego wiersza. To paradoks Russella, powód, dla którego lista aksjomatów w ogóle istnieje.

Auf Deutsch: Stichwörter¶

Aussonderung: eine Eigenschaft wählt eine Teilmenge einer Menge aus, die man schon hat; uneingeschränkt führt sie zu Russell.

Stichwörter: Aussonderungsaxiom (Komprehension, Separation), Eigenschaft, Formel, Teilmenge, Russellsche Antinomie, Axiomenschema.

Run it yourself¶

From the root of your clone of this repository:

python3 13_Axioms_of_Set_Theory/comprehension/examples/comprehension.py