Is the definable club filter normal?

Question

Work in ZFC with no large cardinal assumptions. Say that a (parameter-definable) class $X \subseteq ORD$ is club if it is closed and unbounded in the sense that:

1. For each $\beta \in ORD$, there exists $\gamma \geq \beta$ such that $\gamma \in X$, and

2. For each $\delta, \epsilon \in ORD$, and each increasing function $\beta : \delta \to \epsilon$, if $\beta(\delta') \in X$ for all $\delta' < \delta$, then $\sup_{\delta' < \delta} \beta(\delta') \in X$.

Now let $X \subseteq ORD \times ORD$ be a (parameter-definable) class. Assume that for each $\alpha \in ORD$, the (parameter-definable) class $X(\alpha) := \{\beta \in ORD \mid (\alpha,\beta) \in X\}$ is club in the above sense.

Consider the diagonal intersection $\Delta_{\alpha \in ORD} X(\alpha) := \{\alpha \in ORD \mid \alpha \in \cap_{\beta < \alpha} X(\beta)\}$. This is again a parameter-definable class.

Question: Does ZFC prove (as a schema in $X$) that the above diagonal intersection $\Delta_{\alpha \in ORD} X(\alpha)$ is club in the above sense?

Answer 1

Work in ZF. As Asaf was probably mentioning in his comment, you have asked two distinct questions, one in the title (referring to a filter), and one in the main body of the question (just referring to clubs). Moreover, the notion asked about in the title hasn't been defined clearly. Given what you wrote in the body of the question, I will presume the following definition:

Let's define "the definable club filter is normal" to mean that for each meta-integer $n$ and $X\subseteq\mathrm{Ord}\times\mathrm{Ord}$ which is $\Sigma_n$-definable in parameters, if for each $\alpha\in\mathrm{Ord}$ there is a club proper class $C\subseteq X_\alpha$ such that $C$ is also $\Sigma_n$-definable in parameters, then there is a club $C$ which is definable in parameters with $C\subseteq$ the diagonal intersection of $\left<X_\alpha\right>_{\alpha\in\mathrm{Ord}}$.

Theorem: The definable club filter is normal (under ZF). (We will in fact end up getting $C$ to be $\Sigma_{n+3}$-or-so-definable in the same parameter used to define $X$, and the conversion from the formula defining $X$ to the formula defining $C$ will be recursive.)

Lemma: the answer to the question in the main body of the question is "yes", in fact just assuming ZF.

Proof: This is what I was referring to in my comment above; the proof here is essentially the usual one: the fact that the diagonal intersection is closed, is (as usual) immediate. Let's show it's unbounded. Let $f:\mathrm{Ord}\to\mathrm{Ord}$ be the function where $f(\alpha)$ is the least $\beta>\alpha$ such that $X_\gamma\cap[\alpha,\beta)\neq\emptyset$ for each $\gamma<\alpha$. (Note indeed $f(\alpha)\in\mathrm{Ord}$.) Then $f$ is definable in parameters, and $\alpha<\alpha'\implies f(\alpha)\leq f(\alpha')$. For each $\alpha\in\mathrm{Ord}$ and each $n<\omega$, $f^n(\alpha)$ exists and is in $\mathrm{Ord}$. (By induction on $n$.) Note that $(\alpha,n)\mapsto f^n(\alpha)$ (with domain $\mathrm{Ord}\times\omega$) is definable from parameters. Thus, by Collection, for each $\alpha\in\mathrm{Ord}$ we can find $\beta\in\mathrm{Ord}$ such that $f^n(\alpha)<\beta$ for each $n<\omega$. Now fix $\alpha\in\mathrm{Ord}$ and let $\beta=\sup_{n<\omega}f^n(\alpha)\in\mathrm{Ord}$. Note that $\beta\in\Delta_{\gamma\in\mathrm{Ord}}X_\gamma$, which proves the diagonal intersection is unbounded, as desired.

Proof of theorem: Fix $n,X$. Given a pair $(\varphi,p)$ where $\varphi$ is a $\Sigma_n$ formula with two free variables and $p$ some set, let $C_{\varphi,p}=\{x\bigm|\varphi(x,p)\}$. Say $(\varphi,p)$ is good if $C_{\varphi,p}$ is a club proper class of ordinals. Let $\mathscr{G}$ be the class of good pairs. Let $f:\mathrm{Ord}\to V$ be the class function where $f(\alpha)$ is the least $\beta\in\mathrm{Ord}$ such that for all $\gamma<\alpha$, there is a good $(\varphi,p)\in V_\beta$ such that $C_{\varphi,p}\subseteq X_\gamma$. For $\alpha\in\mathrm{Ord}$ let $D_\alpha=\bigcap_{(\varphi,p)\in\mathscr{G}\cap V_{f(\alpha)}}C_{\varphi,p}$. Note that $D_\alpha$ is club proper class, much like in the proof of the lemma.

Note that $\mathrm{Lim}\cap\Delta_{\alpha\in\mathrm{Ord}}D_\alpha\subseteq\Delta_{\alpha\in\mathrm{Ord}}X_\alpha$. But $\Delta_{\alpha\in\mathrm{Ord}}D_\alpha$ is club proper class by the lemma, and so so is $\mathrm{Lim}\cap\Delta_{\alpha\in\mathrm{Ord}}D_\alpha$.