Complexity of $L[\mathrm{cf}]$

Question

Assuming large cardinal axioms, which real numbers are in $L[\mathrm{cf}]$, where $\mathrm{cf}$ is the cofinality function on ordinals?

$L[\mathrm{cf}]$ is the minimal inner model that 'knows' the cofinality of every ordinal in V, or more precisely, $∀α\,\{(β,\mathrm{cf}(β)):β<α\}∈L[\mathrm{cf}]$. Cofinality in $L[\mathrm{cf}]$ need not equal cofinality in $V$.

I have a solution to a simpler problem:
Theorem: A real number is in $L$[Card] iff it is in the minimal inner model with a proper class of measurable cardinals (assuming the sharp for this model exists). Here, Card is the cardinality function.
Corollary (under the same assumption): The theory of $(L[\mathrm{Card}],∈,\mathrm{Card})$ is $Δ^1_3$.
Proof sketch of the theorem: Starting with the minimal inner model $M$ with a proper class of measurable cardinals, iterate the first measurable cardinal until it becomes $ω_1^V$, the second until it becomes $ω_2^V$, and so on for every regular successor cardinal in $V$. For the converse, every $ω_{α+ω}$ can be shown to be measurable in HOD^L[Card] with $\{ω_{α+1}, ω_{α+2}, ω_{α+3}, ...\}$ Prikry generic over HOD^L[Card].
Additional details on the proof: If $M$ is iterated until we get $M'$ with measurable cardinals matching regular $V$-cardinals except that the next measurable cardinal after $ω_α^V$ is $ω_{α+ω}^V$, then $S = (ω_{α+1},ω_{α+2},...)$ is Prikry generic over $M'$ since if a measurable cardinal is iterated, a cofinal sequence of length $ω$ of its past values is Prikry generic. Now, $\mathrm{HOD}^{L[\mathrm{Card}]}⊂\mathrm{HOD}^{M'[S]}=M'$ and $S∈L[\mathrm{Card}]$, so $S$ is also Prikry generic over $\mathrm{HOD}^{L[\mathrm{Card}]}$.

For the cofinality problem, my conjecture is to use a model $M$ (closely related to $L[\mathrm{cf}]$) such that:
nonmeasurable regular cardinals in $M$ have $V$-cofinality $ω$,
measurable cardinals of order $α$ in $M$ have $V$-cofinality $ω_{α+1}$ (or $ω_α$ if $α$ is weakly inaccessible (in $V$) plus a finite ordinal),
and $M$ is obtained by iterating away the least mouse with a measure concentrating on cardinals with $o(κ)=κ$, and iterating the measures until the above correspondences hold. However, I do not know whether this works, or for that matter, whether the theory of $L[\mathrm{cf}]$ is generically absolute.

An extension of the problem is to set $\mathrm{cf}(κ)=κ+α$ iff $κ$ is weakly $α$-Mahlo, which is well-defined for $α≤κ^+$. A $κ^+$-Mahlo $κ$ is called greatly Mahlo. For comparison, a limit ordinal $κ$ has cofinality $≥α$ iff for every (infinite) regular $β<α$, ordinals of cofinality $β$ are stationary below $κ$. (Also, if singular $κ$ pose a problem, I would be happy to see a solution for this extension with $\mathrm{cf}(κ)$ restricted to regular $κ$.) It appears plausible that the construction using orders of measurability can be extended to this problem, with weakly greatly Mahlo cardinals corresponding to $M$-cardinals that are strong up to a measurable. If that is the case, then under large cardinal axioms, all reals in $L[\mathrm{cf}]$ are still $Δ^1_3$.

Answer 1

Дмитро, can you expand a bit on how you prove that every ℵ_α+ω is measurable in the HOD of L[Card] and why the sequence of the ℵ_α+ns is Prikry generic, assuming there is a sharp for an inner model with a proper class of measurable cardinals? Thanks, Ralf. Regardless of that, the result is correct: if L[Card] doesn't have an inner model with a proper class of measurable cardinals, then we may compare K^L[Card] with the sharp for an inner model with a proper class of measurable cardinals; a half-open interval from Card may then be used to produce a measure on an iterate of K^L[Card] which may be pulled back to K^L[Card]; this measure is in L[Card], which gives a contradiction. Your question about the complexity of the reals of L[cf] is related to the question: which reals does C* have (where C* is the least inner model which knows which ordinals have countable cofinality)? Magidor showed C* has 0^† and more, and with him I showed (assuming a measurable cardinal above a Woodin cardinal in V) that all the reals of C* are in M₁, the least inner model with one Wodin cardinal (so that K^C* exists and is 1-small).