So this is probably a silly question, but:
Consider the statement $$(*) \quad\mbox{Every $\Pi^1_2$ set of countable ordinals contains or is disjoint from a club.}$$ By "$\Pi^1_2$ set of ordinals," I mean a set of reals which is $\Pi^1_2$ (in a real parameter) and which consists of codes for ordinals (and is closed under isomorphism of coded ordinals, although that's not essential).
Now, $(*)$ follows from large cardinals. In fact, much more does: generally, large cardinals imply that the club filter is "close" to an ultrafilter, in that reasonably definable sets of countable ordinals either contain or are disjoint from a club.
My problem is, I have believed for a while that $(*)$ is provable in ZFC. However, the other day I mentioned this in passing to a friend, and he asked what the proof was, and I realized I couldn't remember it. I vaguely recall an easy application of Shoenfield absoluteness, but I can't reconstruct it. So my question is:
Is $(*)$ provable in ZFC? And if so, what does the proof look like?
I haven't fully checked the complicated coding details, but here's a way to prove that (*) is false in $L.$
Assume $V=L.$ For each $\alpha\lt\omega_1,$ let $t_\alpha$ be the $\lt_L$-least function mapping $\omega$ one-onto onto $\alpha.$ For any $n\lt\omega$ and any $\beta\lt\omega_1,$ let $A_{n,\beta}=\lbrace \alpha\lt\omega_1 \mid t_\alpha(n)=\beta\rbrace.$ By Fodor's lemma, for each $n\lt\omega,$ there is some $\beta_n\lt\omega_1$ such that $A_{n,\beta_n}$ is stationary. Now, $\cap_{n\lt\omega}A_{n,\beta_n}=\lbrace\alpha\lt\omega_1\mid(\forall n\lt\omega)(t_\alpha(n)=\beta_n)\rbrace,$ which has at most one element, so it trivially doesn't contain a closed unbounded set. Therefore some $A_{n,\beta_n}$ doesn't contain a closed unbounded set.
We claim that each $A_{n,\beta}$ is $\Pi^1_2.$ Let $s$ be a real that codes $\beta.$ For any real $x,$ the following are equivalent:
(1) $x$ codes an ordinal in $A_{n,\beta};$
(2) for every countable transitive model $M$ of ZFC containing $x$ and $s,$ $M \models t(n)=\beta,$ where $M \models "\!x$ codes the ordinal $\alpha, s$ codes the ordinal $\beta,$ and $t$ is the $\lt_L-$least function mapping $\omega$ one-one onto $\alpha\!".$
(3) for every real $u,$ if $u$ codes a countable well-founded model of ZFC, and if there exist integers $x', \,s', \,a', \,b',$ and $t'$ coding members of (the model coded by) $u$ such that:
$\bullet \;u$ satisfies: $x'$ and $s'$ are reals coding the ordinals $a'$ and $b',$ respectively,
$\bullet$ for each $k\lt\omega, \;k\in x\iff u$ satisfies $k\in x',$ and $k\in s\iff u$ satisfies $k\in s',$
and $\bullet \;u$ satisfies: $t'$ is the $\lt_L-$ least function mapping $\omega$ one-one onto $a',$
then
$\bullet \;u$ satisfies: $t'(n)=b'.$
All the quantifiers here are numeric except the ones at the very beginning, so we can write this as:
"for every real $u,$ $u$ is not well-founded or $\ldots",$
which is $\Pi^1_2,$ if I haven't made a mistake in the analytical hierarchy computation.
One should really replace ZFC here by some finite subset of ZFC that is large enough to prove all the facts about $L$ and absoluteness you need; if you do that, the proof is formalizable in ZFC.
Added later: The counterexample above actually appears to be $\Delta^1_2,$ since $"\!x\in A_{n,\beta}\!"$ is also equivalent to: "there exists $u$ such that $u$ codes a countable transitive model and there exist integers $x', \,s',$ etc., such that all the bulleted statements above hold."
Also, maybe I should have pointed out that this solves the problem since a stationary set that doesn't contain a closed unbounded set is the same thing as a set which neither contains nor is disjoint from a club.
A minor fix: $A_{n,\beta}$ should be defined as $\lbrace \alpha \lt \omega_1 \mid \alpha \ge \omega$ and $t_\alpha(n)=\beta\rbrace,$ since the way I set it up, $t_\alpha$ isn't defined for $\alpha \lt \omega.$ This doesn't change anything substantial in the proof though.