So, finally, this is part 4 of my
series about the irrefutability of the AC from ZF. We are almost there!
Theorem 1: Let ZF-Formulae

be given. Then

. We then say that
reflects the

.
Proof: Let

be given. Without loss of generality we may assume that the

can be written without universal quantifiers, as we can replace every universal quantifier by a negated existential quantifier of the negated quantfied formula.
Recursively define a sequence

where

and

is the smallest ordinal

, such that if

is a subformula of one of the

, we have

. Let

be the supremum of the

. It is sufficient to show that for all subformulae

of any

we have

, which goes by structural induction. If

is of the form

this is trivial. The step over

is clear. We can assume that every occurence of

is in the scope of an occurence of

, and therefore, instead of having an induction step for

, we have an induction step for

:

, and let

. By induction hypothesis,

. For the other direction, let

, then

. By induction hypothesis, we have

.
□
We can do everything we did in Part 1 as well directly in ZF. Alphabets become sets, and formulae become finite sequences. Especially, there is a set of all formulae, which is countable. Notice that there is no need to fix a special "encoding" for formulae, it is clear that one exists, and it is clear that all such encodings have to be equivalent. For a ZF-formula

, let

be its embedding into ZF, that is,

is a set.
For every set

we can define an interpretation, interpreting

by

. We write

if this interpretation (for all valuations) models

, notice that in this case,

is a relation inside ZF. Trivially, we have

.
Definition: Now we can define the class of

of
ordinal definable sets:

where we write

to denote that there must exist an encoded ZF-formula.
This class is interesting, as it messes around with the intuition about two meta-layers. However, it is not yet our goal.
Definition: The
transitive closure 
of a set

is the smallest

such that every element of

is also subset of

.
Definition: The class

of
hereditary ordinal definable sets is defined by

Since

, trivially

.
Lemma 1: 
.
Proof: "=>": From

directly follows

, therefore,

. For

we have

, that is,

, therefore,

.
"<=": For

and

we have

. Therefore,

.
□
Lemma 2: For every ZF-formula

we have

.
Proof: Let

,

such that

, and

. By Theorem 1 there is a

such that

reflects

, therefore

.
□
Theorem 2: 
is an inner model.
Proof: Due to Part 3, it is sufficient to show (I1), (I2) and (I3). By Lemma 1, (I1) holds.
Let

, and

such that

. Then trivially,

. But by Lemma 2 we have

. Trivially, we also have

, so by Lemma 1,

. Thus, (I2) holds.
For (I3), let

be a

-formula, choose arbitrary

, and let

. Then

by (I1), so by Lemma 1, it is sufficient to show that

. As

we have

, therefore there are

and

and for

there are

,

sucht hat

and

. Let

, and

. By Theorem 1 we get a

such that

reflects

. Therefore



which is in

. Therefore,

.
□
Lemma 3: There exists a surjective functor

.
Proof: In Part 2 we proved that there is a bijection

, so it is sufficient to give a surjective functor

. Now let

be an enumeration of all ZF-formulae. Define

Then

is surjective.
□
Lemma 4: There exists a surjective functor
Proof: Since

, use

.
□
Theorem: (AC) holds in
Proof: By Lemma 4, we have our surjective

. For

, define

. By Lemma 2 we know that for every

,

, and since

, we have

. Let

be arbitrary but fixed. Then there exists an

such that

. Now define a well-ordering

by


is a well-ordering, and

. Thus, in

, the well-ordering theorem holds, therefore, AC holds in

.
□