CHARACTERIZATION OF □_{κ} IN CORE MODELS

ERNEST SCHIMMERLING AND MARTIN ZEMAN

Abstract. We present a general construction of a □_{κ}-sequence in Jensen’s fine structural extender models. This construction yields a local definition of a canonical □_{κ}-sequence as well as a characterization of those cardinals κ, for which the principle □_{κ} fails. Such cardinals are called subcompact and can be described in terms of elementary embeddings. Our construction is carried out abstractly, making use only of a few fine structural properties of levels of the model, such as solidity and condensation.

AMS Subject Classification: 03E05, 03E45, 03E55 Keywords: Square sequence, Extender, Extender model, Fine Structure

In [32], we announced two main results on the combinatorial principle □_{κ} in extender models, that is, in fine structural models L[E] constructed relative to coherent extender sequences. The purpose of the present paper is to give a selfcontained proof of the second result, namely to give a characterization of □_{κ} in Jensen extender models. The current paper should be considered a sequel to [32], where the background material, history, connections with other results and topics and the basic definitions can be found. For the reader’s convenience, we nevertheless recall some crucial notions. Definition (Jensen). Given a cardinal κ, we say that ⟨C_{α}; κ < α < κ^{+} & lim(α)⟩ is a □_{κ}-sequence iff

a) C_{α} is a closed unbounded subset of α;

b) Cᾱ = C_{α} ∩ ᾱ whenever ᾱ ∈ lim(C_{α});

c) otp(C_{α}) ≤ κ. The principle □_{κ} postulates the existence of a □_{κ}-sequence.

Recall that the property b) of square sequences is called coherency. The principle □_{κ} was originally discovered in L by Jensen. With later developements, a wide

2 ERNEST SCHIMMERLING AND MARTIN ZEMAN

variety of similar principles proved to be useful; we will consider just the following generalization. Definition (Schimmerling). Given two cardinals κ and λ, we say that

⟨C_{α}; κ < α < κ^{+} & lim(α)⟩

is a □_{κ,<λ}-sequence iff a) C_{α} is a nonempty family of closed unbounded subset of α satisfying |C_{α}| < λ;

b) C ∩ ᾱ ∈ Cᾱ whenever C ∈ C_{α} and ᾱ ∈ lim(C);

c) otp(C) ≤ κ for all C ∈ C_{α}. The principle □_{κ,<λ} postulates the existence of a □_{κ,<λ}-sequence. Also, we write □_{κ,λ} for □_{κ,<λ^{+}}.

Clearly, □_{κ,1} is just Jensen’s □_{κ}. It is shown in [2, 4, 5] and [11] that □_{κ,λ} does not, in general, follow from □_{κ,<λ̄} for λ̄ < λ. In extender models, however, exactly the opposite happens. Our ultimate result along these lines shows that the failure of □_{κ} is equivalent to that of □_{κ,<κ} and that both are equivalent to a large cardinal property called subcompactness. This property was abstracted by Jensen from Solovay’s proof of the failure of square from supercompactness. A very closely related property was considered few years earlier by Burke [3] who proved that □_{κ} fails whenever

S_{κ} = {x ∈ 𝒫_{κ}(κ^{+}); otp(x) is a cardinal}

is stationary. It follows easily from our main theorem that in L[E], the stationarity of S_{κ} is equivalent to the subcompactness of κ.

What makes subcompactness an attractive large cardinal axiom is that, unlike supercompactness, it can be satisfied in extender models of the kind known today. More precisely, if we could prove weak iterability (see preliminaries) of the premice that appear in background certified constructions similar to those in [13, 22] or [37], we would obtain extender models with subcompact cardinals whenever such constructions are carried out in a sufficiently rich universe. Definition (Jensen). A cardinal κ is subcompact iff given any A ⊂ κ^{+}, there are μ < κ, Ā ⊂ μ^{+} and an elementary embedding

σ : ⟨H_{μ^{+}}, Ā⟩ → ⟨H_{κ^{+}}, A⟩

CHARACTERIZATION OF □_{κ} IN CORE MODELS 3

with critical point equal to μ.

It is clear that σ(μ) = κ whenever σ is as in the previous definition. Notice also that μ is measurable, as it is the critical point of an embedding defined on the entire 𝒫(μ). (Actually, σ witnesses that μ is superstrong, and even 1-extendible.) Since any large cardinal property of μ that is uniformly first order expressible over H_{μ^{+}} is carried up to κ, we see that κ is weakly compact, Ramsey, strongly Π_{n}^{1}-indescribable, etc. On the other hand, κ need not be measurable: If U is a normal measure of Mitchell order 0 and M is the ultrapower of V by U then κ is not measurable anymore, but remains subcompact in M. The preservation of subcompactness follows from the fact that M agrees with V on H_{κ^{+}} and that each embedding σ witnessing subcompactness is an element of H_{κ^{+}}. Theorem 0.1 (Main Theorem). The following statements are equivalent in any Jensen extender model:

a) □_{κ}.

b) □_{κ,<κ}.

c) κ is not subcompact.

d) The set of all ν < κ^{+} satisfying E_{ν} ≠ ∅ is non-stationary in κ^{+}. The heart of the theorem is the implication d) ⟶ a), and its proof is based

on a generalization of Jensen’s original construction of a □_{κ}-sequence in L. His construction uses the so called “condensation properties” of L. An example of a condensation property is Gödel’s result that any elementary substructure of J_{α} has, as its Mostowski collapse, some Jᾱ. The condensation properties used by Jensen to prove □_{κ} in L are more sophisticated. It was realized early on that the kinds of condensation used by Jensen in L fail in general for L[E]. The bulk of this paper is concerned with overcoming this difficulty. Jensen [17] proved the failure of □_{κ} under the assumption that κ is subcompact; this proof is a straightforward elaboration on Solovay’s proof mentioned above. Later [15] he showed that in L[E], the failure of d) implies the failure of □_{κ}. His arguments can easily be adapted to yield both b) ⟶ c) and c) ⟶ d). We give the proofs of both implications at the end of the paper; they are presented with Jensen’s permission.

The methods developed in this paper seem to be applicable to a wide variety of combinatorial constructions in extender models. One such application is the

4 ERNEST SCHIMMERLING AND MARTIN ZEMAN

construction of morasses [33, 34]; these play a key role in studying cardinal transfer properties of extender models. Another such application is Jensen’s global square principle. It postulates the existence of a coherent sequence of closed unbounded sets C_{α} ⊂ α defined on all limit ordinals α and satisfying the requirement otp(C_{α}) < α. Jensen proved that the global square principle is equivalent to the conjunction (∀κ)□_{κ} & □^{S} where □^{S} is the global square principle restricted to the class S of all singular cardinals. More precisely, □^{S} postulates the existence of a global square sequence ⟨C_{α}; α ∈ S⟩ with the additional property that C_{α} ⊂ S whenever otp(C_{α}) > ω. It is shown in [43] that □^{S} holds in any Jensen-type extender model; this result does not require any smallness condition.

The paper is organized as follows. Section 1 contains a detailed description of our notation. In order to make the paper self-contained and because Jensen’s fine structure for extender models is not as well known as that of Mitchell-Steel’s, we chose to make this description quite comprehensive. Section 2 is devoted to protomice, that is, to structures that arise in the course of the construction of a □_{κ}-sequence and that fail to be premice. In particular, to each protomouse M we assign a unique L[E]-level N(M) and establish the exact relationship between the fine structure of M and that of N(M). We then prove a sort of condensation lemma for protomice. It might happen that some L[E]-levels N can have many associated protomice; the crucial point of the construction is a method for finding a canonical protomouse for each such N. We shall develop such a method at the end of Section 2. Section 3 contains the actual construction of a □_{κ}-sequence. The construction involves a certain amount of non-uniformity. κ^{+} is partitioned into two subsets, 𝒮^{0} and 𝒮^{1}. We construct a □_{κ}-sequence on either of them independently, and obtain the final □_{κ}-sequence by merging the two partial sequences. Each of these constructions is treated in a separate subsection. On 𝒮^{0}, we imitate Jensen’s L-construction in a more general setting, and without any substantial new ingredients. The only thing we have to verify is that the construction on 𝒮^{0} will not conflict with that on 𝒮^{1}, more precisely, that C_{α} ⊂ 𝒮^{0} whenever α ∈ 𝒮^{0}. On 𝒮^{1}, the situation is completely new and the construction deals with protomice rather than with L[E]-levels. There are two main issues we have to deal with. First, showing that the recipe for choosing the canonical protomouse is preserved under the embeddings arising in the course

CHARACTERIZATION OF □_{κ} IN CORE MODELS 5

of the construction; these embeddings have very weak preservation properties. Second, as in the case of 𝒮^{0}, we have to verify that our construction will not conflict with that on 𝒮^{0}, in other words, that C_{α} ⊂ 𝒮^{1} whenever α ∈ 𝒮^{1}. The last subsection of Section 3 contains the proofs of the remaining implications of the main theorem.

Acknowledgement. The first author was supported in part by NSF grant DMS-0088948. Various parts of the work presented in this paper were done while the second author was affiliated to the following institutions: Humboldt Universität zu Berlin (Mathematisches Institut), Universität Wien (Institut für Formale Logik), Slovak Academy of Sciences (Mathematical Institute). During the preparation of the paper for publication, the second author was partially supported by NSF grant DMS-0204728. The second author would like to thank Ronald Jensen, who initially directed him towards inner models, for his support and many helpful discussions.

1. Preliminaries

In this section we shall introduce our notation and terminology and recall some background material. The construction will be carried out in Jensen’s setting [13]. We shall first explain how our version of the general fine structure theory differs from that of Mitchell-Steel’s. The difference is mainly only notational and the reader familiar with the other version will easily be able to find the appropriate translation. We then introduce Jensen premice, which are, in contrast to Mitchell-Steel’s premice, based on delayed indexing of extenders. This indexing was originally suggested by S. Friedman. A detailed description of both the general fine structure theory as well as Jensen premice can be found in [44]. Finally, we state a list of lemmata which will be used in the course of the construction. We believe that, using the material from this section, the proof of □_{κ} will be self-contained and understandable to a reader with basic knowledge of the inner model theory.

Fine Structure. We shall recapitulate the general fine structure theory for acceptable J-structures of the form ⟨J_{α}^{B}, D⟩. The reason for this is that we would like to apply fine structural arguments to a class of structures broader than that of premice. In our notation, J_{α}^{B} is the J-structure of height α constructed relative to B, and the language for this structure includes a predicate symbol denoting B. The

6 ERNEST SCHIMMERLING AND MARTIN ZEMAN

domain of J_{α}^{B} is denoted by |J_{α}^{B}|, but we will be sloppy with the notation whenever there is no danger of confusion and write simply J_{α}^{B} instead. For an acceptable structure M we define the n-th projectum ϱ_{M}^{n} and the n-th standard (master) code with respect to some p ∈ M, denoted by A_{M}^{n,p}, in the usual way. The ultimate projectum ϱ_{M}^{ω} is the ordinal ϱ satisfying ϱ = ϱ_{M}^{n} for all but finitely many n ∈ ω. Setting H_{M}^{n} = |J_{ϱ}^{B}| where ϱ = ϱ_{M}^{n}, the structure M^{n,p} = ⟨H_{M}^{n}, A_{M}^{n,p}⟩ is called the n-th reduct of M with respect to p. The Σ_{1}-Skolem function for M^{n,p} is denoted by h_{M}^{n,p}. We write h_{M} instead of h_{M}^{0,∅}. A formula φ is a Q-formula iff it is of the form (∀u_{1}) ⋯ (∀u_{ℓ})(∃v_{1} ⊃ u_{1})(∃v_{ℓ} ⊃ u_{ℓ})φ̄(v_{1}, ⋯, v_{ℓ}) where φ̄ is a Σ_{1}-formula with no free occurences of u_{1}, ⋯, u_{ℓ}. Q-statements are downward preserved by Σ_{1}- preserving maps, and upward preserved by maps that are Σ_{0}-preserving and cofinal. A map σ : M → N is cofinal just in case that for every y ∈ N there is some x ∈ M such that y ⊂ σ(x). Being an acceptable structure is a Q-property, i.e. there is a fixed Q-sentence ψ such that for every transitive structure M closed under forming singletons, M is acceptable iff M ⊧ φ. The requirement that M is closed under forming singletons is necessary, as this property cannot be expressed in a Q-fashion. To see this, choose any a ⊂ ω that is not an element of J_{α}. Then id : J_{α} → J_{α} ∪{a} is Σ_{0}-preserving and cofinal map between two transitive structures, but J_{α} ∪ {a} is not closed under forming singletons.

In order to avoid talking about reducts, we introduce Jensen’s Σ^{∗}-language, whose detailed description can be found in [9] or [44]. This language differs from the usual language for acceptable J-structures in that it has variables of ω many types, say v^{i} of type i for every i ∈ ω. The formulae are built in the usual way, but there are restrictions on quantifying. Bounded quantifiers ∃v^{i} ∈ v^{j} and ∀v^{i} ∈ v^{j} are allowed only for j ≥ i and we can bind a variable of type i in a formula φ only if φ is of sufficiently low complexity. More precisely, formulae containing only bounded quantifiers of type 0 are Σ_{0}^{(0)} and for every i, each Σ_{1}^{(i)} formula is Σ_{0}^{(i+1)} by definition. Propositional connectives preserve the complexity. Finally, if φ is Σ_{0}^{(i)}, then so are (∃v^{i} ∈ v^{j})φ and (∀v^{i} ∈ v^{j})φ, granting that j ≥ i. A formula φ is Σ_{ℓ}^{(i)} iff it consists of an alternating block of unbounded quantifiers for variables of type i followed by a Σ_{0}^{(i)}-formula, where the above block has length ℓ and its leftmost quatifier is ∃. Π_{ℓ}^{(i)} formulae are defined dually. A formula φ is Σ^{∗} iff it is

CHARACTERIZATION OF □_{κ} IN CORE MODELS 7

Σ_{1}^{(i)} for all i ∈ ω. Finally, φ is Q^{(i)} iff it is of the form (∀u^{i})(∃v^{i} ⊃ u^{i})φ̄(v^{i}) where φ̄ is a Σ_{1}^{(i)}-formula in which u^{i} is not free.

Semantically, variables of type i range over the i-th reduct, so binding variables of type i means quantifying over the i-th reduct. That a relation A ⊂ M is Σ_{ℓ}^{(n)}(M) in p, resp. Σ_{ℓ}^{(n)}(M) is defined in the obvious way. It can be shown that

ωϱ_{M}^{n} = the least ordinal ζ such that there is a Σ_{1}^{(n)}(M) subset of ζ which is not an element of M,

and that A_{M}^{n,p}, h_{M}^{n,p} are uniformly Σ_{1}^{(n)}(M) in p. More precisely, there are fixed Σ_{1}^{(n)} formulae Φ_{n} and Ψ_{n} such that given arbitrary M, n and p ∈ M, Φ_{n} and Ψ_{n} define A_{M}^{n,p} and h_{M}^{n,p} from p, respectively. As we have already mentioned above, the Σ^{∗}-language enables us to talk about the definability over the n-th reduct without making any explicit reference to the reduct. For ℓ > 0 and an arbitrary p we have: A ⊂ H_{M}^{n} is Σ_{ℓ}^{(n)}(M) in p iff A is Σ_{ℓ}(M^{n,p}); if ℓ = 0, only the implication ← holds.

Fix n ∈ ω. A parameter p ∈ [On ∩ M]^{<ω}, such that there is a new Σ_{1}^{(n)}(M) in p subset of ωϱ_{M}^{n} (by “new” we mean a set A such that A ∩ ωϱ_{M}^{n} is not an element of M), is called good, and the collection of all good parameters is denoted by P_{M}^{n}. P_{M}^{∗} = P_{M}^{n} for the least n satisfying ϱ_{M}^{n} = ϱ_{M}^{ω}. Let <^{∗} be the canonical well-ordering of [On ∩ M]^{<ω}, where a <^{∗} b means that a is lexicographically less than b when a and b are viewed as descending sequences of ordinals. The <^{∗}-least element of P_{M}^{∗} is called the standard parameter of M and denoted by p_{M}; the <^{∗}-least element of P_{M}^{n} is called the standard parameter above the n-th projectum and denoted by p_{M}^{n}.

Given an n ∈ ω, there is a class of partial Σ_{1}^{(n)}(M) functions called good functions, which can be treated the same way as elements of M in many situations. This class comprises all partial Σ_{1}^{(n)}(M)-functions with range contained in H_{M}^{n} and their compositions. It follows that for every Σ_{1}^{(n)}(M)-relation R(v_{1}^{i_{1}}, …, v_{ℓ}^{i_{ℓ}}) and any list of good Σ_{1}^{(n)}(M)-functions F_{1}(z⃗), …, F_{ℓ}(z⃗), the composition R(F_{1}(z⃗), …, F_{ℓ}(z⃗)) is again Σ_{1}^{(n)}(M), provided that the ranges of the functions are contained in the domains of these corresponding variables. Morever, the definition of such a composition is uniform and depends only on the definitions of R and F_{i}. A formula φ is a functionally absolute definition for a good function if it defines a good function over every acceptable J-structure. It can be shown that every good function has a functionally absolute definition. An example of a good function is

8 ERNEST SCHIMMERLING AND MARTIN ZEMAN

any h_{M}^{n,p}; its functionally absolute definition is uniform in the parameter p. Another example is the Σ_{1}^{(n)} Skolem function h̃_{M}^{n+1}(z, p) whose domain is contained in H_{M}^{n} × M and which is defined as follows. For a fixed p, h̃_{M}^{n+1}(−, p) is the composition of all h_{M}^{i,p↾i} for i ≤ n, where the innermost function is h_{M}^{n,p}. For instance, h̃_{M}^{2}(⟨i, x⟩, p) = h_{M}^{0,∅}(i_{0}, h_{M}^{1,p}(i_{1}, x)) where i = ⟨i_{0}, i_{1}⟩. Since these functions are universal, each good Σ_{1}^{(n)}-function is equal to h̃_{M}^{n+1}(⟨i, −⟩, −) for some i ∈ ω.

We can now generalize the notion of a Σ_{1}-hull. A Σ_{1}^{(n)}-hull of X ⊂ M is defined in the obvious way. It follows that the Σ_{1}^{(n)}-hull of X is exactly the closure of X under the good Σ_{1}^{(n)}(M)-functions and this closure is, in turn, equal to the image of [X]^{<ω} under h̃_{M}^{n+1}. We denote this image by h̃_{M}^{n+1}(X). More generally, for any X ⊂ H_{M}^{n} and Y ⊂ M we let

h̃_{M}^{n+1}(X ∪ Y) =^{def} {h̃_{M}^{n+1}(⟨i, z⟩, p); z ∈ [X]^{<ω} & p ∈ [Y]^{<ω} & i ∈ ω}.

Recall also that h_{M}^{n,p}(X ∪ {q}) is the set of all values h_{M}^{n,p}(i, ⟨x, q⟩) where i ∈ ω and x ∈ [X]^{<ω} (we assume that X ∪ {q} ⊂ H_{M}^{n}). In most of cases, X and Y will have sufficient closure properties, so that e.g. the images of X and [X]^{<ω} under the Skolem functions will be the same. If p ∈ [On ∩ M]^{<ω} and h̃_{M}^{n+1}(X ∪ {p}) = M (i.e. every x ∈ M is Σ_{1}^{(n)}(M)-definable from p) then p is clearly in P_{M}^{n}(diagonalize to get a new subset of the projectum). The collection of all such parameters is denoted by R_{M}^{n} and we call them very good parameters. R_{M}^{∗} then has the obvious meaning. M is n-sound iff p_{M}^{n} ∈ R_{M}^{n} and M is sound iff p_{M} ∈ R_{M}^{∗}. It can be proved that M is sound iff P_{M}^{∗} = R_{M}^{∗} (and similarly for n-soundness). M is sound above α iff M = h̃_{M}^{n+1}(α ∪ {p_{M}^{n+1}}) where n is such that ωϱ_{M}^{n+1} ≤ α < ωϱ_{M}^{n}.

We shall often work with Σ_{ℓ}^{(n)}-preserving maps π : M → N. Sometimes we will briefly write

π : M ⟶_{Σ_{ℓ}^{(n)}} N.

Note that each such map is automatically Σ_{1}^{(i)} for i < n. For any p ∈ M and q = π(p), the restriction π ↾ H_{M}^{n} : M^{n,p} → N^{n,q} is Σ_{ℓ}-preserving. Moreover, the converse holds whenever p ∈ R_{M}^{n}, i.e. each such restriction can be lifted to the original map – this fact is known as the downward extension of embeddings lemma. Finally, if both p ∈ R_{M}^{n} and q ∈ R_{N}^{n}, the map π ↾ H_{M}^{i}, viewed as a map between

CHARACTERIZATION OF □_{κ} IN CORE MODELS 9

the corresponding reducts, is in fact Σ_{ℓ+n−i}^{(i)}-preserving for every i ≤ n. A Σ_{ℓ}^{(n)}- preserving map π is cofinal iff π has the above preservation degree and π′′H_{M}^{n} is cofinal in H_{N}^{n}. We will often say that π is cofinal at the n-th level. If f is a good Σ_{1}^{(n)}(M)-function in p and π is Σ_{0}^{(n+1)}-preserving, we can define π(f) as the unique good Σ_{1}^{(n)}(N)-function in π(p) with the same functionally absolute definition, as such a function does not depend on the choice of functionally absolute definition for f.

Solidity is a means for characterizing standard parameters. Fix a finite set of ordinals p ∈ M and any ordinal ν ∈ M. Let n be such that ωϱ_{M}^{n+1} ≤ ν < ωϱ_{M}^{n}. Let W_{M}^{ν,p} be the transitive collapse of h̃_{M}^{n+1}(ν ∪ {p − (ν + 1)}) and σ be the inverse to the collapsing map. W_{M}^{ν,p} is called the standard solidity witness to ν with respect to M and p and σ is the associated witness map . As σ is Σ_{1}^{(n)}-preserving, we have

M ⊧ Φ_{n}(i, ξ_{1}, …, ξ_{ℓ}, q) iff W_{M}^{ν,p} ⊧ Φ_{n}(i, ξ_{1}, …, ξ_{ℓ}, q̄)

for every ξ_{1}, …, ξ_{ℓ} < ν and i ∈ ω, where Φ_{n} is the universal Σ_{1}^{(n)}-formula fixed above, q = p−(ν +1) and σ(q̄) = q. A generalized solidity witness for ν with respect to M and p is a pair ⟨Q, r⟩, where Q ⊃ ν is an acceptable J-structure, r ∈ Q is a finite set of ordinals and

M ⊧ Φ_{n}(i, ξ_{1}, …, ξ_{ℓ}, q) ⟶ Q ⊧ Φ_{n}(i, ξ_{1}, …, ξ_{ℓ}, r)

for all ξ_{1}, …, ξ_{ℓ} < ν and i ∈ ω. Clearly, W_{M}^{ν,p} is a generalized solidity witness, but the converse need not hold. On the other hand, W_{M}^{ν,p} ∈ M iff M contains some generalized solidity witness for ν with respect to M and p. If p ∈ P_{M}^{∗} and for each ν ∈ p there is a generalized solidity witness ⟨Q, r⟩ with respect to M and p such that ⟨Q, r⟩ is in M, then p = p_{M} (and similarly for p_{M}^{n}). We say that M is solid iff also the converse holds, i.e. if every ν ∈ p_{M} has a generalized solidity witness with respect to M and p in M (similarly we define n-solidity). Note that if M is solid, then p_{M}^{n} is a lengthening of p_{M}^{m} whenever m < n. Thus, if M is solid then M is sound above α iff M = h̃_{M}^{n+1}(α ∪ {p_{M}}) where n is such that ωϱ_{M}^{n+1} ≤ α < ωϱ_{M}^{n}.

It follows easily that the statement “⟨Q, r⟩ is a generalized solidity witness for ν with respect to M and p” is Π_{1}^{(n)}. Hence, the property of being a generalized solidity witness is preserved upward under Σ_{1}^{(n)}-maps and downward under Σ_{0}^{(n)}-maps. We stress that these preservation properties are typical for generalized solidity witnesses

10 ERNEST SCHIMMERLING AND MARTIN ZEMAN

and fail for standard solidity witnesses – this is the point of introducing generalized solidity witnesses. If M is solid and π(p_{M}) ∈ P_{N}^{∗} then π(p_{M}) = p_{N}. We shall often use one further criterion for preservation of the standard parameter which we state as a lemma on its own.

Lemma 1.1 ([44]). Suppose M is solid, p ∈ M is a finite set of ordinals such that p ∩ α = ∅ and M = h̃_{M}^{n+1}(α ∪ {p}) for some n ∈ ω. If every ν ∈ p has a generalized solidity witness with respect to M and p that is an element of M, then p = p_{M} − α.

A parameter p ∈ P_{M}^{n} is n-universal iff 𝒫(ωϱ_{M}^{n}) ∩ M̄ = 𝒫(ωϱ_{M}^{n}) ∩ M where M̄ is the transitive collapse of h̃_{M}^{n}(ωϱ_{M}^{n} ∪ {p}); note that ωϱn ; M̄ = ωϱ_{M}^{n} in this case. If n = ω we talk about universality. If p_{M}^{n} is n-universal, M̄ is called the n-th core of M and is denoted by core_{n}(M); the inverse to the corresponding collapsing map is called the n-core map. It follows that p_{M}^{n} collapses to pn ; M̄ and the n-core map is cofinal at the n-th level. If n = ω we talk about the core of M, which we denote by core(M), and the core map. (Here p_{M}^{ω} means p_{M}.) More generally, if ωϱ_{M}^{n+1} ≤ ν < ωϱ_{M}^{n} then the transitive collapse of h̃_{M}^{n+1}(ν ∪ {p_{M}}) is called the core of M above ν and denoted by core_{ν}(M); the inverse to the collapsing map is called the associated core map. Thus, if ν = ωϱ_{M}^{n} then core_{ν}(M) = core_{n}(M).

Our constructions will utilize direct limits of diagrams of the form ⟨M_{ι}, σ_{ῑι}; ῑ ≤ ι < γ⟩ where each M_{ι} is acceptable and ⟨σ_{ῑι}⟩_{ῑ≤ι} is a system of commuting maps such that for a fixed n ∈ ω, each σ_{ῑι} : Mῑ → M_{ι} is Σ_{0}^{(n)}-preserving. We are primarily interested in the case where the direct limit of ⟨M_{ι}, σ_{ῑι}; ῑ ≤ ι < γ⟩ is well-founded; such a direct limit is represented by a unique acceptable structure M together with the direct limit maps σ_{ι} : M_{ι} → M such that each σ_{ι}(x) is the object represented by the thread ⟨σ_{ιι′}(x); ι ≤ ι′ < γ⟩. Then σ_{ι} ∘ σ_{ῑι} = σῑ and M = ⋃{rng(σ_{ι}); ι < γ}. If, moreover, there are p_{ι} ∈ P_{M_{ι}}^{n} such that p_{ι} = σ_{ῑι}(pῑ) whenever ῑ ≤ ι < γ, then p = σ_{ι}(p_{ι}) ∈ P_{M}^{n}, all maps σ_{ι} are Σ_{0}^{(n)}-preserving and H_{M}^{m} = ⋃{σ′′_{ι}H_{M_{ι}}^{m}; ι < γ} whenever m ≤ n. One important property of the direct limit maps σ_{ι} is that, although they are merely Σ_{0}^{(n)}-preserving, they actually downward preserve Σ_{1}^{(n)}- statements on a tail-end of γ. To see this, consider a Σ_{0}^{(n)}-formula φ(v_{0}, v_{1}, …, v_{ℓ}) and any a^{1}, …, a^{ℓ} ∈ M. If M ⊧ (∃z^{n})φ(z^{n}, a^{1}, …, a^{ℓ}) then there is an ι_{0} < γ such that for all ι ≥ ι_{0} we have M_{ι} ⊧ (∃z^{n})φ(z^{n}, a_{ι}^{1}, …, a_{ι}^{ℓ}) where σ_{ι}(a_{ι}^{h}) = a^{h}. To see this, pick a witness b ∈ H_{M}^{n} such that M ⊧ φ(b, a^{1}, …, a^{ℓ}) and an ι_{0} such that

CHARACTERIZATION OF □_{κ} IN CORE MODELS 11

{b, a^{1}, …, a^{ℓ}} ⊂ rng(σ_{ι_{0}}). Then b_{ι} = σ_{ι}^{−1}(b) ∈ H_{M_{ι}}^{n} and M_{ι} ⊧ φ(b_{ι}, a_{ι}^{1}, …, a_{ι}^{ℓ}) whenever ι ≥ ι_{0}. The downward preservation property we just verified guarantees that if ζ = h̃_{M}^{n+1}(ξ, p) and (ξ, p) = σ_{ι}(ξ_{ι}, p_{ι}), then ζ_{ι} ≃ h̃_{M_{ι}}^{n+1}(ξ_{ι}, p_{ι}) is defined on an tail-end of γ and ζ = σ_{ι}(ζ). The point here is that h̃_{M_{ι}}^{n+1} is good, i.e. it has a functionally absolute definition. Since Π_{1}^{(n)}-statements are automatically downward preserved under Σ_{0}^{(n)}-preserving embeddings, the above argument actually establishes the downward tail-end preservation for Σ_{2}^{(n)}-statements. Thus, if ψ(u_{1}, …, u_{ℓ}) is a Π_{2}^{(n)}-formula and M_{ι} ⊧ ψ(a_{ι}^{1}, …, a_{ι}^{ℓ}) on an tail-end of γ, then M ⊧ (a^{1}, …, a^{ℓ}).

Extenders and Coherent Structures. Consider two transitive structures M and N that satisfy a sufficiently large fragment of ZFC. Given a cofinal elementary embedding π : M → N and a pair of ordinals κ, λ such that κ is the critical point of π, λ ∈ N is primitive recursively closed and the Σ_{0}-hull of rng(π)∪λ is the entire N, the map F : 𝒫(κ) ∩ M → 𝒫(λ) defined by

F (x) = π(x) ∩ λ

is the extender on M at (κ, λ) derived from π. Then κ is the critical point and λ the length of F, and we denote them cr(F) and λ(F), respectively. In this situation, N is called the ultrapower of M by F and we denote it by Ult(M, F). Also, π is called the associated ultrapower map. The requirement that λ is primitive resursively closed enables us to code finite tuples of ordinals below λ by elements of λ via the Gödel pairing function ⟨η, ξ⟩ ↦ ≺η, ξ≻.

The term “ultrapower” here is not chosen accidentally; it is namely the case that N is the transitive isomorph to the term model 𝔻(M, F) resulting from the ultrapower construction. The domain of 𝔻(M, F) consists of all equivalence classes [α, f] where α < λ, f ∈ M is a function with domain κ, and the pair ⟨α′, f′⟩ is in the same equivalence class as ⟨α, f⟩ just in case that ≺α, α′≻ ∈ F ({≺η, η′≻; f(η) = f′(η′)}). The predicates of the term model are then defined in the obvious way. We will often write

π : M ⟶_{F} N

to express that N = Ult(M, F) and π is the associated ultrapower map.

12 ERNEST SCHIMMERLING AND MARTIN ZEMAN

A closer inspection of the ultrapower construction reveals that in order to establish the basic facts about Ult(M, F) and π one needs merely a finite list of Σ_{0}-properties of F (see [44]), so our definition of an extender is easily seen to be equivalent to the traditional one where an extender is presented as a coherent system of measures on κ indexed by finite subsets of λ. Also in our case it will be useful to have such a “local” characterization of extenders, i.e. a characterization that does not make any reference to the ultrapower map. It can be shown that for primitive recursively closed λ, F is an extender on M at (κ, λ) just in case that

F : 𝒫(κ) ∩ M ⟶ 𝒫(λ)

and for every A_{1}, …, A_{ℓ}, B ∈ 𝒫(κ) ∩ M, if B is primitive recursive in A_{1}, …, A_{ℓ}, then F (B) is primitive recursive in F (A_{1}), …, F (A_{ℓ}) by the same definition.

For α < λ, the measure {x ⊂ κ; α ∈ F (x)} is denoted by F_{α}. Notice that if we want to represent F as a coherent system of measures, these measures can be indexed by ordinals below λ, as λ is primitive recursively closed. Given any primitive recursively closed λ̄ < λ, the “restriction” F | λ̄ of F to λ̄ is the unique extender at (κ, λ̄) satisfying dom(F | λ̄) = dom(F) and (F | λ̄)(x) = F (x) ∩ λ̄.

An extender F at (κ, λ) is weakly amenable with respect to M iff the power set of κ remains unchanged in the corresponding ultrapower, which, in turn, is equivalent to the requirement that for every α < λ and R ∈ M ∩ 𝒫(κ × κ), the set of all ξ < κ satisfying R′′{ξ} ∈ F_{α} is an element of M. F is Σ_{1}-amenable with respect to M if each F_{α} is Σ_{1}(M) for α < λ, and F is close to M iff it has both these properties. The definition of Σ_{1}-amenability does not involve any uniformity, more precisely, for α ≠ β it allows that F_{α} is Σ_{1}(M) in p and F_{β} is Σ_{1}(M) in q where p ≠ q. Finally, F is whole iff π(κ) = λ. An ordinal λ̄ < λ is a cutpoint of F iff F | λ̄ is whole.

Recall that, since π is the ultrapower map of M by F, each x ∈ N is of the form π(f)(α) for some f ∈ ^{κ}M ∩ M and α < λ. If x is an ordinal less than π(κ), we can choose f such that f : κ → κ, and if x ⊂ π(κ) in the ultrapower, we can choose f such that f : κ → 𝒫(κ). In both cases, f can be recursively encoded into a subset of κ, and this coding is uniform. Also, the same applies to functions f with domain ^{n}κ for some n ∈ ω and range contained in κ or 𝒫(κ). Hence, granting that F is whole, we can pretend that we are applying F instead of π to f and

CHARACTERIZATION OF □_{κ} IN CORE MODELS 13

shall write F (f) instead of π(f). In this notation, for instance, if f : ^{n}κ → κ and a ∈ ^{n}λ, we would write F (f)(a) for π(f)(a) instead of using the correct, but clumsy F (f^{∗})^{∗∗}(a) where f^{∗} = {≺η_{1}, …, η_{n}, η≻; f(η_{1}, …, η_{n}) = η} and g^{∗∗} = {⟨η_{1}, …, η_{n}, η⟩; ≺η_{1}, …, η_{n}, η≻ ∈ g}. In general, we will write g(ξ_{1}, …, ξ_{ℓ}) or g(x) instead of g(≺ξ_{1}, …, ξ_{ℓ}≻) for any function g whose domain is contained in ordinals and any finite sequence of ordinals x = ⟨ξ_{1}, …, ξ_{ℓ}⟩, and g(ξ_{1}, …, ξ_{ℓ}, y) instead of g(≺ξ_{1}, …, ξ_{ℓ}, ζ_{1}, …, ζ_{k}≻) where y = ⟨ζ_{1}, …, ζ_{k}⟩ is a finite sequence of ordinals. The expressions F (f)(α_{1}, …, α_{n}), F (f)(a) and F (f)(α_{1}, …, α_{ℓ}, b) then have the obvious meaning. These expressions do make sense even if a, b are finite sets of ordinals, as we can naturally view them as finite increasing sequences.

A J-structure M is coherent iff M is of the form ⟨J_{α}^{A}, F ⟩ where J_{α}^{A} is acceptable, F is a whole extender at (κ, λ) with dom(F) = 𝒫(κ) ∩ J A ; ᾱ for some ᾱ ≤ κ^{+M} and J_{α}^{A} = Ult(J A ; ᾱ, F). Thus, F need not be weakly amenable, but M is always an amenable structure. Clearly, F is weakly amenable iff ᾱ = κ^{+M} (that is, iff F is an extender on M). If F happens to be weakly amenable, we shall sometimes write “F is a total extender on M” to stress this fact. The property of being a coherent structure is a Q-property, i.e. there is a fixed Q-sentence ψ such that for every transitive structure M = ⟨U, F ⟩ closed under forming singletons, M is a coherent structure iff M ⊧ ψ. On the other hand, the weak amenability of F cannot be expressed in a Q-fashion; it is genuinely Π_{2}. Notice also that the statement “λ̄ is a cutpoint of F ” is Π_{1} over a coherent structure M = ⟨J_{α}^{A}, F ⟩.

Fine Ultrapowers. A fine ultrapower of an acceptable J-structure M is obtained by an ultrapower construction which makes use not only of functions that are elements of M, but also of those, which are reasonably definable over M. If k ≤ ω, F is at (κ, λ) and n is such that ωϱ_{M}^{n+1} ≤ κ < ωϱ_{M}^{n}, setting m = min{k, n} we define

Γ_{k}(κ, M) = {f : κ → M; f is a good Σ_{1}^{(m−1)}(M)-function};

here we make a convention that good Σ_{1}^{(−1)}(M)-functions are precisely those functions that are elements of M. Notice that for each k ≤ ω we have ^{κ}M ∩ M ⊂ Γ_{k}(κ, M) since each f ∈ ^{κ}M ∩ M has a functionally absolute Σ_{0}-definition. So Γ_{0}(κ, M) = ^{κ}M ∩ M. Using functions from Γ_{k}(κ, M) we build the term model 𝔻^{k}(M, F) which, provided that it is well-founded, gives rise to the k-ultrapower

14 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Ult^{k}(M, F) of M; if k = ω we talk about the ∗-ultrapower Ult^{∗}(M, F) and denote the associated term model by 𝔻^{∗}(M, F). We also write Γ(κ, M) instead of Γ_{ω}(κ, M) in this case. The domain of 𝔻^{k}(M, F) consists of all equivalence classes [α, f] where α < λ and f ∈ Γ_{k}(κ, M). The equivalence relation in question, as well as the predicates of the term model are defined in the same manner as in the case of ordinary ultrapowers (see above); that these definitions make sense follows from the fact that the definability degree of the functions f is at most n − 1. Notice also that 0-ultrapowers are just ordinary ultrapowers, that is, ultrapowers, where the functions f are elements of M. To indicate that π is the corresponding ultrapower map, we briefly write

π : M ⟶_{F}^{k} N, resp. π : M ⟶_{F}^{∗} N.

Analogously to the case of ordinary ultrapowers, each x ∈ N is of the form π(f)(α) for some f ∈ Γ_{k}(κ, M) and α < λ.

If k ≥ 0, we have the Łoś theorem for Σ_{0}^{(m)}-formulae, where m is as above. The k-ultrapower map π is Σ_{0}^{(m)}-preserving and Σ_{2}^{(i)}-preserving for every i < m. If i < n then π(ωϱ_{M}^{i}) = ωϱ_{N}^{i}. Moreover, if R_{M}^{m} is nonempty, then π(p) ∈ R_{N}^{m} for every p ∈ R_{M}^{m} and π is Σ_{0}^{(m)} cofinal, which means that every x ∈ H_{N}^{m} is of the form π(f)(α) for some f ∈ H_{M}^{m} and α < λ. In this case, forming a k-ultrapower of M is equivalent to forming the corresponding (ordinary) ultrapower of the m-th reduct (relative to some p ∈ R_{M}^{m}) and to additional lifting the associated ultrapower map to M. For k = 0, the ultrapower map is always Σ_{0}-preserving and cofinal. If F is weakly amenable or Σ_{1}-amenable with respect to M or if h_{M}^{n,p} maps κ onto κ^{+M} for some p, then the ∗-ultrapower map π is Σ_{0}^{(n)}-preserving and cofinal (that is, cofinal at the n-th level); if F is close to M, then π is fully Σ^{∗}-preserving.

The ultrapower construction can be generalized in the sense that the role of an extender is played by a sufficiently preserving embedding; the resulting structure is called a pseudoultrapower. (Roughly speaking, this is the process of deriving an extender and taking an ultrapower combined into one.) More precisely, let σ : J_{τ}^{A} → J B ; τ̃ be Σ_{0}-preserving and cofinal. Suppose that M = ⟨J_{α}^{A}, C⟩ and τ = κ^{+M}. For k, n, m as above we let Γ_{k}(σ, M) = Γ_{k}(κ, M); if k = ω we write briefly Γ(σ, M). Now the ultrapower construction can be carried out using σ in place of an extender and the corresponding version of the Łoś theorem will hold

CHARACTERIZATION OF □_{κ} IN CORE MODELS 15

for the term model 𝔻^{k}(M, σ). If k = ω, we write briefly 𝔻^{∗}(M, σ) and if k = 0, we simply omit the superscript. Granted that the term model is well-founded, we can transitivize it to obtain a structure N = ⟨J_{β}^{B}, D⟩ which is an end-extension of J B ; τ̃, and a map σ̃_{k} : M → N extending σ. We write σ̃ for σ̃_{ω}. The map σ̃, resp. σ̃_{k}, is called the canonical extension, resp. k-extension, of σ to M. Letting κ̃ = σ(κ), we have τ̃ = σ̃(τ) = κ̃^{+N}. As in the case of extenders, σ̃_{k} is always Σ_{0}^{(m)}-preserving where m is as above and, if k = 0, also cofinal; moreover, for k > 0, this map is Σ_{2}^{(i)}-preserving whenever i < m. If R_{M}^{m} is nonempty, then σ̃_{k}(p) ∈ R_{N}^{m} for every p ∈ R_{M}^{m} and σ̃_{k} is Σ_{0}^{(m)} cofinal. Furthermore, if h_{M}^{n,p} maps κ onto τ for some p then σ̃ (note that k = ω here) is Σ_{0}^{(n)} cofinal; but this is all we can say about preservation properties of these maps in general. As before, each x ∈ N is of the form σ̃_{k}(f)(ξ) for some f ∈ Γ_{k}(σ, M) and ξ < κ̃; if x ∈ H_{N}^{m} and σ̃_{k} is cofinal then f can be chosen from H_{M}^{m}. Furthermore, there is an obvious relationship between the k-pseudoultrapower of M and the (ordinary) pseudoultrapower of M^{k,p} for p ∈ R_{M}^{k}. We shall often use the following criterion on the well-foundedness of pseudoultrapowers (we only state the version useful for us where k = ω). Its proof can be found in [44].

Lemma 1.2 (Interpolation lemma). Let σ : M → N′ be Σ_{0}^{(n)}-preserving where M, n, κ, τ are as above (in particular, ωϱ_{M}^{n+1} ≤ κ < ωϱ_{M}^{n}), let N′ = ⟨J_{β}^{B′}, D′⟩, κ̃ = σ(κ) and τ̃ = sup(σ′′τ). Then the canonical extension σ̃ : M → N of σ ↾ |J_{τ}^{A}| : J_{τ}^{A} → J B′ ; τ̃ exists and there is a unique Σ_{0}-preserving map σ′ : N → N′ such that σ = σ′∘σ̃ (thus, σ′ ↾ |J B′ ; τ̃| = id and σ′(τ̃) = κ̃^{+N′}). In fact, σ′ is Σ_{1}^{(n−1)}-preserving. Moreover, if σ̃ is Σ_{0}^{(n)}-preserving and cofinal (i.e. cofinal at the n-th level) then σ′ is Σ_{0}^{(n)}-preserving.

Premice and Extender Models. The main objects of our interest are coherent structures M = ⟨J_{α}^{E}, E_{ωα}⟩ constructed relative to an extender sequence E. The predicate E is not literally an extender sequence, but a set (class) of triples {⟨ν, x, y⟩; ν ∈ On & x, y ⊂ On} such that, setting E_{ν} = {⟨x, y⟩; ⟨ν, x, y⟩ ∈ E}, E_{ν} = ∅ whenever ν is a successor ordinal and, for a limit ordinal ων, E_{ων} is either the empty set or else an extender on J_{ν}^{E}, that is, dom(E_{ων}) = 𝒫(cr(E_{ων})) ∩ J_{ν}^{E}. For ν ≤ α we set M||ν = ⟨J_{ν}^{E}, E_{ων}⟩.

16 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Definition ([13, 44]). A potential premouse is an acceptable structure M of the from ⟨J_{α}^{E}, E_{ωα}⟩ constructed relative to an extender sequence satisfying:

a) If ν ≤ α then either E_{ων} is empty or else M||ν is a coherent structure and E_{ων} is weakly amenable with respect to M||ν.

b) If ν < α then M||ν is sound. To understand the exact meaning of b), see the discussion concerning the initial

segment condition below. The ordinal α is called the height of M; we denote it by ht(M). To indicate that E is the extender sequence of M, we shall write E^{M}. It is clear that if E_{ων} is an extender then ων = ν. The top extender E_{ωα} is denoted by E_{top}^{M}. Potential premice with top extenders are called active, those without top extenders are called passive. It follows easily from a) that if N = Ult(M||ν, E_{ν}) then E^{N} ↾ ν = E ↾ ν; since ν is a cardinal in N, we also have E_{ν}^{N} = ∅. Definition. A premouse is a potential premouse which satisfies the so-called initial segment condition (ISC):

If E_{ν}^{M} ≠ ∅ and λ̄ is a cutpoint of E_{ν}^{M}, then E_{ν}^{M} | λ̄ ∈ M||ν.

Given a potential premouse M and a ν ≤ ht(M), it follows easily that λ(E_{ν}^{M}) is a cardinal in M iff E_{ν}^{M} is superstrong in M. If λ̄ is a cutpoint of E_{ν}^{M} then λ̄ is a limit cardinal in M||ν. To see this, notice that the canonical map that embeds the coherent structure associated with E_{ν}^{M} | λ̄ into M||ν is Σ_{0}-preserving and cofinal. Granting that M is a premouse, E_{ν}^{M} | λ̄ is a superstrong extender in M||ν. Thus, the existence of cutpoints is a very strong large cardinal axiom under the initial segment condition.

Extender models are models of the form L[E] constructed relative to an extender sequence, whose each proper initial segment is a premouse which is weakly iterable in the sense specified below.

We shall consider normal k-iterations of (potential) premice where k-ultrapowers are taken at successor steps as defined in [13, 44]. Let us briefly recall the notation. If ℑ is a normal iteration then T^{ℑ} is the tree structure indicating where the iteration maps live, ν_{i} = ν_{i}^{ℑ} are the iteration indices and D^{ℑ} is the set of indices i for which E_{ν_{i}}^{M_{i}} ≠ ∅. We also set κ_{i} ≃ cr(E_{ν_{i}}^{M_{i}}) and λ_{i} ≃ λ(E_{ν_{i}}^{M_{i}}). Given an i ∈ D^{ℑ}, the T -predecessor of i + 1 is the least ξ ∈ D^{ℑ} such that κ_{i} < λ_{ξ}. Iterations are linear

CHARACTERIZATION OF □_{κ} IN CORE MODELS 17

concatenations of normal iterations. At limit steps of an iteration we choose a cofinal well-founded branch through T^{ℑ}; a function 𝕊 which picks such branches is called iteration strategy. We say that M is (θ, μ, k)-𝕊-iterable, resp. (θ, μ)-𝕊-iterable if every k-iteration, resp. ∗-iteration of M according to 𝕊 of length less than θ which is a concatenation of less than μ normal iterations can be continued. M is (θ, μ)-iterable if there is an iteration strategy (i.e. a ∗-iteration strategy) 𝕊 such that M is (θ, μ)-𝕊-iterable; k-iterability is defined analogously. A premouse M is weakly iterable iff every countable premouse elementarily embeddable into M is (ω_{1} + 1, ω_{1})-iterable. This amount of iterability suffices for developing the basic fine structure theory of extender models along the lines of [13, 44].

The initial segment condition is imposed on premice in order to guarantee the termination of the comparison process. It would be therefore desirable that it is preserved under embeddings arising in condensation arguments and ultrapower constructions. Unfortunately, the initial segment condition need not be downward preserved under maps that are merely Σ_{1}-preserving. To overcome this issue, we divide the class of active premice into subclasses according to the distribution of cutpoints of the top extender, and add a predicate for the cutback of E_{top}^{M} to its largest cutpoint, provided that such a cutpoint exists. Obviously, this procedure involves expanding the language of premice. Originally, the language for premice contained merely the symbols ∈^{·}, E^{·} and F^{·} naming the membership relation, extender sequence and the top extender, respectively. The expanded language for premice also contains a predicate symbol for the cutback of the top extender to its largest cutpoint. As there is no danger of confusion, we shall be a bit sloppy with the notation and shall rarely notationally distinguish between the predicate symbol and the corresponding predicate.

Let us now turn to a more detailed description of the expanded language for premice. Given an active potential premouse M, we let λ_{M} = λ(E_{top}^{M}) and C_{M} be the set of all cutpoints of E_{top}^{M}. We say that M is a type A premouse iff C_{M} = ∅, type B premouse iff C_{M} is nonempty, but bounded in λ_{M} and type C premouse iff C_{M} is unbounded in λ_{M}. For type B premice we we set λ_{M}^{∗} = max(C_{M}) and F_{M}^{∗} = E_{top}^{M} | λ_{M}^{∗}. The standard way of treating type B premice (see e.g. [15]) is to augment the language by adding a constant symbol F^{·}^{∗} whose interpretation is the object

18 ERNEST SCHIMMERLING AND MARTIN ZEMAN

F_{M}^{∗}. This has a consequence that, for type B premice, the standard codes, Skolem functions, reducts and the standard parameter of M are to be computed relative to F_{M}^{∗}. Note that the notion of soundness is also affected by this amendment; this should be kept in mind when dealing with clause b) in the definition of potential premouse. Of course, the projecta will be the same no matter which of the two languages we choose. The point of adding the symbol for F_{M}^{∗} is to guarantee that all embeddings of type B premice into potential premice have F_{M}^{∗} in their ranges, and thus preserve the initial segment condition. In order to simplify the notation, it will be more convenient to add the constant symbol γ^{·} denoting the index γ_{M} of F_{M}^{∗} instead of adding F^{·}^{∗} itself. This does make sense, as it follows by an easy coiteration argument (see [46]) that F_{M}^{∗} is on the E^{M}-sequence. Clearly, γ_{M} is definable from F_{M}^{∗} in a Σ_{1}-fashion over M and vice versa, so all fine structural characteristics of M remain unchanged if the computations are relative to γ_{M} instead of F_{M}^{∗}. Switching from the language with F^{·}^{∗} to that with γ^{·} is therefore a purely cosmetic issue. This completes the discussion of type B premice. In order to obtain a uniform terminology, we also add γ^{·} to the language in the case of type A, type C and passive premice, but we always interpret it as ∅. This trivial amendment to the language does not bring anything new, of course, but will help us to simplify formulations in many situations.

Since most of our arguments will be sensitive to the language we work with, it is convenient to introduce the following terminology. The language for coherent structures is the language containing the symbols ∈^{·} denoting the membership relation, E^{·} denoting the extender sequence the structure is built from and F^{·} denoting the top extender of the structure. The language for premice will also contain the additional symbol γ^{·} intended to denote the restriction of the top extender to its largest cutpoint. Clearly, it does not make any difference whether we treat type A, type C and passive premice in the language for coherent structures or that for premice, and we will usually choose the language for coherent structures (which is actually more natural).

Let us fix a convention that whenever we work with premice, the language in question will always be the language for premice, unless explicitly stated otherwise. For instance, the standard parameters and the Skolem functions h̃_{M}^{n} and h_{M}^{n,p} are

CHARACTERIZATION OF □_{κ} IN CORE MODELS 19

all computed in the language for premice. Similarly, when we say “σ : M → M′ is Σ_{ℓ}^{(n)}-preserving” where M and M′ are two premice, we always mean the Σ_{ℓ}^{(n)}- preservation with respect to the language for premice. In some cases, however, we will ignore this convention and write explicitly that the language in question is the language for premice; the intention here is not to confuse the reader, but rather to stress which language we work with. Notice that if σ : M → M′ is Σ_{0}-preserving with respect to the language for premice then M and M′ are of the same type. On the other hand, if we consider preservation properties with respect to the language for coherent structures, it is, of course, possible that the premice in question are of distinct types.

The following two lemmata summarize basic facts concerning preservation of the initial segment condition. We recall that passive premousehood is a Q-condition and active potential premousehood a Π_{2}-condition, both in the language for coherent structures. Also, being a cutpoint is a Π_{1}-condition in the language for coherent structures. For any type C premouse M we have ωϱ_{M}^{1} = λ_{M} and p_{M} ⊂ λ_{M}, i.e. p_{M}^{1} = ∅. That ωϱ_{M}^{1} ≤ λ_{M} is immediate. To see the converse, we show that given any α < λ_{M} and any A that is Σ_{1}(M) in some p ∈ [On]^{<ω}, the intersection A∩α is in M. Choose λ̃ ∈ C_{M} large enough that α ≤ λ̃ and p ∈ rng(σ); here σ : M̃ → M is the canonical embedding of the coherent structure M̃ associated with E_{top}^{M} | λ̃ into M. The map σ is Σ_{1}-preserving in the language for coherent structures. Letting Ã be the unique set that is Σ_{1}(M̃) in σ^{−1}(p) by the same definition as A, the fact that σ ↾ λ̃ = id guarantees that A ∩ α = Ã ∩ α. By the initial segment condition, M̃ ∈ M, so Ã ∩ α ∈ M as well.

Lemma 1.3. Let M = ⟨J_{ν}^{E}, F ⟩ be an active premouse, M̄ be a potential premouse of the same type as M and let σ : M̄ → M be such that one of the following holds:

a) M is of type A or B and σ is Σ_{1}-preserving;

b) M is of type C and σ is Σ_{0}^{(1)}-preserving or Σ_{2}-preserving.

Then M̄ is a premouse.

For transitive collapses of definable hulls we obtain the following analogue of the above lemma.

20 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Lemma 1.4. Let M be and active premouse and σ : M̄ → M be an uncollapsing embedding associated with a Σ_{1}^{(n)}-hull over M. Assume that one of the following holds:

a) n ≥ 0 and M is of type A or B;

b) n > 0 and M is of type C. Then M̄ is a premouse of the same type as M; moreover, σ(γ_{M}) = γ_{M′} whenever they are of type B.

Consistently with our convention, a) and b) in the above lemmata talk about preservation properties of σ with respect to the language for premice. Recall again that in the case of type A or type C premice, there is no real difference between the two languages. Lemma 1.5. Let M = ⟨J_{ν}^{E}, F ⟩ be an active premouse and let σ : M → M′ be such that one of the following holds:

a) M is of type A or B and σ is Σ_{2}-preserving with respect to the language for coherent structures;

b) M is of type C and σ is Q^{(1)}-preserving with respect to the language for coherent structures and ωϱ_{M′}^{1} = λ_{M′};

c) σ is Σ_{0}-preserving with respect to the language for coherent structures and

cofinal, and maps λ_{M} cofinally into σ(λ_{M}). Then M′ is a premouse of the same type as M; moreover, σ(γ_{M}) = γ_{M′} whenever they are of type B.

Steel’s K^{c}-construction [37] can be carried out in the above setting and provides us with the extender model K^{c} whose initial segments are weakly iterable, which enables us to give a fine structural analysis of the model. Moreover, granting that the set-theoretic universe is sufficiently rich, we can get a Woodin cardinal (see [13] and [14]) or even many Woodin cardinals in K^{c}. [1] describes the largest known K^{c}-model of this kind which can be constructed by present methods; it goes up to an externally measurable cardinal λ that is a limit of Woodin cardinals and cardinals strong up to λ. With a different, carefully-chosen indexing of extenders, one can get even further, slightly beyond a strong limit of Woodin cardinals. The next lemma summarizes all fine structural properties of extender models which will be needed for the construction of square sequences. See [44] for the proof.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 21

Lemma 1.6 (Condensation lemma, [13, 44]). Let M̄ and M be premice of the same type where M is a level of L[E] and let σ : M̄ → M be an embedding which is both cardinal preserving and Σ_{0}^{(n)}-preserving and such that σ ↾ ωϱn+1 ; M̄ = id. Then M̄ is solid and p_{M} is k-universal for every k ∈ ω. Furthermore, if M̄ is sound above ν = cr(σ) then one of the following holds:

a) M̄ = M and σ = id;

b) M̄ is a proper initial segment of M;

c) M̄ = Ult^{∗}(M||η, E_{α}^{M}) where ν ≤ η < ht(M), α ≤ ωη and ν = κ^{+M||η} where κ = cr(E_{α}^{M}); moreover, E_{α}^{M} has a single generator κ;

d) M̄ is a proper initial segment of Ult(M, E_{ν}^{M}). The assumption that σ is cardinal preserving is superfluous unless n = 0, in

which case it cannot be omitted. It might namely happen that M̄, although being of the form ⟨J E ; ᾱ, ∅⟩ where E = E^{M}, is distinct from M||ᾱ, and so is not literally an initial segment of M. By inspecting all cases that might occur in the condensation lemma, one can easily verify that this is the only way the condensation lemma can fail if σ fails to be cardinal preserving. Obviously, Eᾱ ≠ ∅ whenever this happens.

It follows that the ordinal η in c) is in strictly less than κ^{+M} and that M||η projects to κ. Clause d) implies that E_{ν}^{M} is a superstrong extender, as λ(E_{ν}^{M}), being the cardinal predecessor of ν in M̄, is a cardinal in M. In fact, it is easy to see that the set of all ν̄ < λ(E_{ν}^{M})^{+M} such that both

EM ; ν̄ is a superstrong extender and λ(EM̄ ; ν̄) = λ(E_{ν}^{M})

is stationary in M̄. Indeed, if c ∈ M̄ is closed and unbounded in ν then σ(c) is closed in M and has ν as its limit point, so ν ∈ σ(c). Thus, ν witnesses the statement “there is a ζ ∈ σ(c) such that E_{ζ}^{M} is superstrong and λ(E_{ζ}^{M}) = λ(E_{ν}^{M})” in M. But the acceptability of M enables us to phrase this statement inside J_{λ(E_{ν}^{M})^{+M}}^{E} = σ(J Ē ; ν) (here Ē = EM̄), that is, in a Σ_{0}-manner over M. It follows that c contains some index of a superstrong extender whose length is precisely λ(E_{ν}^{M}).

Dodd Parameters. The last ingredient needed in our main construction is some information concerning fine structural properties of the Dodd parameters of certain extenders. A detailed account of this topic can be found [46] where a more general situation is treated. For a sound mouse M = ⟨J_{ν}^{E}, F ⟩ satisfying μ = cr(F) < ωϱ_{M}^{1} < λ_{M}, we inductively define a descending sequence of ordinals δ_{i} as follows:

δ′_{i} = the least δ such that every ordinal less than λ_{M} is of the form F (f)(δ_{0}, …, δ_{i−1}, ξ_{1}, … ξ_{m}) for some m ∈ ω, ξ_{1}, …, ξ_{m} < δ and f : μ → μ in M.

If δ′_{i} is a successor ordinal, we set δ_{i} = δ′_{i}−1. As δ_{i} is descending, after finitely many steps we reach an m such that δ′_{m} is limit. Then δ′_{m} is called the Dodd projectum and denoted by δ_{M}, and d_{M} = {δ_{0}, …, δ_{m−1}} is the Dodd parameter of M. This is the traditional definition of the Dodd projectum and Dodd parameter. Notice that M must be a type A or type B premouse, as ωϱ_{M}^{1} < λ_{M}. If M is of type A, then d_{M} = p_{M} by an easy computation. If M is of type B, one can show that d_{M} = p_{M} ∪ e_{M} where e_{M} is defined below. In either case, the Dodd projectum is equal to ωϱ_{M}^{1}. Let us now turn to our official definitions, which will be more convenient for our purposes. Definition ([46]). Let M be an active premouse such that cr(E_{top}^{M}) < ωϱ_{M}^{1}. The parameter d_{M} is the <^{∗}-least finite set of ordinals d such that M = h_{M}^{∗}(ωϱ_{M}^{1} ∪{d}), if defined. Here h_{M}^{∗} is the canonical Σ_{1}-Skolem function for M computed in the language for coherent structures.

The above definition is formulated for arbitrary active premouse M; if M has a very good parameter, this definition is equivalent to the traditional definition. Clearly, d_{M} ∩ ωϱ_{M}^{1} = ∅. Although it is obvious, let us stress again that the use of h_{M}^{∗} in the above definition is vital; if we used h_{M} instead, d_{M} would be just the least very good parameter from R_{M}^{1}. This is actually the case whenever M is of type A or C, so the notion of Dodd parameter brings something new only for type B premice.

Dodd solidity witnesses are just solidity witnesses with respect to the language for coherent structures. Thus, given an ordinal ν ≥ ωϱ_{M}^{1} and a parameter p in [On ∩ M]^{<ω}, the standard Dodd solidity witness ^{∗}W _{M}^{ν,p} for ν with respect to p and M is the transitive collapse of the hull h_{M}^{∗}(ν ∪ {p − (ν + 1)}). The reader will now easily formulate the definition of a generalized Dodd solidity witness. Obviously, all general facts about solidity witnesses apply to Dodd solidity witnesses. In particular, ^{∗}W _{M}^{ν,p} ∈ M just in case that some generalized Dodd solidity witness with respect to ν and M is an element of M. A premouse M is Dodd solid iff d_{M} is

CHARACTERIZATION OF □_{κ} IN CORE MODELS 23

defined and ^{∗}W _{M}^{ν,d_{M}} ∈ M for every ν ∈ d_{M}. Notice that if M is Dodd solid then d_{M} is nothing but the standard parameter of M with respect to the language of coherent structures. Definition. Let M be a type B potential premouse. The <^{∗}-least finite set of ordinals e such that γ_{M} ∈ h_{M}^{∗}(ωϱ_{M}^{1} ∪ {p_{M} ∪ e}) is denoted by e_{M}.

Obviously, e_{M} is always defined and e_{M} ⊂ γ_{M} + 1. We have already mentioned above that in all relevant cases, the Dodd parameter d_{M} can be computed from the standard parameter of M and the set of ordinals e_{M}. It is of a great importance that the conversion between the Dodd parameter and the standard parameter is Σ_{1} and sufficiently uniform, which guarantees that it is preserved under embeddings with relatively weak preservation properties. Let us now formulate everything rigorously. The following two lemmata summarize the main results concerning Dodd parameters we will rely on. Lemma 1.7 ([46]). Let M be an L[E]-level of type B satisfying cr(E_{top}^{M}) < ωϱ_{M}^{1}. Then d_{M} is defined and:

a) d_{M} = (p_{M} − ωϱ_{M}^{1}) ∪ e_{M}.

b) M is Dodd solid. Lemma 1.8 ([46]). Let M be a type B premouse with cr(E_{top}^{M}) < ωϱ_{M}^{1} and such that there is a Σ_{0}-preserving embedding σ : M → N into an L[E]-level N satisfying σ ↾ ωϱ_{M}^{1} = id. Assume that d is a parameter satisfying:

• d ∩ ωϱ_{M}^{1} = ∅.

• M = h_{M}^{∗}(ωϱ_{M}^{1} ∪ {d}).

• Every ν ∈ d has a generalized Dodd solidity witness with respect to d and

M, that is an element of M. Then

a) d = d_{M};

b) d_{M} = (p_{M} − ωϱ_{M}^{1}) ∪ e_{M};

c) M is sound above ωϱ_{M}^{1}. The preservation properties of σ in the above lemma are, of course, formulated

with respect to the language of premice. Thus, granting that M is active, M and N must be of the same type.

24 ERNEST SCHIMMERLING AND MARTIN ZEMAN

2. Extender Fragments

The construction of a □_{κ} sequence involves interpolation arguments which, in turn, give rise to embeddings with low preservation degree. A typical example is an embedding σ : M̄ → M where M is an active L[E]-level, σ is Σ_{0}-preserving but not cofinal and cr(σ) > cr(E_{top}^{M})^{+M}. The top predicate F̄ of M̄ is then an extender which is not weakly amenable with respect to M̄. In other words, some subsets of cr(F̄) which are in M̄ are not measured by F̄. This means that M̄ is not even a potential premouse and our task is to find a correspondence between M̄ and some suitable level of L[E]. Studying connections between structures like M̄ and levels of L[E] is the main issue addressed in the current section. Structures like M̄ are called protomice and their top extenders can be viewed as “fragments” of total extenders. It will turn out that the fine ultrapower of the longest possible initial segment of M̄ by F̄ is a level of L[E] and we will discuss the relationship between the definability over M̄ and its corresponding L[E]-level. It is clear that each protomouse is associated with at most one such level, but the converse is false in general, and our next task will be identifying the canonical protomice for collapsing L[E]-levels of “local” successor cardinals.

The reader should pay particular attention to the definitions of divisor and strong divisor to come, as they will play important roles in identifying canonical protomice. These two notions were used already in the authors’ earlier papers on square principles in extender models but with different terminology. Before launching into the technicalities, let us offer a bit of motivating discussion. In order to explain the main ideas quickly, it will be necessary for us to be slightly inaccurate, but only in this paragraph. As one familiar with Jensen’s proof of □_{κ} in L would expect, we must consider ordinals κ < τ ≤ α where κ is the largest cardinal in J_{τ}^{E} and L[E] || α is the collapsing L[E]-level for τ, that is, τ is a cardinal in L[E] || α and L[E] || α projects to κ. Let us now focus on the case where κ is the first projectum of the collapsing level M for τ and cr(E_{top}^{M}) < κ. As indicated in the previous paragraph, it is this case that prevents a naive adaptation of Jensen’s method because the corresponding interpolation arguments give rise to protomice. There are, however, canonical club subsets of τ of order type ϑ where μ = cr(E_{top}^{M}) and ϑ = μ^{+L[E]} ≤ κ. One such club set consists of all ordinals of the form τ̄ = κ^{+N}

CHARACTERIZATION OF □_{κ} IN CORE MODELS 25

where N = Ult(M || ζ, F), μ < ζ < ϑ and F is the restriction of E_{top}^{M} to sets in M || ζ and coordinates from κ ∪ d_{M}. We may make additional assumptions about ζ, for example, that M || ζ projects to μ. This allows us to read off that N projects to κ and p_{N} = π(p_{M || ζ}) ∪ q where π : M || ζ → N is the ultrapower map and q is the parameter represented by the identity function on coordinate d_{M}. It is also true that max(q) < π(μ) ≤ min(π(p_{M || ζ})). Moreover, F is the extender derived from the Mostowski collapse of the hull of μ ∪ π(p_{M || ζ}) taken inside N. Identifying F in this way over N (but without reference to E_{top}^{M}!) is key to our proof of the coherency of our ultimate square sequence. Such an F will turn out to be the top extender of some protomouse arising in one of the interpolation arguments in the course of the main construction. We call the pair (μ, q) a divisor of N since it has the data needed to identify F. The challenge is in knowing which divisor to use; what we have said so far does not seem to be enough to guarantee a unique choice. A certain additional closure condition on the ordinals ζ will ensure that (μ, q) is a so-called strong divisor of N. This will make possible a unique choice of divisor.

From now on we shall work in L[E] and fix a cardinal κ for which we intend to construct a □_{κ}-sequence. Throughout this section we assume that

• τ < κ^{+} is such that κ is the largest cardinal in J_{τ}^{E}.

• N is the collapsing level for τ. More precisely, N is a level of L[E], τ is a cardinal in N and ωϱ_{N}^{ω} = κ;

• n = n(N) is such that ωϱ_{N}^{n+1} ≤ κ < ωϱ_{N}^{n}.

Premice and Protomice. Given a coherent structure M = ⟨J_{α}^{E}, F ⟩, let ϑ(M) be the least ϑ such that dom(F) ⊂ J_{ϑ}^{E}. Then μ = cr(F) is the largest cardinal in J_{ϑ(M)}^{E}. If ϑ(M) < κ^{+M}, we define N^{∗}(M) to be the collapsing level of ϑ(M) in M. Definition. A protomouse is a coherent structure M = ⟨J_{α}^{E}, F ⟩ such that N(M) = Ult^{∗}(N^{∗}(M), F) is a level of L[E]. M is a collapsing protomouse for τ iff N(M) is the collapsing L[E]-level for τ. Definition. A pair (μ, q) is a divisor of N iff there is an ordinal λ = λ_{N}(μ, q) such that, setting r = p_{N} − q, the following holds:

a) μ ≤ κ < λ < ωϱ_{N}^{n};

b) q = p_{N} ∩ λ;
c) h̃_{N}^{n+1}(μ ∪ {r}) ∩ ωϱ_{N}^{n} is cofinal in ωϱ_{N}^{n};

26 ERNEST SCHIMMERLING AND MARTIN ZEMAN

d) λ = min (On ∩ h̃_{N}^{n+1}(μ ∪ {r}) − μ). In the next couple of paragraphs, we shall assume that (μ, q) is a divisor of N

and that r = p_{N} − q. So r = p_{N} − λ.

Let N^{∗} be the transitive collapse of h̃_{N}^{n+1}(μ ∪ {r}) and π : N^{∗} → N be the associated uncollapsing map; π is clearly Σ_{0}^{(n)}-preserving and cofinal, μ = cr(π) (so μ is regular in N^{∗}) and λ = π(μ). Notice also that λ > τ, as otherwise κ, being the largest cardinal in J_{τ}^{E}, would also be in h̃_{N}^{n+1}(μ ∪ {r}) − μ, thus contradicting clause d) above. Furthermore,

(1)  μ is both inaccessible in N^{∗} and a limit cardinal in L[E].

Consequently, λ is inaccessible in N. To see (1), it suffices to show that μ is a limit cardinal in N^{∗}; the rest follows from the preservation properties of the map π and acceptability. Pick a μ̄ < μ; then N ⊧ (∃θ < λ)(μ̄ < θ & θ is a cardinal in J_{λ}^{E}), as is witnessed by τ. Since this statement is downward preserved under π, choosing μ̄ arbitrarily large below μ yields that J_{μ}^{E} doesn’t have a largest cardinal. So μ is a limit cardinal in N^{∗}, as N^{∗} is acceptable.

From the fact that π is an embedding arising from collapsing of a Σ_{1}^{(n)}-hull in N and Lemma 1.4 we obtain

(2)  N^{∗} is a premouse of the same type as N.

This is immediate whenever N is passive or active of type A or B. If N is of type C, we have to verify that n > 0. However, if n = 0 then λ_{N} = κ, so there are no cardinals in N strictly between κ and ωϱ_{N}^{0} = On ∩ N. Since λ(μ, q) is a cardinal in N, we have a contradiction with a) in the definition of divisor.

Set p^{∗} = π^{−1}(r). Then N^{∗} = h̃_{N^{∗}}^{n+1}(μ ∪ {p^{∗}}), which together with (1) yields

(3)  ωϱ_{N^{∗}}^{ω} = ωϱ_{N^{∗}}^{n+1} = μ < ωϱ_{N^{∗}}^{n} and p^{∗} ∈ R_{N^{∗}}^{n} = R_{N^{∗}}^{∗}.

Let F be the extender at (μ, λ) derived from π, i.e.

(4)  F = π ↾ (𝒫(μ) ∩ N^{∗}).

Lemma 2.1. π : N^{∗} ⟶_{F}^{∗} N.

Proof. Define an embedding σ : 𝔻^{∗}(N^{∗}, F) → N by σ([α, f]) = π(f)(α) for α < λ and f ∈ Γ(μ, N^{∗}). The map σ is Σ_{0}-preserving by the Łoś theorem, so 𝔻^{∗}(N^{∗}, F)

CHARACTERIZATION OF □_{κ} IN CORE MODELS 27

is well-founded, and we identify it with its transitive isomorph N̄. Let π̄ be the associated ultrapower map. Then π = σ ∘π̄ and π̄ is Σ_{0}^{(n)}-preserving and cofinal, as N^{∗} has a very good parameter, namely p^{∗}. From the cofinality of π, using the Łoś theorem for Σ_{0}^{(n)}-formulae we infer that σ is Σ_{0}^{(n)}-preserving. Finally, the cofinality of π guarantees that σ is in fact Σ_{0}^{(n)}-preserving and cofinal.

Notice that κ ∪ {p_{N}} ⊂ rng(σ), as σ(π̄(p^{∗})) = r = p_{N} − λ and σ is the identity on λ. By the discussion in the previous paragraph, σ is Σ_{1}^{(n)}-preserving, so N = h̃_{N}^{n+1}(κ ∪ {p_{N}}) ⊂ rng(σ). This proves that σ is an isomorphism. It follows that N̄ = N, σ = id and π̄ = π. ⊓ ⊔(Lemma 2.1)

Lemma 2.2. N^{∗} is sound. Proof. For active N^{∗} we can assume w.l.o.g. that λ_{N^{∗}} > μ, as otherwise the conclusion is immediate. Let N̄^{∗} be the core of N^{∗} and σ̄^{∗} the core map. We will show that N̄^{∗} = N^{∗} and σ̄^{∗} = id. The proof of (2) with N̄^{∗} and π ∘ σ̄^{∗} in place of N^{∗} and π yields that N̄^{∗} is a premouse. Let ϑ = μ^{+N^{∗}}. We observe:

(5)  EN̄^{∗} ↾ ϑ = E^{N^{∗}} ↾ ϑ = E ↾ ϑ and ϑ = μ^{+N̄^{∗}}.

To see that E^{N^{∗}} ↾ ϑ = E ↾ ϑ, notice that there are cofinally many ζ in ϑ such that N^{∗} || ζ projects to μ. Given any such ζ, the map π ↾ N^{∗} || ζ : N^{∗} || ζ → N || π(ζ) is fully elementary, so the assumptions of the condensation lemma are met, as π ↾ μ = id and N^{∗} || ζ is sound. From the possibilities given by the condensation lemma, we can easily rule out c) and d), as these require cr(π) to be a successor cardinal in N^{∗}. In order to rule out a), pick an a ⊂ μ which is in N^{∗} but not in N^{∗} || ζ, and observe that a = π(a) ∩ μ ∈ N. It follows that N^{∗} || ζ is a proper initial segment of N. As ζ < ϑ can be chosen arbitrarily large, we have the desired conclusion.

Set ϑ̄ = μ^{+N̄^{∗}}. The argument from the previous paragraph with N̄^{∗} and π ∘ σ̄^{∗} in place of N^{∗} and π yields that EN̄^{∗} ↾ ϑ̄ = E ↾ ϑ̄. So the sequences EN̄^{∗} ↾ ϑ̄ and E^{N^{∗}} ↾ ϑ are compatible in the sense that one of them is an initial segment of the other.

The preservation properties of σ̄^{∗} obviously yield the inclusion 𝒫(μ) ∩ N̄^{∗} || ϑ̄ ⊂ 𝒫(μ) ∩ N^{∗} || ϑ. The universality of p_{N^{∗}}, guaranteed by the condensation lemma, implies that the converse also holds, so ϑ̄ = ϑ. ⊓ ⊔(5)

28 ERNEST SCHIMMERLING AND MARTIN ZEMAN

It follows that F measures all subsets of μ which are in N̄^{∗}, so we can attempt to apply F to N̄^{∗}. Define an embedding σ : 𝔻(N̄^{∗}, F) → N by

σ([α, f]) = π(σ̄^{∗}(f))(α)

for α < λ and f ∈ Γ(μ, N̄^{∗}). Given a Σ_{0}-formula φ together with ordinals α_{0}, …, α_{ℓ} < λ and f_{0}, …, f_{ℓ} ∈ Γ(μ, N̄^{∗}), the Łoś theorem yields

𝔻(N̄^{∗}, F) ⊧ φ([α_{0}, f_{0}], … [α_{ℓ}, f_{ℓ}]) iff ≺α_{0}, …, α_{ℓ}≻ ∈ F (u)

where

u = {≺η_{0}, …, η_{ℓ}≻ ∈ μ; N̄^{∗} ⊧ φ(f_{0}(η_{0}), …, f_{ℓ}(η_{ℓ}))}
= {≺η_{0}, …, η_{ℓ}≻ ∈ μ; N^{∗} ⊧ φ(σ̄^{∗}(f_{0})(η_{0}), …, σ̄^{∗}(f_{ℓ})(η_{ℓ}))}.

Since F is an extender derived from π, the right side of the above equivalence is equivalent to N ⊧ φ(π(σ̄^{∗}(f_{0}))(α_{0}), …, π(σ̄^{∗}(f_{ℓ}))(α_{ℓ})). This proves that σ is structure preserving. Consequently, 𝔻^{∗}(N̄^{∗}, F) is well-founded, so we can identify it with its transitive isomorph N̄. Also, let π̄ be the associated ultrapower map. From the definition of σ̄^{∗} we easily get

(6)  σ ∘ π̄ = π ∘ σ̄^{∗}.

The map π̄ is Σ_{0}^{(n)}-preservning and cofinal; this follows from the fact that N̄^{∗} has a very good parameter, namely the σ̄^{∗}-preimage of p_{N^{∗}}. The argument from the previous paragraph now goes through for Σ_{0}^{(n)}-formulae; of course, this time we have to use the corresponding version of the Łoś theorem. Consequently, σ is Σ_{0}^{(n)}- preserving. The universality of p_{N^{∗}} implies that σ̄^{∗} is Σ_{0}^{(n)}-preserving and cofinal, which together with the cofinality of π and (6) yields that σ is Σ_{0}^{(n)}-preserving and cofinal as well.

We next conclude that N̄ is a premouse of the same type as N̄^{∗}. (Obviously, the case of passive N̄^{∗} is not an issue.) This time we make use of the upward preservation properties of π̄. First assume that N̄^{∗} is of type A or B. If ωϱ1 ; N̄^{∗} > μ, we appply a) of Lemma 1.5, otherwise we use clause c). That all conditions are met follows from the properties of fine ultrapowers. Now assume that N̄^{∗} is of type C. Notice that the assumption μ < λN̄ we made at the beginning implies μ < λN̄^{∗}, so we automatically have ωϱ1 ; N̄^{∗} > μ. The properties of fine ultrapowers guarantee that

CHARACTERIZATION OF □_{κ} IN CORE MODELS 29

π̄ is Q^{(1)}-preserving (this requires to discuss the cases n = 1 and n > 1 separately), so we can apply clause c) of Lemma 1.5.

Set p̄^{∗} = pN̄^{∗}. The universality of p_{N^{∗}} guarantees that that σ̄^{∗}(p̄^{∗}) = p_{N^{∗}} and that N̄^{∗} is sound. We also have the solidity of N̄^{∗}, which follows from the condensation lemma and the fact that π ∘ σ̄^{∗} : N̄^{∗} → N is Σ_{0}^{(n)}-preserving. Using the preservation properties of π̄ we infer that N̄ = h̃n+1 ; N̄(λ ∪ {π̄(p̄^{∗}}) and for every α ∈ p̄^{∗}, the structure π̄(W α,p̄^{∗} ; N̄^{∗}) is a generalized witness to π̄(α) with respect to π̄(p̄^{∗}) and N̄. This yields the inequality ωϱn+1 ; N̄ ≤ λ and, together with Lemma 1.1, also the identity π̄(p̄^{∗}) = pN̄ − λ and the soundness of N̄ above λ.

Let ν be the cardinal successor of λ in N. The agreement in (5) guarantees that

(7)  ν = λ^{+N̄} and EN̄ ↾ ν = E ↾ ν.

We now apply the condensation lemma to N̄, N and σ. Notice that neither of b),

c) and d) is the case: Otherwise we would have N̄ ∈ N || ν, as follows from the fact, given by the discussion in the previous paragraph, that N̄ can be encoded into a Σ_{1}^{(n)}(N̄) subset of λ. But then ν would be collapsed in N, contradicting (7). Thus, N̄ = N and σ = id. As a consequence we obtain that N̄^{∗} is the transitive collapse of h̃n+1 ; N̄(μ ∪ {pN̄ − λ}) = h̃_{N}^{n+1}(μ ∪ {p_{N} − λ}) and π̄ that is the associated uncollapsing map. Hence N̄^{∗} = N^{∗} and π̄ = π. Finally, (6) yields that σ̄^{∗} = id, so N^{∗} is sound. ⊓ ⊔(Lemma 2.2)

Lemma 2.3. N^{∗} is a proper initial segment of N, and thus the collapsing level for ϑ = μ^{+N^{∗}}. Moreover, setting ν = π(ϑ), the structure M = ⟨J_{ν}^{E}, F ⟩ is a protomouse, N(M) = N and ϑ(M) = ϑ (so N^{∗}(M) = N^{∗}). Proof. The fact that π is Σ_{0}^{(n)}-preserving together with (3) and Lemma 2.2 guarantee that we can apply the condensation lemma to π : N^{∗} → N. Clauses c) and d) can be ruled out immediately, as they would imply that μ is not a limit cardinal in N^{∗}, which contradicts (1). Clause a) is obviously false for μ < κ. For μ = κ notice that q ≠ ∅, as κ ∉ rng(π). Then rng(π) is contained in rng(σ_{β}), where β = max(q) and σ_{β} is the witness map for β. This means that N^{∗}, being sound, can be encoded into a Σ_{1}^{(n)}(W_{N}^{β}) subset of μ. Thus, N^{∗} ∈ N, which rules out a) also in this case. It follows that b) must hold, i.e. N^{∗} must be a proper initial segment of N. The rest of the proof is obvious. ⊓ ⊔(Lemma 2.3)

30 ERNEST SCHIMMERLING AND MARTIN ZEMAN

From now on we are fixing the notation: Unless specified otherwise, the symbols μ, ϑ, λ, κ, q, r and N^{∗} will have the same meaning as in the previous lemmata.

There is a class of L[E]-levels which resemble protomice in many respects. For instance, they look very much like protomice with the only difference that their top extenders are total. Also, we will treat them the same way as protomice. We shall see later that the reason why we have to introduce protomice is precisely the existence of such levels.

Definition. The L[E]-level N is pluripotent iff N is active, cr(E_{top}^{N}) < κ and ωϱ_{N}^{1} = κ.

In the next subsection, we will develop fine structure theory for protomice. The language of protomice will consist of the membership predicate, predicate for the extender sequence and that for the top predicate. In other words, it will be the language for coherent structures. Protomice typically arise in interpolation arguments where the target structure is a pluripotent L[E]-level. In order to give a uniform definition of square sequences, we will therefore need to do certain fine structural computations for type B levels in the language for coherent structures, i.e. without referring to γ_{N}. Equivalently, we will need some information about the Dodd parameter. (The Dodd projectum is κ in this case, as is explained in the preliminaries.)

A pluripotent N is of type C exactly when λ_{N} = κ. This means that κ is Σ_{1}- definable over N, so N cannot have any divisors. If N is of type A then d_{M} = p_{M}. For N of type B, there are two ways how to determine divisors: We can use either the standard parameter p_{N} and the language for premice, or else the Dodd parameter d_{N} and the language for coherent structures. The interpolation arguments that are applied in the construction of square sequences will force us to use both, which might badly injure the uniformity of the definition of these sequences. Luckily, the two ways of determining the divisor turn out to be equivalent: The divisors determined by Dodd parameter exactly agree with those determined by the standard parameter with the only exception: The “divisor” (μ, d_{N}) does not have any counterpart when using the standard parameter instead of the Dodd parameter. We shall prove this in the next series of lemmata. Before stating these lemmata notice that for pluripotent

CHARACTERIZATION OF □_{κ} IN CORE MODELS 31

N, the requirements

(8)

λ_{N} ∩ h_{N}^{∗}(μ ∪ {d_{N} − q}) contains an ordinal larger than μ
λ_{N^{∗}} > μ

are equivalent where N^{∗} is the transitive collapse of h_{N}^{∗}(μ ∪ {d_{N} − q}). Lemma 2.4. Let N be pluripotent of type B and let (μ, q) be such that a) – d) of the definition of divisor hold with h_{N}^{∗} in place of h̃_{N}^{n+1} and d_{N} in place of p_{N} (note that n = 0). Suppose further that λ_{N^{∗}} > μ (see (8)). Then γ_{N} ∈ h_{N}^{∗}(μ ∪ {d_{N} − q}), so the transitive collapse N^{∗} of this hull is a type B premouse. Proof. Let π : N^{∗} → N be the uncollapsing map associated with the above hull. Then ωϱ_{N^{∗}}^{ω} = ωϱ_{N^{∗}}^{1} = μ and p^{∗} = π^{−1}(r) is a very good parameter for N^{∗} relative to the language for coherent structures. This is just enough to make the proof of Lemma 2.1 go through. Thus, N = Ult(N^{∗}, F) where F is the extender derived from π and π is the ultrapower map. We stress once again that, by the fact that the first projectum drops to μ, this ultrapower is coarse (that is, it uses only functions that are elements of N^{∗}).

We first show that the largest cutpoint λ_{N}^{∗} of E_{top}^{N} is in the range of π. Recall that λ_{N^{∗}} > μ. Notice also that μ̄ =^{def} cr(E_{top}^{N}) < μ, as μ̄ ∈ rng(π). The embedding π, being a coarse ultrapower map, is continuous at all ordinals of N^{∗}-cofinality other than μ. In particular, π is continuous at λ_{N^{∗}}, so π maps λ_{N^{∗}} cofinally into λ_{N}. The potential premouse N^{∗} cannot be of type C, as otherwise π′′C_{N^{∗}} would be a set of cutpoints of E_{top}^{N} cofinal in λ_{N}. This is impossible, as N is of type B. If N^{∗} were of type A, there would be unboundedly many ordinals of the form E_{top}^{N^{∗}}(f)(μ̄) in λ_{N^{∗}} where f : μ̄ → μ̄ is an element of N^{∗}. By the preservation properties of π, we would have unboundedly many ordinals of the form E_{top}^{N}(f)(μ̄) in λ_{N} where f : μ̄ → μ̄ ranges over functions in N (note that 𝒫(μ̄) ∩ N^{∗} = 𝒫(μ̄) ∩ N). In other words, N would be of type A, which is impossible as well. So N^{∗} is of type B and π(λ_{N^{∗}}^{∗}) is a cutpoint of N. The same argument we used to rule out the possibility that N^{∗} is of type A then shows that π(λ_{N^{∗}}^{∗}) = λ_{N}^{∗}. Now if λ_{N^{∗}}^{∗} < μ, then also γ_{N} < μ and it is easy to see that γ_{N^{∗}} = γ_{N}. From now on suppose that λ_{N^{∗}}^{∗} ≥ μ.

Thus, λ_{N}^{∗} ≥ λ =^{def} π(μ).

By the initial segment condition, E_{top}^{N} | λ_{N}^{∗} = E_{γ_{N}}^{N}, so Ult(J E ; ϑ̄, E_{top}^{N} | λ_{N}^{∗}) = J_{γ_{N}}^{E} where ϑ̄ = μ̄^{+N} = μ̄^{+N^{∗}}. Let σ be the associated ultrapower map. Let further J_{γ^{∗}}^{E^{∗}} = Ult(J E ; ϑ̄, E_{top}^{N^{∗}} | λ_{N^{∗}}^{∗}) with the associated ultrapower map σ^{∗}. Our next task is to show:

(9)  J_{γ^{∗}}^{E^{∗}} is an initial segment of N^{∗}, that is, E^{∗} = E^{N^{∗}} ↾ γ^{∗}.

Given a ζ < γ^{∗} such that Q_{ζ} = J_{γ^{∗}}^{E^{∗}} || ζ projects to λ_{N^{∗}}^{∗}, we show that Q_{ζ} is an initial segment of N^{∗}. Since there are unboundedly many such ordinals ζ in γ^{∗}, this proves (9). A standard approach here would be to observe that Q_{ζ} can be embedded into a proper initial segment of N^{∗} and then apply the condensation lemma. However, we restrict ourselves to make use of Lemma 1.6 instead of the full condensation lemma, so we can only consider embeddings whose target structures are L[E]-levels. For this reason we have to do some extra work.

Let σ̃^{∗} be the ultrapower map associated with Ult(J E ; ϑ̄, E_{top}^{N^{∗}}). Pick a ϑ′ < ϑ̄ such that μ̄ is the largest cardinal in J_{ϑ′}^{E}, the embedding σ^{∗} maps ϑ′ cofinally into σ^{∗}(ϑ′) =^{def} ν′ and ζ < ν′. This is possible, since there are unboundely many ordinals ϑ′ in ϑ̄ satisfying the former two requirements (obviously, σ^{∗} is continuous at any ordinal of N^{∗}-cofinality strictly smaller than μ). It is also easy to see that σ̃^{∗} maps ϑ′ cofinally into σ̃^{∗}(ϑ′) =^{def} ν̃′. We know that N^{∗} is an amenable structure, so F̃^{∗} = E_{top}^{N^{∗}} ↾ (𝒫(μ̄) ∩ J_{ϑ′}^{E}) ∈ N^{∗}. Let F^{∗} = F̃^{∗} | λ_{N^{∗}}^{∗}. A standard argument shows that our choice of ϑ′ guarantees that σ̃^{∗} ↾ J_{ϑ′}^{E} and σ^{∗} ↾ J_{ϑ′}^{E} are the ultrapower maps associated with Ult(J_{ϑ′}^{E}, F̃^{∗}) and Ult(J_{ϑ′}^{E}, F^{∗}), respectively. Define an embedding σ̄^{∗} : J_{ν′}^{E^{∗}} → J_{ν̃′}^{E^{N^{∗}}} in the usual way, i.e. σ̄^{∗}(σ^{∗}(f)(α)) = σ̃^{∗}(f)(α) for f ∈ J_{ϑ′}^{E} with dom(f) = μ̄ and α < λ_{N^{∗}}^{∗}. Then σ̄^{∗} is Σ_{0}-preserving and cofinal, has critical point λ_{N^{∗}}^{∗} and σ̄^{∗} ∈ N^{∗}. By applying π we obtain that π(σ̄^{∗}) : π(J_{ν′}^{E^{∗}}) → J_{π(ν̃′)}^{E} is Σ_{0}- preserving and cofinal and has critical point λ_{N}^{∗}. Letting Q̃_{ζ} = N^{∗} || σ̄^{∗}(ζ), we see that π(σ̄^{∗}) ↾ π(Q_{ζ}) : π(Q_{ζ}) → π(Q̃_{ζ}) is fully elementary and also the remaining assumptions of the condensation lemma are met. Exactly as in the proof of (5) we infer that π(Q_{ζ}) = N || π(ζ). So Q_{ζ} is an initial segment of N^{∗} by the preservation properties of π. This completes the proof of (9).

A standard verification yields that π^{∗} : σ^{∗}(f)(α) ↦ σ(f)(π(α)) is an embedding of J_{γ^{∗}}^{E} into J_{γ_{N}}^{E} which is Σ_{0}-preserving and cofinal, and which agrees with π up to λ_{N^{∗}}^{∗}. We improve this by further showing that, in fact, π^{∗} and π agree up to γ^{∗},

CHARACTERIZATION OF □_{κ} IN CORE MODELS 33

which has an immediate consequence that

(10)  π maps γ^{∗} cofinally into γ_{N}.

By the basic properties of ultrapowers, each ζ < γ^{∗} can be written in the form otp(σ(f)(α)) where f : μ̄ → 𝒫(μ̄) is in N^{∗} and α < λ_{N^{∗}}^{∗}. According to our convention introduced in the preliminaries (see the subsection on extenders and coherent structures), we can think of f as the set of all Gödel pairs ≺η, ξ≻ satisfying ξ ∈ f(η) and write E_{top}^{N^{∗}} | λ_{N^{∗}}^{∗} instead of σ^{∗}. We obtain:

π(ζ) = π(otp[(E_{top}^{N^{∗}} | λ_{N^{∗}}^{∗})(f)(α)]) = π(otp[(E_{top}^{N^{∗}}(f) ∩ λ_{N^{∗}}^{∗})(α)]) =
= otp[(E_{top}^{N}(f) ∩ λ_{N}^{∗})(π(α))] = otp[(E_{top}^{N} | λ_{N})(f)(π(α))] = π^{∗}(ζ).

Since λ_{N^{∗}}^{∗} is the largest cardinal in J_{γ^{∗}}^{E^{∗}}, (9) guarantees that γ^{∗} ≤ (λ_{N^{∗}}^{∗})^{+N^{∗}}. We show that γ^{∗} is actually strictly smaller than (λ_{N^{∗}}^{∗})^{+N^{∗}}. Recall that γ^{∗} > μ. If γ^{∗} were the cardinal successor of λ_{N^{∗}}^{∗} in N^{∗} then π, being a coarse ultrapower embedding, would map γ^{∗} cofinally into the N-cardinal π(γ^{∗}). But (10) tells us that the cofinal image of γ^{∗} under π is γ_{N}, and this is certainly not a cardinal in N, as it indexes an extender on E.

Finally we are ready to show that γ_{N} ∈ rng(π). Assume for a contradiction that this is not the case. Then π(γ^{∗}) > γ_{N}, as follows from (10). For the rest of the proof, let Q̄ be the collapsing level for γ^{∗} in N^{∗} and Q = π(Q̄). Notice that Q is an initial segment of N, and thus an L[E]-level. So the preservation properties of π guarantee that Q̄ is a premouse that is sound and solid. By our assumptions, Q̄ projects to λ_{N^{∗}}^{∗} and γ^{∗} = (λ_{N^{∗}}^{∗})^{+Q̄}. The interpolation lemma guarantees that the canonical extension π̃ : Q̄ → Q̃ of π ↾ J_{γ^{∗}}^{E^{N^{∗}}} : J_{γ^{∗}}^{E^{N^{∗}}} → J_{γ_{N}}^{E} to Q̄ exists and is Σ_{0}^{(m)}- preserving and cofinal where m is such that ωϱm+1 ; Q̄ ≤ λ_{N^{∗}}^{∗} < ωϱm ; Q̄. The cofinality of π̃ follows from the soundness of Q̄. Moreover, letting p̃ =^{def} π̃(pQ̄), standard fine structural computations yield:

• ωϱm+1 ; Q̃ ≤ λ_{N}^{∗} < ωϱm ; Q̃;

• h̃m+1 ; Q̃(λ_{N}^{∗} ∪ {p̃}) = Q̃;

• π̃(W β̄,pQ̄ ; Q̄) is a generalized solidity witness for β = π(β̄) with respect to Q̃ and p̃ whenever β ∈ p̃, and this witness is an element of Q̃.

34 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Finally, there is a Σ_{0}^{(m)}-preserving map π′ : Q̃ → Q which is the identity on γ_{N} and π′(γ_{N}) = π(γ^{∗}).

In order to be able to use the condensation lemma, we must verify that Q̃ is a premouse. This is certainly true if Q̄ is passive or ωϱ1 ; Q̄ > λ_{N^{∗}}^{∗}, as in this case we can directly apply a) or b) of Lemma 1.5. The map π̃ is easily seen to be Σ_{2}- preserving and, if Q̄ is of type C, also Q^{(1)}-preserving; in the latter case we also have ωϱ1 ; Q̃ = λQ̃ (this, actually requires a discussion of two cases, namely ωϱ2 ; Q̄ = λ_{N^{∗}}^{∗} and ωϱ2 ; Q̄ > λ_{N^{∗}}^{∗}). Now suppose that Q̄ is active and its first projectum drops to λ_{N^{∗}}^{∗}. Let κ̄ and τ̄ be the critical point of EQ̄ ; top and its Q̄-successor, respectively. If τ̄ > λ_{N^{∗}}^{∗}, then π̃, being a coarse pseudoultrapower embedding, maps τ̄ cofinally into π̃(τ̄). If τ̄ < λ_{N^{∗}}^{∗}, then τ̄ is in fact a successor cardinal in N^{∗}, as λ_{N^{∗}}^{∗} is a limit cardinal in N^{∗}. So π, being a coarse ultrapower embedding, maps τ̄ cofinally to π(τ̄) and the same is true with π̃ in place of π, as π̃ is an extension of π. In either case, the top extender of Q̃ is weakly amenable, so Q̃ is a potential premouse. The cofinality of π′′τ̄ in π(τ̄) also guarantees that λQ̄ > λ_{N^{∗}}^{∗}, as otherwise ht(Q̄) = γ^{∗} and π(γ^{∗}) would be the cofinal image of γ^{∗} under π. By (10), the latter is nothing other than γ_{N}, so γ_{N} ∈ rng(π), which contradicts our initial assumption. Hence λQ̄ > λ_{N^{∗}}^{∗}, and the premousehood of Q̃ then follows from c) of Lemma 1.5.

At last we can apply the condensation lemma to π′ : Q̃ → Q. Here we will substantially use the fact that γ_{N} ∈ Q̃ and the consequence γ_{N} = cr(π′). To see this, it suffices to show that γ^{∗} ∈ Q̄. But ht(Q̄) = γ^{∗} is only possible if Q̄ is active, since J_{γ^{∗}}^{E^{∗}} is a ZFC^{−}-model. Then λ(Q̄) = λ_{N^{∗}}^{∗}, and the argument from the end of the previous paragraph yields a contradiction. Option a) in the condensation lemma is impossible, as λ_{N}^{+Q̃} = γ_{N} < π(γ^{∗}) = λ_{N}^{+Q}. Option b) fails, as γ_{N} indexes an extender in Q but, being a Q̃-cardinal, cannot index any extender in Q̃. Option c) is false, as Q̃ is sound above λ_{N}. Finally, option d) cannot occur as Q̃ projects to λ_{N}, while γ_{N} is a cardinal in Ult(Q, E_{γ_{N}}). This yields the desired contradiction and completes the proof of the lemma. ⊓ ⊔(Lemma 2.4)

Lemma 2.5. Let N be pluripotent of type B and let (μ, q) be as in the previous lemma. Assume further that λ_{N^{∗}} > μ. Then q = p_{N} ∩ λ. Moreover, e_{N} and γ_{N} are Σ_{1}(N)-definable one from the other with respect to the language for coherent

CHARACTERIZATION OF □_{κ} IN CORE MODELS 35

structures, and using only parameters from μ ∪ {r} where r = p_{N} − λ. It follows that (μ, q) is a divisor.

On the other hand, if N is pluripotent of type B and (μ, q) is a divisor of N such that λ_{N^{∗}} > μ, then e_{N} ∈ rng(π) where π = π_{N}(μ, q). Moreover, we have the same conclusion regarding the relationship between e_{N} and γ_{N} as before. Proof. We only give a proof of the former; the latter follows by a similar and, in fact, simpler argument. It follows from the previous lemma that γ_{M} is in the range of π. If γ_{N} < κ then γ_{N} < μ, since no ordinals from [μ, κ) are in the range of π. So there is nothing to prove, as d_{N} = p_{N} and e_{N} = ∅. From now on assume γ_{N} ≥ κ; the argument we have just given yields γ_{N} ≥ λ.

Let μ̄ be, as in the proof of the previous lemma, the common critical point of E_{top}^{N} and E_{top}^{N^{∗}} and let e′ = e_{N} −λ. From Lemma 1.7 we obtain r ∪e′ = d_{N} −λ, and from the previous lemma we have γ_{N} ∈ h_{N}^{∗}(μ ∪ {r, e′}). If e_{N} = ∅, the conclusions of the current lemma follow immediately. So suppose that e_{N} is nonempty. We now borrow Lemma 2.14 from the next subsection. We found it more natural to place the lemma there, although it states a general fact about pluripotent L[E]-levels which depends merely on elementary properties of premice. As γ_{N} is in h_{N}^{∗}(μ ∪ {r, e′}), there is an f : μ̄ → μ̄ such that γ_{N} = E_{top}^{N}(f)(r, e′, ξ) for some ξ < μ. From the fact that r ⊂ p_{N} and e_{N} is the ≤^{∗}-least d with the property that γ_{N} = E_{top}^{N}(f)(p_{N}, d, ξ) for some f as above and ξ < κ we immediately obtain e_{N} ≤^{∗} e′. Hence e_{N} = e′, as e′ ⊂ e_{N}. This shows that q = p_{N} ∩ λ. Also, it is clear that γ_{N} is Σ_{1}(N)-definable from parameters in μ ∪ {r, e_{N}}.

We now show that e_{N} ∈ h_{N}^{∗}(μ ∪ {r, γ_{N}}). Let e be the ≤^{∗}-least finite set of ordinals in h_{N}^{∗}(μ ∪ {r, γ_{N}}) such that γ_{N} = E_{top}^{N}(f)(r, e, ξ) for some f : μ̄ → μ̄ and ξ < μ. If e_{N} ≠ e, then e_{N} <^{∗} e, so there is a g : μ̄ → μ̄ such that e_{N} witnesses the statement

(∃x, η)[x <^{∗} d & η < λ′ & γ_{N} = E_{top}^{N}(g)(r, x, η)]

holds in N where λ′ = min(h_{N}^{∗}(μ ∪ {r, γ_{N}}) − μ). To see that η can be bounded by λ′, note that λ′ ≥ λ > κ, as h_{N}^{∗}(μ ∪ {r, γ_{N}}) ⊂ h_{N}^{∗}(μ ∪ {r, e_{N}}) and η can be certainly bounded by κ. Notice also that g ∈ h_{N}^{∗}(μ∪{r, γ_{N}}). The above statement, being Σ_{1}, is then witnessed by some e′ and η from h_{N}^{∗}(μ∪{r, γ_{N}}). Obviously, such an η is smaller than μ. So e was not chosen minimally after all. Contradiction.

36 ERNEST SCHIMMERLING AND MARTIN ZEMAN

The argument just given shows that

h_{N}(μ ∪ {r}) = h_{N}^{∗}(μ ∪ {r, γ_{N}}) = h_{N}^{∗}(μ ∪ {r, e_{N}}),

so q is a divisor of N. ⊓ ⊔(Lemma 2.5)

It only remains to discuss the case where λ_{N^{∗}} = μ; it is clear that q = d_{N} in this case. By the proof of (1), μ is inaccessible in L[E] both in Lemma 2.3 as well as in the following lemma. Furthermore, if π is the associated uncollapsing map and F the derived extender, then N = Ult^{∗}(N^{∗}, F) = Ult(N^{∗}, F) and π turns out to be the associated ultrapower map, as follows from the proof of Lemma 2.1. Lemma 2.6. Let N be pluripotent and μ ≤ κ be such that

a) h_{N}^{∗}(μ) is cofinal in N;

b) λ =^{def} min(h_{N}^{∗}(μ) − μ) = λ_{N}.

If N^{∗} is the transitive collapse of h_{N}^{∗}(μ), then N^{∗} = N || ϑ where ϑ = ht(N^{∗}) = μ^{+N^{∗}}. Moreover, we can define a protomouse M(N) similarly as in Lemma 2.3. Proof. As before, μ = cr(π) where π is as above. We observe that μ is a cutpoint of E_{top}^{N}. This follows from the equality E_{top}^{N}(f)(ξ) = E_{top}^{N^{∗}}(f)(ξ) < μ for f : μ̄ → μ̄ and ξ < μ which, in turn, is a consequence of the fact that μ = cr(π). So N^{∗} is a proper initial segment of N by the initial segment condition. Clearly, μ^{+N^{∗}} = ht(N^{∗}). Notice also that N^{∗} can be of type A or C even if N is of type B in this case.

⊓ ⊔(Lemma 2.6)

The discussion in the previous three lemmata guarantees that the following definition is consistent with our earlier definiton of divisor. Definition. Given a pluripotent N, a pair (μ, q) is a divisor of N iff a) – d) of our earlier definition hold with h_{N}^{∗} and d_{N} in place of h̃_{N}^{n+1} and p_{N}, respectively.

The protomouse associated with the divisor (μ, q) of N is denoted by N(μ, q) and its top extender by F_{N}(μ, q). The further auxiliary parameters associated with N and (μ, q) are denoted in the obvious way, i.e. we write ϑ_{N}(μ, q) for ϑ(N(μ, q)), π_{N}(μ, q) for the associated ultrapower map π, λ_{N}(μ, q) for π(μ) = λ(F), r(μ, q) for r = p_{N} − q = π(p_{N^{∗}}), ν_{N}(μ, q) for π(ϑ_{N}(μ, q)), etc. If N is clear from the context we omit the subscript; this applies also to the notation which will be introduced later.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 37

Let us finally stress that for an active L[E]-level N we have the equivalence

(11)  λ_{N^{∗}(μ,q)} > μ iff λ_{N}(μ, q) < λ_{N},

which is obvious by (8). Notice this statement provides us with a nontrivial piece of information only if N is pluripotent. Also, λ_{N}(μ, q) = λ_{N} implies that N is pluripotent.

Definability: Premice versus Protomice. For our fixed local successor τ, the associated collapsing level N is the object of our primary interest. As we have already indicated, some arguments will require us to replace this collapsing level by a protomouse, say M. What will be important for us later is the ability to talk about N in the language of the structure M and vice versa. We now develop a uniform procedure which provides such a translation. Also, our later applications will require that such a translation procedure between M and N works even in those cases where N is not necessarily an L[E]-level. Thus, unless specified otherwise, throughout this subsection we shall assume:

A) M = ⟨J_{ν}^{E}, F ⟩ is a coherent structure such that J_{ν}^{E} is a premouse all of whose proper initial segments are solid and F is an extender at μ, λ; B) ϑ < μ^{+M}, μ is the largest cardinal in J_{ϑ}^{E}, dom(F) = 𝒫(μ) ∩ J_{ϑ}^{E} and N^{∗} is

the collapsing level for ϑ in M; C) ωϱ_{N^{∗}}^{n+1} ≤ μ < ωϱ_{N^{∗}}^{n};

D) π : N^{∗} ⟶_{F}^{∗} N.

This is certainly true of any L[E]-level N and N(μ, q) where (μ, q) is a divisor of N. Notice also that N^{∗}, being a proper initial segment of J_{ν}^{E}, is sound and solid. This means that π is Σ_{0}^{(n)}-preserving and cofinal. Setting r = π(p_{N^{∗}}), we obtain N = h̃_{N}^{n+1}(λ ∪ {r}), so ωϱ_{N}^{n+1} ≤ λ. Also, each α ∈ r has a generalized solidity witness in N with respect to r and N, namely π(W_{N^{∗}}^{ᾱ,p_{N^{∗}}}) where ᾱ is the π-preimage of α. By Lemma 1.1, r = p_{N} − λ whenever N is solid, in particular, whenever N is an L[E]-level. Recall that if N is active, then N^{∗} and N are of the same type whenever λ_{N}(μ, q) < λ_{N}. Lemma 2.7. Assume N is either passive or else λ_{N}(μ, q) < λ_{N}. Let φ(v_{0}, …, v_{ℓ}) be a Σ_{1}^{(n)}-formula in the language for premice. There is a Σ_{1}-formula φ^{∗}(v_{0}, …, v_{ℓ}) in the language for coherent structures such that for every tuple x_{1}, …, x_{ℓ} ∈ J_{λ}^{E} we

38 ERNEST SCHIMMERLING AND MARTIN ZEMAN

have

N ⊧ φ(r, x_{1}, …, x_{ℓ}) iff M ⊧ φ^{∗}(ϑ, x_{1}, …, x_{ℓ})

If N is active with λ_{N}(μ, q) = λ_{N} then an analogous conslusion holds for any Σ_{1}-formula φ(v_{1}, …, v_{ℓ}) in the language for coherent structures: There is a Σ_{1}- formula φ^{∗}(v_{0}, …, v_{ℓ}) in the language for coherent structures such that for every tuple x_{1}, …, x_{ℓ} ∈ J_{λ}^{E} we have

N ⊧ φ(x_{1}, …, x_{ℓ}) iff M ⊧ φ^{∗}(ϑ, x_{1}, …, x_{ℓ})

Moreover, the formula φ^{∗} depends only on φ and is independent of M. In fact, φ^{∗} effectively computable from φ. Proof. If N is as in the first part of the lemma and active then N^{∗} and N are of the same type, so it does make sense to use the language for premice, as the constant symbol γ^{·} is interpreted in the same way in both N^{∗} and N. In the second part of the lemma, however, the two structures might be of different types; this explains why we demand that φ is a formula in the language for coherent structures.

We give a proof of the first part of the lemma where N is either passive or λ_{N}(μ, q) < λ_{N}, as the proof of the second part is similar. Furthermore, we will focus on the special case where each x_{i} is an ordinal less than λ, and write α_{i} instead of x_{i}. The same argument proves the lemma in its full generality if we additionally employ the fact that each x ∈ J_{λ}^{E} is Σ_{1}(J_{λ}^{E})-definable from an ordinal α < λ as the α-th element of J_{λ}^{E} in the ordering <_{E}.

Suppose φ is of the form (∃z^{n})ψ(z^{n}, v_{0}, …, v_{ℓ}) where ψ is Σ_{0}^{(n)}. Then N ⊧ φ(r, α_{1}, …, α_{ℓ}) iff (∃u ∈ H_{N^{∗}}^{n})[N ⊧ (∃z^{n} ∈ π(u))ψ(z^{n}, r, α_{1}, …, α_{ℓ})]. Using the Łoś theorem, the latter can be expressed in a Σ_{1}-fashion over M as

(∃Q, p^{∗}, μ, a, y, u, m)φ_{0}^{∗}(Q, p^{∗}, μ, a, y, u, m, ϑ, α_{1}, …, α_{ℓ})

where φ_{0}^{∗}(Q, p^{∗}, μ, a, y, u, m, ϑ, α_{1}, …, α_{ℓ}) is the conjunction of the following statements:

• Q is an initial segment of M and m ∈ ω
• ωϑ = μ^{+Q}, ωϱ_{Q}^{m+1} = μ < ωϱ_{Q}^{m}, p^{∗} = p_{Q} and u ∈ H_{Q}^{m}
• a = {≺η_{1}, …, η_{ℓ}≻ ∈ μ; Q ⊧ (∃z ∈ u)ψ(z, p^{∗}, η_{1}, … η_{ℓ})}
• y = F (a) and ≺α_{1}, … α_{ℓ}≻ ∈ y

CHARACTERIZATION OF □_{κ} IN CORE MODELS 39

It is obvious that the conversion from φ to φ^{∗} is effective and independent on M. ⊓ ⊔(Lemma 2.7)

The same proof yields in fact a “boldface” version of the above lemma, but the conversion from φ to φ^{∗} is then not uniform. As any parameter c ∈ N is of the form π(f)(α) for some α < λ and f ∈ Γ(μ, N^{∗}), the image π(f) is a good Σ_{1}^{(n−1)}(N)-function in a parameter from rng(π). Then φ^{∗} will clearly depend on the functionally absolute definition of f and both α as well as the above mentioned parameter from rng(π) must also be considered. Lemma 2.8. Let φ(v, v_{0}, …, v_{ℓ}) be as in Lemma 2.7 and c ∈ N. There is a Σ_{1}- formula φ^{∗}(v, v_{0}, …, v_{ℓ}) in the language for coherent structures and a c^{∗} ∈ J_{λ}^{E} such that for every α_{1}, …, α_{ℓ},

N ⊧ φ(c, r, α_{1}, …, α_{ℓ}) iff M ⊧ φ^{∗}(c^{∗}, ϑ, α_{1}, …, α_{ℓ})

if N is as in the first part of Lemma 2.7, and

N ⊧ φ(c, α_{1}, …, α_{ℓ}) iff M ⊧ φ^{∗}(c^{∗}, ϑ, α_{1}, …, α_{ℓ})

if N is as in the second part of Lemma 2.7. ⊓ ⊔(Lemma 2.8) Corollary 2.9. Given a finite set of ordinals q ⊂ λ, the following conversions hold between N and M. In particular, these conversions hold between N and N(μ, q) whenever N is an L[E]-level and (μ, q) a divisor thereof. In the two clauses below, A is computed in the language for premice if N is either passive or else λ_{N}(μ, q) < λ_{N}, and in the language for coherent structures otherwise. A^{∗} is computed in the language for coherent structures.

a) To every A that is Σ_{1}^{(n)}(N) in the parameter r ∪ q there is an A^{∗} that is Σ_{1}(M) in the parameters q and ϑ such that A ∩ λ = A^{∗} ∩ λ.

b) To every A ∈ Σ_{1}^{(n)}(N) there is an A^{∗} in Σ_{1}(M) such that A ∩ λ = A^{∗} ∩ λ.

⊓ ⊔(Corollary 2.9)

The following three lemmata provide us with the dual conversions. Lemma 2.10. Let φ(v_{1}, …, v_{ℓ}) be a Σ_{1}-formula in the language for coherent structures.

Assuming that N is either passive or else λ_{N}(μ, q) < λ_{N}, there is a Σ_{1}^{(n)}-formula ∗φ(v, v′, v_{0}, …, v_{ℓ}) in the language for premice and an ordinal ξ_{0} < μ such that for

40 ERNEST SCHIMMERLING AND MARTIN ZEMAN

every x_{1}, …, x_{ℓ} ∈ M we have

M ⊧ φ(x_{1}, …, x_{ℓ}) iff N ⊧ ^{∗}φ(r, ξ_{0}, μ, x_{1}, …, x_{ℓ}).

If N is active with λ_{N}(μ, q) = λ_{N}, there is a Σ_{1}-formula ^{∗}φ(v_{0}, …, v_{ℓ}) in the language for coherent structures such that for every x_{1}, …, x_{ℓ} ∈ M we have

M ⊧ φ(x_{1}, …, x_{ℓ}) iff N ⊧ ^{∗}φ(μ, x_{1}, …, x_{ℓ}).

As before, the formula ^{∗}φ depends only on φ and is independent of M and, in fact, can be effectively computed from φ. Proof. Since φ is a Σ_{1}-formula, M ⊧ φ(x_{1}, …, x_{ℓ}) iff there is a ζ < ων such that ⟨S_{ζ}^{E}, F ∩ S_{ζ}^{E}⟩ ⊧ φ(x_{1}, …, x_{ℓ}). Fixing an ordinal ξ_{0} < μ such that h̃_{N}^{n+1}(ξ_{0}, r) = λ, the latter is expressible in a Σ_{1}^{(n)}-fashion over N in the parameters r, μ, ξ_{0} as

(∃ζ^{n}, λ^{n}, η_{1}^{n}, η_{2}^{n}, f^{n}, G^{n}, Q^{n})^{∗}φ_{0}(ζ^{n}, λ^{n}, η_{1}^{n}, η_{2}^{n}, f^{n}, G^{n}, Q^{n}, r, ξ_{0}, μ, x_{1}, …, x_{ℓ})

where^{∗}φ_{0}(ζ^{n}, λ^{n}, η_{1}^{n}, η_{2}^{n}, f^{n}, G^{n}, Q^{n}, r, ξ_{0}, μ, x_{1}, …, x_{ℓ}) is the conjunction of the following statements:

• η_{1}^{n}, η_{2}^{n} < μ and ζ^{n} < (λ^{n})^{+N}
• ζ^{n} = h̃_{N}^{n+1}(η_{1}^{n}, r), f^{n} = h̃_{N}^{n+1}(η_{2}^{n}, r) and λ^{n} = h̃_{N}^{n+1}(ξ_{0}, r)
• f^{n} : λ^{n} ⟶^{onto} 𝒫(λ^{n}) ∩ S_{ζ^{n}}^{E}
• G^{n} = {⟨f^{n}(η) ∩ μ, f^{n}(η)⟩; η < μ} and Q^{n} = ⟨S_{ζ^{n}}^{E}, G^{n}⟩
• Q^{n} ⊧ φ(x_{1}, …, x_{ℓ})

It is clear that the conversion from φ to ^{∗}φ is effective and does not depend on M. ⊓ ⊔(Lemma 2.10)

An argument similar to that above yields a version of the previous lemma where the pair of parameters ξ_{0}, μ is replaced by ϑ; the conversion from φ to ^{∗}φ is again effective. Lemma 2.11. Suppose φ(v_{1}, …, v_{ℓ}) is a Σ_{1}-formula in the language for coherent structrures.

Assuming that N is either passive or else λ_{N}(μ, q) < λ_{N}, there is a Σ_{1}^{(n)}-formula ∗φ(v, v_{0}, …, v_{ℓ}) such that for every x_{1}, …, x_{ℓ} ∈ M,

M ⊧ φ(x_{1}, …, x_{ℓ}) iff N ⊧ ^{∗}φ(r, ϑ, x_{1}, …, x_{ℓ}),

CHARACTERIZATION OF □_{κ} IN CORE MODELS 41

and the obvious reformulation is true if N is active with λ_{N}(μ, q) = λ_{N}.

As before, the formula ^{∗}φ depends only on φ and is independent of M and, in fact, can be effectively computed from φ. ⊓ ⊔(Lemma 2.11) Corollary 2.12. Given any c ∈ M, the following conversions hold between M and N. In particular, these conversions hold for N and N(μ, q) where N is an arbitrary L[E]-level and (μ, q) is a divisor thereof. The situation here is dual to that in Corollary 2.9, so ^{∗}A is computed in the language for premice if N is either passive or else λ_{N}(μ, q) < λ_{N}, and in the language for coherent structures otherwise. A is computed in the language for coherent structures.

a) To every A from Σ_{1}(M) in c there is an ^{∗}A in Σ_{1}^{(n)}(N) in c, r, ϑ such that

A ∩ λ = ^{∗}A ∩ λ.

b) To every A ∈ Σ_{1}(M) there is an ^{∗}A ∈ Σ_{1}^{(n)}(N) such that A ∩ λ = ^{∗}A ∩ λ.

⊓ ⊔(Corollary 2.12)

When dealing with singletons definable over N, there is another way of switching between the languages of N and M. Such a conversion is then not uniform in the above sense, but will be useful for proving that certain properties of protomice are preserved under embeddings with weak preservation properties. The formulations of the next lemmata make use of the convention we made at the end of the section on extenders and coherent structures in preliminaries. Thus, if f is a function defined on ordinals, we will write f(a) even if a is a finite set or sequence of ordinals, as such objects are recursively encodable into ordinals. Lemma 2.13. Let b ⊂ λ be finite, ζ < λ and y ⊂ λ.

a) If ζ, resp. y, is Σ_{1}^{(n)}(N)-definable from r and b, then there is an f : μ → μ, resp. f : μ → 𝒫(μ) in N^{∗} such that ζ = F (f)(b), resp. y = F (f)(b).

b) If ζ = F (f)(b), resp. y = F (f)(b) where f : μ → μ, resp. f : μ → 𝒫(μ) is in N^{∗}, then ζ, resp. y is Σ_{1}^{(n)}(N)-definable from r, b and some ξ < μ.

As usual, here we consider Σ_{1}^{(n)}(N)-definability with respect to the language for premice if λ_{N}(μ, q) < λ_{N}, and with respect to the language for coherent structures if λ_{N}(μ, q) = λ_{N}. Proof. We give a proof for ζ. To see a), suppose ζ is the unique object such that N ⊧ (∃z^{n})ψ(z^{n}, ζ, r, b) where ψ is a Σ_{0}^{(n)}-formula. Fix a δ^{∗} < ωϱ_{N^{∗}}^{n} large enough

42 ERNEST SCHIMMERLING AND MARTIN ZEMAN

such that, setting δ = π(δ^{∗}), there is a z ∈ S_{δ}^{E} witnessing this existential statement; such a δ^{∗} exists since π is cofinal at the n-th level. Define a partial map f : μ → μ as follows:

f(x) ≃ the unique ξ < μ satisfying N ⊧ (∃z^{n} ∈ S_{δ^{∗}}^{E})ψ(z^{n}, ξ, p_{N^{∗}}, x)

Then f, being a Σ_{0}^{(n)}(N) subset of μ < ωϱ_{N^{∗}}^{n}, is an element of N^{∗}. Applying π, it follows that π(f)(x), if defined, is the unique ordinal ξ < λ such that we have (∃z^{n} ∈ J_{δ}^{E})ψ(z^{n}, ξ, r, x) in N. But for x = b we know that π(f)(x) is defined, so F (f)(b) = π(f)(b) = ζ. Obviously, f can be turned into a total function on μ by setting f(x) = 0 whenever f(x) is undefined by the above definition.

To see b), suppose ζ = F (f)(b) for f, b as above; since N^{∗} is sound, there is a ξ < μ such that f = h̃_{N^{∗}}^{n+1}(ξ, p_{N^{∗}}). The preservation properties of π, yield π(f) = h̃_{N}^{n+1}(ξ, r), so ζ can be defined in a Σ_{1}^{(n)}-fashion over N as follows:

(∃g^{n})(g^{n} = h̃_{N}^{n+1}(ξ, r) & ζ = g^{n}(b)).

⊓ ⊔(Lemma 2.13)

The following is a version of the previous lemma that will be useful when dealing with pluripotent L[E]-levels N. Lemma 2.14. Let N = ⟨J_{ν}^{E}, F ⟩ be a coherent structure such that F is at μ, λ and dom(F) = 𝒫(μ) ∩ N. Suppose further that b ⊂ λ is finite, ζ < λ and y ⊂ λ.

a) If ζ, resp. y is Σ_{1}(N)-definable from b then there is an f : μ → μ, resp. f : μ → 𝒫(μ) in N such that ζ = F (f)(b, μ), resp. y = F (f)(b, μ).

b) If ζ = F (f)(b, μ), resp. y = F (f)(b, μ)) for an f ∈ N such that f : μ → μ, resp. f : μ → 𝒫(μ), then ζ, resp. y is Σ_{1}(N)-definable from b and f.

Both a) and b) concerns Σ_{1}(N)-definability in the language for coherent structures.

In particular, a) and b) is true of any pluripotent L[E]-level N. Proof. Note first that b) follows immediately: The fact that ζ = F (f)(b, μ) can be expressed in a Σ_{1}-fashion in b over N as

(∃w)(⟨f, w⟩ ∈ F & ζ = w(≺b, μ≻)).

The ordinal μ can be elimitated from this definition, as it is Σ_{1}-definable over N without parameters.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 43

To see the converse a), let ζ be the unique object such that N ⊧ (∃z)ψ(z, ζ, b) for a Σ_{0}-formula ψ. Let π be the ultrapower map associated with Ult(J_{ϑ}^{E}, F), where ϑ = μ^{+N}. Pick a δ^{∗} < ϑ large enough such that μ is the largest cardinal in J_{δ^{∗}}^{E} and the above formula still holds in Ñ = ⟨J_{δ}^{E}, F̃⟩, where δ = π(δ^{∗}) and F̃ = F ∩ J_{δ}^{E}. Fix an enumeration g : μ ⟶^{onto} 𝒫(μ) ∩ J_{δ^{∗}}^{E}, which is itself in N. For convenience suppose that π maps δ^{∗} cofinally to δ; this holds whenever cf^{N}(δ^{∗}) ≠ μ (thus, there are stationarily many – in the sense of J_{ν}^{E} – such ordinals δ^{∗} below ϑ). Setting

g^{∗}(η) = ⟨⟨g(η̄), g(η̄) ∩ η⟩; η̄ < η⟩

and g̃(η) = ⟨J_{δ^{∗}}^{E}, g^{∗}(η)⟩ for η < μ, it is easy to verify that π(g̃)(μ) = Ñ. Define a partial map f : μ → μ by

f(≺x, η≻) ≃ the unique ξ < μ such that g̃(η) ⊧ (∃z)ψ(z, ξ, x);

then π(f)(x, μ) is the unique ordinal ξ < λ such that π(g̃)(μ) = Ñ satisfies (∃z)ψ(z, ξ, x), provided that such a ξ exists. As before, we know that for x = b such a ξ exists, so F (f)(b, μ) = ζ. ⊓ ⊔(Lemma 2.14)

The previous lemmata give us a method for expressing the statement “(μ′, q′) is a divisor of N” over N(μ, q) whenever μ′ ≥ μ and q′ is a bottom segment of q. The important point here is that over N(μ, q) we use the language for coherent structures, and the above statement is uniformly expressible in this language, no matter what kind of premouse N is or whether λ_{N}(μ, q) < λ_{N}. Lemma 2.15. Let (μ, q) be a divisor of N where N is the collapsing L[E]-level for τ < κ^{+}. Let further μ ≤ μ′ ≤ κ and q′ = q ∩ λ̄ for some λ̄ ≤ max(q) + 1 where max(∅) = κ + 1 by definition. Set r′ = q − q′ and F = F (μ, q). Then (μ′, q′) is a divisor of N iff for every ξ < μ′ and f : μ → μ we have

(12)  ζ = F (f)(r′, ξ) & ζ ≤ max(q′) ⟶ ζ < μ′

The same is also true for pluripotent N and μ′ > μ with F = E_{top}^{N}, μ = cr(F) and q a bottom part of d_{N}. Proof. Let (μ, q) be a divisor of N where N is the collapsing L[E]-level for τ and let F = F_{N}(μ, q). Let us first discuss the case where N is either passive or else λ_{N}(μ, q) < λ_{N}. Granting (12), we show that (μ′, q′) is a divisor of N. Let ζ ≤ max(q′) be such that ζ = h̃_{N}^{n+1}(ξ, r ∪ r′) for some ξ < μ′. By Lemma 2.13,

44 ERNEST SCHIMMERLING AND MARTIN ZEMAN

ζ = F (f)(r′, ξ) for some ξ < μ ≤ μ′. So ζ < μ′ by (12). This tells us that h̃_{N}^{n+1}(μ′ ∪ {r, r′}) ∩ (max(q′) + 1) = μ′, which verifies a), b) and d) of the definition of divisor. To see that also c) holds, notice that h̃_{N}^{n+1}(μ′ ∪ {r, r′}) ⊃ h̃_{N}^{n+1}(μ ∪ {r}) and (μ, q) is a divisor.

Now assume that (μ′, q′) is a divisor of N. If ζ = F (f)(r′, ξ) for some function f : μ → μ and an ordinal ξ < μ′, then, again by Lemma 2.13, there is a ξ′ < μ such that ζ = h̃_{N}^{n+1}(ξ, {ξ′, r′, r}), so ζ ∈ h̃_{N}^{n+1}(μ′ ∪ {r′, r}). As (μ′, q′) is a divisor and ζ ≤ max(q′), we have ζ < μ′.

If N is active with λ_{N}(μ, q) = λ_{N} (recall that N is automatically pluripotent in this case) then the same argument goes through, but we have to work in the language for coherent structures. Here we also use the consequence of Lemmata 2.4 and 2.5 that, granting that N is pluripotent and h_{N}^{∗}(μ′ ∪{d_{N} −q′}), the pair (μ′, q′) is a divisor for N computed in the language for coherent structures just in case that (μ′, q′) is a divisor for N computed in the language for premice.

Finally consider the case where N is pluripotent, F = E_{top}^{N} and μ = cr(F). We can again imitate the above argument, this time using Lemma 2.14 in place of Lemma 2.13. Notice that μ occurs as a parameter in F (f)(r′, ξ, μ). This is, however, harmless, as any candidate (μ′, q′) for a divisor must satisfy the restriction μ′ > μ. Indeed, the ordinal μ, being the critical point of the top predicate F, is automatically in the range of π_{N}(μ′, q′). ⊓ ⊔(Lemma 2.15)

Protomice, Fine Structure and Condensation. Using the lemmata from the previous subsection we determine the relationship between the fine structural parameters of N(μ, q) from those of N. Moreover, we establish a sort of condensation lemma for protomice. We first turn to general facts about coherent structures. For our later purposes, it will be useful to introduce “solidity” witnesses in the following weaker sense. To understand the next definition, we recommend to recall the facts about solidity witnesses from preliminaries. Definition. Let M = ⟨J_{ν}^{E}, F ⟩ be a coherent structure satisfying A) – D) from the previous subsection and let N be the premouse associated with M. Given a finite s ⊂ λ and an α such that ϑ ≤ α < λ, we define the standard witness W_{M}^{α,s} for α with respect to M and s to be the transitive collapse of h_{M}(α ∪ {s}) and, similarly, the standard witness W_{N}^{α,r∪s} for α with respect to N and s ∪ r to be the transitive

CHARACTERIZATION OF □_{κ} IN CORE MODELS 45

collapse of h̃_{N}^{n+1}(α ∪ {r ∪ s}). The canonical witness maps are then defined in the obvious way. More generally, a generalized witness for α with respect to M and s is a pair ⟨Q, t⟩, where Q is an acceptable J-structure and t ⊂ Q a finite set of ordinals such that given any ξ_{1}, …, ξ_{ℓ} < α,

M ⊧ Φ(i, ξ_{1}, …, ξ_{ℓ}, s) ⟶ Q ⊧ Φ(i, ξ_{1}, …, ξ_{ℓ}, t)

where Φ is the universal Σ_{1}-formula. A generalized witness for α with respect to N and r ∪ s is a pair ⟨Q, t⟩, where Q is an acceptable J-structure and t ⊂ Q a finite set of ordinals such that given any ξ_{1}, …, ξ_{ℓ} < α,

N ⊧ Φ(i, ξ_{1}, …, ξ_{ℓ}, r ∪ s) ⟶ Q ⊧ Φ(i, ξ_{1}, …, ξ_{ℓ}, t)

where Φ is the universal Σ_{1}^{(n)}-formula.

The main point of this definiton is that generalized witnesses in this weaker sense are related merely to Σ_{1}^{(n)}-satisfaction even if α < ωϱ_{N}^{n+1} (and correspondingly for M), so they omit too much information to be able to say anything about the solidity of N, resp. M. The reason why we introduce them is that they might become genuine solidity witnesses after collapsing certain Skolem hulls in the original structure, which will be utilized in our later constructions. We again stress that this notion is defined exclusively for the present context, i.e. for coherent structures satisfying A) – D) as above, and should be considered as an ad hoc notion introduced for our convenience. Lemma 2.16. Let M = ⟨J_{ν}^{E}, F ⟩ be a coherent structure satisfying A) – D) from the previous subsection. Then

a) ωϱ_{M}^{1} = ωϱ_{N}^{n+1}. Denote this common value by ωϱ. Granting that μ < ωϱ, the following holds:

b) p_{M}^{1} = p_{N}^{n+1} ∩ λ.

c) M is 1-sound iff N is (n + 1)-sound.

d) Let s be a finite subset of λ and ϑ ≤ α < λ. Then W_{N}^{α,s∪r} = Ult^{∗}(N^{∗}, G) where G is the top extender of W_{M}^{α,s}. Moreover, the associated ultrapower embedding is precisely the uncollapsing map associated with the Σ_{1}^{(n)}(W_{N}^{α})- hull of μ ∪ {r ∪ s − (α + 1)}.

e) M is 1-solid iff N is (n + 1)-solid.

46 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Proof. Note first that neither ωϱ_{M}^{1} nor ωϱ_{N}^{n+1} is larger than λ. In the following we show that a) – c) are direct consequences of Corollaries 2.9 and 2.12.

If A is a Σ_{1}(M)-relation in p_{M}^{1} then there is a Σ_{1}^{(n)}(N)-relation ^{∗}A in p_{M}^{1}, r and ϑ such that ^{∗}A agrees with A up to ωϱ_{M}^{1}. Choose A such that A ∩ ωϱ_{M}^{1} ∉ M. Then ∗A∩ωϱ_{M}^{1} is not a member of J_{ν}^{E} and therefore of N. This follows from acceptability and the fact that ν is a cardinal in N. Thus, ωϱ_{N}^{n+1} ≤ ωϱ_{M}^{1}. The dual argument using Corollary 2.9 yields the converse, which proves a).

From now on suppose that μ < ωϱ. The ordinal ωϱ, being smaller than λ, is a cardinal in both M and N. By our assumption on ϑ we have ϑ < ωϱ. Given A as above, there is a Σ_{1}^{(n)}(N) relation ^{∗}A such that A(η) ⟷ ^{∗}A(p_{M}^{1}, r, ϑ, η) whenever η < λ. (Here we use Lemma 2.11.) From ^{∗}A we obtain a new subset of ωϱ which Σ_{1}^{(n)}(N) in p_{M}^{1} ∪ r, so r ∪ (p_{N}^{n+1} ∩ λ) = p_{N}^{n+1} ≤^{∗} r ∪ p_{M}^{1} and, consequently, p_{N}^{n+1} ∩λ ≤^{∗} p_{M}^{1}. As before, the dual argument yields the converse, which proves b).

If M is 1-sound, then every ξ < λ is Σ_{1}(M)-definable from p_{M}^{1} = p_{N}^{n+1} ∩ λ and a parameter less than ωϱ. Thus, every ξ < λ is Σ_{1}^{(n)}(N) definable from r∪(p_{N}^{n+1}∩λ) = p_{N}^{n+1} and parameters less then ωϱ, in other words, N = h̃_{N}^{n+1}(ωϱ ∪ {p_{N}^{n+1}}). Thus, p_{N}^{n+1} ∈ R_{N}^{n+1}, i.e. N is (n + 1)-sound. The converse follows again by the dual argument. This proves c).

Next we prove e) from d). To see that the 1-solidity of M implies the (n + 1)- solidity of N, notice that W_{M}^{α}, being the transitive collapse of h_{M}(α ∪ {p_{M}}), can be encoded into a Σ_{1}(M) subset a of α. Such an a is in J_{ν}^{E} by acceptability and W_{M}^{α} can be reconstructed from a inside J_{ν}^{E}. But then also W_{N}^{α} is in J_{ν}^{E} by d). For the converse use again the dual argument.

It remains to prove d). Let σ̄ : W_{M}^{α,s} → M be the canonical witness map, λ̄ = λ(G) and ν̄ = ht(W_{M}^{α,s}). As σ̄ is Σ_{1}-preserving, dom(G) = 𝒫(μ) ∩ J_{ϑ}^{E}, so G can be applied to N^{∗} (notice that N^{∗} is an initial segment of W_{M}^{α,s}). Let W be the ∗-ultrapower of N^{∗} by G and π̄ : N^{∗} → W the associated ultrapower map. This ultrapower exists, as σ : π̄(f)(ξ) ↦ π(f)(σ̄(ξ)) is a structure preserving embedding of 𝔻^{∗}(N^{∗}, G) to N; here π̄ is viewed as a map into 𝔻^{∗}, f ranges over Γ(μ, N^{∗}) and ξ < λ̄. (To verify this, use Łos’ theorem for Σ_{0} formulae.) By the remarks at the beginning of the previous subsection, π̄ is Σ_{0}^{(n)}-preserving and cofinal, and W = h̃_{W}^{n+1}(λ ∪ {r̄}) where r̄ = π̄(p_{N^{∗}}).

CHARACTERIZATION OF □_{κ} IN CORE MODELS 47

Using the cofinality of both π̄ and π together with the Łoś theorem for Σ_{0}^{(n)}- formulae we show that σ is Σ_{0}^{(n)}-preserving and cofinal. Also, π = σ∘π̄ and σ agrees with σ̄ up to ν̄. It follows that σ(r̄) = r, σ ↾ α = id and, letting s̄ be the σ̄-preimage of s − (α + 1), also σ(s̄) = σ̄(s̄) = s − (α + 1). As each ζ < λ is Σ_{1}(W_{M}^{α,s})-definable from s̄ and parameters below α, Lemma 2.10 combined with the observation at the end of the previous paragraph allow us to conclude that W = h̃_{W}^{n+1}(α ∪ {r̄∪ s̄}), so h̃_{N}^{n+1}(α ∪ {r ∪ s − (α + 1)}) = rng(σ). But this means that W = W_{N}^{α,r∪s} and σ is the associated witness map. ⊓ ⊔(Lemma 2.16)

The next corollary summarizes the properties of protomice N(μ, q) associated with L[E]-levels. Let us explain the notation used in d) below. Let N be an L[E]- level, α < λ_{N}(μ, q) and W_{N}^{α,p_{N}} be the standard witness. Let further σ_{α} : W_{N}^{α,p_{N}} → N be the associated canonical witness map. Setting (r_{α}, q_{α}, λ_{α}) = σ_{α}^{−1}(r, q, λ) where λ = λ_{N}(μ, q) and κ_{α} = (σ^{−1})′′κ, the pair (μ, q_{α}) satisfies a) – d) in the definition of divisor with W_{N}^{α,p_{N}} in place of N and (r_{α}, q_{α}, κ_{α}, λ_{α}) in place of (r, q, κ, λ). Then W_{N}^{α,p_{N}} (μ, q) is the coherent structure ⟨J_{ν_{α}}^{E_{α}}, G⟩ where E_{α} is the extender sequence of W_{N}^{α,p_{N}}, ν_{α} is the cardinal successor of λ_{α} in W_{N}^{α,p_{N}} and G is the extender derived from the uncollapsing embedding associated with h̃_{W}^{n+1}(μ ∪ {r̄}) (here W = W_{N}^{α,p_{N}}). Intuitively, W_{N}^{α,p_{N}} (μ, q) is the protomouse associated with W_{N}^{α,p_{N}} and (μ, q_{α}). Corollary 2.17. Given a divisor (μ, q) of N,

a) ωϱ_{N(μ,q)}^{1} = κ is the ultimate projectum of N(μ, q). Granting that μ < κ, the following holds:

b) p_{N(μ,q)} = p_{N} ∩ λ if N is not pluripotent, and p_{N(μ,q)} = d_{N} ∩ λ otherwise.

c) N(μ, q) is sound and solid.

d) If N is not pluripotent and p =^{def} p_{N(μ,q)}, then for every α ∈ p we have

W_{N(μ,q)}^{α,p} = W_{N}^{α,p_{N}} (μ, q).

If N is pluripotent then the same holds with W_{N}^{α,d_{N}} in place of W_{N}^{α,p_{N}}; this time everything is computed in the language for coherent structrues.

⊓ ⊔(Corollary 2.17)

It follows from our previous results that in b), the latter condition says something new only if λ_{N}(μ, q) = λ_{N}. The next lemma gives a more detailed information

48 ERNEST SCHIMMERLING AND MARTIN ZEMAN

about the definability of standard witnesses over N. We will need such a detailed information only in the proof of Lemma 3.12, so the reader can skip over this lemma now and return to it when necessary. Lemma 2.18. Let (μ, q) be a divisor of N such that q ≠ d_{N} if N is pluripotent. Assume that ⟨Q, t⟩ ∈ N is a generalized witness for β with respect to N and r ∪ s where μ ≤ β < λ and s ⊂ λ. Then W_{N}^{β,r∪s} ∈ N is Σ_{0}-definable inside N from ⟨Q, t⟩, β and ϑ = ϑ_{N}(μ, q). By d) of Lemma 2.16, W_{N(μ,q)}^{β,s} is also Σ_{0}-definable inside N from ⟨Q, t⟩, β and ϑ.

If M is a coherent structure, ϑ(M) ≤ β < λ_{M} and ⟨Q, t⟩ is a generalized witness for β with respect to M and some s ⊂ λ_{M}, then W_{M}^{β,s} is Σ_{0}-definable inside M from ⟨Q, t⟩, β and ϑ(M). Proof. The proof is a refinement of the standard argument which shows that if some generalized solidity witness for α with respect to N and p is in N then so is the standard solidity witness. We shall focus on the proof of the first part of the lemma. The proof of the second part is similar and, in fact, much easier, so we leave it to the reader. Set p = r ∪ s. Let W = W_{N}^{β,p}, let σ : W → N be the canonical witness map and let σ(p̄) = p. We can define a Σ_{0}^{(n)}-preserving embedding σ̃ : W → Q sending p̄ to t which is the identity on β by

h̃_{W}^{n+1}(ξ, p̄) ↦ h̃_{Q}^{n+1}(ξ, t),

as every element of W can be written in the form on the left hand side. Given a Σ_{0}^{(n)}-formula φ(v_{1}, …, v_{ℓ}), each of the following statements is a consequence of the previous one:

W ⊧ φ(h̃_{W}^{n+1}(ξ_{1}, p̄), …, h̃_{W}^{n+1}(ξ_{ℓ}, p̄))
N ⊧ φ(h̃_{N}^{n+1}(ξ_{1}, p), …, h̃_{N}^{n+1}(ξ_{ℓ}, p))
Q ⊧ φ(h̃_{Q}^{n+1}(ξ, t), …, h̃_{Q}^{n+1}(ξ_{ℓ}, t)).

As substituting h̃^{n+1} into a Σ_{0}^{(n)}-formula yields a Σ_{1}^{(n)}-statement, the first implication follows from the fact that σ is Σ_{1}^{(n)}-preserving, and the second implication follows from the definition of a generalized witness. It is now easy to verify that σ̃ is well-defined and Σ_{0}^{(n)}-preserving, as well as that σ̃ ↾ β is the identity and σ̃(p̄) = t.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 49

Let

ωϱ̃ = sup(σ̃′′ωϱ_{W}^{n}).

Then

rng(σ̃) = {y ∈ Q; (∃z ∈ J E^{Q} ; ϱ̃)(∃ξ < β)Q ⊧ ψ(z, y, ξ, t)}

where (∃z^{n})ψ(z^{n}, y, x, u) is the functionally absolute Σ_{1}^{(n)}-definition of h̃^{n+1} and ψ is a Σ_{0}^{(n)}-formula. Thus, rng(σ̃) is an element of N which is Σ_{0}-definable from Q, t, β and ϱ̃. Clearly, this applies also to W, which is the transitive collapse of rng(σ̃).

It remains to eliminate ϱ̃ form the definition of W. Here we use the fact that (μ, q) is a divisor of N. If π = π_{N}(μ, q) and N^{∗} = N^{∗}(μ, q), then π maps ωϱ_{N^{∗}}^{n} cofinally into ωϱ_{N}^{n}. But rng(π) = h̃_{N}^{n+1}(μ ∪ {r}) ⊂ rng(σ), so letting r̄ be the top segment of p̄ of length |r|, we obtain:

• If ξ < μ, then h̃_{W}^{n+1}(ξ, r̄) is defined iff h̃_{N^{∗}}^{n+1}(ξ, p_{N^{∗}}) is defined.

• Y = h̃_{W}^{n+1}(μ ∪ {r̄}) is cofinal in ωϱ_{W}^{n}, so σ̃′′Y ∩ ωϱ_{Q}^{n} is cofinal in ωϱ̃.

Now it follows easily that

ωϱ̃ = sup{ζ < ωϱ_{Q}^{n}; (∃ξ < μ)(h̃_{N^{∗}}^{n+1}(ξ, p_{N^{∗}}) is defined and ζ = h̃_{Q}^{n+1}(ξ, t̄))}

where t̄ is the top part of t of length |r| = |p_{N^{∗}}|. The objects ϱ_{Q}^{n} and h̃_{Q}^{n+1} are Σ_{0}-definable from Q; the objects N^{∗}, p_{N^{∗}}, h̃_{N^{∗}}^{n+1} and μ are Σ_{0}-definable from ϑ and t̄ is Σ_{0}-definable from t and |p_{N^{∗}}|. Thus, Q, t and ϑ are all parameters we need in the definition of ϱ̃. ⊓ ⊔(Lemma 2.18)

We are now ready to state a condensation lemma for protomice. Recall again that all fine structural parameters of protomice are computed in the language for coherent structues. Lemma 2.19. Let M̄ be a coherent structure and let σ : M̄ → N(μ, q). Assume further that the following conditions are met:

a) ωϱ1 ; M̄ = κ and M̄ is sound and solid;

b) σ is a Σ_{0}-preserving map which is the identity on τ̄ = κ^{+M̄} and such that σ(τ̄) = τ and σ(pM̄) = q;

c) μ < κ. Then M̄ = N̄(μ, pM̄) where N̄ is the collapsing level for τ̄.

50 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Proof. Let F̄, λ̄, ν̄, ϑ̄, N̄^{∗}, n̄ have the obvious meaning. We can assume w.l.o.g. that σ is not cofinal; otherwise σ would be Σ_{1}-preserving and, by soundness of N(μ, q), we would have M̄ = N(μ, q) and σ = id. Our assumption implies that ϑ̄ < ϑ and N̄^{∗} is a proper initial segment of N^{∗}. Also, the non-cofinality of σ guarantees that τ̄ < τ, as otherwise τ could be definably collapsed over ⟨J E ; ν̃, F ∩ J E ; ν̃⟩ ∈ N where F = F (μ, q) and ν̃ = sup(σ′′ν̄). Thus, τ̄ = cr(σ).

Let N̄ = Ult^{∗}(N̄^{∗}, F̄) and π̄ : N̄^{∗} → N̄ be the associated ultrapower map. Let further π = π(μ, pM̄). Using the methods from the proof of Lemma 2.16 d) we show that this ultrapower exists, π̄ is Σ_{0}^{(n̄)}-preserving and cofinal and, letting σ̃ : N̄ → π(N̄^{∗}) be the map defined by

σ̃(π̄(f)(α)) = π(f)(σ(α))

for f ∈ Γ(μ, N̄^{∗}) and α < λ_{M}, σ̃ is Σ_{0}^{(n̄)}-preserving and cofinal (here we apply the cofinality of π̄ at the n̄-th level together with the Łoś theorem for Σ_{0}^{(n̄)}-formulae) and σ̃ ↾ λM̄ = σ ↾ λM̄. Hence τ̄ = cr(σ̃).

Assume first that N̄^{∗} is either passive or else λN̄^{∗} > μ. In this case the conclusions of the previous paragraph apply to the language for premice. Similarly as in the case of the pseudoultrapower in the proof of Lemma 2.4 we can apply Lemma 1.5 and infer that N̄ is a premouse of the same type as N̄^{∗}. Furthermore, ωϱn̄+1 ; N̄ = κ < ωϱn̄ ; N̄, pN̄ = π̄(pN̄^{∗})∪pM̄ and N̄ is sound, as follows from Lemma 2.16. This verifies the assumptions of the condensation lemma. A simple discussion of the four cases given by the condensation lemma will give us the conclusion that N̄ is a proper initial segment of π(N̄^{∗}). Thus N̄ is an L[E]-level, as this is certainly true of π(N̄^{∗}). It follows that M̄ = N̄(μ, pM̄). Here are more details as to the application of the condensation lemma. Option a) is impossible, as τ̄ < τ is the cardinal successor of κ in N̄. Option c) contradicts the soundness of N̄, and option d) contradicts the fact that N̄ projects to κ while τ̄ is a cardinal in Ult(π(N̄^{∗}), Eτ̄).

From now on suppose that N̄^{∗} is active with λN̄^{∗} = μ. Then N̄ is a potential premouse which need not be of the same type as N̄^{∗}. Now we have to be more careful when applying Lemma 2.16; the conclusions of this lemma apply to the language for coherent structures in this case. Notice first that ωϱ1 ; N̄ = κ < λN̄, as h∗ ; M̄(κ ∪ {pM̄}) = N̄. It follows that N̄ cannot be of type C.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 51

Let λ̃ = sup(σ̃′′λN̄). If λ̃ < λ(F̃) where F̃ is the top extender of π(N̄^{∗}) then λ̃ is a cutpoint of F̃. To see this, pick any monotonic f : μ̄ → μ̄ that is an element of π(N̄) and any α < λ̃; here μ̄ = cr(F̃) = cr(EN̄^{∗} ; top). It suffices to consider just monotonic maps, as any f′ : μ̄ → μ̄ from π(N̄^{∗}) is dominated by such a map. Let ᾱ < λN̄ be such that σ̃(ᾱ) ≥ α. Notice that f ∈ N̄ and, letting ζ̄ = EN̄ ; top(f)(ᾱ), we have ζ̄ < λN̄ and

F̃(f)(α) ≤ F̃(f)(σ̃(ᾱ)) = σ̃(EN̄ ; top(f)(ᾱ)) = σ̃(ζ̄) < λ̃.

If λ̃ = λ(F̃) let N′ = π(N̄^{∗}) and σ̃′ = σ̃. Otherwise let N′ = π(N̄^{∗}) || ν̃ where ν̃ is the index of F̃ | λ̃. If σ′ : N′ → π(N̄^{∗}) is the canonical embedding (i.e. σ′ : Eν̃(f)(α) ↦ π(f)(α) for f : μ̄ → μ̄ in N̄^{∗} and α < λ̃) then cr(σ′) = λ̃ and it is easy to see that rng(σ̃) ⊂ rng(σ′). Define σ̃′ by σ̃′ = (σ′)^{−1} ∘ σ̃. In either case, σ̃′ : N̄ → N′ is Σ_{0}-preserving and cofinal with respect to the language for coherent structures, and maps λN̄ cofinally into λ_{N′}. We will use this to show that N̄ is a potential premouse of the same type as N′ and σ̃′ has the above preservation properties with respect to the language for premice. Since we already know that N′ cannot be of type C, so assume w.l.o.g. that N′ is of type B; the proof is even easier for N′ of type A.

Recall that λ∗ ; N̄ is the largest cutpoint of EN̄ ; top. We show that σ̃′(λ∗ ; N̄) is the largest cutpoint of E_{top}^{N′}. Since being a cutpoint of the top extender is a Π_{1}-property in the language for coherent structures, it suffices to show that there are no cutpoints of E_{top}^{N′} above σ̃′(λ∗ ; N̄). If λ′ > σ̃′(λ_{N′}^{∗}) were a cutpoint of E_{top}^{N′}, we would have λN̄ < λ̄ < λN̄ where λ̄ is the pointwise preimage of λ′ under σ̃′; the inequality on the right follows from the cofinality of σ̃′. Now we obtain a contradiction by showing that λ̄ is a cutpoint of N̄: If f : μ̄ → μ̄ is in N̄ and α < λ̄ then σ̃′(EN̄ ; top(f)(α)) = E_{top}^{N′}(f)(σ̃′(α)) < λ′, so EN̄ ; top(f)(α)) < λ̄.

Working in the language for coherent structures, from Lemma 2.16 we obtained that h∗ ; N̄(κ ∪ {pM̄}) = N̄ and W α,pM̄ ; N̄ ∈ N̄ whenever α ∈ pM̄; recall that pM̄ = σ^{−1}(q). The former obviously guarantees that ᾱ =^{def} max(pM̄) ≥ λ∗ ; N̄, and the latter implies that the top extender G of W α,pM̄ ; N̄ is an element of N̄. Since EN̄ ; top | λ∗ ; N̄ = G | λ∗ ; N̄, we see that N̄ satisfies the initial segment condition. So N̄ is a premouse. Now it is easy to verify that σ̃′(EN̄ ; top | λ∗ ; N̄) = E_{top}^{N′} | λ_{N′}^{∗}, which implies that the preservation properties of σ̃′ transfer to the language of premice.

52 ERNEST SCHIMMERLING AND MARTIN ZEMAN

The rest of the argument is then similar to that in the previous case where λN̄^{∗} > μ. We intend to apply the condensation lemma, this time to σ̃′ : N̄ → N′. This is possible, as N′ is an L[E]-level, cr(σ̃′) = cr(σ) = τ̄, ωϱ1 ; N̄ ≤ τ and, as we have seen above, σ̃′ has the required preservation properties. It only remains to verify that N̄ is sound with respect to the language for premice. But this follows immediately from the two properties of pM̄ applied in the previous paragraph and from Lemma 1.8 The discussion of the four cases in the condensation lemma is then the same as in the previous case. So we conclude that N̄ is the collapsing L[E]-level for τ̄. Since this time we work in the language for coherent structures, we have pM̄ = dN̄. It is now clear from the definition following Lemma 2.6 that M̄ = N̄(μ, pM̄). ⊓ ⊔(Lemma 2.19)

We shall also need the version of this condensation lemma with pluripotent L[E]- levels as target structures. Lemma 2.20. Let M̄ be a coherent structure and let σ : M̄ → N where N is pluripotent. Assume further that the following conditions are met:

a) ωϱ1 ; M̄ = κ and M̄ is sound and solid;

b) σ is a Σ_{0}-preserving map which is the identity on τ̄ = κ^{+M̄} and such that σ(τ̄) = τ and σ(pM̄) = d_{N};

c) μ < κ. Then M̄ = N̄(μ, pM̄) where N̄ is the collapsing level for τ̄. Proof. The proof is virtually the same as that of the previous lemma.

⊓ ⊔(Lemma 2.20)

Strong Divisors. The construction of a □_{κ}-sequence in L is based on the fact that to every local successor one can assign a uniquely determined collapsing structure, namely the collapsing level, and that this assignment is preserved under interpolation arguments. The circumstances in L[E] are complicated by the fact that premousehood of pluripotent L[E]-levels is not preserved under such arguments. More preciely, such arguments give rise to collapsing protomice. One way of dealing with this issue is incorporating protomice in the construction. This means that to every local successor we have to decide whether the collapsing structure used in the construction will be an L[E]-level of some protomouse associated with it. As

CHARACTERIZATION OF □_{κ} IN CORE MODELS 53

there can be a large collection of protomice associated with the same collapsing level, have to find a canonical way of choosing such a protomouse.

Given a fixed q, elementary properties of Skolem hulls imply that the set

𝒟_{q} = 𝒟_{q}(N) = {μ < κ; (μ, q) is a divisor of N}

is closed in κ and λ(μ_{1}, q) ≥ λ(μ_{2}, q) whenever μ_{1} < μ_{2}. Thus, one might attempt to choose the divisor with the shortest possible q and largest possible μ, and show that such divisors are preserved in interpolation arguments. This works in some situations, as Lemma 2.15 enables us to express, uniformly over N(μ, q), that there are no divisors (μ′, q′) ≠ (μ, q) with μ ≤ μ′ and q′ a bottom segment of q. In fact, one can give a proof of □_{κ} in Jensen extender models below a measurable Woodin cardinal based on this choice of divisor [45]. The smallness condition is used to rule out the possibility that too many L[E]-levels will have a divisor (μ′, q′) “overlapping” the chosen (μ, q) in the sense that q′ is a bottom segment of q and μ′ < μ. Notice that Lemma 2.15 will not help here. For the choice of a canonical divisor that avoids the use of any unnecessary smallness condition we need a more sophisticated tool. The following is an elaboration on a notion from [25]. Definition. A divisor (μ, q) of N is strong iff for every ξ < μ and every x of the form h̃_{N}^{n+1}(ξ, p_{N}) we have x ∩ μ ∈ N^{∗}(μ, q). If N is pluripotent, we define the notion of strong divisor in the same way, but with h_{N}^{∗} and d_{N} in place of h̃_{N}^{n+1} and p_{N}, respectively.

By acceptability, (μ, q) is strong iff x ∩ μ ∈ J_{ϑ(μ,q)}^{E} for every x as above. Equivalently,

(13)  (μ, q) is strong iff 𝒫(μ) ∩ N^{∗}(μ, q) = 𝒫(μ) ∩ N′(μ)

where N′(μ) is the transitive collapse associated with h̃_{N}^{n+1}(μ ∪ {p_{N}}). If N is pluripotent, we define N′(μ) in the same way, but with h_{N}^{∗} and d_{N} in place of h̃_{N}^{n+1} and p_{N}, respectively. Notice also that E^{N′} ↾ μ^{+N′} = E ↾ μ^{+N′} by the proof of (5).

Translating facts about fine structural parameters between N and N(μ, q) requires that μ < κ. In particular, it is not clear how to translate facts concerning the soudness and standard parameters if μ = κ. For this reason, all lemmata in the previous subsection require the assumption μ < κ. The next lemma tells us that this assumption is automatically satisfied if (μ, q) is a strong divisor.

54 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Lemma 2.21. Suppose (κ, q) is a divisor. Then (κ, q) is not strong. Proof. By Lemmata 2.3 and 2.6, N^{∗}(μ, q) is a proper initial segment of N projecting to κ. Thus, there is a subset of κ in N which is not in N^{∗}(μ, q). By the soundness, resp. Dodd soundness of N we have N′(μ) = N, so (μ, q) cannot be strong by (13). ⊓ ⊔(Lemma 2.21)

The next couple of lemmata will enable us to prove preservation of strong divisors under maps with weak preservation properties that arise in interpolation arguments. The first of them provides us with a characterization of strong divisors. Lemma 2.22. Let (μ, q) be a divisor of N. If N is pluripotent, assume moreover that λ_{N}(μ, q) < λ_{N}. The following are equivalent:

a) (μ, q) is strong;

b) N^{∗}(μ, q) = core(N′(μ));

c) |p_{N′(μ)}| = |p_{N^{∗}(μ,q)}| = |r| (recall r = p_{N} − q). Proof. If μ = κ then a) – c) are obviously false, so we can assume w.l.o.g. that μ < κ. Let N^{∗} = N^{∗}(μ, q) and N′ = N′(μ). Also, let π′ : N′ → N be the associated uncollapsing map and π^{∗} = π′^{−1}∘π : N^{∗} → N′. Both π′ and π^{∗} are Σ_{0}^{(n)}-preserving and cofinal, and N^{∗} and N′ have the same (n + 1)-st projectum μ. The map π′ is sufficiently preserving to guarantee that N′ is a premouse; if N is pluripotent then γ_{N} is in the range of π by Lemma 2.4. By the condensation lemma, N′ is solid and its standard parameter is universal.

Setting p′ = π^{∗}(p_{N^{∗}}), the parameter p′ is a top segment of p_{N′}. More precisely,

(14)  p′ = p_{N′} − min(p′).

This follows from Lemma 1.1; just observe that N′ = h̃_{N′}^{n+1}(min(p′)∪{p′}) and that for every α ∈ p_{N^{∗}}, the structure π^{∗}(W_{N^{∗}}^{α}) is a generalized witness for π^{∗}(α) with respect to N and p′.

To see that a) implies b), notice first that p′ ∈ P_{N′}^{n+1}. This follows by the standard argument: Pick an A that is Σ_{1}^{(n)}(N^{∗}) in p_{N^{∗}} and such that A ∩ μ ∉ N^{∗}. Letting A′ be Σ_{1}^{(n)}(N′) in the parameter p′ by the same definition, we have A′ ∩ μ = A ∩ μ, so A′ ∩ μ ∉ N′ by (13). Hence p′ = p_{N′} by (14) and the ≤^{∗}-minimality of p_{N′}.

Clause c) is an immediate consequence of b), so it remains to derive a) from c). By (14) we know that p_{N′} is a lengthening of p′; clause then c) implies that they

CHARACTERIZATION OF □_{κ} IN CORE MODELS 55

actually agree. So N^{∗} is the transitive collapse of h_{N′}^{n+1}(μ ∪ {p_{N′}}) and a) follows from the universality of p_{N′} and (13). ⊓ ⊔(Lemma 2.22)

Again, we will need the version of the previous lemma for pluripotent N with λ_{N}(μ, q) = λ_{N}. As we already know, this is possible only if q = d_{N}. Notice also that μ must be a cutpoint of E_{top}^{N}, so N must be of type B. Lemma 2.23. Assume N is pluripotent and (μ, d_{N}) is a divisor of N such that λ_{N}(μ, d_{N}) = λ_{N}, the following are equivalent:

a) (μ, d_{N}) is strong;

b) E_{top}^{N′(μ)} | μ ∉ N′(μ).

Proof. Let γ̄ be such that Eγ̄ = E_{top}^{N} | μ and let N^{∗} = N^{∗}(μ, d_{N}). Then Eγ̄ = E_{top}^{N^{∗}} = E_{top}^{N′(μ)} | μ. Recall also that N′(μ) agrees with N up to μ^{+N′(μ)} and that N^{∗}, N′(μ) and N all agree up to γ̄. More precisely, E^{N^{∗}} ↾ γ̄ = E^{N′(μ)} ↾ γ̄ = E^{N} ↾ γ̄.

Since γ̄ = ht(N^{∗}), the agreement between N^{∗} and N′(μ) together with (13) guarantee that (μ, d_{N}) is strong just in case that γ̄ is the cardinal successor of μ in N′(μ). If γ̄ = μ^{+N′(μ)} then E_{top}^{N′(μ)} | μ cannot be an element of N′(μ), as it collapses γ̄. If γ̄ ≠ μ^{+N′(μ)} then Eγ̄ = EN′(μ) ; γ̄ ∈ N′(μ) by the agreement between N′(μ) and N. ⊓ ⊔(Lemma 2.23)

Notice also that in the situation from the previous lemma, ⟨⟨J E ; γ̄, Eγ̄⟩, ∅⟩ is the standard witness for μ with respect to N′(μ) and ∅. This terminology is consistent with that introduced at the beginning of the subsection on fine structure for protomice. We will make use of this fact in the proof of Lemma 3.12.

The strongness of a divisor (μ, q) can also be characterized over the associated protomouse N(μ, q); this fact will play an important role in our main construction. Definition. Let M be a coherent structure with the top extender F and μ = cr(F). We say that an ordinal ϑ ≤ ϑ(M) is closed in M relative to p ∈ [λ_{M}]^{<ω} just in case that F (f)(p, ξ) ∩ μ ∈ J_{ϑ}^{E^{M}} for every f : μ → 𝒫(μ) from J_{ϑ}^{E^{M}} and every ξ < μ.

If M is a protomouse, we say that ϑ ≤ ϑ(M) is closed in M iff ϑ is closed in M relative to p_{M}.

If M is a pluripotent L[E]-level, we say that ϑ ≤ ϑ(M) is closed in M iff ϑ is closed in M relative to d_{M}.

56 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Notice that if ϑ ≤ ϑ(M) is a limit of ordinals that are closed in M relative to q then ϑ itself is closed in M relative to q. Thus, the set of all ϑ ≤ ϑ(M) which are closed in M relative to q is closed. Notice also that if M is a pluripotent L[E]-level then ϑ(M) is trivially closed in M. Lemma 2.24. Let (μ, q) be a divisor of N. Then

ϑ(μ, q) is closed in N(μ, q) iff (μ, q) is a strong divisor of N.

Proof. Given a divisor (μ, q) of N, Lemma 2.13 guarantees that for each x ⊂ λ we have x ∈ h̃_{N}^{n+1}(μ ∪ {p_{N}}) (resp. x ∈ h_{N}^{∗}(μ ∪ {d_{N}}) whenever N is pluripotent with λ_{N}(μ, q) = λ_{N}) just in case that x is of the form F (f)(q, ξ) for some ξ < μ and f : μ → 𝒫(μ) from dom(F); here F = F_{N}(μ, q). So (μ, q) is strong iff x ∩ μ ∈ N^{∗}(μ, q) for each such x which, in turn is equivalent to the requirement that F (f)(q, ξ) ∩ μ ∈ J_{ϑ(μ,q)}^{E} for each f and ξ as above. ⊓ ⊔(Lemma 2.24)

For a fixed q, we define

𝒟_{q}^{∗} = 𝒟_{q}^{∗}(N) = {μ < κ; (μ, q) is a strong divisor of N}.

Lemma 2.25. 𝒟_{q}^{∗} is closed and bounded in κ. Proof. It suffices to prove that 𝒟_{q}^{∗} is closed; its boundedness then follows immediately from Lemma 2.21. Given a limit point μ of 𝒟_{q}^{∗}, the pair (μ, q) is clearly a divisor of N. Suppose for a contradiction that (μ, q) is not strong. As usual, the proof splits into two cases, depending on whether N is pluripotent and λ_{N} = λ_{N}(μ, q), or not.

Let us first focus on the case where N is either not pluripotent or else λ_{N}(μ, q) < λ_{N}. Let π = π_{N}(μ, q), π′ : N′(μ) → N be the uncollapsing embedding associated with N′(μ) and π^{∗} = (π′)^{−1} ∘ π. Let further r′ and p′ be the π′-preimage of r and p_{N}, respectively. Then both N^{∗}(μ, q) and N′(μ) are premice; this follows from Lemma 2.4 for pluripotent N of type B. Also, γ_{N} is in the ranges of both π and π′ in this case. As in the proof of Lemma 2.22 we observe that p_{N′(μ)} is a lengthening of r′.

Granting that (μ, q) is not strong, p_{N′(μ)} is a proper lengthening of r′. Here we use the previous lemma. Let α = max(p_{N′(μ)} − r′). As N′(μ) is solid (this follows from the condensation lemma), W ∈ N′(μ) where W is the standard solidity witness for

CHARACTERIZATION OF □_{κ} IN CORE MODELS 57

α with respect to N′(μ) and p_{N′(μ)}. Let r′_{α} be the preimage of r′ under the canonical witness map σ′_{α} : W → N′(μ). Pick ξ < μ such that ⟨α, W, r′_{α}⟩ = h̃_{N′(μ)}^{n+1}(ξ, p′); this is possible since p′ ∈ R_{N′(μ)}^{n+1}. Pick further a strong divisor (μ̄, q) for N such that ξ < μ̄ < μ. Let π̄′ : N′(μ̄) → N be the uncollapsing map associated with N′(μ̄) and p̄′ = (π̄′)^{−1}(p_{N}). Notice that σ =^{def} (π′)^{−1} ∘ π̄′ is a Σ_{1}^{(n)}-preserving embedding of N′(μ̄) into N′(μ) which sends p̄′ to p′. By our choice of μ̄, the range of σ contains α, W as well as r′_{α}. Let φ(x_{1}, ⋯, x_{ℓ}) be a Σ_{1}^{(n)}-formula. Since W is the standard solidity witness for α with respect to N′(μ) and p_{N′(μ)}, the premouse N′(μ) satisfies the Π_{2}^{(n)}-statement

(∀ξ_{1} ⋯ ξ_{ℓ} < α)(φ(ξ_{1} ⋯ ξ_{ℓ}, r′) ⟷ W ⊧ φ(ξ_{1} ⋯ ξ_{ℓ}, r′_{α})).

Since Π_{2}^{(n)}-statements are downward preserved under σ, the same is true of ᾱ, r̄′, Q̄ and r̄′_{α} in N′(μ̄) where ᾱ, Q̄ and r̄′ ; ᾱ is the σ-preimage of α, W and p′_{α}, respectively. Thus, if A is any set of ordinals which is Σ_{1}^{(n)}(N′(μ̄))-definable in the parameter r̄′ then A ∩ μ̄, being Σ_{1}^{(n)}(Q̄)-definable in r̄′_{α}, is an element of N′(μ̄). It follows that r̄′ ≠ p_{N′(μ̄)}. By Lemma 2.22, (μ̄, q) cannot be strong after all, a contradiction.

Now consider the case where N is pluripotent and λ_{N}(μ, q) = λ_{N}. Notice that λ_{N}(μ̄, d_{N}) = λ_{N} whenever (μ̄, d_{N}) is a divisor of N with μ̄ ≤ μ. Assuming that (μ, d_{N}) is not strong, E_{top}^{N′(μ)} | μ = E_{γ}^{N′(μ)} for a suitable γ. Here we simply apply Lemma 2.23. Let (γ′, μ′) = π′(γ, μ) where π′ : N′(μ) → N is the uncollapsing map associated with N′(μ). Then E_{top}^{N} | μ′ = E_{γ′} and γ = h_{N}^{∗}(ξ, d_{N}) for some ξ < μ. Pick a strong divisor (μ̄, d_{N}) such that ξ < μ̄ < μ. Then both γ′ and μ′ are in the range of π̄′ : N′(μ̄) → N, the uncollapsing map associated with N′(μ̄). Since π̄′ is the identity on μ′, necessarily μ′ = π̄′(μ̂) for some μ̂ ≥ μ̄. So E_{top}^{N′(μ̄)} | μ̂ = EN′(μ̄) ; γ̂ where π̄′(γ̂) = γ′ and, consequently, E_{top}^{N′(μ̄)} | μ̄ ∈ N′(μ̄). Again by Lemma 2.23, (μ̄, d_{N}) cannot be strong, which yields the desired contradiction. ⊓ ⊔(Lemma 2.25)

The next lemma rules out that a strong divisor can be overlapped by any other divisor, and thus solves the issue of overlapping discussed in the introduction to this subsection. Lemma 2.26. Let (μ, q) be a strong divisor of N and q̄ be a proper bottom segment of q. Then there is no μ̄ ≤ μ such that (μ̄, q̄) is a divisor of N.

58 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Proof. Suppose the contrary; let this be witnessed by (μ̄, q̄). Let r̄ = p_{N} − q̄; clearly r̄ is a proper lengthening of r and α = max(q) is an element of r̄− q̄. If N is pluripotent and λ_{N}(μ, q) = λ_{N}, then γ_{N} is in the range of π_{N}(μ̄, q̄) by Lemma 2.4, so it must also be in the larger rng(π′) where π′ : N′(μ) → N is the associated map. It follows that N′(μ) is a premouse and, consequently, E_{top}^{N′(μ)} | μ ∈ N′(μ). By Lemma 2.23, this contradicts the strongness of (μ, q).

Let us now focus on the remaining case where N is either not pluripotent or else λ_{N}(μ, q) < λ_{N}. As in the proofs of the previous lemmata we observe that h̃_{N}^{n+1}(μ̄ ∪ {r̄}) = rng(π_{N}(μ̄, q̄)) contains a generalized witness ⟨Q, t⟩ for α with respect to N and p_{N}, so ⟨Q, t⟩ must be in the range of the larger embedding π′ : N′(μ) → N. Notice that ⟨Q, t⟩ is a generalized solidity witness for α with respect to N and r = p_{N} −q. Then ⟨Q′, t′⟩ =^{def} (π′)^{−1}(⟨Q, t⟩) is a generalized witness for (π′)^{−1}(α) ≥ μ with respect to N′(μ) and r′ =^{def} (π′)^{−1}(r). As in the proof of the previous lemma we conclude that p_{N′(μ)} must be a proper lengthening of r′. Again by Lemma 2.23, this contradicts the strongness of (μ, q). ⊓ ⊔(Lemma 2.26)

We are now ready to define the notion of canonical protomouse associated with N. By Lemma 2.25, each 𝒟_{q}^{∗}(N) has a largest element, provided that it is nonempty. The protomouse we are looking for is that associated with the shortest possible q and the maximal element of 𝒟_{q}^{∗}(N). The previous lemma implies that this divisor is in fact fully determined by the requirement that μ is largest possible: Indeed, if (μ, q) is a strong divisor with the largest possible μ then no divisor (μ′, q′) ≠ (μ, q) with q′ ⊃ q and μ′ ≥ μ can be strong. On the other hand, if q′ is a proper segment of q, then (μ′, q′) can only be a divisor if μ′ > μ, and none of such divisors can be strong by our choice of μ. We thus set:

(15)

q(N) ≃ the shortest q such that 𝒟_{q}^{∗}(N) ≠ ∅
μ(N) ≃ max(𝒟_{q}^{∗}(N)).

If N is pluripotent and does not admit strong divisors, i.e. (μ(N), q(N)) as in (15) is undefined, we set

(16)

(μ(N), q(N)) = (μ, d_{N}) where μ = cr(E_{top}^{N})
N(μ(N), q(N)) = N

CHARACTERIZATION OF □_{κ} IN CORE MODELS 59

In view of the remarks preceding Lemma 2.24, we can consider (μ, d_{N}) a strong divisor of N.

3. The Square Sequence

With the technical means developed in the previous sections, we are ready to begin with the construction of a □_{κ}-sequence. As it is typical for constructions of square sequences in fine structural models, we shall actually construct a socalled □′_{κ}-sequence indexed by ordinals from a certain c.u.b. subset of κ^{+}. Such a sequence can easily be turned into a □_{κ}-sequence in the usual sense using merely combinatorial manipulations (see [6]). Recall that we work in L[E]. Theorem 3.1. Let 𝒮 be a c.u.b. subset of κ^{+} such that all τ ∈ 𝒮 satisfy:

• κ is the largest cardinal in J_{τ}^{E}.

• J_{τ}^{E} is a fully elementary substructure of J_{κ^{+}}^{E}.

• E_{τ} = ∅. Then there is a sequence

𝒞 = ⟨C_{τ}; τ ∈ 𝒮⟩

satisfying the following requirements:

• C_{τ} ⊂ 𝒮 ∩ τ is closed.

• C_{τ} is unbounded in τ whenever τ is a limit point of 𝒮 and cf(τ) > ω.

• C_{τ} ∩ τ̄ = Cτ̄ whenever τ̄ ∈ C_{τ}; this property is called coherency.

• otp(C_{τ}) ≤ κ Moreover, each C_{τ} is uniformly definable over N_{τ} ∪{N_{τ} } where N_{τ} is the collapsing L[E]-level for τ.

The requirement that E_{τ} = ∅ holds on a c.u.b. set, or equivalently, that only nonstationarily many τ < κ^{+} can index an extender, constitutes a smallness condition on the extender sequence E, and at the same time an upper bound at which our methods break down. However, □_{κ} turns out to fail in L[E] if we move beyond this bound, so our methods are in fact optimal. We shall return to these matters in detail in the last subsection which summarizes the proof of the main theorem; for now just notice that if E_{τ} ≠ ∅ for stationarily many τ < κ^{+}, then E_{τ} is a superstrong extender with λ(E_{τ}) = κ.

60 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Defining the Square Sequence. This subsection is devoted to the notation, which is quite massive. We split the set 𝒮 into two disjoint parts 𝒮^{0} and 𝒮^{1} depending on whether we can imitate Jensen’s construction of square in L in the more general L[E]-context or not. It will turn out that a modification of the same construction that employs protomice in place of L[E]-levels will provide us with a square sequence on 𝒮^{1}.

To each τ ∈ 𝒮 we assign several auxiliary objects. Our notation builds on that developed in the previous section, recall also the introductory settings there.

• N_{τ} is the collapsing level for τ.

• n_{τ} = n(N_{τ}) is the unique n such that ωϱ_{N_{τ}}^{n+1} = κ < ωϱ_{N_{τ}}^{n}.

• p_{τ} = p_{N_{τ}}.

• If N_{τ} is pluripotent, then d_{τ} = d_{N_{τ}}.

• ϱ_{τ} = ϱ_{N_{τ}}^{n_{τ}} and ℋ_{τ} = H_{N_{τ}}^{n_{τ}} (that is, ℋ_{τ} = H^{N_{τ}} (ωϱ^{n_{τ}}) = |J_{ϱ^{nτ}}^{E} |).

• A_{τ} = A_{N_{τ}}^{n_{τ} ,p_{τ} ↾n_{τ}}.

• h̃_{τ} = h̃_{N_{τ}}^{n_{τ} +1} and h_{τ}^{♯} = h_{N_{τ}}^{n_{τ} ,p_{τ}}.

• If N_{τ} is pluripotent, h_{τ}^{∗} = h_{N_{τ}}^{∗}.

• For each k ∈ ω, let ψ̃_{k}(z, y, x, w) be a fixed Σ_{0}^{(k)}-formula in the language for premice such that

(∃z^{k})ψ̃_{k}(z^{k}, y^{0}, x^{k+1}, w^{0})

constitutes a functionally absolute Σ_{1}^{(k)}-definition for the Skolem function y = h̃_{Q}^{k+1}(x, w) in any acceptable J-structure Q for this language. Then

H̃_{τ} = {(z, y, x, w) ∈ H_{N_{τ}}^{n_{τ}} × |N_{τ} | × H_{N_{τ}}^{n_{τ} +1} × |N_{τ} |; N_{τ} ⊧ ψ̃_{n_{τ}} (z, y, x, w)}.

By our restrictions on τ, the object N_{τ} is always defined, being the longest initial segment of L[E] in which τ looks like a successor cardinal.

𝒮^{0} = 𝒮 − 𝒮^{1}
𝒮^{1} = {τ ∈ 𝒮; (μ(N_{τ}), q(N_{τ})) is defined};

in other words, 𝒮^{1} consists of all ordinals τ such that N_{τ} either admits a strong divisor or is a pluripotent L[E]-level.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 61

Before going further, recall the notation introduced at the end of the subsection on premice and protomice in the previous section. Recall also that if N_{τ} is pluripotent and does not admit strong divisors then N(cr(E_{top}^{N_{τ}}), d_{N}) = N_{τ}. For τ ∈ 𝒮^{1} we set:

• q_{τ} = q(N_{τ}), m_{τ} = |q_{τ} |, and μ_{τ} = μ(N_{τ}).

• d_{τ} = d_{N_{τ}} whenever N_{τ} is pluripotent.

• r_{τ} = p_{τ} − q_{τ} if N_{τ} is not pluripotent, and r_{τ} = d_{τ} − q_{τ} if N_{τ} is pluripotent.

• M_{τ} = N_{τ} (μ_{τ} , q_{τ}).

• λ_{τ} = λ_{N_{τ}} (μ_{τ} , q_{τ}), ν_{τ} = ν_{N_{τ}} (μ_{τ} , q_{τ}) and ϑ_{τ} = ϑ_{N_{τ}} (μ_{τ} , q_{τ}).

• h_{τ} = h_{M_{τ}} and if M_{τ} is a pluripotent L[E]-level, then h_{τ} = h_{M_{τ}}^{∗}.

• Let ψ(z, y, x, w) be fixed Σ_{0}-formula in the language for coherent structures such that (∃z)ψ(z, y, x, w) constitutes functionally absolute Σ_{1}-definition for the function y = h_{Q}(x, w) where Q is any acceptable J-structure for this language. Then

H_{τ} = {(z, y, x, w) ∈ |M_{τ} | × |M_{τ} | × H_{M_{τ}}^{1} × |M_{τ} |; M_{τ} ⊧ ψ(z, y, x, w)}.

We are now ready to give the first approximation to the sequence 𝒞. As we have already mentioned, we define 𝒞 in such a way that 𝒞 ↾ 𝒮^{i} will be a □′_{κ}-sequence on 𝒮^{i}, that is, C_{τ} ⊂ 𝒮^{i} for any τ ∈ 𝒮^{i} where i ∈ {0, 1}. Since 𝒮^{0} and 𝒮^{1} partition 𝒮, we immediately have that 𝒞 is a □′_{κ}-sequence on 𝒮. We shall treat the two cases τ ∈ 𝒮^{0} and τ ∈ 𝒮^{1} simultaneously. Let us now define the above mentioned approximations

ℬ = ⟨B_{τ}; τ ∈ 𝒮⟩ and ℬ^{∗} = ⟨B_{τ}^{∗}; τ ∈ 𝒮⟩.

Definition. Given τ ∈ 𝒮^{0}, B_{τ} is the set of all τ̄ ∈ 𝒮^{0} ∩ τ satifying:

• Nτ̄ is a premouse of the same type as N_{τ}.

• nτ̄ = n_{τ}.

• There is a map σ_{τ̄τ} : Nτ̄ → N_{τ} that is Σ_{0}^{(n_{τ})}-preserving with respect to the language for premice and such that

a) τ̄ = cr(σ_{τ̄τ}) and σ_{τ̄τ} (τ̄) = τ;

b) σ_{τ̄τ} (pτ̄) = p_{τ};

c) to each α ∈ p_{τ} there is a generalized witness Q_{τ} (α) for α with respect to N_{τ} and p_{τ} such that Q_{τ} (α) ∈ rng(σ_{τ̄τ}).

62 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Solidity witnesses in clause c) are, of course, computed with respect to the language for premice. The map σ_{τ̄τ} always has a critical point since, by the restrictions imposed on the elements of 𝒮, each N_{τ} is strictly longer than J_{τ}^{E}. Notice that σ_{τ̄τ} is uniquely determined; this follows from the soundness of Nτ̄. Given any x ∈ Nτ̄, there is a ξ < κ such that x = h̃τ̄(ξ, pτ̄); as Σ_{1}^{(n_{τ})}-statements are upward preserved under Σ_{0}^{(n_{τ})}-embeddings and Skolem functions h̃τ̄ and h̃_{τ} have functionally absolute Σ_{1}^{(n_{τ})}-definitions, σ(x) = h̃_{τ} (ξ, p_{τ}) for any map σ satisfying the requirements of the above definition. Notice also that clause c) in the above definition does not have any influence on the uniqueness of σ_{τ̄τ}, which will be important in the coming lemmata. One further crucial fact about σ_{τ̄τ} is that σ_{τ̄τ} is not Σ_{1}^{(n_{τ})}-preserving, hence

(17)  σ_{τ̄τ} is non-cofinal at the n_{τ} -th level.

Otherwise σ_{τ̄τ} would be Σ_{1}^{(n_{τ})}-preserving, so h̃τ̄(ξ, pτ̄) would be defined iff h̃_{τ} (ξ, p_{τ}) would. By the soundness of N_{τ}, we would have rng(σ_{τ̄τ}) = N_{τ}, and from this the obviously false conslusion Nτ̄ = N_{τ}. Finally we note that clause c) in the above definition will be used only once in the entire construction, namely in the proof that C_{τ} is closed, to make sure that certain direct limits are sound. The condition in c) cannot be strengthened in the sense that we would require standard solidity witnesses to be members of the corresponding ranges; this follows from the fact that we are forced to deal with embeddings with very weak preservation properties which typically do not map standard witnesses to standard witnesses (and similarly in the case of preimages). Thus, the requirement that standard witnesses are in the range of σ_{τ̄τ} would damage the coherency of our putative square sequences. Definition. Given τ ∈ 𝒮^{1}, B_{τ} is the set of all τ̄ ∈ 𝒮^{1} ∩ τ satisfying:

• (μτ̄, mτ̄) = (μ_{τ} , m_{τ}).

• There is a map σ_{τ̄τ} : Mτ̄ → M_{τ} that is Σ_{0}-preserving with respect to the language for coherent structures and such that

a) τ̄ = cr(σ_{τ̄τ}) and σ_{τ̄τ} (τ̄) = τ;

b) σ_{τ̄τ} (qτ̄) = q_{τ};

c) to each α ∈ q_{τ} there is a generalized witness Q_{τ} (α) for α with respect to M_{τ} and q_{τ} such that Q_{τ} (α) ∈ rng(σ_{τ̄τ}).

CHARACTERIZATION OF □_{κ} IN CORE MODELS 63

Clause c) is, of course, formulated with respect to the language for coherent structures; in particular, solidity witnesses are computed relative to this language. As before we observe that σ_{τ̄τ} is uniquely determined and clause c) in the above definition does not have any influence on its uniqueness. Again, σ_{τ̄τ} is not Σ_{1}- preserving. In particular,

(18)  σ_{τ̄τ} is non-cofinal.

That M_{τ} is strictly longer than J_{τ}^{E} follows from the fact that λ_{τ} > τ. So again we have τ̄ = cr(σ_{τ̄τ}).

From now on we shall work with a fixed τ. Set

• n = n_{τ}. Lemma 3.2. Let τ ∈ 𝒮^{i} for i ∈ {0, 1} and let τ^{∗} < τ̄ satisfy all requirements of the definition of B_{τ} except possibly clause c). Then rng(σ_{τ^{∗}τ}) ⊂ rng(σ_{τ̄τ}). Proof. Assume w.l.o.g. that τ ∈ 𝒮^{0}; the proof for τ ∈ 𝒮^{1} is similar (and, in fact, much simpler). The first step is to show

(19)  sup((σ_{τ^{∗}τ})′′ωϱ_{τ^{∗}}) < sup((σ_{τ̄τ})′′ωϱτ̄).

Suppose this is false. Pick a ξ < κ such that h̃τ̄(ξ, pτ̄) = τ^{∗}; this is witnessed by some z ∈ ℋτ̄ in the sense that H̃τ̄(z, τ^{∗}, ξ, pτ̄) holds. By applying σ_{τ̄τ} we obtain H̃_{τ} (σ_{τ̄τ} (z), τ^{∗}, ξ, p_{τ}). Choose a ζ̄ < ωϱτ̄ such that z ∈ SE ; ζ̄ where ζ = σ_{τ̄τ} (ζ̄). By the failure of (19), there is a ζ^{∗} < ωϱ_{τ^{∗}} such that ζ ≤ ζ′ =^{def} σ_{τ^{∗},τ} (ζ^{∗}). Then the statement (∃u^{n} ∈ S_{ζ′}^{E})(∃δ^{n} < τ)H̃_{τ} (u^{n}, δ^{n}, ξ, p_{τ}) holds in N_{τ} and, being a Σ_{0}^{(n)}- statement, can be pulled back by σ_{τ^{∗}τ}. It follows that τ̃ = h̃_{τ^{∗}}(ξ, p_{τ^{∗}}) is defined and σ_{τ^{∗}τ} (τ̃) = h̃τ̄(ξ, pτ̄) = τ^{∗}, which contradicts the fact that τ^{∗} = cr(σ_{τ^{∗}τ}). This proves (19).

With (19) at hand, the same argument as above, but with the roles of τ̄ and τ^{∗} swapped, yields the conclusion

(20)  h̃_{τ^{∗}}(ξ, p_{τ^{∗}}) is defined ⟶ h̃τ̄(ξ, pτ̄) is defined

whenever ξ < κ. It follows that σ_{τ^{∗}τ} (h̃_{τ^{∗}}(ξ, p_{τ^{∗}})) = h̃_{τ} (ξ, p_{τ}) = σ_{τ̄τ} (h̃τ̄)(ξ, pτ̄) whenever h̃_{τ^{∗}}(ξ, p_{τ^{∗}}) is defined. Since N_{τ^{∗}} is sound, this completes the proof of the lemma.

64 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Regarding the proof of (20), notice that this time we have to consider also those points in rng(σ_{τ^{∗}τ}) which are not elements of the n-th reduct. To make sure that “pulling back” in the above argument can be applied here, we need to know that the relation (∃x^{0})(x^{0} = h̃_{τ} (ξ, p_{τ})) is uniformly Σ_{1}^{(n)}, i.e. it can be expressed in the form (∃u^{n})H′_{τ} (u^{n}, ξ, p_{τ}) where H′_{τ} is uniformly Σ_{0}^{(n)}. This is a consequence of the fact that h̃_{τ} is a good Σ_{1}^{(n)}-function, so the substitution of h̃_{τ} for v^{0} in the relation defined by Σ_{1}^{(0)}-formula (∃x^{0})(x^{0} = v^{0}) yields the required result. To each ξ < κ, if z witnesses the left side of (20), i.e. if H′_{τ^{∗}}(z, ξ, p_{τ^{∗}}), then H′_{τ} (σ_{τ^{∗},τ} (z), ξ, p_{τ}) and we can bound σ_{τ^{∗},τ} (z) by some σ_{τ̄τ} (SE ; ζ̄) where ζ̄ < ωϱτ̄. Pulling back by σ_{τ̄τ} then yields (∃u^{n} ∈ SE ; ζ̄)H′ ; τ̄(u^{n}, ξ, pτ̄), and thus the right side of (20). ⊓ ⊔(Lemma 3.2)

Lemma 3.3. Let τ ∈ 𝒮^{i} for i ∈ {0, 1} and τ̄ ∈ B_{τ}. Then B_{τ} ∩ τ̄ = Bτ̄ − min(B_{τ}). Proof. Suppose w.l.o.g. that τ ∈ 𝒮^{0}. Pick a τ^{∗} ∈ B_{τ} ∩ τ̄. We first show that τ^{∗} ∈ Bτ̄. By the previous lemma, rng(σ_{τ^{∗}τ}) ⊂ rng(σ_{τ̄τ}), so we can define a map σ : N_{τ^{∗}} → Nτ̄ by σ = (σ_{τ̄τ})^{−1} ∘ σ_{τ^{∗}τ}. It is a routine to verify that σ satisfies all requirements imposed on σ_{τ^{∗}τ̄} except possibly clause c), which we verify now. Given ᾱ ∈ pτ̄, let α = σ_{τ̄τ} (ᾱ) and σ_{τ^{∗}τ̄}(α^{∗}) = ᾱ. The definition of B_{τ} guarantees that we have a generalized witness Q_{τ} (α) for α with respect to N_{τ} and p_{τ} in the range of σ_{τ^{∗}τ}, and we know that the σ_{τ̄,τ} -preimage Q̄(ᾱ) of Q_{τ} (α) is in the range of σ. But “Q is a generalited witness for α with respect to N and p” is a Π_{1}^{(n)}- statement, so it is downward preserved under Σ_{0}^{(n)}-maps. It follows that Q̄(ᾱ) is a generalized witness for ᾱ with respect to Nτ̄ and pτ̄. This proves that τ^{∗} ∈ Bτ̄ and thus the inclusion ⊂.

Let τ′ = min(B_{τ}). Pick a τ^{∗} ∈ Bτ̄ − τ′ that is larger than τ′. Define an embedding σ : N_{τ^{∗}} → N_{τ} by σ = σ_{τ̄τ} ∘ σ_{τ^{∗}τ̄}. Again, σ meets all requirements in the above definition except possibly clause c), which suffices to conclude that σ = σ_{τ^{∗}τ}. Regarding c), if Q(α) ∈ rng(σ_{τ′τ}) is a generalized witness for α ∈ p_{τ} with respect to N_{τ} and p_{τ}, then Q(α) is in the range of σ_{τ^{∗}τ} by the previous lemma, so τ^{∗} ∈ B_{τ}. This proves the inclusion ⊃. ⊓ ⊔(Lemma 3.3)

By the previous lemma, the sequence ℬ is almost coherent; the only deficiency of ℬ is that the initial segments of B_{τ} might grow as τ decreases. This can be fixed by adding all potential initial segments to each B_{τ}. For τ ∈ 𝒮 we set

CHARACTERIZATION OF □_{κ} IN CORE MODELS 65

• τ(0) = τ;
• τ(i + 1) ≃ min(B_{τ(i)});
• ℓ_{τ} = the least i such that B_{τ(i)} = ∅.

The number ℓ_{τ} is defined for every τ ∈ 𝒮, otherwise ⟨τ_{i}⟩_{i} would constitute an infinite decreasing sequence of ordinals. We are now ready to define a fully coherent sequence ℬ^{∗}. Given any τ ∈ 𝒮,

• B_{τ}^{∗} = B_{τ(0)} ∪ ⋯ ∪ B_{τ(ℓ_{τ} −1)}

• σ_{τ̄τ}^{∗} = σ_{τ(1)τ(0)} ∘⋯∘σ_{τ(j)τ(j−1)} ∘σ_{τ̄τ(j)} whenever τ̄ ∈ B_{τ}^{∗} and j is such that

τ̄ ∈ B_{τ(j)}.

Lemma 3.4. ℬ^{∗} is a coherent sequence.

Proof. Pick a τ ∈ 𝒮 and a τ̄ ∈ B_{τ}^{∗}. Assume w.l.o.g. that τ̄ > τ(ℓ_{τ} − 1) = min(B_{τ}^{∗}). We first observe

(21)  min(Bτ̄) ∈ B_{τ}^{∗} and Bτ̄ = B_{τ}^{∗} ∩ [min(Bτ̄), τ̄)

This follows from Lemma 3.3. Let j be such that τ̄ ∈ B_{τ(j)}. Then τ(j + 1) ∈ Bτ̄, and either τ(j + 1) = min(Bτ̄) or else Bτ̄ ∩ τ(j + 1) is an end-tail of B_{τ(j+1)} ⊂ B_{τ}^{∗}. This proves the first part of (21). To see the second part, we observe that Bτ̄ agrees with B_{τ(j)} on [τ(j + 1), τ̄) and Bτ̄ agrees with B_{τ(j+1)} on [min(Bτ̄), τ(j + 1)).

Define τ̄(i) from τ̄ the same way τ(i) was defined from τ. Let ℓ̄ = ℓτ̄. Using (21) we inductively show that B_{τ̄(i)} is a segment of B_{τ}^{∗} for all i < ℓ̄. It follows that B∗ ; τ̄ is a (not necessarily initial) segment of B_{τ}^{∗}. But B∗ ; τ̄ must be in fact an initial segment of B_{τ}^{∗}; otherwise τ̄(ℓ̄− 1) > τ(ℓ_{τ} − 1) which would mean that B_{τ̄(ℓ̄−1)} is nonempty. Contradiction. ⊓ ⊔(Lemma 3.4)

Since each σ_{τ̄τ}^{∗} is the unique Σ_{0}^{(n)}-preserving map from Nτ̄ to N_{τ} with critical point τ̄ sending pτ̄ to p_{τ}, Lemma 3.2 guarantees that rng(σ_{τ^{∗}τ}^{∗}) ⊂ rng(σ_{τ̄τ}^{∗}) whenever τ^{∗} < τ̄ are in 𝒮^{0}. On 𝒮^{1}, the situation is analogous. Thus, we can define σ_{τ^{∗}τ̄}^{∗} by σ_{τ^{∗}τ̄}^{∗} = (σ_{τ̄τ}^{∗})^{−1} ∘σ_{τ^{∗}τ}^{∗} for any τ^{∗} ≤ τ̄ from B_{τ}^{∗} ∪{τ}. It follows immediately that

(22) σ_{τ^{∗}τ̄}^{∗} : N_{τ^{∗}} → Nτ̄ is the unique map that is Σ_{0}^{(n)}-preserving with respect to the language for premice, has critical point τ^{∗}, and sends τ^{∗} to τ̄ and p_{τ^{∗}} to pτ̄ whenever τ ∈ 𝒮^{0} and τ^{∗} ≤ τ̄ are in B_{τ}^{∗} ∪ {τ} and σ_{τ^{∗}τ̄}^{∗} : M_{τ^{∗}} → Mτ̄ is the unique map that is Σ_{0}-preserving with respect to the language for coherent structures, has critical point τ^{∗}, and sends τ^{∗} to τ̄ and q_{τ^{∗}} to qτ̄ whenever τ ∈ 𝒮^{1} and τ^{∗} ≤ τ̄ are in B_{τ}^{∗} ∪ {τ}.

To complete the definition of the square sequence, we will make use of the following crucial lemma, whose proof will constitute the rest of this section. Lemma 3.5. For every τ ∈ 𝒮 of uncountable cofinality, B_{τ} is a c.u.b. subset of τ on a tail-end. In other words, there is a τ̄ < τ such that B_{τ} − τ̄ is closed and unbounded in τ.

To each τ ∈ 𝒮, let β_{τ} be the least β ∈ B_{τ}^{∗} ∪ {τ} such that B_{τ}^{∗} − β is closed in τ. The ordinal β_{τ} is always defined and if cf(τ) > ω, then β_{τ} < τ, as follows from the previous lemma and the fact that B_{τ} is a tail-end of B_{τ}^{∗}. Set

C_{τ}^{∗} = B_{τ}^{∗} − β_{τ}  and  𝒞^{∗} = ⟨C_{τ}^{∗}; τ ∈ 𝒮⟩

Given τ̄ ∈ C_{τ}^{∗}, we know that τ̄ ∈ B_{τ}^{∗}, τ̄ ≥ β_{τ} and that B_{τ}^{∗}, B∗ ; τ̄ cohere. It follows that βτ̄ = β_{τ}. Consequently, C∗ ; τ̄ = B∗ ; τ̄ − βτ̄ = B_{τ}^{∗} ∩ τ̄ − β_{τ} = C_{τ}^{∗} ∩ τ̄. The sequence 𝒞^{∗} thus satisfies all requirements of a □′_{κ}-sequence with the only exception that the sets C_{τ}^{∗} might have large order type.

We now observe that for τ ∈ 𝒮^{1}, the order type of C_{τ}^{∗} is always small. To each τ^{∗} < τ̄ from C_{τ}^{∗} we have the map σ_{τ^{∗}τ̄}^{∗} : M_{τ^{∗}} → Mτ̄ satisfying (22), so dom(F_{τ^{∗}}) ⊂ dom(Fτ̄) and this inclusion is strict, as σ_{τ^{∗}τ̄}^{∗} is non-cofinal. Hence ϑ_{τ^{∗}} < ϑτ̄. It follows that ϑτ̄ ↦ τ̄ is a strictly monotone enumeration of C_{τ}^{∗} with domain contained in ϑ_{τ}. But ϑ_{τ} ≤ μ^{+} ≤ κ since μ_{τ} < κ, so otp(C_{τ}^{∗}) ≤ otp(ϑ_{τ}) ≤ κ.

The above discussion shows that for τ ∈ 𝒮^{1}, our construction already yields a □′_{κ}-sequence. For τ ∈ 𝒮^{0} this is not obvious and to arrange that the order types are small, we will replace the sets C_{τ}^{∗} by suitably chosen subsets.

Let X_{τ} (ξ) be the Σ_{1}^{(n)}-hull of {ξ, p_{τ} } in N_{τ}. We define sequences ⟨τ_{ι}⟩, ⟨ξ_{ι}^{τ} ⟩ in the following way:

CHARACTERIZATION OF □_{κ} IN CORE MODELS 67

• τ_{0} = min(C_{τ}^{∗} ∪ {τ})
• ξ_{ι}^{τ} ≃ the least ξ < κ such that X_{τ} (ξ) is not contained in rng(σ_{τ_{ι}τ}^{∗})

• τ_{ι+1} = the least τ̄ ∈ C_{τ}^{∗} ∪ {τ} such that X_{τ} (ξ_{ι}^{τ}) is contained in rng(σ_{τ̄τ}^{∗})

• τ_{γ} = sup{τ_{ι}; ι < γ} for limit γ
• ι_{τ} = the least ι such that τ_{ι} = τ

If τ_{ι} < τ, then ξ_{ι}^{τ} is always defined; just choose a ξ < κ such that τ_{ι} = h̃_{τ} (ξ, p_{τ}) and observe that X_{τ} (ξ) is not contained in rng(σ_{τ_{ι}τ}^{∗}), as τ_{ι} = cr(σ_{τ_{ι}τ}^{∗}). Set

C′_{τ} = {τ_{ι}; ι < ι_{τ} }

Lemma 3.6. ⟨C′_{τ}; τ ∈ 𝒮^{0}⟩ is a □′_{κ}-sequence on 𝒮^{0}. Proof. Given ι < ι_{τ}, the above definition immediately yields that τ_{ι+1} > τ_{ι}. It follows that ⟨τ_{ι}; ι < ι_{τ} ⟩ is a normal sequence, hence C′_{τ} is closed. Furthermore, if τ is not ω-cofinal, C′_{τ} is unbounded since each X_{τ} (ξ_{ι}^{τ}) is countable and therefore contained in rng(σ_{τ̄τ}^{∗}) for sufficiently large τ̄ ∈ C_{τ}^{∗} (recall that C_{τ}^{∗} is c.u.b. in τ in this case). We next observe that if ῑ < ι, then X_{τ} (ξ_{ι}^{τ}) is not contained in rng(σ_{τῑτ}^{∗}), as rng(σ_{τῑτ}^{∗}) ⊂ rng(σ_{τ_{ι}τ}^{∗}). So ξ_{ι}^{τ} < ξτ ; ῑ would contradict the minimality of ξτ ; ῑ. Furthermore, since X_{τ} (ξτ ; ῑ) ⊂ rng(σ_{τ_{ῑ+1}τ}^{∗}) ⊂ rng(σ_{τ_{ι}τ}^{∗}), the ordinals ξ_{ι}^{τ} and ξτ ; ῑ must be distinct. This proves that ⟨ξ_{ι}^{τ}; ι < ι_{τ} ⟩ is a strictly increasing sequence of ordinals smaller than κ. As an immediate consequence we have ι_{τ} ≤ κ and that ι ↦ τ_{ι} is a strictly monotone enumeration of C′_{τ}. So otp(C′_{τ}) ≤ κ. It only remains to prove that the sequence ⟨C′_{τ}; τ ∈ 𝒮^{0}⟩ is coherent.

Pick a τ̄ ∈ C′_{τ}. Assume that τ̄ > min(C′_{τ}); otherwise there is nothing to prove. Since τ̄ ∈ C_{τ}^{∗}, we know that C∗ ; τ̄ = C_{τ}^{∗} ∩ τ̄. By induction on ι we show that τ̄_{ι} ≃ τ_{ι} whenever ι < ιτ̄. For ι = 0 this follows immediately and the same applies to limit ι. It remains to prove that τ̄_{ι+1} ≃ τ_{ι+1}, granted that this equality holds with ι in place of ι + 1. Here we utilize the following fact.

(23)  If X_{τ} (ξ) ⊂ rng(σ_{τ̄τ}^{∗}), then X_{τ} (ξ) = (σ_{τ̄τ}^{∗})′′Xτ̄(ξ).

The inclusion ⊃ in the conclusion of (23) follows immediately, as Σ_{1}^{(n)}-statements are upward preserved under σ_{τ̄,τ}^{∗}. Now suppose y ∈ X_{τ} (ξ). This means that there is an i ∈ ω and ζ < ωϱ_{τ} such that (∃u^{n} ∈ S_{ζ}^{E})H̃_{τ} (u^{n}, y, ⟨i, ξ⟩, p_{τ}); take ζ to be the

68 ERNEST SCHIMMERLING AND MARTIN ZEMAN

least such. Then ζ is uniquely characterized by the following Σ_{0}^{(n)}-statement (24)

(∃u^{n} ∈ S_{ζ}^{E})H̃_{τ} (u^{n}, y, ⟨i, ξ⟩, p_{τ}) & (∀v^{n} ∈ S_{ζ}^{E})(∀u^{n} ∈ v^{n})¬H̃_{τ} (u^{n}, y, ⟨i, ξ⟩, p_{τ}),

Since y = h̃_{τ} (⟨i, ξ⟩, p_{τ}) and h̃ is a good Σ_{1}^{(n)}-function, substituting h̃_{τ} (⟨i, ξ⟩, p_{τ}) for y in (24) yields that ζ is Σ_{1}^{(n)}-definable over N_{τ} from ξ and p_{τ}, so ζ ∈ X_{τ} (ξ). By our assumption that X_{τ} (ξ) ⊂ rng(σ_{τ̄,τ}^{∗}), there are ȳ, ζ̄ ∈ Nτ̄ such that y = σ_{τ̄τ}^{∗} (ȳ) and ζ = σ_{τ̄τ}^{∗} (ζ̄). Then (24) holds in Nτ̄ with τ̄, ζ̄, ȳ and pτ̄ in place of τ, ζ, y and p_{τ}; this witnesses that (∃u^{n})H̃τ̄(u^{n}, ȳ, ⟨i, ξ⟩, pτ̄), i.e. that ȳ = h̃τ̄(⟨i, ξ⟩, pτ̄) ∈ Xτ̄(ξ). This proves (23).

Now suppose τ_{ι} = τ̄_{ι} < τ̄. Recall that σ_{τ′τ}^{∗} = σ_{τ̄τ}^{∗} ∘ σ_{τ′τ̄}^{∗} for any τ′ < τ̄. By the easy part of (23), for any ξ < κ we have

X_{τ} (ξ) ⊂ rng(σ_{τ_{ι}τ}^{∗}) ⟶ Xτ̄(ξ) ⊂ rng(σ_{τ_{ι}τ̄}^{∗}).

It follows that ξτ̄ ; ι ≥ ξ_{ι}^{τ}. Since we are assuming that τ̄ ∈ C′_{τ} and τ_{ι} < τ̄, we have τ_{ι+1} ≤ τ̄, so X_{τ} (ξ_{ι}^{τ}) ⊂ rng(σ_{τ̄τ}^{∗}). Using the full strength of (23) we obtain

(25)  X_{τ} (ξ_{ι}^{τ}) = (σ_{τ̄τ}^{∗})′′Xτ̄(ξ_{ι}^{τ}),

so Xτ̄(ξ_{ι}^{τ}) ⊄ rng(σ_{τ̄_{ι},τ̄}^{∗}). It follows that ξτ̄ ; ι = ξ_{ι}^{τ}. Letting ξ_{ι} be this common value,

(25) guarantees that for every τ′ ∈ [τ̄_{ι}, τ̄] ∩ C_{τ}^{∗},

X_{τ} (ξ_{ι}) ⊂ rng(σ_{τ′τ}^{∗}) ⟷ Xτ̄(ξ_{ι}) ⊂ rng(σ_{τ′τ̄}^{∗}),

which in turn implies that τ̄_{ι+1} = τ_{ι+1}. ⊓ ⊔(Lemma 3.6)

It is now obvious that if we define 𝒞 = ⟨C_{τ}; τ ∈ 𝒮⟩ by

C_{τ} = \{ \begin{matrix}C′_{τ} & if τ ∈ 𝒮^{0} \\ C_{τ}^{∗} & if τ ∈ 𝒮^{1}, \end{matrix}

then 𝒞 is a □′_{κ}-sequence on 𝒮. To complete the construction, we have to give the proof of Lemma 3.5. The rest of this section is devoted to this task.

When τ ∈ 𝒮^{0}. Let τ ∈ 𝒮^{0} be a limit point of 𝒮 with uncountable cofinality. We first define an approximation D to B_{τ}. The set D is the set of all τ̄ ∈ 𝒮∩τ satifying:

• Nτ̄ is a premouse of the same type as N_{τ}.

• nτ̄ = n_{τ}.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 69

• There is a map σ_{τ̄τ} : Nτ̄ → N_{τ} which is Σ_{0}^{(n_{τ})}-preserving with respect to the language for premice and such that

a) τ̄ = cr(σ_{τ̄τ}) and σ_{τ̄τ} (τ̄) = τ;

b) σ_{τ̄τ} (pτ̄) = p_{τ};

c) to each α ∈ p_{τ} there is a generalized witness Q_{τ} (α) for α with respect

to N_{τ} and p_{τ} such that Q_{τ} (α) ∈ rng(σ_{τ̄τ}).

Generalized witnesses in clause c) are, of course, computed in the language for premice. The only difference between D and B_{τ} is that we also allow ordinals from 𝒮^{1} to be elements of D. Later we prove that there are only boundedly many such ordinals in τ. Obviously, B_{τ} ⊂ D. Lemma 3.7. D is unbounded in τ. Proof. Given a τ′ < τ, we shall find a τ̃ ≥ τ′ in D. Form the elementary hull of {N_{τ} , τ′, 𝒮} in J_{κ^{++}}^{E}. Let H be the transitive collapse of this hull and let σ_{0} : H → J_{κ^{++}}^{E} be the associated uncollapsing map. Notice that both κ and κ^{+} are in rng(σ_{0}). We set:

• N̄, κ̄, τ̄, 𝒮̄ = σ_{0}^{−1}(N_{τ} , κ, τ, 𝒮);

• σ = σ_{0} ↾ N̄ : N̄ → N_{τ};
• τ̃ = sup(σ′′τ̄).

As 𝒮 is a c.u.b. subset of τ, its σ_{0}-preimage 𝒮̄ is c.u.b. in τ̄. It follows that σ′′𝒮̄ is cofinal in τ̃, so τ̃ is a limit point of 𝒮. Thus, τ̃ ∈ 𝒮. Notice also that τ̃ < τ, as rng(σ) is countable, and that τ′ < τ̃, as τ′ ∈ rng(σ). Our aim is to show that τ̃ ∈ D.

Since N_{τ} is in the range of σ_{0}, all first order properties of N_{τ} are downward preserved under σ_{0}. In particular, N̄ is premouse of the same type as N_{τ}. Recall that N_{τ} is not pluripotent, as τ ∈ 𝒮^{0} and (μ(N_{τ}), q(N_{τ})) is always defined for pluripotent N_{τ}. Thus, either cr(EN̄ ; top) ≥ κ̄ or else ωϱ1 ; N̄ > κ̄. Working in the language for premice, the following is standard to verify:

• τ̄ = κ̄^{+N̄};

• ωϱω ; N̄ = ωϱn+1 ; N̄ = κ̄ < ωϱn ; N̄ where n = n_{τ};

• σ(pN̄) = p_{τ};

• N̄ is sound and solid;

• σ(W ᾱ,pN̄ ; N̄) = W_{N_{τ}}^{α,p_{τ}} whenever ᾱ ∈ pN̄ and α = σ(ᾱ).

70 ERNEST SCHIMMERLING AND MARTIN ZEMAN

By the interpolation lemma (Lemma 1.2), the canonical extension σ̃ : N̄ → Ñ of σ ↾ J EN̄ ; τ̄ : J EN̄ ; τ̄ → J E ; τ̃ exists, and is Σ_{0}^{(n)}-preserving and cofinal. Also, there is a Σ_{0}^{(n)}-preserving embedding σ′ : Ñ → N_{τ} satisfying σ′ ↾ τ̃ = id, σ′(τ̃) = τ and σ′ ∘ σ̃ = σ. Notice also that τ̃ = κ^{+Ñ} = σ̃(τ̄). Our aim is to show that Ñ = Nτ̃, nτ̃ = n and σ′ = σ_{τ̃τ}, which will prove the lemma. At this point we are only able to state these preservation properties with respect to the language for coherent structures, since it is not clear that Ñ is a premouse of the same type as N_{τ} and N̄, and that the constant sympbol γ̇ is interpreted in Ñ in the correct way.

We would like to apply the condensation lemma to the embedding σ′ : Ñ → N_{τ}, so let us verify that this is possible. We first show that Ñ is a premouse of the same type as N̄ and N_{τ}. This will also take care of the first clause in the definition of D. Assume that N_{τ} is active, as otherwise there is nothing to prove. To see that Ñ is a potential premouse, we have to check the weak amenability of the top extender, as the rest is automatically preserved. Notice that either n > 0, in which case σ̃ is Σ_{2}-preserving, or else n = 0, in which case σ̃ is Σ_{0}-preserving and cofinal and, being a coarse pseudoultrapower embedding, maps successor cardinals of N̄ cofinally into their images. In the former case, the potential premousehood of N̄ is automatically upward preserved under σ. In the latter case we have μ̄ =^{def} cr(EN̄ ; top) ≥ κ̄ (recall that this follows from our assumption that N_{τ} is not pluripotent), so ϑ̄ =^{def} μ̄^{+N̄} is mapped cofinally into its image (σ̃(μ̄))^{+Ñ}. It follows that EÑ ; top measures all subset of cr(EÑ ; top) in Ñ. Now if N̄ is of type A or B then Ñ is of the same type by the preservation properties of σ̃ and Lemma 1.5. If Ñ is of type C then n > 0, again by our assumption that N_{τ} is not pluripotent. Then either n > 1, in which case σ̃ is Σ_{2}^{(1)}-preserving, or else n = 1, in which case σ̃ is Σ_{0}^{(1)}-preserving and cofinal, and so Q^{(1)}-preserving. In either case, Ñ is a type C premouse by b) of the same lemma. It follows that the preservation properties of the maps σ̃ and σ′ hold with respect to the language for premice.

Form now on work in the language for premice. As a next step, we have to verify that the fine structural requirements are met. More precisely,

ωϱω ; Ñ = ωϱn+1 ; Ñ ≤ κ and Ñ is sound.

Let p̃ = σ̃(pN̄). By the properties of pseudoultrapowers, every a ∈ Ñ is of the form σ̃(f)(ξ) where ξ < κ and f is a good Σ_{1}^{(n−1)}(N̄)-function in some q̄ ∈ N̄. Fix a

CHARACTERIZATION OF □_{κ} IN CORE MODELS 71

functionally absolute Σ_{1}^{(n−1)}-definition φ(u, v, z) for f, i.e. φ is such that y = f(x) iff N̄ ⊧ φ(x, q̄, y). Setting q̃ = σ̃(q̄), φ(x, q̃, y) defines σ̃(f) over Ñ. Pick an η < κ̄ such that q̄ = h̃n+1 ; N̄(η, pN̄); this is possible, as N̄ is sound and ωϱn+1 ; N̄ = κ̄. From the fact that this identity is upward preserved under σ̃ and that substituing h̃n+1 ; N̄ into φ results in a Σ_{1}^{(n)}-statement (recall that h̃n+1 ; N̄ is a good Σ_{1}^{(n)}(N̄)-function) we infer that a is the unique object z satisfying

Ñ ⊧ φ(ξ, h̃n+1 ; Ñ(σ̃(η), p̃, z),

so a is Σ_{1}^{(n)}(Ñ)-definable in the parameter p̃ and ordinals ξ, σ̃(η) < κ. This proves that h̃n+1 ; Ñ(κ ∪ {p̃}) = Ñ. As an immediate consequence we have ωϱn+1 ; Ñ ≤ κ. In fact, ωϱn+1 ; Ñ = κ since κ is a cardinal in L[E] and our construction takes place there. Thus, p̃ ∈ Rn+1 ; Ñ. To see that Ñ is sound, it suffices to prove that p̃ = pÑ. By our construction, σ′(p̃) = p_{τ} and W_{N_{τ}}^{α,p_{τ}} ∈ rng(σ) ⊂ rng(σ′) whenever α ∈ p_{τ}, so for every α̃ ∈ p̃, W_{N_{τ}}^{α,p_{τ}} ∈ rng(σ′) is a generalized witness for α = σ′(α̃) with respect to N_{τ} and p_{τ}. Recall that the property of being such a witness is Π_{1}^{(n)} whenever α is not smaller than the (n + 1)-st projectum, and therefore is downward preserved under σ′. So σ′^{−1}(W_{N_{τ}}^{α,p_{τ}}) is a generalized witness for α̃ with respect to Ñ and p̃ in Ñ whenever α̃ ∈ p̃. As p̃ ∈ P ∗ ; Ñ = P n+1 ; Ñ, we have p̃ = pÑ. This completes the proof of the fact that Ñ is sound. Moreover, we have shown that σ′(p̃) = p_{τ}.

Now apply the condensation lemma to σ′ : Ñ → N_{τ}. Clause a) is impossible, as κ^{+Ñ} = τ̃ < τ = κ^{+N_{τ}}. Clause c) is false, as it would imply that Ñ is not sound. Finally, d) is not the case, as Eτ̃ = ∅. It follows that Ñ is a proper initial segment of N_{τ}, and thus of L[E]. Since τ̃ = κ^{+Ñ} and Ñ projects to κ, Ñ is the collapsing level for τ̃ in L[E], i.e. Ñ = Nτ̃. That nτ̃ = n is clear from the discussion in the previous paragraph. Also, σ′ = σ_{τ̃τ}, as σ′ ↾ κ = id and σ′(pτ̃) = p_{τ} and σ′ is fully determined by these two properties. To see that τ̃ is in D, it suffices to show that σ′ satisfies clause c) in the definition of D. But this also follows immediately from the previous paragraph. ⊓ ⊔(Lemma 3.7)

Lemma 3.8. D is closed in τ. Proof. Let τ̃ be a limit point of D. So τ̃ ∈ 𝒮, as 𝒮 is closed. To see that τ̃ has the required properties, we shall use the properties of direct limits developed in the fine structure subsection in the preliminaries. Form the direct limit ⟨Ñ, σ_{τ̄τ̃}; τ̄ ∈ D ∩ τ̃⟩

72 ERNEST SCHIMMERLING AND MARTIN ZEMAN

of the diagram ⟨Nτ̄, σ_{τ^{∗}τ̄}; τ^{∗} ≤ τ̄ & τ^{∗}, τ̄ ∈ D∩τ̃⟩. This direct limit is well-founded, as there is a Σ_{0}-preserving embedding σ : Ñ → N_{τ} defined by σ : σ_{τ̄τ̃}(x) ↦ σ_{τ̄τ} (x). From now on consider Ñ to be transitive. Notice that σ ∘ σ_{τ̄τ̃} = σ_{τ̄τ}. For ξ < τ̃ we have σ_{τ̃τ} (ξ) = σ_{τ̄τ} (ξ) = ξ where τ̄ is such that ξ < τ̄ < τ̃, so σ_{τ̃τ} ↾ τ̃ = id. Also, the thread ⟨τ̄; τ̄ ∈ D ∩ τ̃⟩ clearly represents τ̃ in Ñ, so τ̃ = σ_{τ̄τ̃}(τ̄) and σ_{τ̃τ} (τ̃) = τ. It follows that τ̃ = κ^{+Ñ} and τ̃ = cr(σ_{τ̃τ}). By the discussion of direct limits at the end of the fine structure subsection in the preliminaries, the maps σ_{τ̄τ̃} are in fact Σ_{0}^{(n)}-preserving where n = n_{τ}. As in the previous lemma, these preservation properties hold with respect to the language for coherent structures, as it is not clear that Ñ is a premouse of the same type as N_{τ} and the constant γ̇ is correctly interpreted in Ñ. Our aim is to show that Ñ = Nτ̃, and again we intend to use the condensation lemma. Thus, we have to show that the asuumptions are met.

The first step towards this is the verification that Ñ is a premouse of the same type as N_{τ}. To see that Ñ is a potential premouse, recall that Π_{2}-properties which hold on a tail-end are upward preserved under direct limit maps. We know that each N_{τ_{ι}} is of the same type as N_{τ}. If they are of type A, then so is Ñ, as the statement “(∀λ̄ < λ_{N})(λ̄ is not a cutpoint of E_{top}^{N})” is Π_{2}(N) for any N. If N_{τ} is of type B, then σ_{τ^{∗}τ̄}(γ_{N_{τ^{∗}}}) = γ_{Nτ̄}, so σ_{τ^{∗}τ̄}(λ_{N_{τ^{∗}}}^{∗}) = λ_{Nτ̄}^{∗}, as λ_{N}^{∗} is the largest cardinal in J_{γ_{N}}^{E^{N}} for any N. Set (γ̃, λ̃^{∗}) = σ_{τ̄τ̃}(γ_{Nτ̄}, λ_{Nτ̄}^{∗}); the preservation properties of the direct limit maps then guarantee that λ̃^{∗} is a cutpoint of EÑ ; top and EÑ ; top ↾ λ̃^{∗} = EÑ ; γ̃. Now, exactly as in the case of type A premice, we can show that there are no cutpoints of EÑ ; top larger than λ̃^{∗}. Hence Ñ is of type B as well, λ̃^{∗} = λ∗ ; Ñ and γ̃ = γÑ. It remains to discuss the case where N_{τ} is of type C. Then ωϱ_{Nτ̄}^{1} = λ_{Nτ̄} > κ, as both N_{τ} and all Nτ̄ are in 𝒮. It follows that n > 0, so Π_{2}^{(1)}-statements which hold on a tail-end of D ∩ τ̃ are upwards preserved under the direct limit maps. Notice also

that ωϱ1 ; Ñ = ⋃{σ′′_{τ̄τ̃}ωϱ_{Nτ̄}^{1}; τ̄ ∈ D ∩ τ̃} = ⋃{σ′′_{τ̄τ̃}λ_{Nτ̄}; τ̄ ∈ D ∩ τ̃} = λÑ. That Ñ is of

type C can be expressed by the Q^{(1)}-statement

(∀ζ^{1})(∃λ̄^{1} ≥ ζ^{1})(λ̄^{1} is a cutpoint of EÑ ; top),

so it is true in Ñ by the preservation properties of the direct limit maps. Now given any λ̄ < λÑ,

EÑ ; top | λ̄ = {⟨x, y⟩; (∃y′)(⟨x, y′⟩ ∈ EÑ ; top & y = y′ ∩ λ̄},

CHARACTERIZATION OF □_{κ} IN CORE MODELS 73

so EÑ ; top | λ̄ is Σ_{1}(N)-definable in λ̄. But we have seen that λ̄ < ωϱ1 ; Ñ = λÑ, so EÑ ; top | λ̄ being a bounded subset of λÑ, must be in Ñ. This proves that Ñ is a type C premouse. From now on we know that the preservation properties of all maps στ̄τ̃ and σ hold with respect to the language for premice.

Let p̃ = σ_{τ̄τ̃}(pτ̄) for τ̄ ∈ D ∩ τ̃. Given an x ∈ Ñ, there is a τ̄ ∈ D ∩ τ̃ and an x̄ ∈ Nτ̄ such that x = σ_{τ̄τ̃}(x̄). By the soundness of Nτ̄, there is an ξ < κ satisfying x̄ = h̃τ̄(ξ, pτ̄). This statement, being Σ_{1}^{(n)}, is upward preserved by σ_{τ̄τ̃}, so x = h̃n+1 ; Ñ(ξ, p̃). Since x was arbitrary, Ñ = h̃n+1 ; Ñ(κ ∪ {p̃}). As in the proof of the previous lemma we conclude that ωϱω ; Ñ = ωϱn+1 ; Ñ = κ and p̃ ∈ Rn+1 ; Ñ. Now notice that σ_{τ̃τ} (p̃) = p_{τ} and that for any α ∈ p_{N_{τ}}, there is a generalized witness for α with respect to N_{τ} and p_{τ} in rng(σ). The latter follows from the fact that rng(σ) ⊃ rng(σ_{τ̄τ}) and that rng(σ_{τ̄τ}) contains such witnesses, as is ensured by c) in the defintion of D. From now on we can literally repeat the proof of the previous lemma and infer that Ñ is sound and p̃ = pÑ, and, consequently, that Ñ = Nτ̃, nτ̃ = n and σ = σ_{τ̃τ}. Thus, τ̃ ∈ D. ⊓ ⊔(Lemma 3.8)

Lemma 3.9. D is a subset of 𝒮^{0} on a tail-end, i.e. there is a τ̄ < τ such that D − τ̄ ⊂ 𝒮^{0}. Proof. Suppose the contrary, i.e. let ⟨τ_{ι}; ι < δ⟩ be an increasing sequence cofinal in τ such that each τ_{ι} is in 𝒮^{1}. Due to the pigeonhole principle, we can assume w.l.o.g. that |q_{τ_{ι}}| = m for some fixed m ∈ ω. Furthermore, we can assume that the sequence ⟨μ_{τ_{ι}}; ι < δ⟩ is monotone (not necessarily strictly), as we can always replace it by a monotone subsequence ⟨μ_{τ_{ι(ξ)}}; ξ < δ′⟩ where ι(ξ) is inductively defined by

ι^{∗}(ξ) = sup{ι(ξ̄) + 1; ξ̄ < ξ}
ι(ξ) ≃ the least ι such that ι^{∗}(ξ) ≤ ι < δ and μ_{τ_{ι}} = min{μ_{τ_{η}}; ι^{∗}(ξ) ≤ η < δ}

where sup(∅) = 0. Let μ = sup{μ_{τ_{ι}}; ι < δ}, let q be the bottom segment of p_{τ} with exactly m elements and let r = p_{τ} − q. Notice that μ ≤ κ and that q = σ_{τ_{ι}τ} (q_{τ_{ι}}) and r = σ_{τ_{ι}τ} (r_{τ_{ι}}) for all ι < δ.

We show that (μ, q) is a divisor of N_{τ} by verifying all clauses in the definition of a divisor. From the proof of previous lemma we know that ⟨N_{τ} , σ_{τ_{ι}τ}; ι < δ⟩ is the direct limit of the diagram ⟨N_{τ_{ι}}, σ_{τῑτ_{ι}}; ῑ ≤ ι < δ⟩. We shall use properties of fine structural direct limits discussed in the fine structure subsection in the preliminaries

74 ERNEST SCHIMMERLING AND MARTIN ZEMAN

without further reference. Notice first that

(26)  ωϱ_{τ} = ⋃_{ι<δ} σ′′_{τ_{ι}τ} ωϱ_{τ_{ι}}.

We further observe that

(27)  h̃_{τ} (μ ∪ {r}) = ⋃_{ι<δ} σ′′_{τ_{ι}τ} h̃_{τ_{ι}}(μ_{τ_{ι}} ∪ {r_{τ_{ι}}}).

The inclusion ⊃ follows from the fact that Σ_{1}^{(n)}-statements are upward preserved under σ_{τ_{ι}τ}, so if y = h̃_{τ_{ι}}(ξ, r_{τ_{ι}}) for some ξ < μ_{τ_{ι}} then σ_{τ_{ι}τ} (y) = h̃_{τ} (ξ, r). The converse follows from the properties of direct limits that Σ_{1}^{(n)} statements are downward preserved on a tail-end. So if y = h̃_{τ} (ξ, r), then for a sufficiently large ι < δ, the value y_{ι} = h̃_{τ_{ι}}(ξ, r_{τ_{ι}}) is defined and σ_{τ_{ι}τ} (y_{ι}) = y. This proves (27). Now as (μ_{τ_{ι}}, q_{τ_{ι}}) is a divisor for N_{τ_{ι}} for any ι < δ, each hull h̃_{τ_{ι}}(μ_{τ_{ι}} ∪ {r_{τ_{ι}}}) is cofinal in ωϱ_{τ_{ι}}. This together with (26) and (27) yields that h̃_{τ} (μ ∪ {r}) is cofinal in ωϱ_{τ}, which proves clause c) in the definition of divisor.

To verify d), we show

(28)  h̃_{τ} (μ ∪ {r}) ∩ (max(q) + 1) ⊂ μ.

Recall that we have set max(∅) = κ here. Fix a ζ ≤ max(q) such that ζ = h̃_{τ} (ξ, r) for some ξ < μ. Pick an ι < δ such that ζ̄ = h̃_{τ_{ι}}(ξ, r_{τ_{ι}}) is defined and so ζ = σ_{τ_{ι}τ} (ζ̄). Hence ζ̄ ≤ max(q_{τ_{ι}}). As (μ_{τ_{ι}}, q_{τ_{ι}}) is a divisor, ζ̄ < μ_{τ_{ι}}. So ζ = σ_{τ_{ι}τ} (ζ̄) = ζ̄ < μ_{τ_{ι}} ≤ μ, which proves (28). Thus, setting λ to be the least ordinal in h̃_{τ} (μ, r) − μ, we have λ > max(q_{τ}). On the other hand, λ ≤ σ_{τ_{ι}τ} (λ_{τ_{ι}}) < ωϱ_{τ}; the former inequality is a consequence of the fact that σ_{τ_{ι}τ} (λ_{τ_{ι}}) is obviously in h̃_{τ} (μ ∪ {r}). This verifies a), b) and d) and completes the proof of the claim.

Recall that N_{τ} as well as all N_{τ_{ι}} fail to be pluripotent, as τ ∈ 𝒮^{0} and all N_{τ_{ι}} are of the same type as N_{τ}. This means that divisors of these premice are determined by the standard parameters, and not by the Dodd parameters. Moreover, (μ, q) is not strong, as no τ ∈ 𝒮^{0} admits a strong divisor. The remaining part of the argument makes a substantial use of Lemma 2.22 as well as of its proof. By that lemma, p_{N′_{τ} (μ)} is a proper lengthening of r′ = π′^{−1}(r) where π′ : N′_{τ} (μ) → N_{τ} is the uncollapsing embedding associated with the Σ_{1}^{(n)}-hull h̃_{τ} (μ_{τ} ∪ {p_{τ} }). Let β′ be the largest element of p_{N′_{τ} (μ)} − r′. Then W_{N′_{τ} (μ)}^{β′,r′} ∈ N′_{τ} (μ), as the preservation properties of π′ combined with the condensation lemma guarantee that N′_{τ} (μ) is

CHARACTERIZATION OF □_{κ} IN CORE MODELS 75

solid. Letting Q = π′(W_{N′_{τ} (μ)}^{β′,r′}) and t = π′(t′) where t′ is the preimage of r′ under the associated canonical witness map, ⟨Q, t⟩ is a generalized witness, in the weak sense introduced immediately above Lemma 2.16, for β = π′(β′) with respect to N_{τ} and r. We have to consider this weaker notion of a solidity witness, as it might happen that β < κ = ωϱ_{N_{τ}}^{n+1} while ⟨Q, t⟩ contains information merely about Σ_{1}^{(n)}(N_{τ})-definable subsets of β. Let ξ, η < μ be such that ⟨Q, t⟩ = h̃_{τ} (ξ, p_{τ}) and β = h̃_{τ} (η, p_{τ}); such ordinals exist, as rng(π′) = h̃_{τ} (μ_{τ} ∪ {p_{τ} }). Let ι < δ be sufficiently large so that η, ξ < μ_{τ_{ι}} and both β̄ = h̃_{τ_{ι}}(η, p_{τ_{ι}}) and T̄ = h̃_{τ_{ι}}(ξ, p_{τ_{ι}}) are defined. Then σ_{τ_{ι}τ} (β̄, T̄) = (β, ⟨Q, t⟩), so T̄ is of the form ⟨Q̄, t̄⟩, and is a generalized witness, in the weak sense, for β̄ with respect to N_{τ_{ι}} and r_{τ_{ι}}; to see this, recall that being a generalized witness in the weak sense is a Π_{1}^{(n)}-property, and therefore is downward preserved under the Σ_{0}^{(n)}-preserving map σ_{τ_{ι}τ}. Moreover, both β̄ and ⟨Q̄, t̄⟩ are in the range of π′_{τ_{ι}} = h̃_{τ_{ι}}(μ_{ι} ∪ {p_{ι}}) by our choice of η, ξ and ι. Finally β̄ ≥ μ_{τ_{ι}}, as β ≥ μ (this follows easily from the definition of β) and μ_{ι} ≤ μ. Thus, if (β̄, ⟨Q̄, t̄⟩) = π′_{τ_{ι}}(β̄′, ⟨Q̄′, t̄′⟩), then β̄′ ≥ μ_{τ_{ι}} and ⟨Q̄′, t̄′⟩ is a generalized witness for β̄′ with respect to N′_{τ_{ι}}(μ_{τ_{ι}}) and r′_{τ_{ι}} that is an element of N′_{τ_{ι}}(μ_{τ_{ι}}). Notice that ⟨Q̄′, t̄′⟩ turns out to be a generalized witness in the strong sense, as the (n + 1)-st projectum of N′_{τ_{ι}}(μ_{τ_{ι}}) is precisely μ_{τ_{ι}}. By the first part of the proof of Lemma 2.18, the standard witness W′ =^{def} W_{N′_{τι} (μ_{τι})}^{β̄′,r′_{τι}} is an element of N′_{τ_{ι}}(μ_{τ_{ι}}) as well. Let t′_{τ_{ι}} be the preimage of r′_{τ_{ι}} under the associated canonical witness map. Since this map is Σ_{1}^{(n)}-preserving, for any set A which is Σ_{1}^{(n)}(N′_{τ_{ι}}(μ_{τ_{ι}})) in the parameter r′_{τ_{ι}} we can find some A′ which is Σ_{1}^{(n)}(W′)-definable in the parameter t′_{τ_{ι}} such that A ∩ β̄′ = A′ ∩ β̄′ ∈ N′_{τ_{ι}}(μ_{τ_{ι}}). Then r′_{τ_{ι}} ∉ P_{τ_{ι}}^{n+1}, as β̄′ ≥ μ_{τ_{ι}}. In other words, p_{N′_{τι} (μ_{τι})} is a proper lengthening of r′_{τ_{ι}}. By Lemma 2.22, the divisor (μ_{τ_{ι}}, q_{τ_{ι}}) is not strong, a contradiction. ⊓ ⊔(Lemma 3.9)

Let τ̄ be minimal with the property that D − τ̄ ⊂ 𝒮^{0}. By the previous lemmata, τ̄ < τ and B_{τ} − τ̄ = D − τ̄ is closed and unbounded in τ. This completes the proof of Lemma 3.5 for τ ∈ 𝒮^{0}.

When τ ∈ 𝒮^{1}. Here we adopt the same strategy as for τ ∈ 𝒮^{0}. We again assume that τ is a limit point of 𝒮, of uncountable cofinality, but now, of course, τ ∈ 𝒮^{1}.

Let D be the set of all τ̄ ∈ 𝒮^{1} ∩ τ satisfying:

76 ERNEST SCHIMMERLING AND MARTIN ZEMAN

• (μ_{τ} , m_{τ}) determines a strong divisor of Nτ̄, i.e. setting q∗ ; τ̄ to be the bottom segment of pτ̄ of length m_{τ}, the pair (μ_{τ} , q∗ ; τ̄) is a strong divisor of Nτ̄.

• Setting M ∗ ; τ̄ = Nτ̄(μ_{τ} , q∗ ; τ̄), there is a map σ_{τ̄τ} : M ∗ ; τ̄ → M_{τ} which is Σ_{0}- preserving with respect to the language for coherent structures and such that

a) τ̄ = cr(σ_{τ̄τ}) and σ_{τ̄τ} (τ̄) = τ;

b) σ_{τ̄τ} (q∗ ; τ̄) = q_{τ};

c) to each α ∈ q_{τ} there is a generalized witness Q_{τ} (α) for α with respect

to M_{τ} and q_{τ} such that Q_{τ} (α) ∈ rng(σ_{τ̄τ}).

Generalized witnesses in clause c) are, of course, computed in the language for coherent structures. Notice that M ∗ ; τ̄ is never a pluripotent L[E]-level, even if M_{τ} is, as its top extender cannot measure all subsets of μ_{τ}. This follows from the fact that σ_{τ̄τ} is not cofinal. We first prove that D is closed unbounded in τ, and then that (μ_{τ} , q∗ ; τ̄) = (μτ̄, qτ̄) on a tail-end of D. The proofs of the following lemmata are, as expected, variants of the proofs of the corresponding lemmata from the previous case adapted to protomice. Lemma 3.10. D is unbounded in τ. Proof. Let τ′ < τ; we have to find a τ̃ ≥ τ′ in D. Let M = N_{τ} (μ_{τ} , q_{τ}). It might happen (and it often will!) that M = N_{τ} is a pluripotent premouse. Recall that M can only be of type A or B, as τ ∈ 𝒮. The following argument will be carried out in the language for coherent structures even in the case where M is a type B premouse.

As before construct M̄, κ̄, τ̄ ∈ H and an embedding σ : H → J_{κ^{++}}^{E} such that σ(M̄, κ̄, τ̄, μ̄, ϑ̄) = M, κ, τ, μ_{τ} , ϑ where ϑ = ϑ(M). Also, setting τ̃ = sup(σ′′τ̄), it follows as before that τ′ ≤ τ̃ < τ and that τ̃ is a limit point of 𝒮, so τ̃ is an element of 𝒮. From the preservation properties of σ we infer the following facts about M̄:

• M̄ is a coherent structure that is a premouse just in case that M is. If M is a premouse, then M is pluripotent and M̄ is a premouse of the some type as M. If M is a protomouse, then the top extender of M̄ is not weakly amenable with respect to M̄.

• τ̄ = κ̄^{+M̄}.

• ωϱω ; M̄ = ωϱ1 ; M̄ = κ̄.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 77

• If q̄ is the standard parameter of M̄, then σ(q̄) = q_{τ}.

• ϑ̄ is closed in M̄ relative to q̄, see Lemma 2.24 and the preceding definition.

• M̄ is sound and solid;

• σ(W ᾱ,q̄ ; M̄) = W_{M}^{α,q_{τ}} whenever ᾱ ∈ q̄ and α = σ(ᾱ).

Form the canonical extension σ̃ : M̄ → M̃ of σ ↾ J EM̄ ; τ̄ : J EM̄ ; τ̄ → J E ; τ̃. Let σ′ : M̃ → M be the embedding given by the interpolation lemma. Notice that, as ωϱ1 ; M̄ = κ̄, this extension is a coarse extension. Exactly as in the proof of Lemma 3.7 we infer:

• M̃ is a coherent structure, and σ̃ : M̄ → M̃ is Σ_{0}-preserving and cofinal;

• σ̃ is a coarse pseudoultrapower map and σ̃(κ̄, τ̄) = (κ, τ̃);

• cr(σ′) = τ̃ and σ′(τ̃) = τ;

• hM̃(κ ∪ {q̃}) = M̃ where q̃ = σ̃(q̄);

• ωϱω ; M̃ = ωϱ1 ; M̃ = κ and q̃ ∈ RM̃;

• letting t̄ be the preimage of q̄ under the canonical witness map associated

with W ᾱ,q̄ ; M̄,

⟨Q(α̃), t̃⟩ = σ̃(⟨W ᾱ,q̄ ; M̄), t̄⟩)

is a generalized witness for α̃ = σ̃(ᾱ) with respect to M̃ and q̃ that is an element of M̃;

• q̃ = pM̃;

• M̃ is solid and sound;

• σ′(pM̃) = q_{τ} and σ′(Q(α̃)) = W_{M}^{α,q_{τ}} whenever α̃ ∈ q̃ and α = σ′(α̃), as

σ′ ∘ σ̃ = σ. We note that the equality q̃ = pM̃ follows from its two preceding clauses. Since q̃ ∈ PM̃, we do not need to know beforehands that M̃ is solid. See the subsection on fine structure, the part on solidity, in the preliminaries.

Applying Lemma 2.19 (resp. Lemma 2.20), we conclude that M̃ = Nτ̃(μ_{τ} , q̃). Thus, M̃ is always a protomouse, even if M is a premouse. This is caused by the fact that σ′ is non-cofinal. Let F̄, F̃ and F be the top extender of M̄, M̃ and M, respectively. So cr(F̃) = μ_{τ}. Recall that F̄ and F̃ determine cofinal maps from ϑ̄ and ϑ̃ = ϑ(M̃) to ht(M̄) and ht(M̃), respectively. Also, these maps have the same Σ_{1}-definition over the respective structures (in M̄, for instance, the map is defined by otp(a) ↦ otp(F̄(a))). This together with the fact that σ̃ is cofinal implies that

78 ERNEST SCHIMMERLING AND MARTIN ZEMAN

σ̃ maps ϑ̄ cofinally into ϑ̃. To see that τ̃ ∈ D, it suffices to prove that (μ_{τ} , q̃) is a strong divisor of Nτ̃. By Lemma 2.24, this is equivalent to showing that ϑ̃ is closed in M̃ relative to q̃.

Assume we have established:

(29) There are unboundedly many ϑ^{∗} < ϑ that are closed in M relative to q_{τ}.

It follows that there are unboundedly many ϑ̄^{∗} < ϑ̄ which are closed in M̄ relative to q̄. That ϑ̄^{∗} is closed in M̄ relative to q̄ is equivalent to

(∀w)(∀f ∈ J EM̄ ; ϑ̄^{∗})(∀ξ < μ_{τ})[w = F̄(f)(q̄, ξ) ⟶ w ∩ μ̄ ∈ J EM̄ ; ϑ̄^{∗}].

This is a Π_{1}-statement, so the same holds of σ̃(ϑ̄^{∗}), q̃ and F̃ϑ̃^{∗} in M̃, which proves that σ̃(ϑ̄^{∗}) is closed in M̃ relative to q̃. So ϑ̃ is closed in M̃ relative to q̃, as σ̃ maps ϑ̄ cofinally into ϑ̃.

To complete the proof, we have to verify (29). If M is a premouse, (29) follows by a simple closure argument. We now give a more general argument which also goes through for protomice. Notice that cf(ϑ) = cf(τ) > ω, as

ϑ′ ↦ sup({F (f)(q_{τ} , ξ); f : μ_{τ} → μ_{τ} & f ∈ J_{ϑ′}^{E} & ξ ∈ κ} ∩ τ)

is a monotone map mapping ϑ cofinally into τ. This follows from the regularity of τ in M and the fact that for each ϑ^{∗}, the values on the right side are determined by F_{ϑ^{∗}}, which is an element of M. Suppose (29) fails. Let δ = cf(ϑ) and let ⟨ϑ′_{ξ}; ξ < δ⟩ be a normal sequence unbounded in ϑ such that ϑ′_{0} is above all ordinals that are closed in M relative to q_{τ}. To each ξ < δ fix a map f_{ξ} : μ_{τ} → 𝒫(μ_{τ}) and an ordinal η_{ξ} < μ_{τ} such that F (f_{ξ})(q_{τ} , η_{ξ}) ∩ μ_{τ} ∉ J_{ϑ′_{ξ}}^{E}. For limit ξ, let g(ξ) be the least ξ̄ such that f_{ξ} ∈ J_{ϑ′ ; ξ̄}^{E}. Then g is a regressive function defined on all limit ordinals below δ, so it has a constant value, say ξ^{∗}, on some stationary S ⊂ δ. Thus, for ξ ∈ S we have f_{ξ} ∈ J_{ϑ^{∗}}^{E} where ϑ^{∗} = ϑ′_{ξ^{∗}}. As μ_{τ} is the largest cardinal in J_{ϑ}^{E}, there is an enumeration f^{∗} ∈ J_{ϑ}^{E} of all functions f : μ_{τ} → 𝒫(μ_{τ}) which are in J_{ϑ^{∗}}^{E}. Define f′ : μ_{τ} → 𝒫(μ_{τ}) by

f′(ζ) = {≺ξ, η, η′≻; η′ ∈ f^{∗}(ξ)(ζ, η) & η, ξ < μ_{τ} }.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 79

Clearly, f′ ∈ J_{ϑ}^{E} and F (f′)(q_{τ}) is a subset of λ_{τ}. As ϑ is closed, F (f′)(q_{τ})∩μ_{τ} ∈ J_{ϑ′_{ξ′}}^{E} for some ξ′ ∈ S. Hence

{η′ < μ_{τ}; ≺ξ, η, η′≻ ∈ F (f′)(q_{τ})} ∈ J_{ϑ_{ξ′}}^{E}

whenever η, ξ < μ_{τ}. In particular, this must be true of ξ̃ and η_{ξ′} where ξ̃ < μ_{τ} is such that f^{∗}(ξ̃) = f_{ξ′}. Then

{η′ < μ_{τ}; ≺ξ̃, η_{ξ′}, η′≻ ∈ F (f′)(q_{τ})} = F (f_{ξ′})(q_{τ} , η_{ξ′}) ∩ μ_{τ} ,

and F (f_{ξ′})(q_{τ} , η_{ξ′}) ∩ μ_{τ} ∉ J_{ϑ_{ξ′}}^{E} by our choice of f_{ξ′} and η_{ξ′}. Contradiction. ⊓ ⊔(Lemma 3.10)

Lemma 3.11. D is closed in τ. Proof. We shall closely follow the proof of Lemma 3.8. Let τ̃ < τ be a limit point of D. Then τ̃ ∈ 𝒮. Form the direct limit ⟨M̃, σ_{τ̄τ̃}; τ̄ ∈ D ∩ τ̃⟩ of the diagram ⟨M ∗ ; τ̄, σ_{τ^{∗}τ̄}; τ^{∗} ≤ τ̄ & τ^{∗}, τ̄ ∈ D ∩ τ̃⟩. As before we have the Σ_{0}-preserving map σ : M̃ → M defined by σ_{τ̄τ̃}(x) ↦ σ_{τ̄τ} (x), so M̃ is well-founded and we can consider it to be transitive. The arguments from the proof of Lemma 3.8 can be modified in a straightforward way to obtain the following properties of M̃ and σ. In the clauses below, τ̄ is an arbitrary element of D ∩ τ̃.

• M̃ is a coherent structure.

• σ_{τ̄τ̃}(τ̄) = τ̃ and σ ∘ σ_{τ̄τ̃} = σ_{τ̄τ}.

• cr(σ) = τ̃ and σ(τ̃) = τ.

• hM̃(κ ∪ {q̃}) = M̃ where q̃ = σ_{τ̄τ̃}(q∗ ; τ̄), so ωϱω ; M̃ = ωϱ1 ; M̃ = κ and q̃ ∈ RM̃.

• σ(q̃) = q_{τ}.

• Let α̃ ∈ q̃ and σ(α̃) = α. So α ∈ q_{τ}. If ⟨Q(α), t(α)⟩ is a generalized witness for α with respect to M_{τ} and q_{τ} and ⟨Q(α), t(α)⟩ ∈ rng(σ_{τ̄τ}) for some τ̄ ∈ D ∩ τ then ⟨Q(α̃), t(α̃)⟩ =^{def} σ^{−1}(⟨Q(α), t(α)⟩) is a generalized witness for α̃ with respect to M̃ and q̃.

• q̃ = pM̃.

• M̃ is sound and solid. The very first clause follows from the fact that the direct limit M̃ satisfies Π_{2}- statements which hold on a tail-end of D ∩ τ̃; the rest is clear. By the condensation Lemma 2.19 (resp. Lemma 2.20), M̃ = Nτ̃(μ_{τ} , q̃). Thus, M̃ is always a protomouse.

80 ERNEST SCHIMMERLING AND MARTIN ZEMAN

To complete the proof, we have to show that (μ_{τ} , q̃) is a strong divisor of M̃. We again show that ϑ̃ = ϑ(M̃) is closed in M̃ relative to q̃. So pick an f ∈ J E ; ϑ̃ and ξ < μ_{τ}, and fix some τ̄ ∈ D ∩ τ̃ such that F̃(f) ∈ rng(σ_{τ̄τ̃}) where F̃ is the top extender of M̃. Letting F̄ be the top extender of M ∗ ; τ̄, we have

F̃(f)(q̃, ξ) ∩ μ_{τ} = σ_{τ̄τ̃}(F̄(f)(q∗ ; τ̄, ξ) ∩ μ_{τ}) = F̄(f)(q∗ ; τ̄, ξ) ∩ μ_{τ} ∈ J_{ϑτ̄}^{E} ⊂ J E ; ϑ̃.

The second equality is a consequence of the fact that σ_{τ̄τ̃}(μ_{τ}) = μ_{τ}, and the membership relation follows from assumption that (μ_{τ} , q∗ ; τ̄) is a strong divisor of Nτ̄. (Notice that this in fact proves that ϑτ̄ is closed in M̃ relative to q̃ for each τ̄ ∈ D∩τ̃. Also, the set of all ϑτ̄ is c.u.b. in ϑ̃.) ⊓ ⊔(Lemma 3.11)

Lemma 3.12. There is a τ̄ < τ such that for every τ′ ∈ D − τ̄ we have (μ_{τ} , q_{τ′}^{∗}) = (μτ̄, qτ̄). Consequently, D − τ̄ = B_{τ} − τ̄. Proof. We will again follow the proof of the corresponding Lemma 3.9. Suppose for a contradiction that ⟨τ_{ι}; ι < δ⟩ is an increasing sequence cofinal in τ such that (μ_{τ_{ι}}, q_{τ_{ι}}) ≠ (μ_{τ} , q_{τ_{ι}}^{∗}). By the definition of (μ_{τ_{ι}}, q_{τ_{ι}}), each q_{τ_{ι}} is a bottom part of q_{τ_{ι}}^{∗}, say q_{τ_{ι}}^{∗} = q_{τ_{ι}} ∪ s_{τ_{ι}}. Moreover, μ_{τ_{ι}} > μ_{τ} for every ι < δ. This follows again from the definition of (μ_{τ_{ι}}, q_{τ_{ι}}) if q_{τ_{ι}} = q_{τ_{ι}}^{∗}, and from Lemma 2.26 otherwise. Arguing as in the proof of Lemma 3.9, we can assume w.l.o.g. that ⟨μ_{τ_{ι}}; ι < δ⟩ is a monotone sequence and all q_{τ_{ι}} have a fixed size, say m. Then σ_{τῑτ_{ι}}(q_{τῑ}, s_{τῑ}) = (q_{τ_{ι}}, s_{τ_{ι}}) whenever ῑ ≤ ι < δ, and we can set (recall the notation from the beginning of this section, in particular that introduced in the subsection “Defining the square sequence”)

q = σ_{τ_{ι}τ} (q_{τ_{ι}});
s = σ_{τ_{ι}τ} (s_{τ_{ι}});
r = r_{τ};
μ = sup_{ι<δ} μ_{τ_{ι}}.

The former two values clearly do not depend on ι. Also, s might be empty, in which case q = q_{τ}. We first observe that (μ, q) is a divisor of N_{τ}. As q is a bottom part of q_{τ} and μ > μ_{τ}, this divisor cannot be strong by the definition of (q_{τ} , μ_{τ}). Using a reflection argument we then derive a contradiction to the fact that all (μ_{τ_{ι}}, q_{τ_{ι}}) are strong.

CHARACTERIZATION OF □_{κ} IN CORE MODELS 81

Recall that M = N_{τ} (μ_{τ} , q_{τ}). To see that (μ, q) is a divisor of N_{τ}, we first verify clause c) from the definition of a divisor. Assuming that M is a protomouse, h̃_{τ} (μ∪{r∪s}) ⊃ h̃_{τ} (μ_{τ} ∪{r}) whenever N_{τ} is not pluripotent, and h_{τ} (μ∪{r∪s}) ⊃ h_{τ} (μ∪{r}) whenever N_{τ} is pluripotent. In either case, the hull on the left is cofinal in ωϱ_{τ}, as the hull on the right is. If M = N_{τ} then h_{τ} (μ ∪ {s}) is cofinal in N_{τ} by the elementary properties of coherent structures (r = ∅ in this case). Now it suffices to show that h̃_{τ} (μ∪{r∪s})∩(max(q)+1) = μ in the former case where M is a protomouse and N_{τ} is not pluripotent, and that h_{τ} (μ∪{r∪s})∩(max(q)+1) = μ in the latter two cases where either M is a protomouse and N_{τ} is pluripotent or else M = N_{τ}. This will guarantee that (μ, q) has the rest of the properties of divisors. Suppose first that M is a protomouse, and pick a ζ from the above intersection. Let F_{τ} and F_{τ_{ι}} be the top extender of M and M_{τ_{ι}}^{∗}, respectively. By Lemma 2.13, ζ is of the form F_{τ} (f)(ξ, s) for some f : μ_{τ} → μ_{τ} and ξ < μ. For ι is sufficiently large such that f ∈ dom(F_{τ_{ι}}) and ξ < μ_{τ_{ι}} set ζ_{ι} = F_{τ_{ι}}(f)(ξ, s_{τ_{ι}}), then clearly σ_{τ_{ι}τ} (ζ_{ι}) = ζ. Since ζ ≤ max(q), we have ζ_{ι} ≤ max(q_{τ_{ι}}). Again by Lemma 2.13, ζ_{ι} ∈ h̃_{τ_{ι}}(μ_{τ_{ι}} ∪ {r_{τ_{ι}}}) if N_{τ_{ι}} is not pluripotent, and ζ_{ι} ∈ h_{τ_{ι}}(μ_{τ_{ι}} ∪ {r_{τ_{ι}}}) if N_{τ_{ι}} is pluripotent; this follows from the fact that (μ_{τ_{ι}}, q_{τ_{ι}}) is a divisor of N_{τ_{ι}} (recall that M_{τ_{ι}} is a protomouse). Hence ζ_{ι} < μ_{τ_{ι}} and, consequently, ζ = σ_{τ_{ι}τ} (ζ_{ι}) < μ_{τ_{ι}} ≤ μ. This completes the proof that (μ, q) is a divisor if M is a protomouse. If M = N_{τ}, the argument is the same, but we have to use Lemma 2.14 instead of Lemma 2.13, i.e. this time ζ will be of the form F_{τ} (f)(ξ, s, μ_{τ}). Clearly, the presence of μ_{τ} as a parameter here will not do any harm, as μ_{τ} < μ.

Recall the notation introduced in Section 2, the subsection on strong divisors. π′ : N′_{τ} (μ) → N_{τ} is the uncollapsing map associated with the hull h̃_{τ} (μ ∪ {p_{τ} }) if N_{τ} is not pluripotent, and with h_{τ} (μ ∪ {d_{τ} }) otherwise. Let π′(r′, s′) = (r, s). As we have already mentioned, the divisor (μ, q) cannot be strong. This means that for some β′ such that μ ≤ β′ < min(s′) we have

(30)  W_{N′_{τ} (μ)}^{β′,r′∪s′} ∈ N′_{τ} (μ).

To see this, we have to discuss two cases. The notion of solidity witness used here is the weaker one introduced immediately above Lemma 2.16. That is, forming solidity witnesses is sensitive to definability degree Σ_{1}^{(n_{τ})} in the language corresponding to N_{τ}. If N_{τ} is not pluripotent or else if λ_{N_{τ}^{∗}}(μ_{τ} , r ∪ s) > μ_{τ}, then (30) follows from

82 ERNEST SCHIMMERLING AND MARTIN ZEMAN

Lemma 2.22. We know that p_{N′_{τ} (μ)} is a proper lengthening of r′ ∪ s′, so it suffices to let β′ be the maximum of p_{N′_{τ} (μ)} − (r′ ∪ s′). If λ_{N_{τ}^{∗}}(μ_{τ} , r ∪ s) = μ_{τ} (so N_{τ} is pluripotent and r ∪ s = ∅), we use Lemma 2.23. By the remark after this lemma, W_{N′(μ)}^{μ,∅} = N^{∗}(μ, d_{τ}) ∈ N′(μ), so we let β′ = μ in this case. Let t′ be the preimage of p_{N′_{τ} (μ)} − (β′ + 1) under the canonical witness map. We now apply π′ to W_{N′(μ)}^{β′,r′∪s′} and infer that:

• ⟨Q, t⟩ = ⟨π′(W_{N′(μ)}^{β′,r′∪s′}), π′(t′)⟩ is a generalized witness for β = π′(β′) with respect to N_{τ} and r ∪ s.

• ⟨Q, t⟩ ∈ h_{τ} (μ ∪ {d_{τ} }) or ⟨Q, t⟩ ∈ h̃_{τ} (μ ∪ {p_{τ} }), depending on whether N_{τ} is pluripotent or not.

• ⟨W_{N_{τ}}^{β,r∪s}, t^{∗}, β⟩ ∈ h_{τ} (μ ∪ {d_{τ} , ϑ_{τ} }) or ⟨W_{N_{τ}}^{β,r∪s}, t^{∗}, β⟩ ∈ h̃_{τ} (μ ∪ {p_{τ} , ϑ_{τ} }), depending on whether N_{τ} is pluripotent or not. Here t^{∗} is the preimage of (r ∪ s) − (β + 1) under the canonical witness map.

• ⟨W_{M}^{β,s}, w, β⟩ ∈ h_{τ} (μ ∪ {d_{τ} , ϑ_{τ} }) or ⟨W_{M}^{β,s}, w, β⟩ ∈ h̃_{τ} (μ ∪ {p_{τ} , ϑ_{τ} }), depending on whether N_{τ} is pluripotent or not. Here w is the preimage of s−(β+1) under the canonincal withess map.

• ⟨W_{M}^{β,s}, w, β⟩ = F (f)(ξ, ϑ_{τ} , q_{τ}) for some f ∈ dom(F) and ξ < μ. Here, F is the top extender of M.

The second clause follows from the first one by the fact that generalized witnesses for the n-th level are preserved under Σ_{1}^{(n)}-preserving embeddings. The third clause follows from the second by the first part of Lemma 2.18: Just notice that W_{N_{τ}}^{β,r∪s} is Σ_{0}-definable from Q, β and ϑ_{τ} and both Q and β are in h̃_{τ} (μ ∪ {p_{τ} , ϑ_{τ} }) (we assume w.l.o.g. that either N_{τ} fails to be pluripotent or else λ_{N_{τ}^{∗}}(μ_{τ} , r_{τ} ∪ s) > μ_{τ}; the proof in the other case is similar). The step from the third clause to the fourth one is a straightforward application of d) from Lemma 2.16 if M is a protomouse; if M = N_{τ}, then there is nothing to prove, as W_{M}^{β,s} = W_{N_{τ}}^{β,r∪s}. The last clause is obtained from the fourth one by Lemmata 2.13 and 2.14, depending on whether M ≠ N_{τ} or M = N_{τ}. Notice that in the latter case, Lemma 2.14 requires adding μ_{τ} as an additional parameter. This is, however superfluous in the above application, as μ_{τ} is Σ_{1}-definable from ϑ_{τ}, so we can “absorb” μ_{τ} in f and ϑ_{τ}.

Pick an ι sufficiently large such that ξ < μ_{τ_{ι}} and f ∈ dom(F_{τ_{ι}}^{∗}), where F_{τ_{ι}}^{∗} is the top extender of M_{τ_{ι}}^{∗}. Then F_{τ_{ι}}^{∗}(f)(ξ, ϑ_{τ} , q_{τ_{ι}}^{∗}) is of the form ⟨Q_{ι}, w_{ι}, β_{ι}⟩ where

CHARACTERIZATION OF □_{κ} IN CORE MODELS 83

⟨Q_{ι}, w_{ι}⟩ is a generalized witness for β_{ι} = σ_{τ_{ι}τ}^{−1} (β) with respect to M_{τ_{ι}}^{∗} and s_{τ_{ι}}. Also, β_{ι} ≥ σ_{τ_{ι}τ}^{−1} (μ) = μ ≥ μ_{τ_{ι}}. Furthermore, we have:

• ⟨Q_{ι}, w_{ι}⟩ ∈ h_{τ_{ι}}(μ_{τ_{ι}} ∪ {d_{τ_{ι}}}) or ⟨Q_{ι}, w_{ι}⟩ ∈ h̃_{τ_{ι}}(μ_{τ_{ι}} ∪ {p_{τ_{ι}}}) depending on whether N_{τ_{ι}} is pluripotent or not.

• ⟨W_{M_{τι}^{∗}}^{β_{ι},s_{τι}} , w_{ι}^{∗}⟩ ∈ h_{τ_{ι}}(μ_{τ_{ι}} ∪ {d_{τ_{ι}}}) or ⟨W_{M_{τι}^{∗}}^{β_{ι},s_{τι}} , w_{ι}^{∗}⟩ ∈ h̃_{τ_{ι}}(μ_{τ_{ι}} ∪ {p_{τ_{ι}}}) depending on whether N_{τ_{ι}} is pluripotent or not. Here w_{ι}^{∗} is the preimage of s_{τ_{ι}} − (β_{ι} + 1) under the canonical witness map.

• ⟨W_{N_{τι}}^{β_{ι},r_{τι} ∪s_{τι}} , t_{ι}⟩ ∈ h_{τ_{ι}}(μ_{τ_{ι}} ∪ {d_{τ_{ι}}}) or ⟨W_{N_{τι}}^{β_{ι},r_{τι} ∪s_{τι}} , t_{ι}⟩ ∈ h̃_{τ_{ι}}(μ_{τ_{ι}} ∪ {p_{τ_{ι}}}) depending on whether N_{τ_{ι}} is pluripotent or not. Here t_{ι} is the preimage of r_{τ_{ι}} ∪ s_{τ_{ι}} − (β_{ι} + 1) under the canonical witness map.

The first clause follows from Lemma 2.13, as M_{τ_{ι}}^{∗} is a protomouse. The second clause is a consequence of the first one and the second part of Lemma 2.18, which guarantees that ⟨W_{M_{τι}^{∗}}^{β_{ι},s_{τι}} , w_{ι}^{∗}⟩ is Σ_{0}-definable from ⟨Q_{ι}, w_{ι}⟩, β_{ι} and ϑ_{τ_{ι}}^{∗} =^{def} ϑ(M_{τ_{ι}}^{∗}). Now it suffices to notice that ϑ_{τ_{ι}}^{∗} < μ_{τ_{ι}} and both ⟨Q_{ι}, w_{ι}⟩ and β_{ι} are in the hull in question, so the same also holds of ⟨W_{M_{τι}^{∗}}^{β_{ι},s_{τι}} , w_{ι}^{∗}⟩. The third clause then follows from d) of Lemma 2.16. Recall that r_{τ_{ι}} = r_{τ_{ι}}^{∗} ∪ s_{τ_{ι}} where r_{τ_{ι}}^{∗} = p_{τ_{ι}} − q_{τ_{ι}}^{∗} (resp. r_{τ_{ι}}^{∗} = d_{τ_{ι}} − q_{τ_{ι}}^{∗}, if N_{τ_{ι}} is pluripotent).

Let π′_{ι} : N′_{τ_{ι}}(μ_{τ_{ι}}) → N_{τ_{ι}} be the associated uncollapsing map and let

(β′_{ι}, r′_{τ_{ι}}, Q′_{ι}, t′_{ι}) = π′_{ι}^{−1}(β_{ι}, r_{τ_{ι}}, W_{N_{τι}}^{β_{ι},r_{τι} ∪s_{τι}} , t_{ι}).

Then ⟨Q′_{ι}, t′_{ι}⟩ is a generalized witness for β′_{ι} with respect to N′_{τ_{ι}}(μ_{τ_{ι}}) and r′_{τ_{ι}}. Notice also that β′_{ι} ≥ μ_{τ_{ι}}, as β_{ι} ≥ μ_{τ_{ι}} and π′_{ι} ↾ μ_{τ_{ι}} = id. Now we can proceed exactly as in the proof of Lemma 3.9. First of all, once ⟨Q′_{ι}, t′_{ι}⟩ is in N′_{τ_{ι}}(μ_{τ_{ι}}), we know that also the standard witness W′_{ι} for β′_{ι} with respect to N′_{τ_{ι}}(μ_{τ_{ι}}) and r′_{τ_{ι}} is in N′_{τ_{ι}}(μ_{τ_{ι}}). Consider two cases. Granting that either N_{τ_{ι}} is not pluripotent or else λ_{N_{τι}^{∗}} (μ_{τ_{ι}}, r_{τ_{ι}}) > μ_{τ_{ι}}, we conclude that every subset of β′_{ι} ≥ μ_{τ_{ι}} which is Σ_{1}^{(n_{τι})}(N′_{τ_{ι}}(μ_{τ_{ι}})) in r′_{τ_{ι}} is Σ_{1}^{(n_{τι})}(W′_{ι}), and therefore is an element of N′_{τ_{ι}}(μ_{τ_{ι}}). Thus, p_{N′_{τι} (μ_{τι})} must be a proper lengthening of r′_{τ_{ι}}. By Lemma 2.22, this means that (μ_{τ_{ι}}, q_{τ_{ι}}) cannot be strong, a contradiction. In the remaining case where N_{τ_{ι}} is pluripotent and λ_{N_{τι}^{∗}} (μ_{τ_{ι}}, r_{τ_{ι}}) = μ_{τ_{ι}}, the same argument yields that E_{top}^{N′_{τι} (μ_{τι})} | μ_{τ_{ι}}, being a cutback of the top extender of W′_{ι}, is an element of N′_{τ_{ι}}(μ_{τ_{ι}}). By Lemma 2.23, the

84 ERNEST SCHIMMERLING AND MARTIN ZEMAN

divisor (μ_{τ_{ι}}, d_{τ_{ι}}) is not strong, which again contradicts the choice of (μ_{τ_{ι}}, d_{τ_{ι}}). ⊓ ⊔(Lemma 3.12)

Let τ̄ be the least as in the previous lemma. Then B_{τ} − τ̄ = D − τ̄ is closed and unbounded in τ. This completes the proof of Lemma 3.5 for τ ∈ 𝒮^{1}.

Proof of Main Theorem. The construction from the previous subsections proves Theorem 3.1 and thus the implication d) ⟶ a) of Main Theorem. Notice also that a) ⟶ b) is trivial, so it suffices to focus on the proofs of b) ⟶ c) and c) ⟶ d)

Proof of b) ⟶ c). Given a subcompact cardinal κ, we show that □_{κ,<κ} fails. Assume for a contradiction that 𝒞 = ⟨C_{α}; κ < α < κ^{+} & lim(α)⟩ is such a sequence. Using a simple coding device, 𝒞 can be treated as a subset of κ^{+}. Fix a cardinal μ, a sequence 𝒞̄ = ⟨C̄_{α}; μ < α < μ^{+} & lim(α)⟩ and an embedding

σ : ⟨H_{μ^{+}}, 𝒞̄⟩ ⟶ ⟨H_{κ^{+}}, 𝒞⟩

witnessing the subcompactness of κ relative to 𝒞. We derive a contradiction by showing that cf(μ^{+}) ≤ μ. Letting ν = sup(σ′′μ^{+}), we know that cf(ν) = μ^{+}. Fix a C ∈ C_{ν}; then C is a closed unbounded subset of ν. We show that each proper initial segment of C is of order type strictly less than ν.

Notice that there are cofinally many γ̄ in μ^{+} such that cf(γ̄) = ω and σ(γ̄) = sup(σ′′γ̄) ∈ C. This follows from the standard closure argument and the fact that σ is continuous at limits of length strictly less than μ. (Given a γ̄_{0}, inductively pick a γ̄_{n+1} such that σ(γ̄_{n}) < γ′ < σ(γ̄_{n+1}) for some γ′ ∈ C; then γ̄ = sup_{n} γ̄_{n} meets the above requirements.) Now pick any such γ̄. Since γ = σ(γ̄) is ω-cofinal, otp(C) < κ for all C ∈ C_{γ}. This follows from the regularity of κ (see the discussion below the definition of subcompactness in the introduction). Applying the regularity of κ to the fact that |C_{γ}| < κ, we find an ε < κ such that otp(C) < ε whenever C ∈ C_{γ}. The least such ε, being definable from C_{γ} ∈ rng(σ), must be in rng(σ) as well, so ε < μ. Thus, C ∩ γ, being an element of C_{γ}, must be of ordertype strictly less than μ. This completes the proof of the implication b) ⟶ c).

Proof of c) ⟶ d). We argue in L[E]. Starting from the hypothesis that there are stationarily many ν < κ^{+} such that E_{ν} ≠ ∅, we show that κ is subcompact. Assume for a contradiction that this is not the case; let A be the <_{L[E]}-least subset

CHARACTERIZATION OF □_{κ} IN CORE MODELS 85

of τ = κ^{+} witnessing this. Notice that A ∈ J_{τ^{+}}^{E}, the support |J_{τ}^{E}| of J_{τ}^{E} is precisely H_{τ} and that any elementary embedding σ : ⟨H_{μ^{+}}, Ā⟩ → ⟨H_{τ} , A⟩ of our interest, being a bounded subset of H_{τ}, is an element of H_{τ}. Consequently, the fact that A witnesses the failure of subcompactness for κ can be expressed as M ⊧ φ(A, τ) where M = L[E] || τ^{+} and φ(A, τ) is the Σ_{1}-statement

(∃H)[H = |J_{τ}^{E}| & ¬(∃κ, μ, ϑ, H̄, Ā, σ ∈ H)φ̃(μ, κ, ϑ, σ, H̄, H, Ā, A)];

here, letting Sat_{N} be the satisfaction predicate for the structure N, (recall that Sat_{N} is uniformly Σ_{0}-definable in the parameter N), φ̃(κ, μ, ϑ, σ, H̄, H, Ā, A) is the conjunction of the following formulae:

• κ is the largest cardinal in H;

• μ < κ & ϑ = μ^{+H} & H̄ = (H_{ϑ})^{H} & Ā ⊂ ϑ;

• σ : H̄ → H & cr(σ) = μ;

• (∀x ∈ H̄)(∀ψ(v) ∈ Fml)[Sat_{⟨H̄,Ā⟩}(ψ(v), x) ⟷ Sat_{⟨H,A⟩}(ψ(v), σ(x))]. A standard closure argument shows that the set of all ordinals ν < τ satisfying

ν ∩ h_{M}(ν ∪ {τ}) = ν is closed unbounded in τ. Since we assume that E_{ν} ≠ ∅ for stationarily many ν, we can pick a ν satisfying both

(31)  ν ∩ h_{M}(ν ∪ {τ}) = ν and E_{ν} ≠ ∅.

Let M′ be the transitive collapse of h_{M}(ν ∪ {τ}) and let σ′ be the associated uncollapsing map. Then M′ is a passive premouse, ωϱ_{M′}^{1} ≤ ν = cr(σ′) and σ′(ν) = τ; this last equality follows from the first part of (31). Thus, ν = κ^{+M′}. By the condensation lemma, M′ is solid and its standard parameter is universal, so M̃ = core_{ν}(M′) exists. Let σ̃ : M̃ → M′ be the associated core map. Notice that ν = κ^{+M̃}, as any surjection g : α → ν such that g ∈ M̃ and α < ν would give rise to the surjection σ̃(g) ↾ α : α → ν that is an element of M′. Consequently, the critical point of σ̃, being at least ν, must be strictly larger than ν, as every ordinal between κ and σ̃(ν) has M′-cardinality equal to κ. Letting σ = σ′ ∘ σ̃ : M̃ → M, the above discussion can be summarized as follows:

• ωϱ1 ; M̃ ≤ ν and M̃ is sound above ν;

• cr(σ) = ν and σ(ν) = τ;

• σ is Σ_{1}-preserving.

86 ERNEST SCHIMMERLING AND MARTIN ZEMAN

These conclusions enable us to apply the condensation lemma to M, M̃ and σ; we show that clause d) of the condensation lemma must be true. Indeed, both a) and b) are impossible, as EM̃ ; ν = ∅ ≠ E_{ν}; the equality on the left follows from the fact that ν is a cardinal in M̃. Clause c) fails, as it requires that M̃ = Ult^{∗}(M || ζ, E_{α}) where M || ζ is the longest initial segment of M which does not collapse ν and E_{α} is an extender with critical point κ for some α ≥ ν. In our case, however, ζ = ν, so the only candidate for α would be ν. This yields an immediate contradiction, as cr(E_{ν}) is certainly smaller than κ. It follows that d) of the condensation lemma holds. Set M′ = Ult(M || ν, E_{ν}). Notice that M̃ is in fact a proper initial segment of M̄ = M′ || ν^{+M′} = Ult(M || ϑ^{+M}, E_{ν}) where ϑ = μ^{+M} and μ = cr(E_{ν}), as M̃ projects to ν.

We are now ready to derive the final contradiction. First we observe that A is in the range of σ. Indeed, as σ is Σ_{1}-preserving and σ(ν) = τ, there is a set B ∈ M̃ such that M̃ ⊧ φ(B, ν). The <M̃-least such set, call it Ã, must be the preimage of A under σ, as otherwise A <_{M} σ(Ã) and the preservation properties of σ would force the existence of some Ã^{∗} <M̃ Ã for which φ(Ã^{∗}, ν) holds in M̃, a contradiction. Notice also that Ã is the <M̃-least set B such that φ(B, ν) holds in M̃, as for any Ã′ <M̃ Ã satisfying φ(Ã′, ν), the set σ(Ã′) <_{M} A would witness the failure of subcompactness of κ, which would contradict our choice of A. Finally, as M̃ is a proper initial segment of M̄, the set Ã satisfies φ(Ã, ν) in M̄ and Ã is <M̄- minimal with this property. This means that Ã is definable in M̄ from the single parameter ν; it follows that Ã is in the range of the associated ultrapower map π̄ : M || ϑ^{+M} → M̄. Set Ā = π̄^{−1}(Ã) and π = σ ∘ π̄. Notice that σ defined merely on a proper initial segment of M̄; however, this will not do any harm, since the objects of our interest H_{τ} and Ã are in the domain of σ. Then π(H_{ϑ}, Ā) = (H_{τ} , A), so

π ↾ H̄ : ⟨H_{ϑ}, Ā⟩ ⟶ ⟨H_{τ} , A⟩

guarantees that A cannot be a witness to the failure of subcompactness of κ. Contradiction. This completes the proof of c) ⟶ d) and thus that of Main Theorem.

⊓ ⊔(Main Theorem)

References

[1] Andretta, A., Neeman, I. and Steel, J. R., The domestic levels of K^{c} are iterable, Israel Journal of Mathematics 125 (2001), 157–201

[2] Ben-David, S. and Magidor, M., The weak □^{∗} is really weaker than the full □, Journal of Symbolic Logic 51(4) (1986), 1029 – 1033.

[3] Burke, D., Generic embeddings and the failure of box, Proceedings of American Mathematical Society 123(9) (1995), 2867 – 2871

[4] Cummings, J. and E. Schimmerling, E., Indexed squares, Israel Journal of Mathematics 131 (2002), 61 – 99

[5] Cummings J., Foreman, M. and Magidor, M., Squares, scales and stationary reflection, Journal of Mathematical Logic 1(1) (2001), 35 – 98

[6] Devlin, K. J., Constructibility, Springer, 1984

[7] Jech, T., Set Theory, Academic Press, 1978

[8] Jensen, R. B., The fine structure of the constructible hierarchy, Annals of Mathematical Logic 4 (1972), 229–308

[9] Jensen, R. B., Measures of order 0, handwritten notes, Oxford, 1988

[10] Jensen, R. B., Nonoverlapping extenders, Handwritten notes, Oxford

[11] Jensen, R. B., Some remarks on □ below 0^{¶}, handwritten notes, Oxford

[12] Jensen, R. B., More on □ below 0^{¶}, handwritten notes, Oxford, 1994

[13] Jensen, R. B., A new fine structure for higher core models, handwritten notes, Berlin, 1997 [14] Jensen, R. B., More on iterability, Handwritten notes, Berlin, 1998

[15] Jensen, R. B., Corrections and remarks, Handwritten notes, Berlin, 1998

[16] Jensen, R. B., T-mice, handwritten notes, Berlin, 2001

[17] Jensen, R. B., private communication

[18] Kanamori, A., The higher infinite, Springer, 1994

[19] Martin, D. A. and Steel J. R., Projective determinacy, Proceedings of National Academy of Sciences USA 85(18) (1988), 6582 – 6586

[20] Mitchell, W. J. and Schimmerling, E., Weak covering without countable closure, Mathematical Research Letters 2(5) (1995), 595 – 609

[21] Mitchell, W. J., Schimmerling, E. and Steel, J. R., The covering lemma up to a Woodin cardinal, Annals of Pure and Applied Logic 84 (1997), 219 – 255

[22] Mitchell, W. J. and Steel J. R., Fine structure and iteration trees , Lecture Notes in Logic 3, Springer-Verlag, Berlin, 1994

[23] Neeman, I., Inner models in the region of a Woodin limit of Woodin cardinals, Annals of Pure and Applied Logic 116 (2002), No. 1-3, 67 – 155

[24] Neeman, I. and Steel, J. R., A weak Dodd-Jensen lemma, Journal of Symbolic Logic 64(3) (1999), 1285 – 1294 [25] Schimmerling, E., Combinatorial principles in the core model for one Woodin cardinal,

Annals of Pure and Applied Logic 74(2) (1995), 153 – 201

[26] Schimmerling, E., Combinatorial set theory and inner models, in C. A. Di Prisco, J. A. Larson, J. Bagaria and A. R. D. Mathias (eds.), Set theory, Techniques and Applications, Curaçao 1995 and Barcelona 1996 Conferences, 207 – 212, Kluwer, 1998

[27] Schimmerling, E., A finite family weak square principle, Journal of Symbolic Logic 64(3) (1999), 1087 – 1110

[28] Schimmerling, E., Covering properties of core models, in S. B. Cooper and J. K. Truss (eds.), Sets and Proofs, 281 – 299, London Mathematical Society Lecture Notes 258, Cambridge University Press, Cambridge, 1999

[29] Schimmerling, E., Woodin cardinals, Shelah cardinals, and the Mitchell-Steel core model, Proceedings of the American Mathematical Society 130(11) (2002), 3385 – 3391

[30] Schimmerling, E. and Steel, J. R., The maximality of the core model, Transactions of the American Mathematical Society 351(8) (1999), 3119 – 3141

[31] Schimmerling, E. and Woodin, W. H., The Jensen covering property, Journal of Symbolic Logic 66(4) (2001), 1505 – 1523

[32] Schimmerling, E. and Zeman, M., Square in core models, Bulletin of Symbolic Logic 7(3) (2001), 305 – 314

[33] Schimmerling, E. and Zeman, M., Cardinal transfer properties in extender models I, submitted

[34] Schimmerling, E. and Zeman, M., Cardinal transfer properties in extender models II, in preparation

[35] Schindler R. D., Steel, J. R. and Zeman, M., Deconstructing inner model theory, Journal of Symbolic Logic 67(2) (2002), 721 – 736

[36] Solovay R. M., Reinhardt W. N. and Kanamori, A., Strong axioms of infinity and elementary embeddings, Annals of Mathematical Logic 13(1) (1978), 73 – 116

[37] Steel, J. R., The core model iterability problem, Lecture Notes in Logic 8, Springer, 1996 [38] Steel, J. R., An outline of inner model theory, Handbook of set theory, Foreman, M.,

Kanamori, A. and Magidor, M. (eds.), to appear

[39] P.D. Welch, D. Phil. dissertation, Oxford 1979

[40] Woodin, W. H., The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal, de Gruyter Series in Logic and Its Applications 1, Walter de Gruyter & Co., Berlin, 1999

[41] Wylie, D. J., Ph. D. dissertation, MIT, 1990

[42] Zeman, M., Ph. D. dissertation, HU Berlin, 1997

[43] Zeman, M., Global □ in extender models, in preparation

[44] Zeman, M., Inner models and large cardinals, de Gruyter Series in Logic and its Applications 5, Walter de Gruyter & Co., Berlin, 2002

[45] Zeman, M., Towards □_{μ} in higher core models, handwritten notes, Berlin, 1998 [46] Zeman, M., Dodd solidity and λ-indexing, of extenders, to appear in Journal of Mathe-

matical Logic

Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, PA 15213-3890, USA

E-mail address: eschimme@andrew.cmu.edu

Department of Mathematics, University of California at Irvine, Irvine, CA 92697-3875, USA

E-mail address: mzeman@math.uci.edu