Getting a model of $\mathsf{ZFC}$ that fails to nicely cover an inner model

Question

Consider the following statement:

$(\dagger)$ $\ $ There is an inner model $M$ such that $M \models \mathsf{GCH}+\square$ and for every countable $X \subseteq \mathrm{Ord}$, there is a countable $Y \in M$ such that $X \subseteq Y$.

When I say $M$ is an ``inner model'' I mean that $M$ is a class (definable with parameters) such that $M \supseteq \mathrm{Ord}$ and $\langle M,\in \rangle \models \mathsf{ZFC}$.

Question: Does the negation of $(\dagger)$ have any large cardinal strength? That is, does the consistency of $\mathsf{ZFC}+\neg(\dagger)$ imply the consistency of large cardinals? And if so, what kind of large cardinals are required for $\neg(\dagger)$?

Here are a few observations:

$\bullet \ $ The statement of $(\dagger)$ seems close in spirit to the statement of Jensen's Covering Lemma. If we were to replace "countable" with "of size $\kappa$" for any uncountable $\kappa$, then this modified version of $(\dagger)$ would follow from the Covering Lemma by taking $M = \mathrm{L}$, and therefore its negation would imply the existence of $0^\sharp$.

$\bullet \ $ However, the Covering Lemma does not imply $(\dagger)$. Furthermore, if we modify $(\dagger)$ by insisting on $M = \mathrm{L}$, then we don't need the failure of the Covering Lemma, or any large cardinal strength at all, to get this modified version of $(\dagger)$ to fail. This is because of Namba forcing. If we start with $\mathrm{L}$ and add a Namba-generic filter $G$, then $\mathrm{L}[G]$ will fail to satisfy ``$(\dagger)$ with $M = \mathrm{L}$.'' However, (I'm fairly certain that) $\mathrm{L}[G]$ is itself still a model of $\mathsf{GCH}+\square$, which means that $\mathrm{L}[G]$ satisfies $(\dagger)$, simply by taking $M = \mathrm{L}[G]$. Therefore Namba forcing does not make $(\dagger)$ fail.

$\bullet \ $ The Singular Cardinals Hypothesis follows from $(\dagger)$. Hence one can force a failure of $(\dagger)$ by forcing $\neg\mathsf{SCH}$, which requires a measurable cardinal $\kappa$ of Mitchell order $\kappa^{++}$. So I know that $\neg(\dagger)$ is consistent relative to large cardinals -- I just don't know whether any large cardinals are actually necessary.

$\bullet \ $ If $(\dagger)$ holds in some ground model $V$, then it continues to hold in any $\omega$-distributive forcing extension of $V$. If $(\dagger)$ and Jensen's Covering Lemma both hold in $V$, then both continue to hold in any cardinal-preserving forcing extension of $V$.

$\bullet \ $ I suppose $(\dagger)$ isn't expressible as a first-order statement in the language of set theory, but it is expressible as a scheme in the metatheory.

My motivation for asking this question is that I've proved a topological theorem using $(\dagger)$ as a hypothesis. I'd like to know my hypothesis can be negated without assuming something with large cardinal strength, like the failure of $\mathsf{SCH}$.

Answer 1

The consistency strength of the failure of $(\dagger)$ is an inaccessible cardinal.

Building on the comment of Mohammad, if $\omega_2^V$ is a successor cardinal in $L$ then there is a set $X \subseteq \aleph_1^V$ such that $L[X]$ computes $\aleph_1, \aleph_2$ correctly, which (assuming $0^\#$ does not exist) is enough, since this model would satisfy $\mathrm{GCH}$.

On the other direction, in the paper "Inner Models from Extended Logics" by Kennedy, Magidor and Vaananen, Theorem 6.6 they show that starting with $V=L$ and an inaccessible cardinal $\kappa$, there is a (modification) of revised-countable-support iteration of a variant of the Namba forcing, such that $V[G] \models \kappa = \aleph_2 = 2^{\aleph_0}$ and $V[G] = (C^*)^{V[G]}$, where the model $C^*$ is $L[A]$, for $A$ the class of all ordinals of countable cofinality.

Since every model witnessing $(\dagger)$ would be able to compute the class $A$ and thus would contain $L[A]$, this model would witness the failure of $(\dagger)$.