In his talk A Condensed History of Condensation, Welch presents the following recursive sharp function, that is total when all sharps exist:
\begin{align*} \# \colon ON &\to \mathcal{P}(ON) \\ \alpha &\mapsto (\#\restriction \alpha)^\# \end{align*}
My question is, why does the co-domain need to be $\mathcal{P}(ON)$, and isn't restricted just to $\mathcal{P}(\omega)$?
I get that maybe for bigger sets $A$ the class of indiscernibles of $L[A]$ will vary, but after all its sharp will always be a set of sentences of the theory of $L[A]$. And isn't this theory always countable (and thus a member of $\mathcal{P}(\omega)$ by Gödel Numbering)? Isn't the only additional symbol of the language of that theory one predicate symbol interpreted as $A$, no matter how big the members of $A$?
I can also frame my question in a more straight forward way. Consider instead the function: \begin{align*} F \colon \mathcal{P}(ON) &\to \mathcal{P}(ON) \\ x &\mapsto x^\# \end{align*}
Assuming all sharps exist, so that $F$ is total, how com some $x^\#$ are not members of $\mathcal{P}(\omega)$?