Why is $0^\sharp$ not definable in $ZFC$?

Question

I have a little question about $0^\sharp$. I'm sure has a nice and easy answer, but I'm just not seeing it and I think it'll help my understanding of $L$ quite a bit if I can piece the answer together.

Given Godel's constructible universe $L$, we can define $0^\sharp$ as follows:

$0^\sharp =_{df} \{ \ulcorner \phi \urcorner | L_{\aleph_\omega} \models \phi [\aleph_1,...,\aleph_n ]\}$

(N.B. There are a bunch of equivalent ways of defining $0^\sharp$, e.g. through an elementary embedding or through Ehrenfeucht-Mostowski sets. We'll see below why this characterisation is interesting)

Now the existence of $0^\sharp$ has some interesting large cardinal consequences: e.g. it implies $V \not = L$ in a dramatic fashion (e.g. Covering fails for $L$ if $0^\sharp$ exists).

It would be bad then, if $0^\sharp$ were definable in $ZFC$ (by Godel's Second). However, the above definition of $0^\sharp$ looks like it should be definable in $ZFC$. Each of $\aleph_1,...,\aleph_n$ is $V$-definable in $ZFC$: Godel coding has all been settled on, $L_{\aleph_\omega}$ is definable in $V$, and Satisfaction is definable over set sized models. So what stops us using Separation to obtain $0^\sharp$ from $\omega$?

Note I'm not looking for the easy answer: $0^\sharp$ exists $\Rightarrow Con(ZFC)$, and so $0^\sharp$ can't be definable in $ZFC$ (assuming that it's consistent).

I am mindful that a bunch of the notions in the definition are either non-absolute or not definable in $L$ (e.g. every definable cardinal is countable in $L$ if there are the relevant indiscernibles). This only suggests that the identity of $0^\sharp$ is not absolute, not that it (whatever it may be) can't be proved to exist in $ZFC$ (exactly like many $\aleph_\alpha$).

What I really want to know is where the above argument breaks down. What part of the definition of $0^\sharp$ prevents it being definable in $ZFC$?

Answer 1

The classical definition of $0^\sharp$ is as (the set of Gödel numbers of) a theory, namely, the unique Ehrenfeucht-Mostowski blueprint satisfying certain properties (coding indiscernibility). This is a perfectly good definition formalizable in $\mathsf{ZFC}$, but $\mathsf{ZFC}$ or even mild extensions of $\mathsf{ZFC}$ are not enough to prove that there are objects that satisfy it. In $L$ there is no EM blueprint with the required properties.

It happens that if it exists, then $0^\sharp$ indeed admits the simple description given in line 4 of your question, but (unlike $0^\sharp$) the set in line 4 always exists (that is, $\mathsf{ZFC}$ proves its existence, pretty much along the lines of the sketch you suggest), so it is not appropriate to define $0^\sharp$ that way (for instance, that set is not forcing invariant in general).

As you mentioned, there are several equivalent definitions of $0^\sharp$. Some of them are readily formalizable in $\mathsf{ZFC}$, some are not. For example, we cannot talk of a proper class of $L$-indiscernibles in $\mathsf{ZFC}$ alone, but $0^\sharp$ could be defined as such a class.

The modern definition of $0^\sharp$ introduces it not as a theory but rather as a certain mouse, a model of the form $(L_\alpha,U)$ for certain $\alpha$, where $U$ is an (external) $L$-$\kappa$-ultrafilter for some $\kappa$ definable in terms of $\alpha$, with the requirement that the iterates of $L_\alpha$ by $U$ are all well-founded (and some additional technical requirements related to the minimality of this model). This is more in tune with the current approach to inner model theory. Again, this definition is formalizable in $\mathsf{ZFC}$ in a straightforward fashion, but the existence of such a mouse cannot be established in $\mathsf{ZFC}$ alone.

Answer 2

The phrase "$0^\sharp$ exists" refers not merely to the existence of that set, but rather also to the assertion that this collection of formulas has the property of being the type of order-indiscernibles in $L$. So one should take the phrase "$0^\sharp$ exists" as asserting not just that that set exists, but also that it has certain properties that make $0^\sharp$ what it is.

Of course, one can always define in ZFC the type of the cardinals $\aleph_n$ in $L$, just as you wrote it down. And there is no problem with defining that set. But in some ZFC models, that set won't give you any power, the reason you would want to care about $0^\sharp$.

For this reason, I find the "$0^\sharp$ exists" terminology to be a little unfortunate. What the phrase is meant to evoke is that there is a combinatorial object with a certain property that we can describe, which gives us the theory of order-indiscernibles for $L$. When it does exist, it happens to be equal to the set you defined, but that set doesn't always have the desired combinatorial property.