\documentclass{amsart}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{mathabx}
\usepackage{stmaryrd}


\theoremstyle{plain}
\newtheorem{thm}{Theorem}[section]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}



\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition}
\newtheorem{exer}{Exercise}
\newtheorem{exam}{Example}


\theoremstyle{remark}
\newtheorem{rem}[thm]{Remark}
\newtheorem{fact}[thm]{Fact}
\newtheorem{hyp}[thm]{Hypothesis}

\newcommand{\Q}{\mathbb{Q}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\res}{\restriction}
\newcommand{\dom}{\operatorname{dom}}
\newcommand{\ran}{\operatorname{ran}}
\newcommand{\cof}{\operatorname{cof}}
\newcommand{\ot}{\text{o.t.}}
\newcommand{\on}{\text{ON}}
\newcommand{\card}{\text{CARD}}
\newcommand{\ac}{\text{AC}}
\newcommand{\zf}{\text{ZF}}
\newcommand{\zfc}{\text{ZFC}}
\newcommand{\sP}{\mathcal{P}}
\newcommand{\sL}{\mathcal{L}}
\newcommand{\ch}{\text{CH}}
\newcommand{\gch}{\text{GCH}}
\newcommand{\vb}{\text{var}}
\newcommand{\pa}{\text{PA}}
\newcommand{\fa}{\text{F}}
\newcommand{\con}{\text{CON}}


\newcommand{\bz}{\boldsymbol{0}}
\newcommand{\lD}{{\Delta}}
\newcommand{\lS}{{\Sigma}}
\newcommand{\lP}{{\Pi}}
\newcommand{\models}{\vDash}
\newcommand{\proves}{\vdash}
\newcommand{\sg}{\text{sg}}
\newcommand{\seq}{\text{Seq}}
\newcommand{\lh}{\text{lh}}
\newcommand{\pred}{\text{pred}}
\newcommand{\hod}{\text{HOD}}
\newcommand{\od}{\text{OD}}
\newcommand{\trcl}{\text{tr\,cl}}
\newcommand{\cl}{\text{cl}}
\newcommand{\rank}[1]{|#1|}
\newcommand{\llex}{<_{\text{lex}}}




\begin{document}




\begin{center}
\bf $V_\kappa$, $H_\kappa$, and $\hod$
\end{center}
\bigskip



Recall that working in $\zf$ (in fact, $\zf-$Power) we have previously
defined $V_\alpha$ for all $\alpha \in \on$. Recall that $V_\alpha$
consists of all sets of rank $< \alpha$ (remember $V_\alpha$ is
a set). The next lemma shows what axioms of set theory hold in these
sets. 


\begin{lem} \label{vk}
Assume $\zf$. Then for any limit ordinal $\alpha> \omega$, 
$V_\alpha \models \zf-$Replacement. Assuming $\zfc$, for any limit
ordinal $\alpha> \omega$, $V_\alpha \models \zfc-$Replacement. 
\end{lem}


\begin{proof}
The empty set axiom holds in $V_\alpha$ as $\emptyset \in V_\alpha$
and the statement $\phi(x)=\neg \exists y \in x$ is $\lD_0$
so absolute. If $x,y \in V_\alpha$ then $\{ x,y \}$ in $V_\alpha$
as $\alpha$ is a limit. Since the statement 
$\phi(x,y,z)=[ x \in z \wedge y \in z \wedge \forall w \in z\ (w \approx
x \vee w \approx y)]$ is $\lD_0$, hence absolute, it follows that 
$V_\alpha \models$ pairing. The union axiom is similar. 
By downwards absoluteness, foundation holds in any class (since we assuming
foundation holds in $V$), so it holds in $V_\alpha$. Since $\alpha >
\omega$, $\omega \in V_\alpha$. As the statement $\phi(x)=$``$x=
\omega$'' is absolute, $V_\alpha \models$ infinity. Extensionality 
holds in $V_\alpha$ as $V_\alpha$ is transitive. 
If $x \in V_\alpha$, then $\sP(x) \in V_\alpha$ as $\alpha$ is a limit. 
The statement $\phi(x,y)=[y=\sP(x)]$, written out, is $\lP_1$ and
hence downwards absolute. Since $v \models \phi(x,\sP(x)$, it follows that 
$V_\alpha \models \phi(x,\sP(x))$. Hence $V_\alpha \models$ Power set. 
To see comprehension, let $\phi(x_1,\dots,x_n,y,z)$ be a formula and
let $a_1,\dots,a_n, b \in V_\alpha$. By comprehension in $V$ applied 
to the formula $\phi^{V_\alpha}(\vec x,y,z)$ (which has the extra
parameter $V_\alpha$ in it)
there is set $w$ such that $\forall z\ (z \in w \leftrightarrow z \in b \wedge 
\phi^{V_\alpha}(\vec a, b, z))$.  Since $b \in V_\alpha$, we also have 
$w \in V_\alpha$. Hence $V_\alpha \models 
\exists w\ \forall z\ (z \in w \leftrightarrow z \in b \wedge 
\phi(\vec a, b, z))$, and so $V_\alpha \models$ Comprehension. 
Finally, suppose $\ac$ holds in $V$. Let $a \in V_\alpha$. By 
$\ac$ in $V$, let $\prec$ be a wellordering of $a$. Since 
$\prec \in \sP \sP \sP (a)$ and $\alpha$ is limit, $\prec \in 
V_\alpha$. The statement $\phi(x,y)=[y$ is a wellordering of$x]$ 
is $\lP_1$, and since it holds in $V$ it holds in $V_\alpha$. Thus,
$V_\alpha \models \ac$. 
\end{proof}


Thus, in $\zf$ we can prove that there are set models for all 
of $\zf$ except replacement. More precisely, for any formulas $\phi$
of $\zf-$Replacement, $\zf \proves \forall \alpha ( \alpha > \omega \wedge 
\alpha $ limit$ \rightarrow \phi^{V_\alpha})$. 


\begin{cor} \label{noreplace}
$\zf-$Replacement $ \nvdash \zf$. 
\end{cor}

\begin{proof}
Replacement clearly does not hold in $V_{\omega \cdot 2}$. 
Let $\phi$ be an instance of replacement so that $\zf \proves
(\neg \phi)^{V_{\omega \cdot 2}}$. If $\zf-$Replacement $\proves 
\zf$, then there would be finitely many axioms $\{\psi_1,\dots,\psi_n\}$
of $\zf-$Replacement such that $\{\psi_1,\dots,\psi_n\} \proves \phi$. 
But, $\zf \proves \psi_1^{V_{\omega \cdot 2}} \wedge \dots \wedge 
\psi_n^{V_{\omega \cdot 2}}$, and so $\zf \proves \phi^{V_{\omega \cdot 2}}$,
a contradiction. 
\end{proof}


In the proof of corollary~\ref{noreplace} we have implicitly
assumed the consistency of $\zf$, though we could get by just assuming the
consistency of $\zf-$Replacement. 


\begin{exer}
Just assuming the consistency of $\zf-$Replacement, show that 
$\zf-$Replacement $ \nvdash \zf$. (hint: let $\phi$ be the instance
of replacement 
which gives the existence of $\omega \cdot 2$. If $\zf-$Replacement
$\nvdash \phi$, we're done, so assume $\zf-$Replacement $\proves \phi$. 
Now follow the above prove for this $\phi$.)
\end{exer}


\begin{exer}
Let $\psi_1,\dots,\psi_n\}$ be axioms of $\zf$. Show that 
$\zf-$Replacement $\cup \{ \psi_1, \dots, \psi_n \} \nvdash 
\zf$. (hint: Working in $\zf$, show that there is a least limit ordinal 
$\alpha > \omega$ such that $V_\alpha \models \psi_1 \wedge \dots \wedge 
\psi_n$. Argue then that there must be a smaller limit ordinal $\beta < \alpha$
such that $V_\beta \models \psi_1 \wedge \dots \wedge \psi_n$.)
\end{exer}






We now define another family of sets called the $H_\kappa$. 
If $P$ is any property, we say set $x$ hereditarily has property 
$P$ if every element of the transitive closure of $x$ has property $P$.

\begin{defn} ($\zfc$)
Let $\kappa$ be an infinite regular cardinal. $H_\kappa$ is the
collection of sets which hereditarily have size less than $\kappa$, 
that is, every element of the transitive closure of $x$ has 
cardinality $< \kappa$. 
\end{defn}


We first give a simple reformulation of the definition.


\begin{lem}
For all sets $x$, $x \in H_\kappa$ iff $| \trcl(x) | < \kappa$. 
\end{lem}


\begin{proof}
Clearly if $| \trcl(x) | < \kappa$ then $x \in H_\kappa$. Suppose now 
$x \in H_\kappa$. Recall $\cl_n(x)$ is defined by: 
$\cl_0(x)=x$, $\cl_{n+1}(x)= \cl_n(x) \cup (\cup \cl_n(x))$. 
If we assume inductively that $|\cl_n(x)| < \kappa$, 
then $\cl_{n+1}(x)$ is a $< \kappa$ union of sets each of which has
size $< \kappa$ by definition of $H_\kappa$. Since $\kappa$
is regular, it follows that $|\cl_{n+1}(x)| < \kappa$. 
Finally, $\trcl(x) = \bigcup_n \cl_n(x)$ and using the regularity
of $\kappa$ again we have $| \trcl(x)| < \kappa$. 
\end{proof}





The definition of $H_\kappa$ shows it is a class, but we now show that is
in fact a set. 




\begin{lem} \label{hkvk}
For all infinite regular cardinals $\kappa$, $H_\kappa \subseteq 
V_\kappa$. 
\end{lem}


\begin{proof}
Suppose $x \notin V_\kappa$, so $\rank{x} \geq \kappa$.
We know from lemma~\ref{} that for every $\alpha < \rank{x}$,
there is a $y \in \trcl(x)$ such that $\rank{y}=\alpha$. 
This clearly forces $| \trcl(x)| \geq \kappa$, so $x \notin H_\kappa$.
\end{proof}


One could give another proof of lemma~\ref{hkvk} as follows. 
Let $x \in H_\kappa$. Using $\ac$, let $\lambda < \kappa$ be the
cardinality of $\trcl(x)$, and let $f \colon \lambda \to 
\{ x \} \cup \trcl(x)$ be a bijection. Define the relation $E$ on $\lambda$ by
$\alpha E \beta$ iff $f(\alpha) \in f(\beta)$. Thus, 
$(\lambda, E)$ ``codes'' the set $\{ x\} \cup \trcl(x)$. Clearly 
$\lambda, E \in V_\kappa$. Let $\pi$ be the collapse map for 
$(\lambda, E)$. We show by induction on $E$ that for all $\alpha \in 
\lambda$ that $\pi(\alpha) \in V_\kappa$. We have 
$\pi(\alpha)= \{ \pi(\beta) \colon \beta \in \lambda \wedge 
\beta E \alpha\}$. By induction, each $\pi(\beta)$ in the above
expression is in $V_\kappa$, so $\pi(\alpha) \subseteq V_\kappa$. 
Since $\kappa$ is regular and $\lambda < \kappa$, $\pi(\alpha) 
\subseteq V_{\gamma}$ for some $\gamma < \kappa$, and hence 
$\pi(\alpha) \in V_{\gamma+1} \subseteq V_\kappa$. In particular,
$x \in V_\kappa$. 


Note that if $x \subseteq H_\kappa$, then to show $x \in H_\kappa$
it is enough to show that $|x| < \kappa$. Also, since each ordinal is
transitive, clearly $H_\kappa \cap \on = \kappa$.



The next lemma shows that $\zfc-$Power holds in the $H_\kappa$.



\begin{lem} ($\zfc$) \label{hk}
For every axiom $\phi$ of $\zfc-$Power, $\zfc \proves 
\forall \kappa\ [ \kappa \text{ regular } \rightarrow 
\phi^{H_\kappa}]$. 
\end{lem}



\begin{proof}
We work in $\zfc$. Let $\kappa$ be an infinite regular cardinal. 
We show that all the axioms of $\zfc$ except power hold in $H_\kappa$. 
Note for the following arguments that by definition $H_\kappa$ is transitive. 
Foundation holds in $H_\kappa$ as it holds in any set or class.
Clearly, $\emptyset \in H_\kappa$, and by absoluteness then 
$H_\kappa$ satisfies the emptyset axiom. If $x,y \in H_\kappa$, then 
$| \{ x,y\}| < \omega < \kappa$, so $\{ x,y \} \in H_\kappa$. By
absoluteness, $H_\kappa$ satisfies the pairing axiom. 
If $x \in H_\kappa$ then $\cup x \subseteq \trcl(x)$, so
$\trcl(\cup x) \subseteq \trcl(x)$, ansd so 
$| \trcl(\cup(x))| \leq |\trcl(x)| < \kappa$. Thus, $\cup(x) \in H_\kappa$. 
By absoluteness, $H_\kappa$ satisfies the union axiom. 
Since $\kappa > \omega$, $\omega \in H_\kappa$ as we noted above. 
By absoluteness, $H_\kappa$ satisfies the infinity axiom. 
Since $H_\kappa$ is transitive, it satisfies extensionality (if 
$x \neq y$ are in $H_\kappa$, then there is a $z \in x$, say, with 
$z \notin y$. By transitivity, $z \in H_\kappa$).

To show comprehension, let $\phi(x_1,\dots,x_n,y,z)$ be a formula, and
let $a_1,\dots,a_n, w \in H_\kappa$. We must show that 
$\exists v \in H_\kappa\ \forall y\in H_\kappa\ (y \in v \leftrightarrow 
(y \in w \wedge \phi^{H_\kappa}(\vec a, y,w)))$. By comprehension in $V$
applied to the formula $\phi^{H_\kappa}(\vec x, y,z)$, there is a 
$v \in V$ such that $\forall y\ (y \in v \leftrightarrow 
(y \in w \wedge \phi^{H_\kappa}(\vec a, y,w)))$. In particular, 
$\forall y \in H_\kappa\ (y \in v \leftrightarrow 
(y \in w \wedge \phi^{H_\kappa}(\vec a, y,w)))$. Thus, it suffices to 
observe that $v \in H_\kappa$, which follows as $v \subseteq w \in H_\kappa$
(any subset of an element of $H_\kappa$ is in $H_\kappa$). 

To show replacement, let $\phi(x_1,\dots,x_n, y,z,w)$ be a formula,
$a_1,\dots,a_n,A \in H_\kappa$, and assume 
$(\forall y \in A\ \exists z\ \phi(\vec a, y,z,A))^{H_\kappa}$. 
Thus, $\forall y \in A \ \exists z \in H_\kappa\ 
\phi^{H_\kappa}(\vec a, y,z, A)$. Applying replacement in $V$ to the 
formula $[\phi^{H_\kappa} \wedge z \in H_\kappa]$, there is a set $B$ such that 
$\forall y \in A \ \exists z \in B \cap \in H_\kappa\ 
\phi^{H_\kappa}(\vec a, y,z, A)$. By $\ac$, there is a $B' \subseteq B$
with $|B'| \leq |A|$ such that 
$\forall y \in A \ \exists z \in B' \cap \in H_\kappa\ 
\phi^{H_\kappa}(\vec a, y,z, A)$. Since $B' \subseteq H_\kappa$ and 
$|B'| < \kappa$, we have $B' \in H_\kappa$. Thus, 
$(\exists B\ \forall y \in A\ \exists z \in B\ \phi(\vec a, y,z,A))^{H_\kappa}$. 

Finally, to see $\ac$ holds in $H_\kappa$, let $a \in H_\kappa$. 
By $\ac$ in $V$, let $\prec$ be a wellordering of $a$. Since 
$\prec \subseteq a \times a$, $|\prec| < \kappa$. Easily 
$\prec \subseteq H_\kappa$, as every ordered pair 
$\langle x,y \rangle$ is in $H_\kappa$ if $x,y \in H_\kappa$. 
So, $\prec \subseteq H_\kappa$, and hence $\prec \in H_\kappa$. 
By downwarda absoluteness, $(\prec$ is a wellordering$)^{H_\kappa}$. 
\end{proof}



\begin{cor} 
$\zfc-$Power $\nvdash$ Power.
\end{cor}


\begin{proof}
Similar to the proof of corollary~\ref{noreplace}, using now the
fact that $\zfc \proves (\neg \text{ Power})^{H_{\omega_1}}$.
\end{proof}



Lemmas~\ref{vk}, \ref{hk} are stated and proved in the metatheory,
however me may formalize their statements and proofs within 
$\zfc$. Lemma~\ref{hk}, for example, then becomes the statement
$\zf \proves \forall \alpha \forall n\ ( (\alpha > \omega \text{ limit} 
\wedge \theta(n) \rightarrow \rho(n, V_\alpha)))$ where 
$\theta$ is the formula which represents the relation 
$R(n) \leftrightarrow n$ codes an axiom of $\zf-$Replacement. 
[The only thing slightly problematic in the formalizations
is where we consider the relativizations $\phi^{V_\kappa}$, $\phi^{H_\kappa}$. 
But lemma~\ref{setdef} gives us a formula $\rho$ which expresses
the formalizations of these notions, e.g., the formalization of
$(\theta_n)^{V_\kappa}$ is the statement $\rho(n,V_\kappa)$.]


Here $\rho$ is the set satisfaction formula of lemma~\ref{setdef}. 
Likewise, lemma~\ref{hk} when formailzed becomes the statement
$\zfc \proves \forall \kappa \forall n\ ( (\kappa \text{ an uncountable
regular cardinal}) 
\wedge \theta'(n) \rightarrow \rho(n, H_\kappa)))$, where 
now $\theta'$ represents 
$R'(n) \leftrightarrow n$ codes an axiom of $\zf-$Power. 


The completeness theorem of first order logic may also be formailzed within
$\zfc$ (or $\zf$ for countable theories, which we consider here). 
It then becomes the statement that $\zf \proves \forall T \subseteq \omega\ 
(\con(T) \leftrightarrow \exists M \ \forall n \in T\ 
\rho(n,M))$. Using this, we may reformulate the formalzed 
lemmas~\ref{vk}, \ref{hk} as consistency results as follows.


\begin{cor} \label{correp}
$\zfc \proves \con(\zfc-\text{Replacement})$.
\end{cor}


\begin{cor} \label{corpow}
$\zfc \proves \con(\zfc-\text{Power})$.
\end{cor}


From G\"odel's theorem, we know that $\zfc \nvdash \con(\zfc)$, 
but these corollaries 
show that if we weaken $\zfc$ a bit, we can prove its formal
consistency within $\zfc$. 





We showed that $H_\kappa \subseteq V_\kappa$ for all infinite
regular $\kappa$. When does equality hold? Now $V_\kappa \subseteq 
H_\kappa$ iff $\forall \alpha < \kappa\ (V_\alpha \in H_\kappa)$ 
(since if $V_\alpha \in H_\kappa$ then any subset of $V_\alpha$
is in $H_\kappa$). Since each $V_\alpha$ is transitive, this is then 
equivalent to $\forall \alpha < \kappa\ (|V_\alpha| < \kappa)$.
By definition of the $\beth$ function, $|V_{\omega+\alpha}|=\beth(\alpha)$. 
So, $V_\kappa = H_\kappa$ iff $\forall \alpha < \kappa\ 
\beth(\alpha) < \kappa$. Now $\beth(\alpha) \geq \alpha$, so 
$\beth(\alpha+1) \geq 2^{|\alpha|}$ for all $\alpha$. Thus, for $V_\kappa$
to equal $H_\kappa$ we must have $\forall \lambda < \kappa\ 
2^\lambda < \kappa$. Since $\kappa$ is assumed regular, we must
then have that $\kappa$ is strongly inaccessible. Conversely, 
if $\kappa$ is strongly inaccessible, the following exercise shows this 
condition is satisfied. 


\begin{exer}
Show that if $\kappa$ is strongly inaccessible then 
$\forall \alpha < \kappa\ (\beth(\alpha) < \kappa)$.
\end{exer}


We thus have:

\begin{fact}
For all infinite regular cardinals $\kappa$, $H_\kappa=V_\kappa$ iff 
$\kappa$ is strongly inaccessible. 
\end{fact}


\begin{cor} \label{corinacc}
$\zfc \nvdash \exists \kappa\ (\kappa \text{ is strongly
inaccessible})$.
\end{cor}

\begin{proof}
If $\zfc \proves \exists \kappa\ (\kappa \text{ is strongly
inaccessible})$, then from the formalized lemmas~\ref{hk}, \ref{vk}
we would have $\zfc \proves \exists \kappa\ \forall n\ 
(\theta(n) \rightarrow \rho(n,H_\kappa))$ where $\theta$ 
represents $R(n) \leftrightarrow \theta_n \in \zfc$, and $\rho$ again is
the set satisfaction formula.
By the formalized completeness theorem, this would give 
$\zfc \proves \con(\zfc)$, a contradiction to G\"odel's theorem.
\end{proof}


Note that the proof of corollary~\ref{corinacc} actually showed the
following.

\begin{cor} \label{cor2inacc}
$\zfc+ \exists \kappa\ (\kappa \text{ is strongly inaccessible})
\proves \con(\zfc)$.
\end{cor}

We sometimes state corollary~\ref{cor2inacc} by saying that 
$\zfc + \exists \kappa\ (\kappa \text{ is strongly inaccessible})$
has a greater consistency strength that $\zfc$.




\begin{exer}
Show corollary~\ref{corinacc} without using G\"odel's theorem. 
[Hint: Suppose $\zfc \proves \exists \kappa\ (\kappa \text{ is strongly
inaccessible})$, and let $\psi_1,\dots,\psi_n$ be a finite
fragment of $\zfc$ such that $\{ \psi_1,\dots,\psi_n \} \proves
\exists \kappa\ (\kappa \text{ is strongly
inaccessible})$. Working in $\zfc$, let $\kappa$ be the least 
strongly inaccessible cardinal. Use lemmas~\ref{hk}, \ref{vk}
and an absoluteness argument to show that there is a strongly
inaccessible $\lambda < \kappa$.] 
\end{exer}




$V_\kappa$ and $H_\kappa$ are sets which we showed satisfy certain
fragments of $\zfc$. We now consider a certain class, $\hod$, which we show
(assuming $\zfc$) satisfies all of $\zfc$. In fact, $\hod$ will
be a transitive class containing all of the ordinals, a so-called 
{\em inner model} of $\zfc$.



We would like to say 
a set $x$ is {\em ordinal-definable} if there is a formula 
$\phi(x_1,\dots,x_n,y)$ and ordinals $\alpha_1,\dots,\alpha_n$
such that $x$ is the unique set $x$ such that 
$\phi(\alpha_1,\dots,\alpha_n,y)$. We would then define $\hod$ to 
be the sets which are hereditarily ordinal definable. The problem with this
is that this definition, at least the way it is stated, is not
a legitimate formula of set theory, i.e., doesn't really seem to define 
a class. The problem, as we mentioned before, is that we cannot
define formual satisfaction over classes, only over sets. 
However, the reflection theorem provides a way to circumvent
this logical problem. For any formula $\phi$ and ordinals 
$\alpha_1,\dots,\alpha_n$, the reflection theorem says that there
is a $\beta > \max \{\alpha_1,\dots,\alpha_n\}$ such that 
$\forall y \in V_\beta\ ( \phi(\vec \alpha,y)^{V_\beta} \leftrightarrow
\phi(\vec \alpha, y) )$. Thus, there should be no loss of generality
in interpreting our formulas in the $V_\beta$. This suggests the
following definition.


\begin{defn}
$\od$ is the class defined by:
\begin{equation*}
\begin{split}
x \in \od & \leftrightarrow \exists \beta \in \on \ \exists \alpha_1,\dots,
\alpha_n < \beta\ \exists n \in \omega \ \forall y \in V_\beta\ 
[(y \approx x) \leftrightarrow \rho(n, \langle \vec \alpha,y\rangle, V_\beta)]
\end{split}
\end{equation*}
where $\rho$ is the formula for set satisfaction from lemma~\ref{setdef}.
Also,
$$
x \in \hod \leftrightarrow \forall y \in \trcl(x)\ (y \in \od).
$$
\end{defn}

Note that the quantification over $\alpha_1,\dots,\alpha_n$
should really be expressed as a quantification over 
sets $z= \langle \alpha_1,\dots,\alpha_n \rangle$ coding the 
sequence. 



Our remarks above concerning the reflection theorem now easily give the
following.

\begin{lem}
Let $\phi(x_1,\dots,x_n,y)$ be a formula of set theory. Then 
$$\zf \proves 
\forall \alpha_1,\dots, \alpha_n \in \on\ \forall x\ 
[ \forall y\ (y \approx x \leftrightarrow \phi(\vec \alpha, y) )
\rightarrow y \in \od ].$$
\end{lem}

By definition $\hod$ is transitive, and it trivially contains all of the 
ordinals.
The next theorem shows that  working in $\zf$ we can show that 
$\hod$ satisfies $\zfc$. We will need th following
ordring on the finite sequences of ordinals.

\begin{defn}
The G\"odel ordering $<_G$ on $\on^{< \omega}$ is defined by:
\begin{equation*}
\begin{split}
\langle \alpha_1,\dots,\alpha_n \rangle 
& <_G \langle \beta_1,\dots,\beta_m \rangle  \leftrightarrow
\max \{ \alpha_1,\dots,\alpha_n \} < \max \{ \beta _1,\dots,\beta_m \} 
\\ & \vee 
(\max \{ \alpha_1,\dots,\alpha_n \} = \max \{ \beta _1,\dots,\beta_m \} 
\wedge n < m)
\\ & \vee
(\max \{ \alpha_1,\dots,\alpha_n \} = \max \{ \beta _1,\dots,\beta_m \} 
\wedge n = m \wedge \vec \alpha \llex \vec \beta),
\end{split}
\end{equation*}
where $\llex$ denotes lexicographic order. 
\end{defn}

The following lemma is clear from the definition.

\begin{lem}
The G\"odel ordering is a class wellordering of $\on^{< \omega}$,
all of whose initial segments are sets.
\end{lem}



\begin{thm} \label{hodthm}
For all axioms $\phi$ of $\zfc$, $\zf \proves \phi^{\hod}$.
\end{thm}


\begin{proof}
Foundation holds in $\hod$, as it holds in any class with the 
$\epsilon$ relation.
Extensionality holds as $\hod$ is transitive. Consider pairing. Let $x,y
\in \hod$. Fix $n \in \omega$, $\alpha_1,\dots,\alpha_n \in \on$, 
and $\beta_1 \in \on$ such that 
$\forall z \in V_\beta\ 
[(z \approx x) \leftrightarrow 
\rho(n, \langle \vec \alpha,y\rangle, V_\beta)$,and
similarly let $m$, $\gamma_1,\dots,\gamma_k$, $\beta_2$ witness 
$y \in \hod$. Then,
\begin{equation*}
\begin{split}
z \in \{ x,y \} \leftrightarrow & 
\exists w\ [ w=V_{\beta_1} \wedge \rho(n, \langle \vec \alpha, z \rangle,
w)] \vee 
\exists w\ [ w=V_{\beta_2} \wedge \rho(m, \langle \vec \gamma, z \rangle,
w)]
\end{split}
\end{equation*}
The righthand is a formula in set theory with ordinal parameters 
$n$, $m$, $\vec \alpha$, $\vec \gamma$, $\beta_1$, $\beta_2$. 
Thus, $\{ x,y \} \in \od$. Since $\{ x,y \} \subseteq \hod$, we have 
$\{ x,y\} \in \hod$. 


Infinity holds in $\hod$ by absoluteness, since $\omega \in \hod$ ($\hod$
contains all the ordinals). 

Consider the union axiom. Let $x \in \hod$, and fix witnesses
$n$, $\vec \alpha$, $\beta$. 
Then
$$
z \in \cup x \leftrightarrow 
\exists w\ \exists y\ [ w= V_\beta \wedge y \in w \wedge 
\rho(n, \langle \vec \alpha, y \rangle, w) \wedge \exists u \in y (z \in u)].
$$
Again, the righthand side is a formula with ordinal parameters
$n$, $\vec \alpha$, $\beta$, and so $\cup x \in \od$. Since 
$\cup x \subseteq \trcl(x) \subseteq \hod$, this shows $\cup x \in \hod$.
By absoluteness, $\hod$ satisfies the union axiom. 


To show comprehension, let $\phi(x_1,\dots,x_n, y,z)$ be a formula,
and $a_1,\dots, a_n, A \in \hod $. We must show that $B \in 
\hod$, where
$$
B=\{ z \in A \colon \phi^{\hod}(a_1,\dots,a_n,A,z) \}. 
$$
Note that $B$ exists in $V$ by comprehension in $V$. 
Then,
\begin{equation*}
\begin{split}
x=B & \leftrightarrow \forall z\ [z \in B \leftrightarrow 
\exists u_1,\dots u_n\ \exists v\ ( u_1= a_1 \wedge \dots 
\wedge u_n=a_n \wedge v=A \\ & \wedge 
\phi^{\hod}(u_1,\dots,u_n, v,z))],
\end{split}
\end{equation*}
where in place of ``$u_1=a_1$'' we use a formula with only 
ordinal parameters (the witnesses for $a_1 \in \hod$) and
likewise for the other $a_i$ and $A$. This shows $B \in \od$,
and since $B \subseteq \hod$ we have $B \in \hod$. Clearly,
$(\forall z\ (z \in B \leftrightarrow z \in A \wedge 
\phi(a_1,\dots,a_n,A,z)))^{\hod}$, and so $\hod$ satisfies 
comprehension. 


To show power set, let $x \in \hod$. Let $\alpha \in \on$ be
large enough so that $\sP(x) \in V_\alpha$. Note that $V_\alpha \in 
\od$ (it is definable from $\alpha$). Since $\hod$ is a class,
$y=V_\alpha \cap \hod \in \od$ as well, and so 
$y \in \hod$. Clearly $(\forall z\ (z \subseteq x \rightarrow 
z \in y)^{\hod}$, so $\hod$ satisfies power set. 




To show replacement,  let $\phi(x_1,\dots,x_n,y,z,w)$ 
be a formula, $a_1,\dots, a_n, A \in \hod$, and 
assume $(\forall y \in A\ \exists z \ \phi(\vec a, y,z, A))^{\hod}$.
Let $\alpha \in \on $ be such that 
$\forall y \in A\ \exists z \in V_\alpha \ \phi(\vec a, y,z, A))^{\hod}$.
As $V_\alpha \in \od$, $B=V_\alpha \cap \hod \in \hod$. 
Then $(\forall y \in A\ \exists z \in B\ \phi(\vec a, y,z, A))^{\hod}$.  


Finally, to show $\ac$ holds in $\hod$, let $x \in \hod$. Every
$y \in x$ is in $\hod$ and has a witness sequence 
$n$, $\vec \alpha$, $\beta$. To compare two elements $y,z$ of $x$,
we take the $<_G$ least witnesses for $y$ and $z$, and compare them 
in the $<_G$ ordering. In more detail, 
define a wellordering of $x$ by:
\begin{equation*}
\begin{split}
y \prec z & \leftrightarrow y \in x \wedge z \in x \wedge 
\exists n \in \omega\ \exists \langle \vec \alpha \rangle \in 
\on^{< \omega}\ \exists \beta_1 \in \on\ 
\\ & \exists m \in \omega\ \exists \langle \vec \gamma \rangle \in 
\on^{< \omega}\ \exists \beta_2 \in \on\ 
\\ & [ \forall u\ (u \approx y \leftrightarrow 
\exists w\ (w \approx V_{\beta_1} \wedge \rho(n, \langle \vec \alpha,
u \rangle, w))) 
\\& \wedge \forall \langle n', \vec \alpha', \beta'_1 \rangle
<_G \langle n, \vec \alpha, \beta_1 \rangle\ 
\neg \forall u\ (u \approx y \leftrightarrow 
\exists w\ (w \approx V_{\beta'_1} \wedge \rho(n', \langle \vec \alpha',
u \rangle, w)))] 
\\ &\wedge
[\forall u\ (u \approx z \leftrightarrow 
\exists w\ (w \approx V_{\beta_2} \wedge \rho(m, \langle \vec \gamma,
u \rangle, w))) 
\\ &\wedge 
\forall \langle m', \vec \gamma', \beta'_2 \rangle
<_G \langle m, \vec \gamma, \beta_2 \rangle\ 
\neg \forall u\ (u \approx z \leftrightarrow 
\exists w\ (w \approx V_{\beta'_2} \wedge \rho(m', \langle \vec \gamma',
u \rangle, w)))] 
\\ & \wedge
\langle n, \vec \alpha, \beta_1 \rangle <_G 
\langle m, \vec \gamma, \beta_2 \rangle
\end{split}
\end{equation*}
Here for ``$y \in x$'' we substitute an appropriate formula
with only ordinal parameters, and likewise for $z \in x$. 


Easily $\prec$ is a wellordering, and the above formula shows
$\prec \in \od$. Since $\prec \subseteq \hod$, we have 
$\prec \in \hod$, and by downwards absoluteness 
$(\prec$ is a wellordering of $x)^{\hod}$. 
\end{proof}



\begin{cor} \label{conac}
If $\zf$ is consistent, then so is $\zfc$. 
\end{cor}

\begin{proof}
Suppose $\zf$ is consistent, but $\zfc$ is not. Then 
$\zf \proves \neg \ac$. Let $\psi_1,\dots, \psi_n$ be finitely
many axioms of $\zf$ such that $\{ \psi_1,\dots, \psi_n \}
\proves \neg \ac$. From theorem~\ref{hodthm}, 
$\zf \proves \psi_1^{\hod} \wedge \dots \wedge \psi_n^{\hod}$. 
Hence, $\zf \proves (\neg \ac)^{\hod}$. But, $\zf 
\proves \ac^\hod$ from theorem~\ref{hodthm}, a contraction
to the consistency of $\zf$. 
\end{proof}


Thus, the axiom of choice cannot introduce a contradiction 
into mathematics, unless one was already present. This is a significant
statement in view of the many ``pathological'' sets that may 
be constructed with $\ac$. For eaxample, with 
$\ac$ a standard construction gives a non-measurable set of reals, 
and it can be shown that $\ac$ is necessary for the construction
(more on this later). 



Finally, we note that although corollary~\ref{conac} was proved
in the meta-theory, the argument is readily formalized, which gives the
following version of the corollary.

\begin{cor}
$\con(\zf) \proves \con(\zfc)$.
\end{cor}

Thus, the theories $\zf$ and $\zfc$ have the same consistency
strength. 













\end{document}