Sun, 09 Oct 2011 20:15:00 GMT

This is part 3 of my posts about the irrefutability of AC in ZF.

We define a hierarchy of sets, the -**hierarchy**.

**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:

Definition: A class is called**inner model** of ZF, if it satisfies

**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:

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

We define a hierarchy of sets, the -

- for limes-ordinals

Definition: The

Definition: A class is called

- for all we have
- for all axioms of ZF we have

Inner models provide a way of getting new models from models of ZF:

Remark:

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 -

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.

- 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

Theorem:

□

We now show the converse, these schemes imply replacement.

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

□

□

□

We finally arrive at...

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

□

Show comments (Requires JavaScript, loads external content and cookies from Disqus.com)