If $T$ is a theorem of ZF which says something only about reals, then one may want to prove $T$ using a theory like 2nd order PA or related theories like ZFC$^-$ or GBC$^-$ (minus accounts for the absence of the Power Set axiom). In many cases this goes through, sometimes rather straightforwardly, but there are important counterexamples like Borel Determinacy.

Therefore I wonder whether the diamond $\Diamond_{\omega_1}$ is provable in [2nd order PA, or ZFC$^-$, or GBC$^-$] + [all reals are constructible].

Or at least whether [2nd order PA, or ZFC$^-$, or GBC$^-$] + [all reals are constructible] + $\Diamond_{\omega_1}$ is equiconsistent with 2nd order PA.

It is not quite clear how one can adequately formulate $\Diamond_{\omega_1}$ in say ZFC$^-$. However in GBC$^-$ a standard definition of $\Diamond_{\omega_1}$ can be reformulated with several class quantifiers. Thus the problem is to figure out whether $\Diamond_{\omega_1}$ is relatively consistent with GBC$^-$. (Not more than the consistency of GBC$^-$ should be assumed.)

  • $\begingroup$ I guess the proof of $\diamondsuit$ presented in Jech's book shows $\mathsf{GBC}^-+\diamondsuit_{\omega_1}$ has the consistency strength below $\mathsf{KM}^-$, by carrying over Jech's argument over $\mathsf{ZFC}^-$ + $V=L$ + "$L_{\omega_1}$ exists", whose consistency strength is equal to that of $\mathsf{KM}^-$. (I guess $\mathsf{GBC}^-$ + $\Pi^1_1$-Separation + $\Sigma^1_1$-Class Choice might be enough.) $\endgroup$
    – Hanul Jeon
    May 12, 2023 at 20:02
  • $\begingroup$ Do you mean third order arithmetic instead of second order arithmetic? I don't see how $\diamond_{\omega_1}$ can be stated in the language of second order arithmetic (unless you think of it as a scheme). $\endgroup$
    – Ali Enayat
    May 13, 2023 at 21:46
  • $\begingroup$ Ali: yes as a shceme. That is, fix a canonical $\Delta_1$ definable diamond-sequence by say Jech-millenium, this is a formula say A of PA2. Say immediately that A defines a (coded) $\omega_1$ sequence of ctble sets of ordinals. Then claim that for any formula B which defines a subclass of $\omega_1$ the class $G$ of ordinals with right guesses is stationary. And stationarity needs another $\forall$ quantifier over formulas. $\endgroup$ May 14, 2023 at 19:21
  • 1
    $\begingroup$ I may add that some ensuing results do not go through in PA2 and/or ZFC$^-$, like eg Jensen's theorem 1970 on minimal $\Pi^1_2$ real singleton - neither via diamond nor via Jensen's original argument (which also involves ordinals bigger than $\omega_1$). $\endgroup$ May 14, 2023 at 19:30
  • $\begingroup$ Your title question doesn't seem to match the questions you ask in the body of the post, since in the title you ask for consistency (which is obviously yes) and in the body you ask for provability. $\endgroup$ Dec 6, 2023 at 14:00

2 Answers 2


Here is my attempt: Let us work over $\mathsf{ZFC^-} + V=L_{\omega_1}$, that is, $V=L$ holds and every set is hereditarily countable. Then consider the following "minimal" definition of the $\diamondsuit$-sequence:

$(S_\alpha,C_\alpha)$ is the $<_L$-least pair $S_\alpha\subseteq\alpha$, $C_\alpha\subseteq \alpha$ such that $S_\alpha\cap\xi \neq S_\xi$ for all $\xi\in C_\alpha$. Otherwise, $S_\alpha=C_\alpha=\alpha$.

It gives a $\Sigma_1$-definable class $\langle S_\alpha\mid \alpha\in\mathrm{Ord}\rangle$. Let us call this sequence the minimal $\diamondsuit$-sequence.

I claim that the minimal $\diamondsuit$-sequence $\langle S_\alpha\mid \alpha\in\mathrm{Ord}\rangle$ really gives a diamond sequence in the following sense:

For every definable class $X=\{\alpha\in\mathrm{Ord}\mid \phi(\alpha,p)\}$ and a definable club $C=\{\alpha\in\mathrm{Ord}\mid \psi(\alpha,q)\}$, there is $\alpha\in C$ such that $X\cap\alpha=S_\alpha$, that is, $$\exists \alpha [\psi(\alpha,p)\land S_\alpha=\{\xi<\alpha\mid \phi(\xi,q)\}.]$$

It mostly follows from the standard proof, which is available in, say, Jech's book. Assume the contrary that our "minimal" $\diamondsuit$-sequence is not a diamond sequence. Then we have formulas $\phi(\alpha,p)$ and $\psi(\alpha,q)$ such that $C=\{\alpha\mid \psi(\alpha,q)\}$ forms a class club and $$\forall\alpha [\psi(\alpha,q)\to S_\alpha\neq \{\xi<\alpha\mid\phi(\xi,p)\}].$$

Now assume that both of $\phi$ and $\psi$ are at most $\Sigma_n$ for some $n\ge 1$. Let us observe that $\vDash_{\Sigma_n}$ enumerates all possible $\Sigma_n$-formulas, and is $\Sigma_n$-definable. Thus we can "well-order" classes of the form $\{x\in L\mid \vDash_{\Sigma_n}\phi(x,p)\}$ in a manner that is coherent with the well-order over $L$.

I should specify the well-order over $L$: Let us recursively define $<_\alpha$ over $L_\alpha$ as follows. For technical convenience, let $\operatorname{Def}(X)$ be the set of all subsets of $X$ definable by formulas of the form $\exists x_0\forall x_1\cdots \mathsf{Q} x_{n-1}\phi(\vec{x},y,p)$ for some bounded formula $\phi$, where $\mathsf{Q}$ is an appropriate quantifier. Let us call such formulas normalized $\Sigma_n$-formulas.

Fix an enumeration $\langle\phi_\nu\mid \nu<\omega^2\rangle$ of all normalized formulas of the aforementioned form such that $\{\phi_{\omega\cdot n+k}\mid k<\omega\}$ is the set of all normalized $\Sigma_n$-formulas. Now consider the following order:

$<_\delta=\bigcup_{\alpha<\delta} <_\alpha$ if $\delta$ is a limit, and for $X,Y\in\operatorname{Def}(L_\alpha)$, we say $X<_{\alpha+1} Y$ if either

  • $X,Y\in L_\alpha\land X<_\alpha Y$, or
  • $X\in L_\alpha \land Y\notin L_\alpha$, or
  • If $\mu, \nu<\omega^2$ are the least ordinals such that $X=\{x\in L_\alpha\mid \phi_\mu(x,p)\}$ and $Y=\{x\in L_\alpha\mid \phi_\mu(x,q)\}$ for some $<_\alpha$-minimal $p,q\in L_\alpha$, then either $\mu<\nu$ or ($\mu=\nu$ and $p<_\alpha q$).

With the help of $\vDash_{\Sigma_n}$, we can enumerate all $\Sigma_n$-definable classes, and we can well-order $\Sigma_n$-definable classes with respect to the above order. However, unlike the usual $<_L$, the well-order between classes is not $\Sigma_n$. I have not computed precisely, but I suspect its complexity is below $\Sigma_{n+3}$.

Thus we can pick the minimal $(\phi,p)$ and $(\psi,q)$ under the above well-order satisfying the failure of "the minimal $\diamondsuit$-sequence" being a diamond.

Now consider the countable $\Sigma_{n+99}$-Skolem hull $M$ of $L$ containing the transitive closure of $p$ and $q$. By Mostowski's collapsing lemma and condensation, we have the collapsing map $\pi\colon M\cong L_\delta$ for some ordinal $\delta$ such that $\pi(p)=p$ and $\pi(q)=q$.

Since our minimal $\diamondsuit$-sequence is $\Sigma_1$-definable without parameters, its definition is absolute between $L_\delta$ and $L$. Furthermore, since $\pi$ fixes $p$ and $q$, $C$ and $X$ are also absolute between $L_\delta$ and $L$. In addition, $L_\delta$ thinks the following holds:

  1. $C\cap\delta=\{\xi<\delta\mid \psi(\xi,q)\}$ is a class club.
  2. For every $\xi<\delta$, if $\psi(\xi,p)$, then $S_\xi\neq \{\eta<\xi\mid \phi(\eta,p)\}$.

From the first fact that $C\cap \delta$ forms a class club, $\delta\in C$. Hence by the assumption, $S_\delta\neq \{\xi<\delta\mid \phi(\xi,p)\}$. However, the second fact with the minimality of $(\phi,p)$ and $(\psi,q)$ tells $(X\cap \delta, C\cap\delta)$ is the $<_L$-least pair witnessing the definition of the minimal $\diamondsuit$-sequence, so $X\cap \delta = S_\delta$, a contradiction.

  • 3
    $\begingroup$ Yes it likely works, see also jdh.hamkins.org/diamond-on-the-ordinals with a similar argument, where the goal is an Ord-long Diamond yet the proof is adaptable to the $\omega_1$-long case. $\endgroup$ May 24, 2023 at 5:40
  • $\begingroup$ @VladimirKanovei I had not aware of Hamkins' argument, but it looks interesting. $\endgroup$
    – Hanul Jeon
    May 24, 2023 at 19:26
  • 3
    $\begingroup$ I myself was informed a few days ago, see also DOI:10.1017/jsl.2017.75 for a JSL paper where the argument was reproduced. $\endgroup$ May 25, 2023 at 20:14

In the case of $\text{GBC}^-$, the answer is no, $\Diamond$ is not provable from the assumption that all reals are constructible. It is consistent with $\text{GBC}^-$ and even $\text{KM}^-$ that $\Diamond$ fails, yet every real is constructible. (Indeed, this is a consequence of the fact that it is consistent with ZFC itself that $\Diamond$ fails and every real is constructible.)

To produce a model of this, start in $L$. Evidently there is a way to force Suslin's Hypothesis (killing all Suslin trees) without adding reals. My understanding is that Jensen provided such an argument in the 1970s, simply performing an iteration of length $\omega_2$ that kills all possible $\Diamond$-sequence candidates, but the difficulty is prove no reals are added. There are better methods available for this today — see the answers on this thread. Let me black box these argument and proceed.

Start in $L$, and perform the forcing to $L[G]$, which will be a model in which every real is constructible, yet $\Diamond$ fails. This will be visible in the $\text{KM}^-$ model arising from the hereditarily countable sets $H_{\omega_1}$ and it classes in $L[G]$.

The relevant feature of the model is that knowing every real is constructible does not imply that every class is constructible, since in effect the forcing created new classes over $H_{\omega_1}$, but no new sets.

A very similar phenomenon arises with KM class theory, where the assertion $V=L$ can be seen as ambiguous. Namely, knowing that $V=\bigcup_\alpha L_\alpha$ does not imply that every class arises constructibly in the continued iteration of the $L$-hierarchy beyond Ord using class codes for metaordinals. This issue is connected with the Class Collection (aka Class Choice) principle. The CC axioms does not hold in all KM models, but it does hold in models of V=L, provided also that every class is constructible. And furthermore, one can cut down the KM model to include just those classes that are constructible, and thereby see that KM and KM+CC are mutually interpretable.

  • 1
    $\begingroup$ I thought for a minute whether your result contradicts my one, and I found that it is not: What I provided is a diamond for definable classes, and what you provided is a model of second-order set theory with the failure of $\diamondsuit$ because there are (non-definable) classes killing diamonds. $\endgroup$
    – Hanul Jeon
    Dec 6, 2023 at 19:20
  • 1
    $\begingroup$ Yes, exactly. I should have mentioned it. The generic $\Diamond$-killing classes will not be definable. One can make them definable in a $\text{ZFC}^-$ model by further forcing above $\omega_1$, of course, by coding into GCH pattern or whatever, but your additional assumption that $V=L_{\omega_1}$ prevents that. $\endgroup$ Dec 6, 2023 at 22:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.