I was recently surprised to discover that if there is a definable well-ordering of the universe, then the diamond principle on the ordinals holds for definable classes, automatically. In fact, the diamond principle for definable classes is simply equivalent in ZFC to the existence of a definable well-ordering of the universe. It follows as a consequence that the diamond principle for definable classes, although seeming to be fundamentally scheme-theoretic, is actually expressible in the first-order language of set theory.

In set theory, the diamond principle asserts the existence of a sequence of objects $A_{\alpha }$, of growing size, such that any large object at the end is very often anticipated by these approximations.  In the case of diamond on the ordinals, what we will have is a definable sequence of $A_{\alpha }\subseteq \alpha$, such that for any definable class of ordinals $A$ and any definable class club set $C$, there are ordinals $\theta \in C$ with $A\cap \theta =A_{\theta }$.  This kind of principle typically allows one to undertake long constructions that will diagonalize against all the large objects, by considering and reacting to their approximations $A_{\alpha }$. Since every large object $A$ is often correctly approximated that way, this enables many such constructions to succeed.

Let me dive right in to the main part of the argument.$$

Theorem. In $\text{ZFC}$, if there is a definable well-ordering of the universe, then ${◊}_{\text{Ord}}$ holds for definable classes. That is, there is a $p$-definable sequence $⟨A_{\alpha }\mid \alpha <\text{Ord}⟩$, such that for any definable class $A\subseteq \text{Ord}$ and any definable closed unbounded class of ordinals $C\subseteq \text{Ord}$ (allowing parameters), there is some $\theta \in C$ with $A\cap \theta =A_{\theta }$.

Proof. The theorem is proved as a theorem scheme; namely, I shall provide a specific definition for the sequence $\overrightarrow{A}=⟨A_{\alpha }\mid \alpha <\text{Ord}⟩$, using the same parameter $p$ as the definition of the global well-order and with a definition of closely related syntactic complexity, and then prove as a scheme, a separate statement for each definable class $A\subseteq \text{Ord}$ and class club $C\subseteq \text{Ord}$, that there is some $\alpha \in C$ with $A\cap \alpha =A_{\alpha }$. The definitions of the classes $A$ and $C$ may involve parameters and have arbitrary complexity.

Let $⊲$ be the definable well-ordering of the universe, definable by a specific formula using some parameter $p$. I define the ${◊}_{\text{Ord}}$-sequence $\overrightarrow{A}=⟨A_{\alpha }\mid \alpha <\text{Ord}⟩$ by transfinite recursion. Suppose that $\overrightarrow{A}\upharpoonright \theta$ has been defined. I shall let $A_{\theta }=\mathrm{\varnothing }$ unless $\theta$ is a $\beth$-fixed point above the rank of $p$ and there is a set $A\subseteq \theta$ and a closed unbounded set $C\subseteq \theta$, with both $A$ and $C$ definable in the structure $⟨V_{\theta },\in ⟩$ (allowing parameters), such that $A\cap \alpha \ne A_{\alpha }$ for every $\alpha \in C$. In this case, I choose the least such pair $(A,C)$, minimizing first on the maximum of the logical complexities of the definitions of $A$ and of $C$, and then minimizing on the total length of the defining formulas of $A$ and $C$, and then minimizing on the Gödel codes of those formulas, and finally on the parameters used in the definitions, using the well-order $⊲\upharpoonright V_{\theta }$. For this minimal pair, let $A_{\theta }=A$. This completes the definition of the sequence $\overrightarrow{A}=⟨A_{\alpha }\mid \alpha \in \text{Ord}⟩$.

Let me remark on a subtle point, since the meta-mathematical issues loom large here. The definition of $\overrightarrow{A}$ is internal to the model, and at stage $\theta$ we ask about subsets of $\theta$ definable in $⟨V_{\theta },\in ⟩$, using the truth predicate for this structure. If we were to run this definition inside an $\omega$-nonstandard model, it could happen that the minimal formula we get is nonstandard, and in this case, the set $A$ would not actually be definable by a standard formula. Also, even when $A$ is definable by a standard formula, it might be paired (with some constants), with a club set $C$ that is defined only by a nonstandard formula (and this is why we minimize on the maximum of the complexities of the definitions of $A$ and $C$ together). So one must give care in the main argument keeping straight the distinction between the meta-theoretic natural numbers and the internal natural numbers of the object theory $\text{ZFC}$.

Let me now prove that the sequence $\overrightarrow{A}$ is indeed a ${◊}_{\text{Ord}}$-sequence for definable classes. The argument follows in spirit the classical proof of $◊$ in $L$, subject to the mathematical issues I mentioned. If the sequence $\overrightarrow{A}$ is not a diamond sequence, then there is some definable class $A\subseteq \text{Ord}$, defined in $⟨V,\in ⟩$ by a specific formula $\phi$ and parameter $z$, and definable club $C\subseteq \text{Ord}$, defined by some $\psi$ and parameter $y$, with $A\cap \alpha \ne A_{\alpha }$ for every $\alpha \in C$. We may assume without loss that these formulas are chosen so as to be minimal in the sense of the construction, so that the maximum of the complexities of $\phi$ and $\psi$ are as small as possible, and the lengths of the formulas, and the Gödel codes and finally the parameters $z,y$ are $⊲$-minimal, respectively, successively. Let $m$ be a sufficiently large natural number, larger than the complexity of the definitions of $⊲$, $A$, $C$, and large enough so that the minimality condition we just discussed is expressible by a ${\mathrm{\Sigma }}_m$ formula. Let $\theta$ be any ${\mathrm{\Sigma }}_m$-correct ordinal above the ranks of the parameters used in the definitions. It follows that the restrictions $⊲\upharpoonright V_{\theta }$ and also $A\cap \theta$ and $C\cap \theta$ and $\overrightarrow{A}\upharpoonright \theta$ are definable in $⟨V_{\theta },\in ⟩$ by the same definitions and parameters as their counterparts in $V$, that $C\cap \theta$ is club in $\theta$, and that $A\cap \theta$ and $C\cap \theta$ form a minimal pair using those definitions with $A\cap \alpha \ne A_{\alpha }$ for any $\alpha \in C\cap \theta$. Thus, by the definition of $\overrightarrow{A}$, it follows that $A_{\theta }=A\cap \theta$. Since $C\cap \theta$ is unbounded in $\theta$ and $C$ is closed, it follows that $\theta \in C$, and so $A_{\theta }=A\cap \theta$ contradicts our assumption about $A$ and $C$. So there are no such counterexample classes, and thus $\overrightarrow{A}$ is a ${◊}_{\text{Ord}}$-sequence with respect to definable classes, as claimed.
QED

Theorem. The following are equivalent over $\text{ZFC}$.

1. There is a definable well-ordering of the universe, using some set parameter $p$.
2. $V={\text{HOD}}_{\{p\}}$, for some set $p$.
3. ${◊}_{\text{Ord}}$ holds for definable classes. That is, there is a set parameter $p$ and a definable sequence $\overrightarrow{A}=⟨A_{\alpha }\mid \alpha <\text{Ord}⟩$, such that for any definable class $A\subseteq \text{Ord}$ and definable class club $C\subseteq \text{Ord}$, there is some $\alpha \in C$ with $A\cap \alpha =A_{\alpha }$.

Proof. Let me first give the argument, and then afterward discuss some issues about the formalization, which involves some subtle issues.

($1\to 2$) $$Suppose that $⊲$ is a $p$-definable well-ordering of $V$, which means that every set has a $⊲$-minimal element. Let us refine this order by defining $x{⊲}^{\prime }y$, just in case $\text{rank}(x)<\text{rank}(y)$ or $\text{rank}(x)=\text{rank}(y)$ and $x⊲y$. The new order is also a well-order, which now respects rank. In particular, the order ${⊲}^{\prime }$ is set-like, and so every object $x$ is the ${\alpha }^{th}$ element with respect to the ${⊲}^{\prime }$-order, for some ordinal $\alpha$. Thus, every object is definable from $p$ and an ordinal, and so $V={\text{HOD}}_{\{p\}}$, as desired.

($2\to 1$) If $V={\text{HOD}}_{\{p\}}$, then we have the canonical well-order of $\text{HOD}$ using parameter $p$, similar to how one shows that the axiom of choice holds in $\text{HOD}$. Namely, define $x⊲y$ if and only if $\text{rank}(x)<\text{rank}(y)$, or the ranks are the same, but $x$ is definable from $p$ and ordinal parameters in some $V_{\theta }$ with a smaller $\theta$ than $y$ is, or the ranks are the same and the $\theta$ is the same, but $x$ is definable in that $V_{\theta }$ by a formula with a smaller Gödel code, or with the same formula but smaller ordinal parameters. It is easy to see that this is a $p$-definable well-ordering of the universe.

($1\to 3$) This is the content of the theorem above.

($3\to 1$) If $\overrightarrow{A}$ is a $p$-definable ${◊}_{\text{Ord}}$-sequence for definable classes, then it is easy to see that if $A$ is a set of ordinals, then $A$ must arise as $A_{\alpha }$ for unboundedly many $\alpha$. In $\text{ZFC}$, using the axiom of choice, it is a standard fact that every set is coded by a set of ordinals. So let us define that $x⊲y$, just in case $x$ is coded by a set of ordinals that appears earlier on $\overrightarrow{A}$ than any set of ordinals coding $y$. This is clearly a well-ordering, since the map sending $x$ to the ordinal $\alpha$ for which $A_{\alpha }$ codes $x$ is an $\text{Ord}$-ranking of $⊲$. So there is a $p$-definable well-ordering of the universe.
QED

An observant reader will notice some meta-mathematical issues concerning the previous theorem. The issue is that statements 1 and 2 are known to be expressible by statements in the first-order language of set theory, as single statements, but for statement 3 we have previously expressed it only as a scheme of first-order statements. So how can they be equivalent? The answer is that the full scheme-theoretic content of statement 3 follows already from instances in which the complexity of the definitions of $A$ and $C$ are bounded. Basically, once one gets the global well-order, then one can construct a ${◊}_{\text{Ord}}$-sequence that works for all definable classes. In this sense, we may regard the diamond principle ${◊}_{\text{Ord}}$ for definable classes as not really a scheme of statements, but rather equivalent to a single first-order assertion.

Lastly, let me consider the content of the theorems in Gödel-Bernays set theory or Kelley-Morse set theory. Of course, we know that there can be models of these theories that do not have ${◊}_{\text{Ord}}$ in the full second-order sense. For example, it is relatively consistent with ZFC that an inaccessible cardinal $\kappa$ does not have ${◊}_{\kappa }$, and in this case, the structure $⟨V_{\kappa },\in ,V_{\kappa +1}⟩$ will satisfy GBC and even KM, but it won’t have ${◊}_{\text{Ord}}$ with respect to all classes, even though it has a definable well-ordering of the universe (since there is such a well-ordering in $V_{\kappa +1}$). But meanwhile, there will be a ${◊}_{\text{Ord}}$-sequence that works with respect to classes that are definable from that well-ordering and parameters, simply by following the construction given in the theorem.

This leads to several extremely interesting questions, about which I am currently thinking, concerning instances where we can have ${◊}_{\kappa }$ for definable classes in $V_{\kappa }$, even when the full ${◊}_{\kappa }$ fails. Stay tuned!