Problem 24 from Chapter 1 of Kunen's Set Theory: An Introduction to Independence Proofs Just want to make sure I'm tracking Kunen here, and hopefully the proof I have is correct. Comments / Suggestions welcome.
Thanks!
Problem 24. Let T be any consistent set of axioms extending ZF. Show that the Z = {$\psi$ : T $\vdash \psi$} is not recursive.  
Proof:
We prove the contrapositive. So suppose Z recursive. Then 
i.  There is a $\chi(x)$ s.t. T $\vdash \psi$ $\implies$ ZF $\vdash \chi$(' $\psi$ ')
ii. There is a $\chi(x)$ s.t. T $\nvdash \psi$ $\implies$ ZF $\vdash \lnot \chi$('$\psi$') 
for any $\psi$. We note:
14.2: ZF $\vdash \psi \iff \lnot \chi$('$\psi$').  
We must show T inconsistent (i.e., T $\vdash \bot$).  
Subproof 1.
Suppose T $\vdash \psi$.  
ZF $\vdash \chi$('$\psi$') -- By i. and assumption  
T $\vdash \psi \iff \lnot \chi$('$\psi$') -- 14.2 + the fact that T is an extension of ZF
T $\vdash \chi$ ('$\psi$') -- Again, T is an extension of ZF 
T $\vdash \chi$('$\psi$') $\iff \lnot \chi$('$\psi$'). 
Hence T $\vdash \bot$ .
End of Subproof 1.
Subproof 2. 
Suppose on the other hand T $\nvdash \psi$. 
ZF $\vdash \lnot \chi$('$\psi$') -- By assumption and ii.
ZF $\vdash \psi$ -- Previous line and 14.2.
T $\vdash \psi$ -- T is an extension of ZF
T $\vdash \psi \iff$ T $\nvdash \psi$  
T $\vdash \bot$.
End of Subproof 2. 
Hence either way, T $\vdash \bot$.
End of Proof.
 A: No, your proof is not correct.
Here is my attempt:
Theorem
(Assume ZF is consistent.) Let $ T $ be any consistent set of axioms extending $ \mathrm{ZF} $.
Then $ \{ \psi : T \vdash \psi \}$ is not recursive.
Proof. Assume it were recursive. We show that $ T $ is inconsistent. By Theorem 14.1, we find a formula $ \chi(x) $ such that


*

*$ T \vdash \psi $ implies $ \mathrm{ZF} \vdash \chi(\ulcorner \psi \urcorner) $ and

*$ T \nvdash \psi $ implies $ \mathrm{ZF} \vdash \neg \chi(\ulcorner \psi \urcorner) $.


By Theorem 14.2 (the fix-point lemma), we find a sentence $ \psi $ such that $ \mathrm{ZF} \vdash (\psi \leftrightarrow \neg \chi(\ulcorner \psi \urcorner)) $.
We assume $ T \nvdash \psi $. Then $ \mathrm{ZF} \vdash \neg \chi(\ulcorner \psi \urcorner) $ and thus $ \mathrm{ZF} \vdash \psi $ contradicting $ T \nvdash \psi $.
So $ T \vdash \psi $. Then $ \mathrm{ZF} \vdash \chi(\ulcorner \psi \urcorner) $, so $ \mathrm{ZF} \vdash \neg \psi $, whence $ T \vdash \neg \psi $. So $ T \vdash (\psi \land \neg \psi) $, i.e. $ T $ is inconsistent.
QED.

Note that this theorem (like all theorems in section I.14) are facts proven in the metatheory. Do not confuse formal theorems like
$$
\forall a, b, c, d \ \Bigl( \langle a, b \rangle = \langle c, d \rangle \leftrightarrow (a = c \land b = d) \Bigr)
$$
and facts in the metatheory like
$$
\mathrm{ZF} \vdash \forall a, b, c, d \ \Bigl( \langle a, b \rangle = \langle c, d \rangle \leftrightarrow (a = c \land b = d) \Bigr).
$$

Analysis of your proof. My comments are set italic.
We prove the contrapositive. So suppose $ T $ recursive. Then
i. There is a $ \chi(x) $ s.t. $ T \vdash \psi \implies \mathrm{ZF} \vdash \chi(\ulcorner \psi \urcorner) $.
ii. There is a $ \chi(x) $ s.t. $ T \nvdash \psi \implies \mathrm{ZF} \vdash \neg \chi(\ulcorner \psi \urcorner) $.
for any $ \psi $.
First of all, do not mix the metatheory and the theory: You use "$ \implies $" at both levels! Also, there is just one $ \chi(x) $ such that


*

*$ T \vdash \psi $ implies $ \mathrm{ZF} \vdash \chi(\ulcorner \psi \urcorner) $ and

*$ T \nvdash \psi $ implies $ \mathrm{ZF} \vdash \neg \chi(\ulcorner \psi \urcorner) $.
You stated the existence of two (maybe different) formulas.
We note:
14.2: $ \mathrm{ZF} \vdash \psi \iff \neg \chi(\ulcorner \psi \urcorner) $.
There is some $ \psi $ such that $ \mathrm{ZF} \vdash (\psi \leftrightarrow \neg \chi(\ulcorner \psi \urcorner)) $.
We must show $ T $ inconsistent (i.e. $ T \vdash \bot $).
Subproof 1.
What is a "subproof"? The structure of your proof is wrong at this point. A case differentiation does not make sense here because $ T \nvdash \psi $ leads to a contradiction. So $ T \vdash \psi $ anyway!
Suppose $ T \vdash \psi $.
$ \mathrm{ZF} \vdash \chi(\ulcorner \psi \urcorner) \quad $ -- By i. and assumption
$ T \vdash \psi \iff \neg \chi(\ulcorner \psi \urcorner) \quad $ -- 14.2 + the fact that $ T $ is an extension of $ \mathrm{ZF} $
$ T \vdash \chi(\ulcorner \psi \urcorner) \quad $ -- Again, $ T $ is an extension of $ \mathrm{ZF} $
$ T \vdash \chi(\ulcorner \psi \urcorner) \iff \neg \chi(\ulcorner \psi \urcorner) $
Why "$ \iff $"? It must be $ T \vdash (\chi(\ulcorner \psi \urcorner) \land \neg \chi(\ulcorner \psi \urcorner)) $.
Hence $ T \vdash \bot $.
End of Subproof 1.
Subproof 2.
Suppose on the other hand $ T \nvdash \psi $.
Your (main) claim is that $ T $ is inconsistent. Then $ T \nvdash \psi $ cannot be true (because an inconsistent theory proves everything), so you have to treat this as an assumption and not as a second case. You must derive a contradiction, i.e. a contradiction in the metatheoretical logic of your proof. This is not the same as an inner-theoretical contradiction in $ T $.
$ \mathrm{ZF} \vdash \neg \chi(\ulcorner \psi \urcorner) \quad $ -- By assumption and ii.
$ \mathrm{ZF} \vdash \psi \quad $ -- Previous line and 14.2.
$ T \vdash \psi \quad $ -- $ T $ is an extension of $ \mathrm{ZF} $.
$ T \vdash \psi \iff T \nvdash \psi $
Why "$ \iff $"? It must be $ T \vdash \psi $ and $ T \nvdash \psi $.
This step is a big mistake! Be careful with your use of "$ \iff $". You seem to confuse the metatheory and the theory.
$ T \vdash \bot $
$ T \vdash \psi $ and $ T \nvdash \psi $ is the (metatheoretical) contradiction. $ T \vdash \bot $ does not make any sense as you assumed $ T \nvdash \psi $ (see above).
End of Subproof 2.
Hence either way, $ T \vdash \bot $.
End of Proof.
