Replacement: the image of a set under a definable function is a set¶

Level: 201 · for anyone who has reached the scheme on page 115 of Cori and Lascar, the longest formula in the chapter, and wants to know what it says and why Zermelo's list needed it

One line: Replacement says that if a formula F behaves as a function, each input having at most one output, then the outputs on any set of inputs form a set; it is the F of ZF, added by Fraenkel in 1922, and it is needed because Zermelo's axioms can build each stage V_{ω+n} and cannot collect them into one set, the same failure a finite stage shows for n ↦ V_n.

The axiom, read aloud¶

The book's version runs to four lines, and Cunningham's one-line form says the same thing:

∀A ((∀x ∈ A) ∃!y ψ(x, y) → ∃S ∀y (y ∈ S ↔ (∃x ∈ A) ψ(x, y)))

For every set a: if for each x in a there is exactly one y with ψ(x, y), then there is a set s whose members are exactly the y's that some x in a is related to. The hypothesis is what Cori and Lascar's Definition 7.2 calls functional in w₀: ∀w₀ ∀w₁ ∀w₂ ((F[w₀, w₁] ∧ F[w₀, w₂]) ⇒ w₁ ≃ w₂), no input has two outputs. Section 1 of the program checks it for two relations; y = x² passes, x = y² fails because 4 has the partners 2 and −2. A functional formula defines a function φ_F, possibly partial, and the axiom says its image {φ_F(x) : x ∈ a} is a set. Python: {f(x) for x in a}.

Like comprehension, it is a scheme, one axiom per formula F, with parameters v₁ … vₙ quantified at the front.

What it is for¶

Every "the set of f(x) for x in a". The set of squares of the members of a, the set of singletons {x} for x in a, the set of lengths of the words in a list. Section 2 computes two images, and the second is smaller than a: an image may merge inputs, and the axiom does not mind.

Comprehension, for free. Page 116 of the book: given F[x], the formula H[x, y] = (y ≃ x ∧ F[x]) is functional, and its image of a is exactly {x ∈ a : F[x]}. Section 4 computes it both ways. So ZF could drop the comprehension scheme; books keep it because it is the one used in practice and the one Zermelo had.

Recursion along the ordinals. The construction "V₀ = ∅, V_{α+1} = 𝒫(V_α), V_λ = ∪ of the earlier stages" defines a function on the ordinals, and so does "ω + n" for each n. To take the union at a limit, the earlier stages must first be a set, and that is replacement applied to the function α ↦ V_α. Cori and Lascar's proof of Proposition 7.27, that every well-ordered set is isomorphic to a unique ordinal, calls the scheme by name.

What goes wrong without it¶

Zermelo's 1908 axioms, without replacement, are satisfied by the universe V_{ω+ω}: ∅, the finite sets, ω, 𝒫(ω), 𝒫(𝒫(ω)), and so on, through every V_{ω+n}. That universe is big enough for the whole of ordinary analysis, and it cannot prove that the set {V_ω, V_{ω+1}, V_{ω+2}, …} exists, because that set would be the first thing missing from it. The function n ↦ V_{ω+n} is definable, its domain ω is a set, and its image is not.

Section 5 is the same failure in miniature. In V₄, the function n ↦ V_n is defined on {0, 1, 2, 3}, each value is a point of the universe, and the set of the four values has rank 4, one more than V₄ holds. Replacement is the axiom that says a universe may not end this way: whatever can be reached by a definable function from a set can be collected. Section 3 counts, as the other pages do, which images V₄ lacks: those of functions that lift rank, such as x ↦ {x}, never those that lower it.

What the program prints¶

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

1. 'FUNCTIONAL' FIRST: EACH INPUT HAS AT MOST ONE OUTPUT
   F = 'y = x²' on 0..3:         [(0, 0), (1, 1), (2, 4), (3, 9)]   functional: True
   F = 'x = y²', y in -3..3:     [(0, 0), (1, -1), (1, 1), (4, -2), (4, 2), (9, -3), (9, 3)]
                                 functional: False   (4 has partners 2 and -2)
   Only a functional F defines a φ_F, and only then does the scheme apply.

2. THE SCHEME, AND THE IMAGE IN PYTHON
   if F is functional:  ∀a ∃b ∀y (y ∈ b ⇔ ∃x (x ∈ a ∧ F[x, y]))
   b = {φ_F(x) : x ∈ a}, the image of a; Python: {f(x) for x in a}.
   a = V_3 = {∅, {∅}, {{∅}}, {∅, {∅}}}
   { {x} : x ∈ a }  = {{∅}, {{∅}}, {{{∅}}}, {{∅, {∅}}}}
   { ∪x  : x ∈ a }  = {∅, {∅}}   smaller: the image can merge

3. WHERE V_4 RUNS OUT: IMAGES THAT GO A RANK UP
   F = x ↦ {x}   image of a in V_4 for all 16 a: False   fails for 12 sets, e.g. a = {{{∅}}}
   F = x ↦ ∪x    image of a in V_4 for all 16 a: True
   Like pairs and power set, a function that lifts rank asks for a set
   the finite universe lacks; one that lowers rank never does.

4. COMPREHENSION FOR FREE (PAGE 116)
   H[x, y] = (y ≃ x ∧ F[x]) is functional, and its image of a is {x ∈ a : F[x]}:
   {x ∈ V_3 : x has one member}: via H = {{∅}, {{∅}}}, directly = {{∅}, {{∅}}}, equal: True

5. WHY THE AXIOM EXISTS: THE FUNCTION n ↦ V_n
   V_0 = ∅                                        rank 0
   V_1 = {∅}                                      rank 1
   V_2 = {∅, {∅}}                                 rank 2
   V_3 = {∅, {∅}, {{∅}}, {∅, {∅}}}                rank 3
   the image {V_0, V_1, V_2, V_3} has rank 4, so it is not in V_4: True
   V_4 has every V_n for n < 4 and not the set of them. Zermelo's axioms
   without replacement are in the same position at V_(ω+ω): they prove
   each V_(ω+n) exists and cannot collect them, so ω + ω, ℵ_ω and every
   construction 'by recursion on the ordinals' need Fraenkel's axiom.

Po polsku, w skrócie¶

Aksjomat zastępowania mówi: jeśli formuła F zachowuje się jak funkcja, czyli każdy argument ma co najwyżej jedną wartość (Cori i Lascar: F jest „funkcjonalna"), to wartości na dowolnym zbiorze argumentów tworzą zbiór, obraz {φ_F(x) : x ∈ a}; Python pisze {f(x) for x in a}. To litera F w ZF, dodana przez Fraenkela w 1922 roku; z niej wynika za darmo aksjomat wyróżniania, a potrzebna jest do konstrukcji przez rekursję po liczbach porządkowych, bo w granicy trzeba wcześniejsze etapy zebrać w zbiór. Bez niej aksjomaty Zermela spełnia uniwersum V_{ω+ω}, w którym każdy etap V_{ω+n} istnieje, ale zbiór wszystkich tych etapów już nie. Program pokazuje to samo w miniaturze: w V₄ funkcja n ↦ V_n ma wartości V₀, V₁, V₂, V₃, a zbiór tych czterech wartości ma rangę 4 i w V₄ go nie ma.

Auf Deutsch: Stichwörter¶

Ersetzung: das Bild einer Menge unter einer definierbaren Funktion ist eine Menge; was Aussonderung nicht erreicht.

Stichwörter: Ersetzungsaxiom (Ersetzungsschema), definierbare Funktion, Bild, Funktionalformel, Vergleich mit Aussonderung, ω + ω.

Run it yourself¶

From the root of your clone of this repository:

python3 13_Axioms_of_Set_Theory/replacement/examples/replacement.py