[FOM] Cantor Bendixson and the Axiom of Replacement

[D.R. MacIver]

Cantor Bendixson is the following theorem (usually stated for R I think):

Let X be a topological space and E \subseteq X a closed subset. E contains 
a unique largest perfect subset, k(E). (A \subseteq X is perfect if it is 
closed and every element of A is a limit point of A).

The usual proof is this: 

Uniqueness is obvious - if you have two largest perfect subsets they're 
each subsets of the other and so equal.

Define a transfinite sequence E_a as follows:

E_0 = E
E_{a+} = { x : x is a limit point of E_a}

and taking intersections at limit ordinals.

It's clear that each E_a is closed, and so in particular this is a 
decreasing sequence as a closed set contains all its limit points. Usual 
arguments involving Hartog's lemma imply that it's eventually constant, and 
so must terminate in a perfect set, k(E).

Suppose F is a perfect subset of E. We can show by induction that for all 
a, F is a subset of E_a, as if F \subseteq E_a then every point in F is a 
limit point of E_a, and so F \subseteq E_{a+}. Thus F \subseteq k(E), and 
so k(E) is the largest perfect subset of E.

Now, the question is this. Can we proof this theorem in Z set theory? i.e. 
ZF without the axioms of foundation (which shouldn't matter) or replacement 
(which we used crucially there - once in constructing the ordinals, and 
once in the existence of the Hartog ordinal that means the sequence must be 
eventually constant)?

We can prove it in Z + AC, by replacing transfinite induction on the 
ordinals with transfinite induction on a well ordering of P(P(X)) - we'd 
have an injection from P(P(X)) into P(X), which we can't by cantor's 
theorem.

I was wondering if there might be a proof using the bourbaki-witt fixed 
point theorem, which is a theorem of Z set theory (I think), but I haven't 
found one yet.

David MacIver