Wed, 12 Oct 2011 21:39:00 GMT

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 .

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 .

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

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

Definition: The class of

Since , trivially .

"<=": For and we have . Therefore, .

□

□

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

□

Then is surjective.

□

□

is a well-ordering, and . Thus, in , the well-ordering theorem holds, therefore, AC holds in .

□