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
.
□