Trying to suggest to Lispers a way to omit parentheses is
like trying to suggest to Haskellers a way to omit monads.

AC is not refutable in ZF - Part 3
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 V-hierarchy.
  • V_0:=\emptyset
  • V_{\kappa+1}:=\mathbb{P}(V_{\kappa})
  • V_\lambda := \bigcup_{\gamma<\lambda} V_\gamma for limes-ordinals \lambda
Furthermore, we have V_\alpha\subseteq V_\beta for \alpha\le\beta, which can be shown by a trivial inductive argument.

Theorem: We have V=\bigcup_{\gamma\in On} V_\gamma.
Proof: Assume there was an x\in V which is not in V_\alpha for some \alpha. Then it cannot be subset of any V_\alpha, since otherwise it would be element of V_{\alpha+1}. Therefore it must contain an element x' which is not in V_\alpha for every \alpha as well. That is, every set not being in any of the V_\alpha must contain a set not being in any of the V_\alpha, hence, we would get an infinite \ni-chain, which contradicts (FUN). □

Definition: The relativization \phi^W of a formula \phi regarding a class W is defined inductively over the structure on \phi by:
  • \bot^W := \bot
  • (x=y)^W := (x=y)
  • (x\in y)^W := x\in y
  • (\phi\wedge\psi)^W:=\phi^W\wedge\psi^W
  • (\forall_x \phi)^W := \forall_x (x\in W \rightarrow \phi^W)
Intuitively, \phi^W means that \phi holds in W. We will later write W\models\phi to denote that \phi^W holds, defining yet another additional meaning for \models.

Definition: A class W is called inner model of ZF, if it satisfies
  • for all x\in W we have x\subseteq W
  • On\subseteq W
  • for all axioms \phi of ZF we have ZF\models\phi^W
Remark: V is an inner model of ZF, since \phi=\phi^V.

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

Remark: Let W be an inner model of ZF, and {\mathcal M} be a model of ZF with domain M and the \in-relation interpreted by a relation \epsilon\subseteq M^2. Let N=\{a\in M|{\mathcal M}\models a\in W\} and \mathcal N be an interpretation with domain N and \in-relation \epsilon\cap N^2. Then {\mathcal N}\models ZF.

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 \Sigma_0-formula, if every quantifier is bounded, that is, every universal quantifier is of the form \forall_x (x\in y\rightarrow \phi), and equivalently, every existential quantifier is of the form \exists_x (x\in y \wedge \phi). (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 x=y is a \Sigma_0-formula.

We write \forall_{x\in y} \phi for \forall_x (x\in y\rightarrow \phi), and \exists_{x\in y} \phi for \exists_x (x\in y\wedge\phi). Furthermore, if we want to denote a list of variables, then we use the vector notation \vec{x}, and we will use \forall_{\vec{x}} to denote the universal quantification over all of these variables.

Theorem I: Let W be a class. Then the following propositions are equivalent:
  • a. W is an inner model
  • b. W satisfies:
    • (I1) Every element of W is a subset of W
    • (I2) For every x\subseteq W there is an element y\in W such that x\subseteq y
    • (I3) For every \Sigma_0-formula \phi(x,\vec{z}) we have \forall_{\vec{z}\in W}\forall_{u\in W} \{x\in u|\phi(x,\vec{z})\}\in W
To proof Theorem I, some additional work needs to be done. Firstly, we will replace the replacement scheme by two other schemes:

\Sigma_0-comprehension: For every \Sigma_0-formula \phi(x,\vec{z}) we have \forall_{\vec{z}}\forall_u\{x\in u|\phi(x,\vec{z})\}\in V.

Limitation: For every ZF-formula \phi(x,y,\vec{z}) we have \forall_{\vec{z}}\forall_u\exists_v\forall_{x\in u} ((\exists_y \phi(x,y,\vec{z}))\rightarrow \exists_{y\in v}\phi(x,y,\vec{z}))

Theorem: These schemes are derivable from ZF.
Proof: \Sigma_0-comprehension follows by general comprehension, which follows by (RPL). For limitation, let \phi, \vec{z} and u be given, and a=\{x\in u|\exists_y\phi(x,y,\vec{z})\}. Define a function g:a\rightarrow On, g(x)=\min\{\gamma|\exists_{y\in V_\gamma}\phi(x,y,\vec{z})\}; this is well-defined, since such a \gamma always exists according to the above theorem. Then the range of g is a set of ordinals, and therefore has a supremum \alpha. Now set v=V_\alpha. Then v contains an y for every x, such that \phi(x,y,\vec{z}).
□

We now show the converse, these schemes imply replacement.

Lemma: For every ZF-formula \phi(\vec{x}), \forall_{u_1}\ldots\forall_{u_n}\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}\in V can be shown by \Sigma_0-comprehension and limitation, not using full comprehension.
Proof: Recall that for pairs \left<x,y\right>:=\{\{x,y\},\{x\}\}\}. We show that from u,v\in V follows u\cap v,u\backslash v,u\times v\in V: u\cap v=\{x\in u\cup v| x\in u\wedge x\in v\}, u\backslash v = \{x\in u|x\not\in v\} are sets by \Sigma_0-comprehension. By limitation, there exists a set b such that for all x\in u we have an y\in b with \forall_{z\in v} \left<x,z\right>\in y. That is, b contains a superset of \{x\}\times v for every x\in u, that is \bigcup_{r\in b}\{r\} is a superset of u\times v, thus, u\times v=\{a \in \bigcup_{r\in b}\{r\}| \exists_{x\in u}\exists_{y\in v} a=\{\{x,y\},\{x\}\}\} is a set due to \Sigma_0-comprehension.

We now use structural induction on \phi(\vec{x}).

If \phi(\vec{x})=\bot, then \emptyset is the desired set.

If \phi(\vec{x}) is of the form x_i\in x_j, let u_1,\ldots,u_n be given and let W=\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=\{z\in u_1\times\ldots\times u_n|\exists_{x_1\in u_1}\ldots\exists_{x_n\in u_n} (z=\left<x_1,\ldots,x_n\right>\wedge x_i\in x_j)\}, and \exists_{x_1\in u_1}\ldots\exists_{x_n\in u_n} (z=\left<x_1,\ldots,x_n\right>\wedge x_i\in x_j) is a \Sigma_0-formula, which means that W is a set by \Sigma_0-comprehension.

If \phi(\vec{x}) is of the form \phi_1(\vec{x})\wedge\phi_2(\vec{x}), then \{\left<x_1,\ldots,x_n\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=\{\left<x_1,\ldots,x_n\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}\cap\{\left<x_1,\ldots,x_n\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\} and these are both sets by induction.

For \phi(\vec{x})=\phi_1(\vec{x})\rightarrow\phi_2(\vec{x}) notice that \phi(\vec{x})\leftrightarrow \lnot (\phi_1(\vec{x})\wedge\lnot\phi_2(\vec{x})), therefore it is sufficient to show the induction step for negations. Thus, let \phi(\vec{x})=\lnot\phi_3(\vec{x}). Then \{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=u_1\times\ldots\times u_n \backslash \{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi_3(\vec{x})\} which is a set by induction.

For \phi(\vec{x}) = \forall_y \phi_1(\vec{x},y), by limitation we have a set v\in V with \forall_{x_1\in u_1}\ldots\forall_{x_n\in u_n}((\exists_y \lnot\phi_1(\vec{x},y))\rightarrow\exists_{y\in v}\lnot\phi_1(\vec{x},y)). By induction hypothesis, q=\{\left<\vec{x},y\right>\in u_1\times\ldots\times u_n\times v|\phi_1(\vec{x},y)\}\in V, and therefore a=u_1\times\ldots\times u_n\times v-q=\{\left<\vec{x},y\right>\in u_1\times\ldots\times u_n\times v|\lnot\phi_1(\vec{x},y)\}\in V. Therefore, by \Sigma_0-comprehension, b=\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\exists_x\lnot\phi_1(\vec{x})\}=\{z\in u_1\times\ldots\times u_n|\exists_{y\in v}\left<z,y\right>\in a\}\in V, therefore, \{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=u_1\times\ldots\times u_n-b\in V.
□
Lemma: For \Sigma_0-formulae \phi(\vec{x}) and classes W such that x\in W\Rightarrow x\subseteq W follows \forall_{\vec{x}\in W} (\phi(\vec{x})\leftrightarrow\phi^W(\vec{x})).
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 \forall_x\phi\leftrightarrow\lnot\exists_x\lnot\phi. So let \phi(\vec{x})=\exists_{z\in y}\psi(z,\vec{x},y). We may assume that x\neq y, since otherwise the formula would be equivalent to \bot. Let \vec{x},y\in W, then by induction hypothesis \psi^W(z,\vec{x},y)\rightarrow\psi(z,\vec{x},y), and therefore \phi^W(\vec{x},y)\rightarrow\phi(\vec{x},y). For the other direction, assume \phi(\vec{x},y), that is, there is some z\in y such that \psi(z,\vec{x},y). Then y\in W implies y\subseteq W which implies z\in W, so by induction hypothesis, \psi^W(z,\vec{x},y), and since z\in W we have \exists_{z\in y\cap W}\psi^W(z,\vec{x},y), therefore \phi^W(\vec{x}).
□
Corollary: For \Sigma_0-formulae \psi(\vec{x},\vec{y}) and classes W in which every element is a subset we have \forall_{\vec{y}\in W}((\forall_{\vec{x}}\psi(\vec{x},\vec{y}))\rightarrow\forall_{\vec{x}\in W}\psi^W(\vec{x},\vec{y}) and \forall_{\vec{y}\in W}((\exists_{\vec{x}}\psi(\vec{x},\vec{y}))\leftarrow\exists_{\vec{x}\in W}\psi^W(\vec{x},\vec{y})

Theorem: From \Sigma_0-comprehension and limitation follows replacement.
Proof: Let F be a functor, and u\in v. By limitation we get a v\in V with \forall_{x\in u} ((\exists_y F(x)=y)\rightarrow \exists_{y\in v} F(x)=y). Then \{F(x)|x\in u\}=\{y\in v|\exists_{x\in u} F(x)=y\}\in V by the above Lemma.
□

We finally arrive at...

Proof of Theorem I: "a=>b": (I1) by definition. For (I2), consider the V_\alpha-hierarchy inside W, that is, define W_\alpha := V_\alpha^W. For x\in V,x\subseteq W we can find an \alpha such t hat x\subseteq W_\alpha, and W_\alpha\in W. For (I3), let \phi(x,\vec{z}) be a \Sigma_0-formula and let \vec{z}\in W. Because of (I1) we have \phi(x,\vec{z})\leftrightarrow\phi^W(x,\vec{z}) for all x\in W according to the above lemma. Therefore, for every u\in W, \{x\in u|\phi(x,\vec{z})\}=\{x\in u\cap W|\phi^W(x,\vec{z})\}, which is in W by comprehension.
"b=>a": Trivially, On\cap W is transitive, and as every transitive set of ordinals is an ordinal, either On\cap W\in On or On\cap W = On. Assume On\cap W\in On, then by (I2) we have an y\in W such that On\cap W\subseteq y. But On\cap W = \{x\in y|x\in On\} which is in W by (I3), so On\cap W\in On\cap W. Contradiction. Therefore, On\subseteq W. We show the ZF-axioms. (EXT) and (FUN) hold because of the above Corollary, (NUL) and (INF) hold since \omega,\emptyset\in On\subseteq W.  For (UNI), let x\in W, then x\subseteq W and therefore every y\in x is subset of W, therefore \bigcup_{y\in x}y\in W and according to (I2) we find a superset u\in W. But then, \bigcup_{y\in x}y = \{y\in u|\exists_{z\in x} y\in z\}\in W by (I3). Similar for (PAR). For (POW), let x\in W. Then by (I2), since \mathbb{P}(x)\cap W\subseteq W, there exists an u\in W such that \mathbb{P}(x)\cap W\subseteq u. Then by (I3), \mathbb{P}(x)\cap W=\{z\in u|z\subseteq x\}\in W.
We have proven that replacement can be replaced by \Sigma_0-comprehension and limitation, therefore, we show \Sigma_0-comprehension and limitation in W. For \Sigma_0-comprehension, let \phi(x,\vec{z}) be a \Sigma_0-formula. We have to show that \forall_{\vec{z}\in W}\forall_{u\in W}\{x\in u|\phi^W(x,\vec{z})\}\in W. But by the above Lemma, this is the same set as \{x\in u|\phi^W(x,\vec{z})\}, which is in W according to (I3). For limitation, consider again a \Sigma_0-formula \phi(x,y,\vec{z}). Then we have to show \forall_{\vec{z}\in W}\forall_{\vec{u}\in W}\exists_{v\in W}\forall_{x\in U}((\exists_{y\in W}\phi^W(x,y,\vec{z}))\rightarrow\exists_{y\in v}\phi^W(x,y,\vec{z})). Let \vec{z},u\in W, then there exists a v'\in V such that \forall_{x\in u}((\exists_{y\in W}\phi^W(x,y,\vec{z}))\rightarrow\exists_{y\in v'} (y\in W\wedge \phi^W(x,y,\vec{z}))). By (I2) we get a v\in W such that v'\cap W\subseteq v, which trivially satisfies the above formula.
□