I'm working through Kunen's famous book on set theory and I'm puzzled by exercise 19 of chapter VI.
Background for the exercise:
In chapter V (Definition 1.1) the author defines certain function of two variables $Df(A,n)$. This is the set of $n$-place relations on $A$ which are definable by a formula with $n$ free variables relativized to $A$. Defining $Df(A,n)$, first he defines recursively sets Df'(k,A,n),k \in \omega and then sets Df(A,n) = \bigcup_{k \in \omega} Df'(k,A,n).
Then he proves Lemma V 1.3 which says that if $\phi(x_0,...,x_{n-1})$ is any formula and $A$ is any set then the set $\{ s \in A^n : \phi^A(s(0),...,s(n-1)) \}$ is in $Df(A,n)$ ($\phi^A$ means $\phi$ relativized to $A$).
In the next chapter VI (Definition 1.1) the author defines the definable power set of a set $A$, or $\mathcal{D}(A)$. This is the set of subsets of A which are definable from a finite number of elements of $A$ by a formula relativized to $A$. Then in Lemma VI 1.3(c) he proves that the finite subsets of $A$ are in $\mathcal{D}(A)$.
Exercise VI 19:
The exercise asks to define alternatives to $Df$ and $\mathcal{D}$, namely such $Df^*$ and $\mathcal{D}^*$ that $Df^*$ still satisfies Lemma V 1.3 but Lemma VI 1.3(c) is not provable in ZFC. He also gives a hint:
First define $\alpha = \omega$ if CON(ZF) and alpha = the least Gödel number of a contradiction if not-CON(ZF) (does he mean the least Gödel number of a proof of a contradiction?). Then define Df^*(A,n) = \bigcup_{k < \alpha} Df'(k,A,n).
I think I might understand the idea. We suppose that Lemma VI 1.3(c) is provable. Then somehow we show that it is not possible that $\alpha \in \omega$ so that it must be that $\alpha = \omega$. But then we have proved CON(ZF) which is not possible by Gödel's 2nd.
My questions:
First I can't see how Lemma V 1.3 goes through with $Df^*$. For example the proof uses the fact that $Df(A,n)$ is closed under finite intersections. This is easy to see from the definition of $Df$ but what happens if not-CON(ZF) and alpha is a natural and only finitely many Df' are taken into $Df^*$. Doesn't this destroy the finite intersection property?
In more details this is what I tried to do. The case 'conjunction' of the induction on the structure of the formula. We assume $\phi = \phi_1 \wedge \phi_2$ and
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \} \in Df^*(A,n) ]$ and $ZFC \vdash \forall A [ \{ s \in A^n : \phi_2^A(s(0),\ldots,s(n-1)) \} \in Df^*(A,n) ]$.
Then we have to show that
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \wedge \phi_2^A(s(0),\ldots,s(n-1))\} \in Df^*(A,n) ]$
or what is the same
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \} \cap \{ s \in A^n : \phi_2^A(s(0),\ldots,s(n-1))\} \in Df^*(A,n) ]$.
To prove this: working inside the formal theory, let $A$ be a set, $A_1 = \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \}$ and $A_2 = \{ s \in A^n : \phi_2^A(s(0),\ldots,s(n-1)) \}$. Since $A_1, A_2 \in Df^*(A,n)$ there are $k_1,k_2 < \alpha$ such that A_1 \in Df'(k_1,A,n) and A_2 \in Df'(k_2,A,n). If we let $k = \max \{k_1,k_2\}$ then A_1 \cap A_2 \in Df'(k+1,A,n) by definition of the sets Df'. Now in the case of $Df$ there are no problems deducting that $A_1 \cap A_2 \in Df(A,n)$, but in the case of $Df^*$ what can we do if it happens that $k+1 = \alpha$? I can't see how this kind of a situation can be prevented.
Also even if we somehow can prove Lemma V 1.3 with $Df^*$, why does it follow from provability of Lemma VI 1.3(c) (= finite subsets of $A$ are in $\mathcal{D}^*(A)$) that $\alpha \notin \omega$?