This is part 3 of my posts about
the irrefutability of AC in ZF.
We define a hierarchy of sets, the

-
hierarchy.
Furthermore, we have

for

, which can be shown by a trivial
inductive argument.
Theorem: We have

.
Proof: Assume there was an

which is not in

for some

. Then it cannot be subset of any

, since otherwise it would be element of

. Therefore it must contain an element

which is not in

for every

as well. That is, every set not being in any of the

must contain a set not being in any of the

, hence, we would get an infinite

-chain, which contradicts (FUN). □
Definition: The
relativization 
of a formula

regarding a class

is defined inductively over the structure on

by:
Intuitively,

means that

holds in

. We will later write

to denote that

holds, defining yet another additional meaning for

.
Definition: A class

is called
inner model of ZF, if it satisfies
- for all
we have 

- for all axioms
of ZF we have 
Remark: 
is an inner model of ZF, since

.
Inner models provide a way of getting new models from models of ZF:
Remark: Let

be an inner model of ZF, and

be a model of ZF with domain

and the

-relation interpreted by a relation

. Let

and

be an interpretation with domain

and

-relation

. Then

.
Therefore, it is sufficient to give an inner model of ZF satisfying AC to show that AC is not refutable: From a model of ZF, we would get a model of ZF satisfying AC. That is what we are going to do. Before we can do this, we have to do some work to give an alternative classification of inner models.
Definition: A formula is called

-
formula, if every quantifier is
bounded, that is, every universal quantifier is of the form

, and equivalently, every existential quantifier is of the form

. (Recall that our language does not contain existential quantifiers directly, but defines them by universal quantifiers. However, our definition is equivalent to what we would get directly.)
Notice that

is a

-formula.
We write

for

, and

for

. Furthermore, if we want to denote a list of variables, then we use the vector notation

, and we will use

to denote the universal quantification over all of these variables.
Theorem I: Let

be a class. Then the following propositions are equivalent:
- a.
is an inner model - b.
satisfies: - (I1) Every element of
is a subset of 
- (I2) For every
there is an element
such that 
- (I3) For every
-formula
we have 
To proof Theorem I, some additional work needs to be done. Firstly, we will replace the replacement scheme by two other schemes:
-comprehension: For every

-formula

we have

.
Limitation: For every ZF-formula

we have

Theorem: These schemes are derivable from ZF.
Proof: 
-comprehension follows by general comprehension, which follows by (RPL). For limitation, let

,

and

be given, and

. Define a function

; this is well-defined, since such a

always exists according to the above theorem. Then the range of

is a set of ordinals, and therefore has a supremum

. Now set

. Then

contains an

for every

, such that

.
□
We now show the converse, these schemes imply replacement.
Lemma: For every ZF-formula

,

can be shown by

-comprehension and limitation, not using full comprehension.
Proof: Recall that for pairs

. We show that from

follows

:

,

are sets by

-comprehension. By limitation, there exists a set

such that for all

we have an

with

. That is,

contains a superset of

for every

, that is

is a superset of

, thus,

is a set due to

-comprehension.
We now use structural induction on

.
If

, then

is the desired set.
If

is of the form

, let

be given and let


, and

is a

-formula, which means that

is a set by

-comprehension.
If

is of the form

, then



and these are both sets by induction.
For

notice that

, therefore it is sufficient to show the induction step for negations. Thus, let

. Then

which is a set by induction.
For

, by limitation we have a set

with

. By induction hypothesis,

, and therefore


. Therefore, by

-comprehension,


, therefore,

.
□
Lemma: For

-formulae

and classes

such that

follows

.
Proof: By structural induction. For everything except quantors, the relativization can be looped through. For quantors, we may assume that we always have an existential quantifier, since

. So let

. We may assume that

, since otherwise the formula would be equivalent to

. Let

, then by induction hypothesis

, and therefore

. For the other direction, assume

, that is, there is some

such that

. Then

implies

which implies

, so by induction hypothesis,

, and since

we have

, therefore

.
□
Corollary: For

-formulae

and classes

in which every element is a subset we have

and
Theorem: From

-comprehension and limitation follows replacement.
Proof: Let

be a functor, and

. By limitation we get a

with

. Then

by the above Lemma.
□
We finally arrive at...
Proof of Theorem I: "a=>b": (I1) by definition. For (I2), consider the

-hierarchy inside

, that is, define

. For

we can find an

such t hat

, and

. For (I3), let

be a

-formula and let

. Because of (I1) we have

for all

according to the above lemma. Therefore, for every

,

, which is in

by comprehension.
"b=>a": Trivially,

is transitive, and as every transitive set of ordinals is an ordinal, either

or

. Assume

, then by (I2) we have an

such that

. But

which is in

by (I3), so

. Contradiction. Therefore,

. We show the ZF-axioms. (EXT) and (FUN) hold because of the above Corollary, (NUL) and (INF) hold since

. For (UNI), let

, then

and therefore every

is subset of

, therefore

and according to (I2) we find a superset

. But then,

by (I3). Similar for (PAR). For (POW), let

. Then by (I2), since

, there exists an

such that

. Then by (I3),

.
We have proven that replacement can be replaced by

-comprehension and limitation, therefore, we show

-comprehension and limitation in

. For

-comprehension, let

be a

-formula. We have to show that

. But by the above Lemma, this is the same set as

, which is in

according to (I3). For limitation, consider again a

-formula

. Then we have to show

. Let

, then there exists a

such that

. By (I2) we get a

such that

, which trivially satisfies the above formula.
□