(I'm self-studying from Kunen's book Set Theory: An Introduction to Independence Proofs after nearly 30 years out of the field as a practicing lawyer.)
Problem $23$ asks us to assume $\operatorname{Con}(\text{ZF})$ and prove there is a first order formula $\psi$ that represents "$x$ is even" (if $x \in \omega$ is even, ZF proves $\psi([x])$ and if $x \in \omega$ is odd, ZF proves $\lnot \psi([x])$ but such that ZF does not prove $\forall x \in \omega ~(\psi([x]) \lor \psi([x+1]))$.
I'm at a loss. I wondered whether it was some sentence that's not true of non-standard numbers but then I realized that can't be right because there's no first-order way to distinguish standard numbers from non-standard numbers. Nor can I figure out some way to incorporate some statement that's independent of ZFC. This isn't a starred exercise so it's not supposed to be difficult, but for the life of me I'm out of ideas. What am I missing?
Thanks for any help.
Well, that's at least in the right direction: namely, you're definitely going to want to combine the usual definition of even-ness with some ZFC-undecidability.
Throughout I'll be horribly informal, but hopefully clear. Let's assume - correctly - that our definition is going to have the form $$\varphi(x):\quad x\mbox{ is even } \wedge \psi(x)$$ for some "bonus condition" $\psi$. The idea is that we want $\psi([n])$ to be ZF-provable for each specific $n$, but the sentence $\forall x(\psi(x))$ to not be ZF-provable.
Our most basic source of undecidability is of course consistency, and we're going to make headway by unpacking it. Specifically, the single sentence Con(ZF) really has the form "$\forall x(\theta(x))$," where $\theta(x)$ is intuitively "$x$ is not a (code for a) proof of $\perp$ in ZF." When we think about this, we notice that this is looks a lot like our desired $\psi$ - the key point being that each specific code can be checked in ZF.
So we're led to consider the formula
Do you see why this works?