Zero sharp

In mathematical set theory, 0^# (zero sharp, also: 0#) is an important large cardinal number. Formally, 0^# is usually defined as follows:

0^# exists iff there exists a non-trivial elementary embedding j : L → L for the Gödel constructible universe L.

0^#, if it exists, is the real number that codes in the canonical way the Gödel numbers of the true formulas about the indiscernibles in L. Its existence implies that every uncountable cardinal in the set-theoretic universe V is an indiscernible in L and satifies all large cardinal axioms that are realized in L (such as being totally ineffable).

On the other hand, if 0^# does not exist, then the constructible universe L, is the core model - that is, the canonical inner model that approximates the large cardinal structure of the universe considered. In that case, the Covering Lemma holds: If x is an uncountable set of ordinals, then there is a constructible y ⊃ x such that y has the same cardinality as x.

Existence of zero sharp is equivalent to determinacy of lightface analytic games. In fact, the strategy for a universal lightface analytic game has the same Turing degree as 0#.