Exercise in Kunen. Demonstrating a relative interpretation into a set This is a question regarding exercise (II.2.15) in Kunen's Set Theory (2011):
The exercise reads:
"We shall see later that $ZFC\vdash $Con$(\Gamma)$ whenever $\Gamma$ is a finite subset of $ZFC$. Use this to define explicitly, in $ZFC$, a binary relation $E$ on $\omega$ such that $ZFC\vdash\varphi^{\omega,E}$ for each axiom $\varphi$ of $ZFC$".
Now the hint reads:
"List the axioms of $ZFC$ in some computable way, as {$\xi_i:i<\omega$}; let $ZFC_n=${$\xi_i:i<n$}. Working in $ZFC$, we can define $\Gamma$ to be $ZFC$ if $ $Con$(ZFC)$; if $\neg $Con$(ZFC)$, let $\Gamma=ZFC_n$ where $n$ is largest such that $ $Con$(ZFC_n)$. Then clearly $ $Con$(\Gamma)$, and observe that the proof of the Completeness Theorem yields an explicit $E$ such that $(\omega;E)\models \Gamma$".
I'm not sure how to go about this excercise, but I'm under the impression that if I let $\psi$ be the sentence "there is a binary relation $E$ on $\omega$ such that $ZFC\vdash\varphi^{\omega,E}$ for each axiom $\varphi$ of $ZFC$", then I want to show that $ZFC\vdash\psi$. Is this correct?
Any help is appreciated, Thanks.
 A: This kind of thing can be confusing, so let me try to help.
Enumerate the axioms of ZFC in some canonical manner, and let $\Gamma$ be the longest initial segment of this list of axioms that is consistent (perhaps this is all of ZFC, if ZFC is consistent, or perhaps it is the theory arises from only finitely many axioms, if it isn't). In any case, $\Gamma$ is consistent, by definition, and so it has a countable model. Indeed, from $\Gamma$ we can define a canonical model of $\Gamma$, via the Henkin construction. Since the language is finite and we need only countably many Henkin constants, we can view the Henkin construction as resulting definably in a model whose elements are the natural numbers, with a relation $E$. Thus, in ZFC we have defined a relation $E$ on $\omega$, and proved that $(\omega,E)$ satisfies the largest consistent initial segment of ZFC. 
In short, we define the relation $E$ as: 


*

*the relation on the natural numbers that results from applying the Henkin construction to the longest consistent initial segment of the ZFC axioms, carried out so as to produce a relation on the natural numbers, by using the natural numbers as the Henkin constants and then selecting the least from each class for the quotient procedure and then canonically reindexing so as to result in a model with domain exactly $\omega$.


Since ZFC proves, as a theorem scheme, that any particular finite initial segment of the ZFC axioms is consistent, it follows that ZFC proves that any particular ZFC axiom from the meta theory is in $\Gamma$, among the largest consistent initial segment of ZFC. Thus, in ZFC we can prove that  $(\omega,E)$ as we have defined it is a model of any particular axiom of ZFC that we might be given. And that is what I understand the task of the exercise to be, so we're done. 
Note that this is a scheme of assertions, a separate claim about each axiom separately. Meanwhile, if ZFC is consistent, then it is not possible to prove in ZFC that there is a relation $E$ on $\omega$ such that $(\omega,E)$ satisfies every axiom of ZFC, since that claim is equivalent to Con(ZFC), which is not provable in ZFC.
Let me add a bit more, since the idea of this exercise leads into deep waters. The theory $\Gamma$ as I have defined it above provides another alternative way to represent the ZFC of the meta theory inside the object theory. Namely, by definition, $\Gamma$ is the largest consistent fragement of ZFC, and we can prove in ZFC that this contains every single ZFC axiom that we are able to express in the meta theory. But because of the way that we defined it, we can prove in ZFC that $\Gamma$ is consistent, that is, that $\text{Con}(\Gamma)$. And since $\Gamma$ is in agreement as we said with the actual ZFC of the metatheory, this can be seen as a way of proving the consistency of ZFC inside ZFC, despite the incompleteness theorem. Of course, we haven't proved Con(ZFC), as it is usually formulated, in ZFC, and this is impossible by the incompleteness theorem, assuming ZFC is consistent. Feferman has written on this (see related remarks on Marc Alcobé García's question Feferman's extensional and intensional applications of the method of arithmetization and especially Sergei Tropanets's question Clarification of Gödel's second incompleteness theorem), and these ideas form the basis of the model-theoretic proof of the incompleteness theorem (for example, see chapter 6 of Per Lindström's book Aspects of Completeness). 
