# Minimal model of ZF with $0\sharp$

We know that the constructible universe $L$ is an absolute and minimal model of ZF (every standard model of ZF contains "an" $L$, and it is actually the same $L$ for all of them).

It is also my understanding that the existence of $0\sharp$ informally means that $V$ is much "bigger" than $L$ (meaning that if $0\sharp$ exists then even $\aleph_1$ is already an inaccessible cardinal in $L$) and that a sort of converse is true (see: https://en.wikipedia.org/wiki/Jensen%27s_covering_theorem).

Therefore my question is: Is there an absolute minimal model of ZF + $\exists0\sharp$ ? A sort of "$L\sharp$" if we really want to abuse notation?

• Sure. The model is denoted $L[0^\sharp]$. You mimic the construction of $L$, but allow in your language a predicate for $0^\sharp$ (understood as a set of numbers). – Andrés E. Caicedo Feb 28 '16 at 0:18
• Isn't $L(0\sharp)$ smaller? – Alon Navon Feb 28 '16 at 0:26
• We have $L[0^\sharp] = L(0^\sharp)$: In general, for any given set $A$, we have $L[A] \subseteq L(A)$ with equalitiy if and only if $A \cap L[A] = A$. Since $0^\sharp$ may be regarded as a subset of $\omega$, we have $0^\sharp \subseteq L \subseteq L[0^\sharp]$ and thus the claimed equality. – Stefan Mesken Feb 28 '16 at 0:38
• @Stefan Thank you very much, I got my relative constructibility all mixed up, and you cleared a lot. :) This means in essence that we can define a "sharp" sequence. $L_0 = L$, $L_1 = L[0^\sharp]$, $L_2 = L[0^{\sharp\sharp}]$, etc... Just wondering whether there is any use for this? Any other nice properties that make these "L's" "L-ish"? – Alon Navon Feb 28 '16 at 0:49
• Well, $L[A]$ is similar to $L$ in a lot of ways - a major reason for this is, that the usual condensation lemma generalizes to $L[A]$ (which allows us to prove $\operatorname{GCH}$, $\Diamond_\kappa$, $\square_\kappa$, ... on a "tail segment" of $L[A]$). – Stefan Mesken Feb 28 '16 at 1:19

Yes, the minimal such model is $$L[0^\sharp]$$. This model can be built by stages, just as $$L$$, starting with the empty set, taking unions at limit stages, and at each successor stage $$\alpha+1$$ taking the collection of subsets of $$L_\alpha[0^\sharp]$$ definable in $$(L_\alpha[0^\sharp],\in,0^\sharp)$$ from parameters. Here, $$0^\sharp$$ can be thought of as a set of natural numbers, and definability is in the language of set theory with one additional predicate.
Note that for each finite $$n$$, $$L_n[0^\sharp]=L_n$$ (that is, the universes of both structures coincide) and so $$L_\omega[0^\sharp]=L_\omega$$. However, $$0^\sharp$$ is now definable at this stage (as the set of numbers satisfying the new predicate), so $$0^\sharp\in L[0^\sharp]$$.
This is not quite enough. Let $$\varphi(x)$$ be the formula in the language of set theory stating that $$x$$ is $$0^\sharp$$, i.e., stating that $$x$$ is the unique EM blueprint satisfying the three indiscernibility conditions listed in section 9 of
One should also check that $$L[0^\sharp]\models \varphi(0^\sharp)$$, and that whenever $$M$$ is an inner model and $$M\models\varphi(a)$$ for some $$a$$, then $$0^\sharp$$ exists in $$V$$ and $$a=0^\sharp$$, so that $$L[0^\sharp]\subseteq M$$. This is essentially an absoluteness argument, but it is a bit technical so I will skip the details here. The point of proving this is that not only is $$L[0^\sharp]$$ the smallest such model, but it knows it, in the sense that it satisfies $$L[0^\sharp]\models V=L[0^\sharp]$$, and is contained in any inner model that believes in the existence of $$0^\sharp$$.
One can prove more as well, for instance, $$L[0^\sharp]$$ satisfies appropriate analogues of the fine structural properties of $$L$$, so it is not just the least model containing $$0^\sharp$$, it is also a very well-behaved model. Naturally, the construction generalizes to more general sharps and other inner-model theoretic objects, although the absoluteness requirements become more involved.