$A^\#$ and inner models

Solution 1:

One can use the class of indiscernibles to generate elementary embeddings of $L[A]$ to itself with critical point above the supremum of $A$, in much the same way as the indiscernibles of $L$ give us embeddings of $L$ into itself.

By results of Kunen (for $L$, but they generalize straightforwardly), the existence of an embedding $j:L[A]\to L[A]$ that has critical point above the supremum of $A$ implies the existence of $A^\sharp$, so both statements are equivalent.

So, suppose $M$ is an inner model and $M$ thinks that $A^\sharp$ exists. Then $M$ sees an elementary embedding of $L[A]$ into itself. This is clearly seen in $V$ as well. So $A^\sharp$ exists in $V$. The converse does not hold. After all, $L[A]$ sees $A$ but never $A^\sharp$. (However, if $M$ is an inner model that thinks that $A^\sharp$ exists, then $A^\sharp$ exists and coincides with $M$'s idea of it. This can be seen descriptive set theoretically (see below), or using the Kunen characterization. Also, if $A^\sharp$ belongs to $M$, then $M$ thinks that $A^\sharp$ exists, because from the sharp one can easily produce an $L[A]$-normal measure on the indiscernible $i_0$, and one can use this to recover the elementary embeddings.)

There is a better way of thinking about sharps, though, namely in terms of mice. This is probably folklore by now, but a nice reference is Schimmerling's "The ABC's of mice", Bulletin of Symbolic Logic 7 (2001) 485-503.

A sharp is then a model of the form $M=(L_\alpha[A],\in,A,U)$ where $U$ is an (external) measure on some $L_\alpha[A]$ cardinal $\kappa$. We add certain requirements that depend on your fine structural taste (say, $\alpha=\kappa^{++}$ in the sense of $L_\alpha[A]$), $M$ has the same size as $A$ and is sound and iterable. Soundness is a technical condition which essentially ensures $M$ is as small as possible.

Iterability is more complicated but it means that (as you imagine) iterating the process of forming ultrapowers by $U$ and its images only produces well-founded models. All the conditions describing the mouse $A^\sharp$ except for iterability are clearly absolute between inner models and $V$.

Iterability is as well, but this requires an argument. But then absoluteness gives us a positive answer to your question. (This means that if an inner model thinks that the mouse $A^\sharp$ exists, then it does in $V$, and if $A^\sharp$ exists and belongs to an inner model, then the inner model knows that it is $A^\sharp$.)

Consider first the case where $A$ is a subset of $\omega$. Then if one iterates $M$ some countable ordinal number of times, the whole iteration is codable by reals, and we can see that the statement that a real $x$ coding a model is iterable is $\Pi^1_2(x)$ (you basically have to say: every real coding an iteration of $x$ gives a well-founded model). The point is that if some iterate of $x$ is ill-founded, then some countable iterate is ill-founded, so you only need to describe iterations "accessible" by reals.

Finally, if $A$ is not a real, we can pretend that it is by working on a collapse of a sufficiently large initial segment of the universe to verify absoluteness. Or we can form the tree of attempts to build $A^\sharp$ and check that if $M$ thinks that $A^\sharp$ exists, then the tree is ill-founded, so $A^\sharp$ exists in $V$, and if $A^\sharp$ is in $M$, hen $M$ has a witness to the ill-foundedness of the tree. You can see a more detailed sketch of that idea in my paper with Schindler, "Projective well-orderings of the reals", Archive for Mathematical Logic 45 (7) (2006), 783-793, available at my page.

(Of course, one can also go as Jech does and verify the absoluteness of sharps in terms of blueprints, but I prefer the two other approaches I sketched.)