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

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$?

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.

• The appeal to mice brings to mind the proof that a non-trivial mouse exists, and in fact we were the ones to genetically construct it. – Asaf Karagila Aug 10 '16 at 14:55
• karagila.org/2016/… – Andrés E. Caicedo Aug 10 '16 at 15:14
• Good! This is really helpful. I was entirely confused as to how the real and the mouse were interrellated. I now see that this is to get things slightly the wrong way round (the mouse produces the indiscernibles via the iterated ultrapower, and then this yields the desired properties of the real). – Neil Barton Aug 10 '16 at 21:07

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.

• Great! The key thing is the indiscernibles and the relationship they bear to this set, rather than just the set in itself. This clears things up a lot for me, I was really baffled as to why and how the different definitions connected up with one another. – Neil Barton Aug 10 '16 at 21:09
• I think that this is a very common confusion when students of set theory are studying the topic---you're definitely not the first one---and this is part of why I think that some of the terminology can be improved. – JDH Aug 10 '16 at 21:17
• Yeah, it's then (sort of) clear why you get a $j: L \longrightarrow L$. If you've got the set coding the type of order-indiscernibles, you've got the indiscernibles, and so you can just happily stretch them to yield $j$. There's no mystery as to how you make an embedding out of a real, which had me stumped. Thanks! (that's all a bit rough, but the links between the concepts are a whole lot clearer now). – Neil Barton Aug 10 '16 at 21:29
• Hmph. It's a pity it's not possible to accept both answers... – Neil Barton Aug 12 '16 at 15:25