Given $x\subseteq OR$ it is possible to consider its sharp $x^\sharp$: that'is the unique EM-blueprint for a structure of the form $\langle L_\lambda[x],\in, x, y_n, \alpha\rangle_{n\in\omega, \alpha\in x}$ where $\lambda>\omega$ and $\{y_n\}_{n\in\omega}$ is a set of indescirnibles for the structure $\langle L_\lambda[x],\in, x, \alpha\rangle_{\alpha\in x}$. This is the generalized version of the well-known principle $0^\sharp$.
I have read that this kind of subsets cannot be created by forcing. That is, if $x\subseteq OR$ and $x\in V$ then if $\mathbb{P}$ is a forcing notion such that $\Vdash_{\mathbb{P}}\exists x^\sharp$ then necessarily $V\vDash \exists x^\sharp$.
Could someone give me a proof of this fact or provide a good reference to search in?
Thank you!!
What you need to know is that $x^\sharp$, when it is exists, is the unique object satisfying its defining property. So if a notion of forcing $\mathbb{P}$ forced the existence of $x^\sharp$, then there would be a condition $p$ forcing some name $\dot y$ to be the sharp of $\check x$, and in this case, no conditions could ever disagree about what was in $\dot y$, since there is only one possible answer for what is in $x^\sharp$. So we could define $x^\sharp$ in the ground model.
Alternatively, let $G$ and $H$ be mutually generic for the forcing, and then since $\dot y_G=\dot y_H$, since both are $x^\sharp$ in $V[G][H]$, it follows that $x^\sharp\in V[G]\cap V[H]=V$, and so you had $x^\sharp$ already in the ground model $V$.