A note on the schemes of replacement and collection.

A. R. D. MATHIAS ERMIT, Université de la Réunion and Centre de Recerca Matemàtica, Bellaterra, Catalonia

Abstract We derive the schemes of ZF from certain weak forms of the same.

0: Introduction

We denote by Repcoll the axiom scheme that says of each formula Φ(y⃗, z, t⃗) of the language of set

theory that ∀y^{⟶}:∈u ∃!zΦ(y⃗, z, t⃗) ⟹ ∃w ∀y^{⟶}:∈u ∀z(Φ(y⃗, z, t⃗) ⟹ z ∈ w),

where for y⃗ the finite sequence y_{1}, y_{2}, … y_{𝔫} of variables, ∀y^{⟶} :∈ u denotes the corresponding finite sequence of restricted quantifiers ∀y_{1} :∈u ∀y_{2} :∈u … ∀y_{𝔫}:∈u .

The instances of this scheme have hypotheses that are stronger than those of Collection and conclusions that are weaker than those of Replacement, and it might seem that all instances of the scheme of Separation would be needed to show, starting from a w as above, the set-hood of its subclass {z | ∃y^{⟶} :∈ u Φ(y⃗, z, t⃗}, the image of the function on u implicitly defined by Φ. We shall see, however, that over a surprisingly modest base theory, Repcoll yields the full strength of ZF.

Let M_{0}, M_{1} be the systems described in The Strength of Mac Lane Set Theory [M]: the axioms of M_{0} are those of Extensionality, Null Set, Pairing, Sumset, Power Set, and the scheme of Δ_{0} Separation; and M_{1} is M_{0} with the addition of the axioms of Foundation—the assertion that every non-empty set x has a member y with x∩y empty—and the principle TCo of Transitive Containment, the assertion that every set is a member of a transitive set.

We answer a question of A. K. Simpson by showing that all axioms of ZF except the axiom of infinity are provable, classically, in M_{1} + Repcoll, but not in certain weakenings of that system.

1: Establishing ranks

We first prove that every set has a rank; in doing so we shall use the fact, proved in [M] as Theorem 6·9, part (i), that all instances of the scheme of Δ_{0}^{P} separation are provable in the theory M_{0}. A formula is Δ_{0}^{P} if all its quantifiers are of the form Qx :⊆ y or Qx:∈ y where Q is either ∀ or ∃, and x and y are distinct variables. 1·0 DEFINITION A rank function is a function f with domain a transitive set u such that for each x in u,

f(x) = ⋃ {f(y) + 1 | y ∈ x}.

1·1 LEMMA (M_{1}) For each transitive set u there is at most one function, which we denote by ϱ_{u} when it exists, with domain u and satisfying the recurrence

ϱ_{u}(z) = ⋃ {ϱ_{u}(y) + 1 | y ∈ z}.

Proof : The recurrence is of the form f(x) = G(f ↾ x). Consider, using Foundation, a minimal member w̄ of {w | ϱ_{1}(w) ≠ ϱ_{2}(w)}, for distinct solutions ϱ_{1} and ϱ_{2} to the recursion equation. Then ϱ_{1}(w̄) = G(ϱ_{1} ↾w̄) = G(ϱ_{2} ↾w̄) = ϱ_{2}(w̄), a contradiction. ⊣ (1·1)

1·2 REMARK If ϱ_{u} exists and w is a transitive subset of u, then ϱ_{w} exists, and equals the restriction ϱ_{u} ↾w of ϱ_{u} to w. 1·3 COROLLARY If a ∈ Dom ϱ_{u} ∩ Dom ϱ_{v}, then ϱ_{u}(a) = ϱ_{v}(a).

Proof : Both are equal to ϱ_{u∩v}(a). ⊣ (1·3)

1·4 REMARK f = ϱ_{u} is ΔM_{1}_{0}, being equivalent in M_{1} to

\begin{matrix}⋃ u ⊆ u & F n(f) & Dom (f) = u & & ∀x:∈u f(x) ∈ ON & \\ ∀x:∈u ∀y:∈x f(y) < f(x) & ∀x:∈u ∀ζ:∈f(x) ∃y:∈x ζ ⩽ f(y). \end{matrix}

By the transitive closure of a set x is meant a transitive set u of which x is a subset and such that for any transitive set v ⊇ x, u ⊆ v. Evidently there can be at most one such u for given x. 1·5 PROPOSITION (M_{1}) Every set has a transitive closure. Proof : Given x, and applying TCo, let u be a transitive set of which x is a member and therefore a subset. Using Power Set and Δ_{0} Separation, form the set T of all transitive subsets v of u of which x is a subset. T is non-empty, so again using Δ_{0} separation, its intersection, c, say, will be a set. Then certainly c is a transitive set of which x is a subset; and if b is any other, so is b ∩ u, which latter is a member of T and hence a superset of c, so that c ⊆ b, as required. ⊣ (1·5)

1·6 DEFINITION We write tcl(x) for the transitive closure of x.

The smallest transitive set of which x is a member is of course tcl({x}), and the minimal requirement for a set x to have a rank is that ϱ_{tcl({x})}, for which in future we write ϱ_{(x)}, should exist. 1·7 REMARK y = tcl({x}) is equivalent in M_{1} to the Δ_{0}^{P} formula

⋃ y ⊆ y & x ∈ y & ∀v :⊆ y[(⋃ v ⊆ v & x ∈ v) ⟹ v = y].

The following is proved in [M] as proposition 1·24. 1·8 LEMMA (M_{0}) x × y ∈ V.

Henceforth we reason in M_{1} + Repcoll. 1·9 PROPOSITION Each transitive set u carries a rank function ϱ_{u}. Proof : Suppose there is a transitive set u with no rank function with domain u. For each x ∈ u, define F (x) to be the ordinal ϱ_{(x)}(x) assigned to x if there is a rank function ϱ_{(x)} defined on tcl({x}), and to be 0 if there is no such function. Apply Repcoll to obtain a w containing all values F (x) for x ∈ u; w ∩ ON is a set by Δ_{0} separation; take its union and add 1 if necessary to obtain an ordinal κ such that for x ∈ u, ϱ_{(x)}(x), if defined, is less than κ.

Now form the class A = u ∩ {z | ∃f:∈P(κ × u) f = ϱ_{(z)}} of members of u which have a rank function into κ; that will be a set, as it equals u ∩ {z | ∃v:∈ P(u) ∃f:∈ P(κ × u) f = ϱ_{v} & z ∈ v}, which is the intersection of a set and a class that is Δ_{0} in the parameters P(u) and P(κ × u).

A is transitive since y ∈ z ⟹ tcl({y}) ⊆ tcl({z}). Let x̄ = A if A = u, and otherwise, using Foundation, let x̄ be a member of u ∖ A with x̄ ⊆ A. By Repcoll the class R =_{df} {ϱ_{(x)} | x ∈ x̄} is included in some set w; by Δ_{0}^{P} separation that will be a set, since

R = w ∩ {f | ∃x:∈x̄ ∃y:∈P(u) y = tcl({x}) & f = ϱ_{y}}.

The set ⋃ R will be a rank function with domain tcl(x̄): in the case x̄ = u, that gives a rank function on u and therefore a contradiction.

In the case x̄ ∈ u ∖ A, use ⋃ R to form {ζ ⩽ κ | ∀y:∈x̄ ϱ_{(y)}(y) < ζ}; let its infimum be η. Now we have a rank function on tcl({x̄}) after all, with ϱ_{(x̄)}(x̄) = η, and again a contradiction. ⊣ (1·9)

1·10 COROLLARY There is a Σ_{1} function ϱ with domain the universe such that for each set x,

ϱ(x) = ⋃ {ϱ(y) + 1 | y ∈ x}.

Our next task is to prove that, for each ordinal η, the class of sets of rank less than η is a set.

1·11 DEFINITION Call f an attempt if f is a function with domain some ordinal η, and for ordinals less than η, f(0) = ∅, f(ξ + 1) = P(f(ξ)) and if 0 < λ = ⋃ λ < η, f(λ) = ⋃_{ν<λ}f(ν).

1·12 REMARK “f is an attempt” is a Δ_{0}^{P} formula.

1·13 LEMMA There is at most one attempt with a given domain.

Proof : Let f and g be attempts with domain η. Consider η ∩ {ξ | f(ξ) ≠ g(ξ)}, a set by Δ_{0} separation, and therefore, if non-empty, possessed of a minimal element ζ̄. But then f ↾ ζ̄ = g ↾ ζ̄, and so by cases on ζ̄ one shows that f(ζ̄) = g(ζ̄), a contradiction. ⊣ (1·13)

1·14 REMARK If f is an attempt with domain η then for each ζ < η, f ↾ζ will be an attempt with domain ζ.

1·15 PROPOSITION For each ordinal ζ there is an attempt with domain ζ.

Proof : Suppose there is a ζ for which there is no attempt with domain ζ. Our immediate problem is to find a minimal such ζ.

Define, for the ordinals ν less than ζ, G(ν) to be the unique attempt with domain ν, if it exists, and if no such attempt exists, set G(ν) = 0. By Repcoll, there is some set w, which we may take to be transitive, such that every f that is an attempt is in w.

We may form w ∩ {f | f is an attempt}, which is a set by Δ_{0}^{P} separation; its union, also a set, will be the maximal attempt h, and we may find the least ordinal ζ̄ ⩽ ζ not in the domain of that union. ζ̄ is the desired minimal ordinal that is the domain of no attempt.

Trivially ζ̄ ≠ 0, 1; if ζ̄ is a limit ordinal, then h itself is an attempt with domain ζ̄; so ζ̄ is an successor, say ξ + 1, with ξ ≠ 0, and h is the attempt with domain ξ.

Now set f(ν) = h(ν) for ν < ξ; if ξ is a limit ordinal, set f(ξ) = ⋃ {h(ν) | ν < ξ}, and if ξ = η + 1, set f(ξ) = P(h(η)). In either case, f is an attempt with domain ζ̄, a contradiction. ⊣ (1·15)

1·16 COROLLARY For each ζ, the class V_{ζ} =_{df} {x | ϱ(x) < ζ} is a set, and the sequence ⟨V_{ξ} | ξ < ζ⟩ is a set.

Proof : one shows that for f an attempt and ξ in its domain, f(ξ) = V_{ξ}. ⊣ (1·16)

1·17 PROPOSITION For any ordinal η_{0} and set a, the class η_{0} ∩ {η | ∃x:∈a ϱ(x) = η} is a set.

Proof : let a ⊆ u, transitive, and consider ϱ_{u}[a] ∩ η_{0}. ⊣ (1·17)

1·18 REMARK In the next section we shall establish an induction on various classes of formulæ. To preserve the rhythm of the induction it will be convenient to use the alternative names Π_{0} and Σ_{0} for the class of Δ_{0} formulæ.

2: Principles of logic.

Fix a concrete 𝔨. We write Θ(y⃗) for a typical Σ_{𝔨} formula, which we take in the form

∃x_{𝔨}∀x_{𝔨−1}∃x_{𝔨−2} … Q_{2}x_{2}Q_{1}x_{1}Φ_{0}(x_{1}, …, x_{𝔨}, y⃗)

where Φ_{0} is a Δ_{0} formula and the quantifiers Q_{2} and Q_{1} are ∃∀ or ∀∃ according to the parity of 𝔨. The reverse numbering of variables is deliberate.

2·0 DEFINITION Denote by Logik(Σ_{𝔨}(y⃗)) the principle which for each Σ_{𝔨} formula Qx^{⟶}Φ_{0}(x⃗, y⃗) as above asserts that starting from any ordinal η there is a sequence η < ξ_{𝔨} < ξ_{𝔨−1} < ξ_{𝔨−2} < … < ξ_{2} < ξ_{1} such that

\begin{matrix}∀y^{⟶} ∈ V_{η}[∃x_{𝔨}∀x_{𝔨−1}∃x_{𝔨−2} … Q_{2}x_{2}Q_{1}x_{1} & Φ_{0}(x_{1}, …, x_{𝔨}, y⃗) \\ ⟺ ∃x_{𝔨}:∈V_{ξ_{𝔨}} ∀x_{𝔨−1} :∈V_{ξ_{𝔨−1}} ∃ & x_{𝔨−2} :∈V_{ξ_{𝔨−2}} … Q_{2}x_{2} :∈V_{ξ_{2}} Q_{1}x_{1} :∈V_{ξ_{1}} Φ_{0}(x_{1}, …, x_{𝔨}, y⃗)]. \end{matrix}

2·1 PROPOSITION Logik(Σ_{0}(y⃗))

Proof : vacuous. ⊣ (2·1)

2·2 DEFINITION Denote by Separation(Σ_{𝔨}(ẑ, y⃗)) the principle which for each Σ_{𝔨} formula Θ(z, y⃗) asserts that for all sets y⃗ and a the class a ∩ {z | Θ(z, y⃗)} is a set. 2·3 PROPOSITION Separation(Σ_{0}(ẑ, y⃗)). Proof : among the axioms of M_{1}. 2·4 PROPOSITION For 𝔨 ⩾ 1, Logik(Σ_{𝔨}(z, y⃗)) implies Separation(Σ_{𝔨}(ẑ, y⃗)); more precisely, to each instance 𝔄 of Separation(Σ_{𝔨}(ẑ, y⃗)) there is an instance 𝔅 of Logik(Σ_{𝔨}(z, y⃗)) such that ⊢_{M_{1}} (𝔅 ⟹ 𝔄). Proof : let Θ(z, y⃗) be the formula

∃x_{𝔨}∀x_{k−1}∃x_{k−2} … Q_{2}x_{2}Q_{1}x_{1}Φ_{0}(x_{1}, …, x_{𝔨}, z, y⃗)

where Φ_{0} is Δ_{0}. Given a, let η = ϱ(a), and let η < ξ_{𝔨} < ξ_{𝔨−1} < ξ_{𝔨−2} < … < ξ_{2} < ξ_{1} be the sequence of ordinals promised by Logik(Σ_{𝔨}(z, y⃗)). Form the sets a_{i} = V_{ξ_{i}} for 1 ⩽ i ⩽ 𝔨. Then the class a ∩ {z | Θ} equals

a ∩ {z | ∃x_{𝔨}:∈a_{𝔨} ∀x_{𝔨−1} :∈a_{𝔨−1} ∃x_{𝔨−2} :∈a_{𝔨−2} … Q_{2}x_{2} :∈a_{2} Q_{1}x_{1} :∈a_{1} Φ_{0}(x_{1}, …, x_{𝔨}, z, y⃗).}

which is a set by Δ_{0} Separation. 2·5 DEFINITION Denote by Minimisation(Π_{𝔨}(ẑ, y⃗)) the principle which for each Π_{𝔨} formula Ψ(z, y⃗) asserts that for any sets y⃗, if there is a z such that Ψ(z, y⃗) then there is an ordinal η such that there is a z of rank η such that Ψ(z, y⃗) but there is no such z of rank less than η.

That η is evidently unique.

2·6 PROPOSITION Minimisation (Π_{0}(ẑ, y⃗)).

Proof : easy from Δ_{0} Separation, using the existence of V_{η+1}. 2·7 PROPOSITION For 𝔨 ⩾ 1, Separation(Σ_{𝔨}(ẑ, y⃗)) implies Minimisation(Π_{𝔨}(ẑ, y⃗)). Proof : Fix y⃗ and let Ψ(z, y⃗) be Π_{𝔨}. Suppose that z_{0} and η_{0} are such that Ψ(z_{0}, y⃗) and ϱ(z_{0}) = η_{0}. Since the negation of a Π_{𝔨} formula is logically equivalent to a Σ_{𝔨} one, we may use Σ_{𝔨} Separation to form the set V_{η_{0}} ∩ {z | Ψ(z, y⃗)} and call it A. If A is empty, η_{0} is the desired ordinal. Otherwise form η_{0} ∩ {η | ∃z:∈ A ρ(z) = η}, which is a set by Proposition 1·17, and, using Foundation, take its least element, which will be the desired ordinal. ⊣ (2·7)

2·8 DEFINITION Strong Collection(Π_{𝔨}(ẑ, y⃗)) is the principle, for a Π_{𝔨} formula Ψ(z, y⃗), that to each ordinal ζ there is a strictly larger ordinal ξ such that ∀y^{⟶} ∈ V_{ζ}, if there is a z such that Ψ then such a z will be found in V_{ξ}.

2·9 PROPOSITION Strong Collection(Π_{0}(ẑ, y⃗)).

Proof : Use Minimisation (Π_{0}) to produce minimal ranks of witnesses; then use Repcoll to collect those minimal ranks and thus to obtain a strict upper bound ξ for them; finally use the existence of V_{ξ}. ⊣ (2·9)

More generally,

2·10 PROPOSITION Minimisation(Π_{𝔨}(ẑ, y⃗)) implies Strong Collection(Π_{𝔨}(ẑ, y⃗)).

Proof : fix ζ. Let Ψ(z, y⃗) be Π_{𝔨}. We define a function (of several variables) on V_{ζ}: F (y⃗) is the least η such that there is an z of rank η for which Ψ(z, y⃗), if there is such an z; otherwise F (y⃗) = 0.

By Repcoll, there is a bound ξ to such η’s: we may take ξ > ζ. Then

∀y^{⟶}:∈V_{ζ} (∃zΨ ⟺ ∃z:∈V_{ξ} Ψ).  ⊣ (2·10)

2·11 PROPOSITION Logik(Σ_{1}(y⃗)). Proof : Immediate from Strong Collection(Π_{0}(x̂_{1}, y⃗)). ⊣ (2·11)

2·12 PROPOSITION For 𝔨 ⩾ 1, if both Logik(Σ_{𝔨}(x_{𝔨+1}, y⃗)) and Strong Collection(Π_{𝔨}(x̂_{𝔨+1}, y⃗)), then Logik(Σ_{𝔨+1}(y⃗)). Proof : Let Φ(y⃗) be ∃x_{𝔨+1}Ψ(x_{𝔨+1}, y⃗) where for some Δ_{0} formula Φ_{0}, Ψ is the Π_{𝔨} formula

∀x_{𝔨}∃x_{𝔨−1}∀x_{𝔨−2} … Q_{2}x_{2}Q_{1}x_{1}Φ_{0}(x_{1}, …, x_{𝔨}, x_{𝔨+1}, y⃗)

where the quantifiers Q_{2} and Q_{1} are ∀∃ if 𝔨 is even and ∃∀ otherwise. For given η, Strong Collection(Π_{𝔨}(x̂_{𝔨+1}, y⃗)) yields a ξ_{𝔨+1} > η such that

∀y^{⟶}:∈V_{η} [∃x_{𝔨+1}Ψ ⟺ ∃x_{𝔨+1} :∈V_{ξ_{𝔨+1}} Ψ].

Now starting from that ordinal ξ_{𝔨+1} apply Logik(Σ_{𝔨}(x_{𝔨+1}, y⃗)) to the formula ¬Ψ to obtain a strictly increasing sequence ξ_{𝔨} < … < ξ_{1}, with ξ_{𝔨+1} < ξ_{𝔨}, such that for all x_{𝔨+1} and y⃗ in V_{ξ_{𝔨+1}},

Ψ(x_{𝔨+1}, y⃗) ⟺ ∀x_{𝔨}:∈V_{ξ_{𝔨}} ∃x_{𝔨−1} :∈V_{ξ_{𝔨−1}} … Q_{2}x_{2} :∈V_{ξ_{2}} Q_{1}x_{1} :∈V_{ξ_{1}} Φ_{0}(x_{1}, …, x_{𝔨}, x_{𝔨+1}, y⃗).

Then for all y⃗ in V_{η},

Φ(y⃗) ⟺ ∃x_{𝔨+1}Ψ(x_{𝔨+1}, y⃗)
⟺ ∃x_{𝔨+1} :∈V_{ξ_{𝔨+1}} Ψ(x_{𝔨+1}, y⃗)
⟺ ∃x_{𝔨+1} :∈V_{ξ_{𝔨+1}} ∀x_{𝔨}:∈V_{ξ_{𝔨}} … Q_{2}x_{2} :∈V_{ξ_{2}} Q_{1}x_{1} :∈V_{ξ_{1}} Φ_{0}(x_{1}, …, x_{𝔨}, x_{𝔨+1}, y⃗).
⊣ (2·12)

3: Proof of the main theorem

Logik(Σ_{0}) is trivial; we are given Separation(Σ_{0}); we have established Minimization(Π_{0}), Strong Collection(Π_{0}) and Logik(Σ_{1}); and now for each 𝔨 = 1, 2, …, having obtained Logik(Σ_{𝔨}), we obtain

successively Separation(Σ_{𝔨}), Minimization(Π_{𝔨}), Strong Collection(Π_{𝔨}) , and Logik(Σ_{𝔨+1}). Thence we may

derive all instances of the schemes of Replacement and Foundation.

We have proved 3·0 METATHEOREM All instances of the schemes of Separation, Collection, Replacement and Foundation are derivable in the system M_{1} + Repcoll.

4: Closing remarks

Our proof has used TCo but not the Axiom of Infinity. If we replace TCo by the axiom of infinity in our base theory, we may, as we show below, derive TCo, and thus the rest of our argument will hold good, yielding this second result: 4·0 METATHEOREM All instances of the schemes of Separation, Collection, Replacement and Foundation are derivable in the system M_{0} + Foundation + Repcoll + ω ∈ V.

Thus it remains only to establish the following 4·1 PROPOSITION TCo is provable in M_{0} + Foundation + Repcoll + ω ∈ V. Proof : Fix a set x. For 0 < n < ω, we define an attempt of length n to be a function f defined on n such that f(0) = x and that ∀m(m + 1 < n ⟹ f(m + 1) = ⋃ f(m)). Given two distinct attempts f and g with the same domain n, we may use Foundation for sets to find the least m < n such that f(m) ≠ g(m), and thence obtain a contradiction showing f = g. Thus for each n there is at most one attempt of length n.

Hence we may, for each n, define G(n) to be the unique attempt of length n, if it exists, and to be 0 otherwise. By Repcoll, there is a set v which contains all values of G.

Now the property of being an attempt is Δ_{0} in the parameter x; hence we may apply Δ_{0} Separation to v to form the set v̄ of all attempts, and show that the union of the set of all attempts is a function, with domain ⋃ {n | ∃f:∈v̄ dom f = n}, the supremum of the lengths of all attempts; which will be ω if we are lucky, and some n̄ < ω if we are not. But in the latter case, the given union will itself be an attempt and we may extend it to an attempt of length n̄+1, a contradiction.

Thus the union of the set of attempts will be a function of domain ω, and the union of its values will be the desired transitive closure of x. ⊣ (4·1)

Without Infinity

It follows from the work of Hájek and Vopěnka [HV] and of K. Hauschild [H, Theorem II] that TCo is not provable in ZF without the axiom of infinity but with the set form of Foundation. The reason is slightly indirect: class forms of foundation may be derived from the set form if use of TCo is permitted: and that statement may be construed as applying both to set theories like ZF and to class theories like NBG. First Hájek and Vopěnka (for NBG) and then Hauschild (for ZF) have shown that if the axiom of infinity be dropped from either system, then a failure of class foundation may occur.

Hauschild’s construction is roughly this: reason in a universe containing a set C_{0} of distinct objects c_{i} (for i ∈ ω) such that for each i, c_{i} = {c_{i+1}}; then, treating the elements of C_{0} as Urelemente, form the sequence C_{i} where C_{i+1} is the set of all finite subsets of C_{i}, and consider its union ⋃_{i∈ω} C_{i}. That will be a model of ZF less the axiom of infinity, and in it, c_{0} is a member of no transitive set, since any such would have to contain c_{1}, c_{2}, …; but all members of the model are finite sets.

Let us look further at Hauschild’s model. Something must go awry, for if each set has a rank, and each class {x | ϱ(x) < ζ} is a set, then TCo holds.

In this model, Repcoll is true, plus all the axioms of M_{0}, plus set foundation.

All instances of Separation are true, as are all instances of Strong Collection; so there must be a failure of Π_{1} foundation, since TCo is provable using Δ_{0} separation, Δ_{0} collection, elementary set theory and Π_{1} foundation; and indeed we know what failure that will be: the class of those sets that are not members of a transitive set can have no minimal element.

There is also a failure of Σ_{1} foundation. The set C_{0} is a class of the model, being definable as the set of all sets at the tail end of a finite ∈-chain starting from c_{0}, and it has no ∈-minimal element. As we have set foundation and full separation, we may conclude that rank is not definable in that model.

Our base theory above has been M_{1} + Repcoll: and the principle TCo has played an important part in our proof. As we have not used the axiom of infinity, Hauschild’s result shows that we must needs add TCo explicitly to our base theory for our proof to succeed.

In Hauschild’s model, Logik and Minimization become false or, rather, meaningless, as one uses the notion of rank and the other the set-hood of the V_{ζ}’s. Separation and Strong Collection make no mention of either, so it is a beguiling question whether part of our theorem might still hold without TCo.

Without Power Set

Finally, I am grateful to Robert Lubarsky for drawing my attention to the paper [Z] of Andrzej Zarach in which he constructs a model of TCo and Replacement, but without Power Set, in which Collection fails. In such a model, Repcoll will hold, it being trivially weaker than Replacement, and hence the essential character of our use of the Power Set Axiom is confirmed.

R E F E R E N C E S

[HV] P. Hájek and P. Vopěnka, Über die Gültigkeit des Fundierungsaxioms in speziellen Systemen der Mengentheorie, Zeitschr. f. math Logik und Grundlagen d. Math. 9 (1963) 235–241.

[H] K. Hauschild, Bemerkungen, das Fundierungsaxiom betreffend, Zeitschr. f. math. Logik und Grundlagen d. Math. 12 (1966) 51–56.

[M] A. R. D. Mathias, The Strength of Mac Lane Set Theory, Annals of Pure and Applied Logic, 110 (2001) 107–234.

[Z] A. Zarach, Springer Lecture Notes in Logic 6 (1996) 307–322.

16·iv·2002
revised 29·ii·2004
further revised 29·viii·2004
final revision 7·i·2005