If we disregard the model of computation we want to use, a lost melody is a decidable singleton $\{x\}$ such that the point $x$ is non-computable. Classical computability theory cannot admit any lost melodies in $2^\omega$ because there are no decidable singletons in the first place, and it cannot admit lost melodies in $\mathbb{N}$ because there are no non-computable points.
We could weaken the requirement (as you may be doing in your question), and only ask for $\{x\}$ to be $\Pi^0_1$, meaning that we can recognize the complement of $\{x\}$ but not necessarily $\{x\}$ itself. With $2^\omega$ as ambient space, this still doesn't give us any examples. However, if use $\omega^\omega$, then we see that every hyperarithmetical Turing degree has a representative $x$ such that $\{x\}$ is $\Pi^0_1$.
Another way to get lost melodies without using a more powerful model of computation would be to move towards computable analysis, and to use general represented spaces as ambient spaces. This allows us trivial constructions such as considering any singleton $\{p\}$ for $p \in 2^\omega$ as ambient space in its own right, and since $\{p\}$ is trivially a decidable subset of $\{p\}$, we have plenty of lost melodies here. On the other hand, "nice" represented spaces would generally be computably separable, which immediately implies that every computably open (ie $\Sigma^0_1$) singleton consists of a computable point.
For ordinal Turing machines with an oracle $S⊂Ord$,
- the set/class of output locations that are written at some point is $Σ^{L[S]}_{1,S}$ (i.e. $Σ_1$ in $L[S]$ with a predicate for $S$) and can be arbitrary such,
- the set/class of output locations that are eventually 1 is $Σ^{L[S]}_{2,S}$ and can be arbitrary such,
- any set in $L[S]$ (but no set not in $L[S]$) can be 'accidentally' written at some point.
The supremum of eventually writable (as subsets of $ω$) ordinals $τ_0$ is the least ordinal that is not $Δ^{L[S]}_{2,S}$ definable. The supremum of stabilization times $τ_1$ is the supremum of $Δ^{L[S]}_{2,S}$ definable ordinals (possibly uncountable). Similarly, the supremum of writable (as subsets of $ω$) ordinals is the least ordinal not $Δ^{L[S]}_{1,S}$ definable, and the supremum of halting times is the supremum of $Δ^{L[S]}_{1,S}$ definable ordinals.
Your question corresponds to $S=\mathrm{Card}$ (cardinals). I actually considered $S=\mathrm{Card}$ in the question Cardinal Register Machines, but it is worth it to elaborate it further.
Case 1: There is no sharp for a proper class of measurable cardinals. Then:
- $K^{L[\mathrm{Card}]}$ is an iterate of the core model $K$. ($K^{L[\mathrm{Card}]}$ does not have a sharp since otherwise enough cardinals will be indiscernible to generate a proper of class of measurables $K^{L[\mathrm{Card}]}$.)
- If $V=K$ (which holds if $V=L$), then for sets below the least measurable cardinal (or arbitrarily if there are none), $Δ^{L[\mathrm{Card}]}_{1,\mathrm{Card}}=Δ_2$ and $Δ^{L[\mathrm{Card}]}_{2,\mathrm{Card}}=Δ_3$. I think the only difference between $K$ and $L[\mathrm{Card}]$ (if $V=K$) is that every measurable cardinal $κ$ (and its measure) in $K$ is converted into a Prikry sequence $κ,κ^{+},κ^{++},...$ for $κ^{+ω}$.
- Non-absoluteness: There is an ordinal Turing machine $M$ such that if $V$ is a (set) generic extension of $K$ (not sure if this condition is needed), then for every set of ordinals $s$, there is a generic extension $V[G]$ such that in $V[G]$ (and using $\mathrm{Card}^{V[G]}$), $M$ outputs $s$ and halts. (For example, $M$ can check which cardinal successors are computed correctly for the least $L_α[\mathrm{Card}]$ that correctly computes enough cardinals.) I think such $M$ (if it works for all such $s$ and $V$) cannot halt if the above sharp exists: In every case, $\mathrm{Card}$ should in a sense give indiscernibles (and thus be unavailable for coding) until $L[\mathrm{Card}∩α]$ contains all reals in $K$, and if the sharp exists, $M$ should be stuck in the pre-decoding phase.
Case 2: There is a sharp for a proper class of measurable cardinals. Then, $K^{L[\mathrm{Card}]}$ is an iterate of the minimal inner model $K'$ with a proper class of measurable cardinals. Writable (as subsets of $ω$) countable ordinals are exactly $Δ_2^{K'}∩ω_1^{K'}$, and eventually writable — $Δ_3^{K'}∩ω_1^{K'}$. Note that these are $Δ^1_3$ (in $V$) and independent of forcing. As an aside, with stronger large cardinal axioms, more structure becomes forcing-independent; for example, see my questions Complexity of L[cf] and Inner models with all sets generic.
Best Answer
Theorem. (ZFC) There is a (parameter-free) definable injective function $f$ from the class of subsets of ordinals to the class of ordinals (i.e., a definable function $f$ satisfying properties (1) and (2) of the question) if and only if $\mathrm{V = OD}$.
Proof. The right-to-left direction readily follows from the well-known fact that there is a (parameter-free) global well-ordering of the class of all sets $\mathrm{V}$ of order-type $\mathrm{Ord}$ (class of ordinals) in the presence of $\mathrm{ZF + V = OD}$.
For the other direction, recall that it is a theorem of $\mathrm{ZFC}$ that every set can be canonically coded by a subset of ordinals (more precisely, for every set $x$ there is a subset $y$ of ordinals such that $x \in \mathrm{L}(y)$). This makes it clear that if there is a definable injection $f$ of the class of subsets of ordinal into the class $\mathrm{Ord}$ of ordinals, then there is an injection $F$ of the class of all sets $\mathrm{V}$ to $\mathrm{Ord}$. More specifically, given a set $x$, let $F(x)$ be $f(y_0)$, where $f(y_0)$ is the minimum element of the set of all ordinals of the form $f(y)$, where $y$ canonically codes $x$. Since $\mathrm{V=OD}$ is equivalent to the existence of a parameter-free definable injection of $\mathrm{V}$ into $\mathrm{Ord}$, this completes the proof.