Some applications of Supercompact Extender Based Forcings to HOD.

Abstract. Supercompact extender based forcings are used to construct models with $HOD$ cardinal structure different from those of $V$ . In particular, a model where all regular uncountable cardinals are measurable in $HOD$ is constructed.

The supercompact extender based Prikry forcing, developed by the second author in [8], is applied to reduce largely the initial assumptions of this theorem and to give a simpler proof. Namely, we show the following:

Actually, assuming the measurability (or supercompactness) of

λ

V

, we obtain that

{(κ^{+})}^{V [G]}

is measurable (or supercompact) in

{HOD}_{{x}}

In [2], a model with the property

{(α^{+})}^{HOD} < α^{+}

, for every infinite cardinal

α

was constructed. We extend this result, using the supercompact extender based Magidor forcing of the second author [9], and show the following:

The work [1] obtained results similar to our last theorem using iteration of Radin forcing together with Cardinal collapsing.

However, we do not have even inaccessibles in the model of theorem 2. It is possible to modify the construction in order to have measurable cardinals (and bit more) in the model. We do not know how to get supercompacts and it is very unlikely the method used will allow model with supercompacts.

The structure of this work is as follows. In section 2 we give definitions and claims about

HOD

and homogeneous forcing notions which are well known. In section 3 we prove theorem 1. In section 4 we prove theorem 2.

We assume knowledge of large cardinals and forcing. In particular this work depends on the supercompact extender based Prikry-Magidor-Radin forcing.

2. HOD background

We will work in

HOD

of generic extensions, hence the relation between

V [G]

and

{HOD}^{V [G]}

, where

V [G]

is a generic extension, will be our main machinery.

Our main tool will be forcing notions which are homogeneous in some sense. A forcing notion

P

is said to be cone homogeneous if for each pair of conditions

p_{0}, p_{1} \in P

there is a pair of conditions

p_{0}^{∗}, p_{1}^{∗} \in P

such that

p_{0}^{∗} \leq p_{0}

p_{1}^{∗} \leq p_{1}

, and

P ∕ p_{0}^{∗} ≃ P ∕ p_{1}^{∗}

A forcing notion

P

is said to be weakly homogeneous if for each pair of conditions

p_{0}, p_{1} \in P

there is an automorphism

π : P \to P

so that

π (p_{0})

and

p_{1}

are compatible. It is evident a weakly homogeneous forcing notion is cone homogeneous.

An automorphism

π : P \to P

induces an automorphism on

P

-terms by setting recursively

π (⟨ \dot{τ}, p ⟩) = ⟨ π (\dot{τ}), π (p) ⟩

Note ground model terms are fixed by automorphisms, i.e.,

π (\overset{ˇ}{x}) = \overset{ˇ}{x}

, in particular for each ordinal

α

π (\overset{ˇ}{α}) = \overset{ˇ}{α}

An essential fact about a cone homogeneous forcing notion

P

is that for each formula

φ

, either

⊩_{P} φ (α_{1}, \dots, α_{l})

⊩_{P} \neg φ (α_{1}, \dots, α_{l})

. If in addition the forcing

P

is ordinal definable then we get

{HOD}^{V [G]} \subseteq V

, where

G

P

-generic.

In [4] it was shown that an arbitrary iteration of weakly (cone) homogeneous forcing notions is weakly (cone) homogeneous under the very mild assumption that the iterand is fixed by automorphisms. For the sake of completeness, we show here a special case of this theorem, which is enough for our purpose.

Proof. Fix two conditions $p_{0}, p_{1} \in P_{κ}$ . We will construct two conditions $p_{0}^{∗} \leq p_{0}$ and $p_{1}^{∗} \leq p_{1}$ such that $P_{κ} ∕ p_{0}^{∗} ≃ P_{κ} ∕ p_{1}^{∗}$ , by which we will be done. The construction is done by induction on $α \leq κ$ as follows.

Assume $α = β + 1$ , $p_{0}^{∗} ↾β$ , $p_{1}^{∗} ↾β$ , and $π_{β} : P_{β} ∕ p_{0}^{∗} ↾β ≃ P_{β} ∕ p_{1}^{∗} ↾β$ were constructed. We know $⊩_{P_{β} ∕ p_{0}^{∗} ↾β} “ {\dot{Q}}_{β} = π_{β}^{- 1} ({\dot{Q}}_{β}) is cone homogeneous ”$ . Let $ρ_{β} : {\dot{Q}}_{β} \to {\dot{Q}}_{β}$ be a function for which $\dot{τ} [G] = ρ_{β} (\dot{τ}) [π_{β}^{″} G]$ holds, whenever $G \subseteq P_{β}$ is generic and $\dot{τ} [G] \in \dot{Q} [G]$ . If both $p_{0} (β)$ and $p_{1} (β)$ are the maximal element of ${\dot{Q}}_{β}$ then let $p_{0}^{∗} (β)$ and $p_{1}^{∗} (β)$ be the maximal element of ${\dot{Q}}_{β}$ and let $σ_{β} = id$ be the trivial automorphism of ${\dot{Q}}_{β}$ . If either $p_{0} (β)$ or $p_{1} (β)$ is not the maximal element of ${\dot{Q}}_{β}$ then use the the cone homogeneity of ${\dot{Q}}_{β}$ to find $P_{β}$ -names $p_{0}^{∗} (β)$ , $p_{1}^{∗} (β)$ , and ${\dot{σ}}_{β}$ , such that $p_{0}^{∗} ↾β ⊩_{P_{β}} “ p_{0}^{∗} (β) \leq p_{0} (β) ”$ , $p_{1}^{∗} ↾β ⊩_{P_{β}} “ p_{1}^{∗} (β) \leq p_{1} (β) ”$ , and ${\dot{σ}}_{β} : {\dot{Q}}_{β} ∕ p_{0}^{∗} (β) ≃ {\dot{Q}}_{β} ∕ ρ_{β}^{- 1} (p_{1}^{∗} (β))$ is an automorphism. Whatever way ${\dot{σ}}_{β}$ was constructed define the automorphism $π_{β + 1}$ by letting $π_{β + 1} (s) = ⟨ π_{β} (s↾β), ρ_{β} ({\dot{σ}}_{β} (s (β))) ⟩$ , for each $s \leq p_{0}^{∗} ↾β + 1$ .

Assume $α$ is limit and for each $β < α$ we have $p_{0}^{∗} ↾β \leq p_{0} ↾β$ , $p_{1}^{∗} ↾β \leq p_{1} ↾β$ , and $π_{β} : P_{β} ∕ p_{0}^{∗} ↾β ≃ P_{β} ∕ p_{1}^{∗} ↾β$ is an automorphism such that $π_{β} ↾ P_{β^{'}} = π_{β^{'}}$ , whenever $β^{'} \leq β$ . For each $s \leq p_{0}^{∗} ↾α$ let $π_{α} (s) \in P_{α}$ be the condition defined by setting for each $β < α$ , $π_{α} (s) (β) = π_{β + 1} (s↾β + 1) (β)$ . □

The following claim is practically the successor case of the previous one. It is useful when we will have automorphism of forcing notions which are not necessarily cone homogeneous.

Proof. Note there is a function $ρ$ taking $P_{0}$ -names to $P_{1}$ -names such that ${\dot{q}}_{0} [G_{0}] = ρ ({\dot{q}}_{0}) [G_{1}]$ , where $G_{0} \subseteq P_{0}$ is generic and $G_{1} = π_{0}^{″} G_{0}$ .

Set ${\dot{q}}_{1}^{'} = ρ^{- 1} ({\dot{q}}_{1})$ . By the cone homogeneity of ${\dot{Q}}_{0}$ in $V^{P_{0}}$ there are stronger conditions ${\dot{q}}_{0}^{∗} \leq {\dot{q}}_{0}$ and ${\dot{q}}_{1}^{' *} \leq {\dot{q}}_{1}^{'}$ , for which there is (a name of) an automorphism $π_{1} : {\dot{Q}}_{0} ∕ {\dot{q}}_{0}^{∗} \to {\dot{Q}}_{0} ∕ {\dot{q}}_{1}^{' *}$ . Set ${\dot{q}}_{1}^{∗} = ρ {(\dot{q})}_{1}^{' *}$ . Since for generics $G_{0}, G_{1}$ as above we have ${\dot{Q}}_{0} ∕ {\dot{q}}_{1}^{' *} [G_{0}] = {\dot{Q}}_{1} ∕ {\dot{q}}_{1}^{∗} [G_{1}]$ we get $π (p * \dot{q}) = π_{0} (p) * (ρ \circ π_{1} (\dot{q}))$ is the required automorphism. □

While the forcing notions we will use are cone homogeneous we will deliberately break down some of their homogeneity. The relation between

{HOD}^{V [G]}

and

V

will be as follows.

Proof. Assume $⊩_{P} “ Ȧ \subseteq On and Ȧ \in HOD ”$ . Let $G \subseteq P$ be generic. Then in $V [G]$ there are ordinals $α_{1}, \dots, α_{l}, β$ such that for each $α \in On$ ,

\begin{array}{l} α \in Ȧ [G] \Leftrightarrow V_{β} ⊨ φ (α, α_{1}, \dots, α_{l}) . \end{array}

Let $X_{0}^{α} \cup X_{1}^{α} \subseteq P$ be a maximal antichain such that for each $p \in X_{0}^{α}$ ,

\begin{array}{l} p ⊩ “ V_{β} ⊨ \neg φ (α, α_{1}, \dots, α_{l}) ”, \end{array}

and for each $p \in X_{1}^{α}$ ,

\begin{array}{l} p ⊩ “ V_{β} ⊨ φ (α, α_{1}, \dots, α_{l}) ” . \end{array}

Let $Ȧ^{'}$ be a $Q$ -name defined by setting for each $p \in X_{0}^{α} \cup X_{1}^{α}$ .

\begin{array}{l} π (p) ⊩_{Q} “ α \in Ȧ^{'} ” \Leftrightarrow p ⊩_{P} “ α \in Ȧ ” . \end{array}

Since $π^{″} (X_{0}^{α} \cup X_{1}^{α})$ is predense in $Q$ we get $Ȧ^{'} [π (G)] = Ȧ [G]$ , by which we are done. □

Let

C (τ, μ)

be the Cohen forcing for adding

μ

subsets to

τ

, i.e.,

C (τ, μ) = {f : a \to 2 ∣ a \subseteq μ, | a | < τ}

. The following is well known.

Proof. Assume $f, g \in ℂ (τ, μ)$ are conditions. Choose stronger conditions, $f^{∗} \leq f$ and $g^{∗} \leq g$ , such that $dom f^{∗} = dom g^{∗} = dom f \cup dom g$ . Define $π : ℂ (τ, μ) ∕ f^{∗} \to ℂ (τ, μ) ∕ g^{∗}$ by setting $π (f^{'}) = g^{∗} \cup (f^{'} ∖ f^{∗})$ for each $f^{'} \leq f^{∗}$ . It is obvious $π$ is an automorphism. □

3. The cofinality

ω

case

Let us switch to the cone-homogeneity of the Extender Based Prikry forcing. Extender based Prikry forcing was originally developed in [5]. We use a revision of the forcing where the extender can witness supercompactness. This was first developed in [8]. At the suggestion3 of the referee we add intuitive explanation of the extender based Prikry forcing. We will do so by introducing definitions going gradually from the Prikry forcing to the extender based Prikry forcing.

We begin with a definition of Prikry forcing which is more cumbersome than the standard definition. When generalizing to the extender base Prikry forcing this cumbersome definition becomes simpler than the standard definition of the extender based forcing.

Assume

j : V \to M

is an elementary embedding such that

crit (j) = κ

M ⊇^{κ} M

, and

κ

is its sole generator. Define the measure

U

by letting for each

A \subseteq κ

Recall that a condition in Prikry forcing is of the form

⟨ t, A ⟩

, where

t ∈^{< ω} κ

is a finite increasing sequence and

A \in U

. We can always assume that for each ordinal

ν \in A

ν > \max t

. The condition

⟨ t, B ⟩

is said to be a direct extension of the condition

⟨ t, A ⟩

(

⟨ t, B ⟩ ≤^{∗} ⟨ t, A ⟩

) in this forcing if

B \subseteq A

. Let

ν \in A

be an ordinal. Then

{⟨ t, A ⟩}_{⟨ ν ⟩} = ⟨ t ⌢ ⟨ ν ⟩, A ∖ (ν + 1) ⟩

. We say the condition

{⟨ t, A ⟩}_{⟨ ν ⟩}

is a

1

-point extension of

⟨ t, A ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ t, A ⟩

to be

{({⟨ t, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ s, B ⟩

is stronger than the condition

⟨ t, A ⟩

if there are

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ s, B ⟩ ≤^{∗} {⟨ t, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. This is clearly a valid definition of Prikry forcing. If

G

is the generic object then letting

t_{G} = ⋃ {t ∣ ⟨ t, A ⟩ \in G}

we get that

t_{G}

is an

ω

-sequence cofinal in

κ

Let us define again Prikry forcing, increasing the level of cumbersomeness. Starting from the same assumption as above proceed as follows. Define the measure

U

by letting for each

A ⊆^{{κ}} κ

Note a typical function

ν \in A

is of the form

ν : {κ} \to κ

. Define now a condition in Prikry forcing to be of the form

⟨ f, A ⟩

, where

f : {κ} →^{< ω} κ

is a function such that

f (ν)

is a finite increasing sequence, and

A \in U

. Note we can assume for each

ν \in A

ν (κ) > \max f (κ)

. The condition

⟨ f, B ⟩

is said to be a direct extension of the condition

⟨ f, A ⟩

(

⟨ f, B ⟩ ≤^{∗} ⟨ f, A ⟩

) in this forcing is if

B \subseteq A

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. Define the function

f_{⟨ ν ⟩}

by letting

f_{⟨ ν ⟩} (κ) = f (κ) ⌢ ⟨ ν (κ) ⟩

. Define the set of functions in

A

which are above

ν

A_{⟨ ν ⟩} = {μ \in A ∣ μ (κ) > ν (κ)}

. A 1-point extension

{⟨ f, A ⟩}_{⟨ ν ⟩}

⟨ f, A ⟩

is defined to be

⟨ f_{⟨ ν ⟩}, A_{⟨ ν ⟩} ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ f, A ⟩

to be

{({⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ g, B ⟩

is stronger than the condition

⟨ f, A ⟩

if there is

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ g, B ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. This is clearly a valid, if somewhat bizarre, definition of Prikry forcing. If we let

G

be the generic object and define the function

f_{G} : {κ} →^{ω} κ

by setting

f_{G} (κ) = ⋃ {f (κ) ∣ ⟨ f, A ⟩ \in G}

, then

f_{G} (κ)

is an

ω

-sequence cofinal in

κ

Staying in the previous context, let us choose an ordinal

α < j (κ)

. There is a function

F

in the ground model such that

j (F) (κ) = α

. Then

F^{″} f_{G} (κ)

is a sequence Prikry generic for the measure

W

generated by

α

. We can, however, generalize somewhat the forcing so as to be able to read directly the generic sequence corresponding to

α

from the generic object. For this define the measure

U

by letting for each

A ⊆^{{κ, α}} κ

Note a typical function

ν \in A

is of the form

ν : {κ, α} \to κ

such that

ν (κ) < ν (α)

. Define now a condition in Prikry forcing to be of the form

⟨ f, A ⟩

, where

f : {κ, α} →^{< ω} κ

is a function such that both

f (κ)

and

f (α)

are finite increasing sequences, and

A \in U

. Note we can assume for each

ν \in A

\max f (κ) < ν (κ)

and

\max f (α) < ν (α)

. The condition

⟨ f, B ⟩

is a direct extension of the condition

⟨ f, A ⟩

(

⟨ f, B ⟩ ≤^{∗} ⟨ f, A ⟩

) in this forcing if

B \subseteq A

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. Define the function

f_{⟨ ν ⟩}

by setting

Set

A_{⟨ ν ⟩} = {μ \in A ∣ μ (κ) > ν (α)}

. Then define the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

to be

⟨ f_{⟨ ν ⟩}, A_{⟨ ν ⟩} ⟩

. We say the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

is a

1

-point extension of

⟨ f, A ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ f, A ⟩

to be

{({⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ g, B ⟩

is stronger than the condition

⟨ f, A ⟩

(

⟨ g, B ⟩ \leq ⟨ f, A ⟩

) if there is

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ g, B ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. The above is clearly a valid, if strange, definition of Prikry forcing. Letting

G

be the generic object we define the function

f_{G} : {κ, α} →^{ω} κ

by setting

Of course, seeing the above one can immediately generalize to any less than

κ

ordinals below

j (κ)

, which still leaves us in the realm of Prikry forcing. Thus fix

d ∈^{< κ} j (κ)

. It is technically useful to assume

κ \in d

. Define the measure

U

by letting for each

A ⊆^{d} κ

A typical function

ν \in A

is of the form

ν : d \to κ

and for each

α, β \in d

such that

α < β

we have

ν (α) < ν (β)

. While it is not terribly important now, it should be observed that we also have

| ν | < ν (κ)

. Define now a condition in Prikry forcing to be of the form

⟨ f, A ⟩

, where

f : d →^{< ω} κ

is a function such that for each

α \in d

we have

f (α)

is increasing, and

A \in U

. Note if

ν \in A

we can assume for that each

α \in d

we have

\max f (α) < ν (α)

. The condition

⟨ f, B ⟩

is said to be a direct extension of the condition

⟨ f, A ⟩

(

⟨ f, B ⟩ ≤^{∗} ⟨ f, A ⟩

) in this forcing if

B \subseteq A

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

. The function

f_{⟨ ν ⟩}

is the function defined by setting for each

α \in d

Set

A_{⟨ ν ⟩} = {μ \in A ∣ μ (κ) > ν (α) for each α \in d}

. Then define the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

to be

⟨ f_{⟨ ν ⟩}, A_{⟨ ν ⟩} ⟩

. We say the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

is a

1

-point extension of

⟨ f, A ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ f, A ⟩

to be

{({⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ g, B ⟩

is stronger than the condition

⟨ f, A ⟩

(

⟨ g, B ⟩ \leq ⟨ f, A ⟩

) if there is

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ g, B ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. The above is still a valid definition of Prikry forcing. Letting

G

be the generic object and defining the function

f_{G} : d →^{ω} κ

by setting for each

α \in d

f_{G} (α) = ⋃ {f (α) ∣ ⟨ f, A ⟩ \in G}

, we get that for each

α \in d

f_{G} (α)

is an

ω

-sequence cofinal in

κ

. Note the function

f_{G}

defined here is found in the generic extension of the standard Prikry forcing.

In fact, one can use in the previous definition also sets

d

of size

κ

. The usefulness of the ultrafilter

U

is more apparent in this case, when one views a typical function in a measure one set. Thus fix

d ∈^{κ} j (κ)

. It is technically useful to assume

κ \in d

. Define the measure

U

by letting for each

A \subseteq ⋃ {^{d^{'}} κ ∣ d^{'} \subseteq d, | d^{'} | < κ}

A typical function

ν \in A

is of the form

ν : dom ν \to κ

(note

dom ν

and not

d

!), where

dom ν \subseteq d

, and for each

α, β \in dom ν

such that

α < β

we have

ν (α) < ν (β)

. Moreover,

| dom ν | < ν (κ)

. Define now a condition in Prikry forcing to be of the form

⟨ f, A ⟩

, where

f : d →^{< ω} κ

is a function such that for each

α \in d

we have

f (α)

is a finite increasing sequence, and

A \in U

. We can always assume that for each

ν \in A

we have

\max f (α) < ν (α)

for each

α \in dom ν

The condition

⟨ f, B ⟩

is said to be a direct extension of the condition

⟨ f, A ⟩

(

⟨ f, B ⟩ ≤^{∗} ⟨ f, A ⟩

) in this forcing if

B \subseteq A

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. Define the function

f_{⟨ ν ⟩}

by setting for each

α \in d

Set

A_{⟨ ν ⟩} = {μ \in A ∣ μ (κ) > ν (α) for each α \in dom ν}

. Then define the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

to be

⟨ f_{⟨ ν ⟩}, A_{⟨ ν ⟩} ⟩

. We say the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

is a

1

-point extension of

⟨ f, A ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ f, A ⟩

to be

{({⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ g, B ⟩

is stronger than the condition

⟨ f, A ⟩

if there is

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ g, B ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. The above is still a valid definition of Prikry forcing. Letting

G

be the generic object and defining the function

f_{G} : d →^{ω} κ

by setting for each

α \in d

f_{G} (α) = ⋃ {f (α) ∣ ⟨ f, A ⟩ \in G, α \in dom f}

, we get that for each

α \in d

f_{G} (α)

is an

ω

-sequence cofinal in

κ

. Defining the function

f_{G}

as in the previous paragraph we get

κ

cofinal

ω

-sequences, but still all of them are generated by

f_{G} (κ)

Since the ultrapower

M

is closed only under

κ

-sequences, one cannot enlarge

d

to be of size greater than

κ

while keeping the nice properties of Prikry type forcing notions. However, we can use conditions with different domains, thus adding sequence corresponding to each of the ordinals below

j (κ)

. The domain change, however, causes the forcing to be non-isomorphic to Prikry forcing. Thus if

d ∈^{κ} j (κ)

then define the measure

U_{d}

by letting for each

A \subseteq ⋃ {^{d^{'}} κ ∣ d^{'} \subseteq d, | d^{'} | < κ}

Define now a condition in the forcing to be of the form

⟨ f, A ⟩

, where

f : dom f →^{< ω} κ

is a function such that for each

α \in dom f

f (α)

is a finite increasing sequence,

dom f ∈^{κ} j (κ)

, and

A \in U_{dom f}

. If

d \subseteq e

and

A \in U_{e}

then set

A↾d = {ν↾d ∣ ν \in A}

. The condition

⟨ g, B ⟩

is said to be a direct extension of the condition

⟨ f, A ⟩

(

⟨ f, B ⟩ ≤^{∗} ⟨ f, A ⟩

) in this forcing if

g \supseteq f

and

B↾ dom f \subseteq A

. Note this definition of the direct order is a major change from all previous definitions. In fact the direct order is a Cohen forcing for adding

j (κ)

subsets to

κ^{+}

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. The function

f_{⟨ ν ⟩}

is defined by setting for each

α \in dom f

Given a set

A \in U_{d}

set

A_{⟨ ν ⟩} = {μ \in A ∣ μ (κ) > ν (α) for each α \in dom ν}

. Then define the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

to be

⟨ f_{⟨ ν ⟩}, A_{⟨ ν ⟩} ⟩

. We say the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

is a

1

-point extension of

⟨ f, A ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ f, A ⟩

to be

{({⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ g, B ⟩

is stronger than the condition

⟨ f, A ⟩

(

⟨ g, B ⟩ \leq ⟨ f, A ⟩

) if there is

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ g, B ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. This forcing notion is no longer Prikry forcing. Using the same definition of

f_{G}

as before we get

j (κ)

cofinal

ω

-sequence into

κ

. However, while each of the sequences appears in a generic extension by Prikry forcing, the function

f_{G}

itself does not belong to a Prikry generic extension.

The point of the previous forcing is that nothing restricts us from using it with elementary embeddings with many generators, thus we get the extender based Prikry forcing. Thus assume

j : V \to M

is an elementary embedding such that

crit (j) = κ

M ⊇^{κ} M

, and

κ < λ < j (κ)

is a cardinal in

V

. Using the previous definition with conditions

⟨ f, A ⟩

such that

dom f ∈^{κ} λ

, we get that

λ

-many new

ω

-sequences cofinal in

κ

appear in the generic extension, thus

2^{κ} = κ^{ω} \geq λ

. Working out the proof we get that no cardinals are collapsed,

2^{κ} = λ

, and

cf κ = ω

The final generalization achieved so far, along the lines above, is to begin with elementary embedding with even more closure properties, i.e.,

j : V \to M

such that

crit (j) = κ

and

M ⊇^{< λ} M

, where

λ > κ

and then work out the definition above to use

d

of arbitrary size below

λ

. This yields a generic extension in which

cf κ = ω

and

2^{κ}

blows up to whatever cardinal the model

M

catches beginning with

λ

up to

j (κ)

. However, the cardinals above

κ

and below

λ

are collapsed in this extension., which is to be expected when using a

< λ

-supercompact cardinal.

Let

E

be an extender as in [8]. Let

ℙE

be the extender based Prikry forcing derived from

E

. We show

ℙE

is cone homogeneous.

Proof. Set $d = dom f^{p_{0}} \cup dom f^{p_{1}}$ . Set $f_{0}^{∗} = f^{p_{0}} \cup {⟨ α, ⟨ ⟩ ⟩ ∣ α \in d ∖ dom f^{p_{0}}}$ and $f_{1}^{∗} = f^{p_{1}} \cup {⟨ α, ⟨ ⟩ ⟩ ∣ α \in d ∖ dom f^{p_{1}}}$ . Choose a set $A \subseteq π_{d, dom f^{p_{0}}}^{- 1} (A^{p_{0}}) \cap π_{d, dom f^{p_{1}}}^{- 1} (A^{p_{1}})$ so that both $p_{0}^{∗} = ⟨ f_{0}^{∗}, A ⟩$ and $p_{1}^{∗} = ⟨ f_{1}^{∗}, A ⟩$ are conditions. Define $π : ℙE ∕ p_{0}^{∗} \to ℙ E ∕ p_{1}^{∗}$ by setting for each $p \leq p_{0}^{∗}$ , $π (p) = ⟨ f_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}^{p_{1}^{∗}} \cup (f^{p} ↾ (dom f^{p} ∖ d)), A^{p} ⟩$ , where $⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A^{p_{0}^{∗}}$ and $p ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{n - 1} ⟩}^{∗}$ . We claim $π$ is an isomorphism. Note the condition $p$ and $π (p)$ are mostly identical. The condition $π (p)$ can differ from $p$ when $α \in d$ and $f^{π (p)} (α)$ differs from $f^{p} (α)$ . Thus the one point which is not trivial is that $π$ is order preserving.

Assume $p \leq q \leq p_{0}^{∗}$ . We show $π (p) \leq π (q)$ . We need to show there is $\vec{ν} ∈^{< ω} A^{π (q)}$ such that $π (p) ≤^{∗} π {(q)}_{⟨ \vec{ν} ⟩}$ . Choose $\vec{ν} \in A^{q} = A^{π (q)}$ such that $p ≤^{∗} q_{⟨ \vec{ν} ⟩}$ . For the measure one sets we get at once

\begin{array}{l} A^{π (p)} ↾ dom f^{q} = A^{p} ↾ dom f^{q} \subseteq A_{⟨ \vec{ν} ⟩}^{q} = A_{⟨ \vec{ν} ⟩}^{π (q)} . \end{array}

For the functions we have the following. If $α \in dom f^{π (p)} ∖ d$ then

\begin{array}{l} f^{π (p)} (α) = f^{p} (α) = f^{q} (α) ⌢ ⟨ \vec{ν} (α) ⟩ = f^{π (q)} (α) ⌢ ⟨ \vec{ν} (α) ⟩ = f^{π {(q)}_{⟨ \vec{ν} ⟩}} (α) . \end{array}

If $α \in d$ then there is $\vec{μ} ∈^{< ω} A^{p_{0}^{∗}} =^{< ω} A^{p_{1}^{∗}}$ such that $q ≤^{∗} p_{0 ⟨ \vec{μ} ⟩}^{∗}$ , thus $p ≤^{∗} p_{0 ⟨ \vec{μ} ⌢ \vec{ν} ⟩}^{∗}$ , hence

\begin{matrix} f^{π (p)} (α) = f^{p_{1 ⟨ \vec{μ} ⌢ \vec{ν} ⟩}^{∗}} (α) = f_{⟨ \vec{μ} ⌢ \vec{ν} ⟩}^{p_{1}^{∗}} (α) = \\ f_{⟨ \vec{ν} ⟩}^{π (q)} (α) = f^{π (q)} (α) ⌢ ⟨ \vec{ν} (α) ⟩ = f^{π {(q)}_{⟨ \vec{ν} ⟩}} (α) . \end{matrix}

□

For a generic filter

G \subseteq ℙE

define the function

f_{G}

by setting

f_{G} (α) = ⋃ {f^{p} (α) ∣ p \in G, α \in dom f^{p}}

Let us define the Easton products we are going to work with. Let

A \subseteq On

be a set of ordinals. Let

ℂ_{χ, A}

be the Easton product of the Cohen forcing notions yielding, in the generic extension, for each

ξ < \sup A

When forcing with

ℂ_{χ, A}

we will choose

χ

to be large enough so as not to interfere with our intended usage. Due to the (cone) homogeneity of

ℙE

, the sequences forced by

ℙE

are not in

{HOD}^{V^{ℙE}}

. We would like to break the homogeneity of

ℙE

so as to have the Prikry sequence enter

{HOD}^{V^{ℙE}}

. We will achieve this by coding the Prikry sequence into the power set function. We will want the Cohen forcing used to be stabilized by reasonable automorphisms of

ℙE

. Let

ℙ_{E (κ)}

be Prikry forcing using the measure

E (κ)

. Define the function

s : ℙE \to ℙ_{E (κ)}

by setting

s (p) = ⟨ f^{p} ↾ {κ}, A^{p} ↾ {κ} ⟩

, where

A^{p} ↾ {κ} = {ν↾ {κ} ∣ ν \in A^{p}}

. Note

ℙ_{E (κ)} \subseteq ℙE

. Assume a pair of conditions

p, q \in ℙ_{E (κ)}

are compatible in

ℙE

. I.e., there is a condition

r ≤_{ℙE} p, q

. Then

s (r) ≤_{ℙE} p, q

, hence

s (r) ≤_{ℙ_{E (κ)}} p, q

. Hence a maximal antichain in

ℙ_{E (κ)}

is also a maximal antichain in

ℙE

, thus the function

s

is a projection. Thus if

G \subseteq ℙE

is generic then

s^{″} G

ℙ_{E (κ)}

-generic.

Until the end of the section set

ℙ = ℙE * {\dot{ℂ}}_{χ, ḟ_{G} (κ)}

Proof. Since $s (p_{0})$ and $s (p_{1})$ are compatible, we can choose conditions $p_{0}^{'} \leq p_{0}$ and $p_{1}^{'} \leq p_{1}$ such that $f^{p_{0}^{'}} ↾ {κ} = f^{p_{1}^{'}} ↾ {κ}$ . By claim 3.1 there are direct extensions $p_{0}^{∗} ≤^{∗} p_{0}^{'}$ and $p_{1}^{∗} ≤^{∗} p_{1}^{'}$ such that $π_{0} : ℙE ∕ p_{0}^{∗} ≃ ℙ E ∕ p_{1}^{∗}$ is an automorphism. Since $ℂ_{χ, f_{G} (κ)} = π (ℂ_{χ, f_{G} (κ)})$ , where $G \subseteq ℙE$ is generic, we are done by claim 2.3. □

Proof. In order to show $⟨ s (p), 1 ⟩ ⊩_{ℙ} φ (α, α_{1}, \dots, α_{n})$ we will show a dense subset of conditions below $⟨ s (p), 1 ⟩$ forces $φ (α, α_{1}, \dots, α_{n})$ . Let $⟨ p_{0}, {\dot{q}}_{0} ⟩ \leq ⟨ s (p), 1 ⟩$ be an arbitrary condition. By claim 3.2 there is $⟨ p_{0}^{'}, {\dot{q}}_{0}^{'} ⟩ \leq ⟨ p_{0}, {\dot{q}}_{0} ⟩$ and $⟨ p_{1}^{'}, {\dot{q}}_{1}^{'} ⟩ \leq ⟨ p, \dot{q} ⟩$ such that $ℙ ∕ p_{0}^{'} * {\dot{q}}_{0}^{'} ≃ ℙ ∕ p_{1}^{'} * {\dot{q}}_{1}^{'}$ . Thus $⟨ p_{0}^{'}, {\dot{q}}_{0}^{'} ⟩ ⊩_{ℙ} φ (α_{1}, \dots, α_{n})$ . □

We will get a special case of theorem 1 by invoking the last corollary in a model of the form

L [A]

Proof. We will begin by defining the forcing notion $R$ so that for an $R$ -generic filter $I$ we will have ${HOD}^{V [I]} = V [I]$ .

Define by induction the forcing notions $⟨ R_{n} ∣ n \leq ω ⟩$ and sets $⟨ A_{n} ∣ n < ω ⟩$ , as follows. Set $R_{0} = 1$ and $A_{0} = A$ . For each $n < ω$ define $R_{n + 1}$ as follows. In $V [G_{n}]$ , where $G_{n} \subseteq R_{n}$ is generic over $V$ , let $ℂ_{n}$ be the forcing notion $ℂ_{χ_{n}, A_{n}}$ for a large enough $χ_{n}$ . Let $A_{n + 1}$ be $ℂ_{n}$ -generic over $V [G_{n}]$ , i.e., $A_{n + 1}$ is a code for $A_{n}$ . Set $R_{n + 1} = R_{n} * {\dot{ℂ}}_{n}$ , where ${\dot{ℂ}}_{n}$ is an $R_{n}$ -name for $ℂ_{n}$ . Let $R$ be the inverse limit of $⟨ R_{n} ∣ n < ω ⟩$ . Let $I \subseteq R$ be generic.

Invoking $corollary 3.4$ inside $V [I]$ and calculating ${HOD}^{V [I] [G] [H]}$ we get $f_{G} (κ) \in {HOD}^{V [I] [G] [H]} \subseteq V [I] [s^{″} G]$ . For each $n < ω$ , $A_{n} \in {HOD}^{V [I] [G] [H]}$ , thus ${HOD}^{V [I] [G] [H]} \supseteq L [A] [I] [s^{″} G] = V [I] [s^{″} G]$ . □

In order to analyze

{HOD}_{{a}}

, where

a \subseteq κ

, let us derive another line of corollaries stemming from claim 3.2. The problem we face when dealing with

{HOD}_{{a}}

is an automorphism

π

ℙ

might move

ȧ

, the name of

a

. Thus we will need to fine tune the projection

s

First we recall the notion of a good pair from [9]. We say the pair

⟨ N, f ⟩

is a good pair if

N ≺ H_{χ}

is a

κ

-internally approachable elementary substructure,

| N | < λ

, and there is a sequence

⟨ ⟨ N_{ξ}, f_{ξ} ⟩ ∣ ξ < κ ⟩

such that

⟨ N_{ξ} ∣ ξ < κ ⟩

witnesses the

κ

-internal approachability of

N

f = ⋃ {f_{ξ} ∣ ξ < κ}

⟨ f_{ξ} ∣ ξ < κ ⟩

is a

≤^{∗}

-decreasing continuous sequence in

ℙ_{f}^{∗}

, and for each

ξ < κ

f_{ξ} \in ⋂ {D \in N_{ξ} ∣ D is a dense open subset of ℙ_{f}^{∗}}

f_{ξ} \subseteq N_{ξ + 1}

, and

f_{ξ} \in N_{ξ + 1}

Set

ℙ_{E}^{N} = {⟨ f, A ⟩ \in ℙ E ∣ dom f \subseteq N}

. Define the function

s_{N} : ℙE \to ℙ_{E}^{N}

by setting for each

p \in ℙE

s_{N} (p) = ⟨ f^{p} ↾N, A^{p} ↾N ⟩

. Note

ℙ_{E}^{N} \subseteq ℙ E

. Fix two conditions

p, q \in ℙ_{E}^{N}

. Assume they are compatible in

ℙE

, i.e., there is a condition

r \in ℙE

such that

r ≤_{ℙE} p, q

. Thus there are

\vec{ν} ∈^{< ω} A^{p}

and

\vec{μ} ∈^{< ω} A^{q}

such that

r ≤_{ℙE}^{∗} p_{⟨ \vec{ν} ⟩}, q_{⟨ \vec{μ} ⟩}

. Immediately we get

s_{N} (r) ≤_{ℙ_{E}^{N}}^{∗} p_{⟨ \vec{ν} ⟩}, q_{⟨ \vec{μ} ⟩}

. Hence a maximal antichain in

ℙ_{E}^{N}

is a maximal antichain in

ℙE

, hence the function

s_{N}

is a projection.

Proof. In order to show $⟨ s_{N} (p), 1 ⟩ ⊩_{ℙ} φ (α, α_{1}, \dots, α_{n}, ȧ)$ we will show a dense subset of conditions below $⟨ s_{N} (p), 1 ⟩$ forces $φ (α, α_{1}, \dots, α_{n}, ȧ)$ .

Let $⟨ p_{0}, {\dot{q}}_{0} ⟩ \leq ⟨ s_{N} (p), 1 ⟩$ be arbitrary condition. We can choose $p_{1} \leq p$ such that $s_{N} (p_{0}) = s_{N} (p_{1})$ . By claim 3.1 there is $p_{0}^{∗} ≤^{∗} p_{0}$ and $p_{1}^{∗} ≤^{∗} p_{1}$ such that $ℙE ∕ p_{0}^{∗} ≃ ℙ E ∕ p_{1}^{∗}$ .

Recall that if $r \leq p^{∗}$ , $α < κ$ , and $r ⊩_{ℙE} “ α \in ȧ ”$ , then $p_{⟨ ν_{0}, \dots, ν_{l - 1} ⟩}^{∗} ⊩ “ α \in ȧ ”$ , where $⟨ ν_{0}, \dots, ν_{l - 1} ⟩ ∈^{< ω} A^{p^{∗}}$ is such that $r ≤^{∗} p_{⟨ ν_{0}, \dots, ν_{l - 1} ⟩}^{∗}$ . Thus for each $⟨ ν_{0}, \dots, ν_{l - 1} ⟩ \in A^{p_{0}^{∗}} = A^{p_{1}^{∗}}$ , $α < κ$ , and $r \in ℙE ∕ p_{0}^{∗}$ ,

\begin{array}{l} r ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{l - 1} ⟩}^{∗} and r ⊩_{ℙE} “ α \in ȧ ” \Leftrightarrow \\ p_{⟨ ν_{0}, \dots, ν_{l - 1} ⟩ ↾ dom f^{p}} ⊩_{ℙE} “ α \in ȧ ” \Leftrightarrow \\ π (r) ≤^{∗} p_{1 ⟨ ν_{0}, \dots, ν_{l - 1} ⟩}^{∗} and π (r) ⊩_{ℙE} “ α \in π (ȧ) ” . \end{array}

Thus $p_{0}^{∗} ⊩ “ ȧ = π^{- 1} (ȧ) ”$ . Use claim 3.2 to find stronger conditions $⟨ p_{0}^{'}, {\dot{q}}_{0}^{'} ⟩ \leq ⟨ p_{0}^{∗}, {\dot{q}}_{0} ⟩$ and $⟨ p_{1}^{'}, {\dot{q}}_{1}^{'} ⟩ \leq ⟨ p_{0}^{∗}, \dot{q} ⟩$ such that $\tilde{π} : ℙ ∕ p_{0}^{'} * {\dot{q}}_{0}^{'} ≃ ℙ ∕ p_{1}^{'} * {\dot{q}}_{1}^{'}$ is an automorphism. Since $⟨ p_{1}^{'}, {\dot{q}}_{1}^{'} ⟩ ⊩_{ℙ} φ (α_{1}, \dots, α_{n}, ȧ)$ we get $⟨ p_{0}^{'}, {\dot{q}}_{0}^{'} ⟩ ⊩_{ℙ} φ (α_{1}, \dots, α_{n}, π^{- 1} (ȧ))$ . We are done since $p_{0}^{'} ⊩ “ ȧ = π^{- 1} (ȧ) ”$ . □

We will get theorem 1 by beginning with a model where

HOD \supseteq V_{λ + 2}

. For this let us define the following coding. Let

𝔄 = ⟨ A_{α} ∣ α < λ^{+ 3} ⟩

be an enumeration of all subsets of

λ^{++}

. Let

ℂ_{χ, 𝔄}

be the Easton product of the Cohen forcing notions yielding, in the generic extension, for each

α < λ^{+ 3}

and

ξ < λ^{++}

Proof. Let $U \in V$ be a measure on $λ$ . Then $U \in V_{λ + 2}$ , hence $U \in {HOD}^{V [I]}$ , where $I$ is $C_{χ, 𝔄}$ -generic.

Working in $V [I]$ let $G * H$ be $ℙ$ -generic. By corollary 3.8 there is $X \subseteq dom E$ such that $| X | < λ$ , $X \in V [I]$ , and $f_{G} (κ) \in {HOD}_{{a}}^{V [I] [G * H]} \subseteq V [I] [s_{X}^{″} G]$ . The filter $s_{X}^{″} G$ is $s_{X}^{″} ℙ E$ -generic. Since $| X | < λ$ we have $| s_{X}^{″} ℙ E | < λ$ , hence any measure (in $V$ ) over $λ$ trivially lifts to a measure in $V [s_{X} (G)]$ over $λ$ . In particular $U$ lifts to $\bar{\bar{U}}$ , which is definable by $\bar{\bar{U}} = {B \in V [I] [s_{X}^{″} G] \cap 𝒫 (λ) ∣ \exists A \in U B \supseteq A}$ . Since $U \in {HOD}_{{a}}^{V [I] [G * H]}$ we can define in ${HOD}_{{a}}^{V [I] [G * H]}$ , $\bar{U} = {B \in {HOD}_{{a}}^{V [I] [G * H]} \cap 𝒫 (λ) ∣ \exists A \in U B \supseteq A}$ . Since ${HOD}_{{a}}^{V [I] [G * H]} \subseteq V [I] [s_{X}^{″} G]$ we necessarily have $\bar{U} \subseteq \bar{\bar{U}}$ . Thus $\bar{U}$ is a measure on $λ$ in ${HOD}_{{a}}^{V [I] [G * H]}$ . □

4. The global result

In this section we prove theorem 2. The extender based Radin forcing was originally developed in [7]. We use a generalization of the forcing where the extenders can witness supercompactness. This was developed in [9]. Since the introduction in the previous section was very detailed, we will give here only our version of Radin forcing.

Let us begin with with defining the Magidor forcing [6] using two measures. Assume

U_{0}^{'} ◃ U_{1}^{'}

are two normal measures over

κ

. For each

i < 2

let

j_{i} : V \to M_{i} ≃ Ult (V, U_{i}^{'})

be the natural elementary embeddings. Define the measure

U_{0}

by letting for each

A ⊆^{{κ}} κ

Note a typical function

ν \in A

is of the form

ν : {κ} \to κ

. Define the measure

U_{1}

by letting for each

A ⊆^{{κ}} V_{κ}

A typical function

ν \in A

is of the form

ν : {κ} \to V_{κ}

, where

ν (κ) = ⟨ ξ, μ ⟩

and

μ

is a measure over

ξ

. Define by recursion the conditions and ordering of the forcing notion as follows. A basic condition in Magidor forcing is of the form

⟨ f, A ⟩

, where

A \in U_{0} \cap U_{1}

and

f : {κ} \to V_{κ}

is a function such that

f (κ) = ⟨ ⟨ ξ_{0}, μ_{0} ⟩, \dots, ⟨ ξ_{k - 1}, μ_{k - 1} ⟩, ⟨ ξ_{k} ⟩, \dots, ⟨ ξ_{n - 1} ⟩ ⟩

, where

ξ_{0} < \dots < ξ_{n - 1} < κ

and for each

i < k

μ_{i}

is a measure over

ξ_{i}

. A sequence of the form

⟨ ⟨ ξ_{0}, μ_{0} ⟩, \dots, ⟨ ξ_{k - 1}, μ_{k - 1} ⟩, ⟨ ξ_{k} ⟩, \dots, ⟨ ξ_{n - 1} ⟩ ⟩

is said to be

o

-decreasing since we consider

o (⟨ ξ_{i}, μ_{i} ⟩) = 1

and

o (⟨ ξ_{i} ⟩) = 0

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. We define the functions

f_{⟨ ν ⟩ ↓}

and

f_{⟨ ν ⟩ ↑}

as follows. Assume

o (ν) = 0

. In this case we work essentialy as in the Prikry forcing case. We let

f_{⟨ ν ⟩ ↓} = \emptyset

. Define the function

f_{⟨ ν ⟩ ↑}

by letting

f_{⟨ ν ⟩ ↑} (κ) = f (κ) ⌢ ⟨ ν (κ) ⟩

. Note that since

o (ν) = 0

the sequence

f (κ) ⌢ ⟨ ν (κ) ⟩

o

-decreasing if

f (κ)

o

-decreasing. Assume

ν \in A

is a function such that

o (ν) = 1

. In this case we define two functions

f_{⟨ ν ⟩ ↑}

and

f_{⟨ ν ⟩ ↓}

. If we would have let

f_{⟨ ν ⟩ ↑} (κ) = f (ν) ⌢ ⟨ ν (κ) ⟩

then we might have ended with a non

o

-decreasing sequence. Thus we cut the possible problematic tail of

f (κ)

as follows. Set

l = \max {l^{'} ∣ o (f_{l^{'}} (κ)) = 1} + 1

. If the set over which the

\max

above is operating is empty then set

l = 0

. Then let

f_{⟨ ν ⟩ ↑} (κ) = f (κ) ↾l ⌢ ⟨ ν (κ) ⟩

. Whatever is the value of

o (ν)

let

A_{⟨ ν ⟩ ↑} = {τ \in A ∣ \ddot{τ} (κ) > \ddot{ν} (κ)}

. The tail removed from

f (κ)

is ‘pushed down’ by letting

f_{⟨ ν ⟩ ↓} : {\ddot{ν} (κ)} \to \ddot{ν}

be a function such that

f_{⟨ ν ⟩ ↓} (\ddot{ν}) = f (κ) ∖ l

, where

\ddot{ν}

ξ

ν = ⟨ ξ, μ ⟩

. Together with the ‘pushed down function’ we set the pushed down part of

A

to be

A_{⟨ ν ⟩ ↓} = {τ ↓ ν ∣ τ \in A, o (τ) = 0, \ddot{τ} < \ddot{ν}}

, where

τ ↓ ν (ξ) = τ (ξ)

. Finally set

{⟨ f, A ⟩}_{⟨ ν ⟩ ↑} = ⟨ f_{⟨ ν ⟩ ↑}, A_{⟨ ν ⟩ ↑} ⟩

and

{⟨ f, A ⟩}_{⟨ ν ⟩ ↓} = ⟨ f_{⟨ ν ⟩ ↓}, A_{⟨ ν ⟩ ↓} ⟩

. Note

{⟨ f, A ⟩}_{⟨ ν ⟩ ↓}

is a condition in a Prikry forcing. A 1-point extension of

⟨ f, A ⟩

{⟨ f, A ⟩}_{⟨ ν ⟩} = {⟨ f, A ⟩}_{⟨ ν ⟩ ↓} ⌢ {⟨ f, A ⟩}_{⟨ ν ⟩ ↑}

Assume

G

is generic with

⟨ f^{∗}, A^{∗} ⟩ \in G

, where

f^{∗} (κ) = ⟨ ⟩

. Letting

f_{G} (κ) = ⋃ {f (κ) ∣ s ⌢ ⟨ f, A ⟩ \in G}

and

{\ddot{f}}_{G} (κ) = ⟨ \ddot{ν} ∣ ν \in f_{G} (κ) ⟩

we get that

{\ddot{f}}_{G} (κ)

is an

ω^{2}

sequence cofinal in

κ

. Moreover if

s ⌢ ⟨ g, B ⟩ ⌢ t ⌢ ⟨ f, A ⟩ \in G

then setting

g_{G} (κ) = ⋃ {⟨ g^{'}, B^{'} ⟩ \leq ⟨ g, B ⟩ ∣ s^{'} ⌢ ⟨ g^{'}, B^{'} ⟩ ⌢ t^{'} ⌢ ⟨ f, A ⟩ \in G}

and

{\ddot{g}}_{G} (τ) = ⟨ \ddot{ν} ∣ ν \in g_{G} (κ) ⟩

. Then

\ddot{g} (τ)

is an

ω

-sequence cofinal in

dom g

Let us switch to the extender based Magidor forcing using two extenders. Assume

E_{0}^{'} ◃ E_{1}^{'}

are two extenders over

κ

. For each

i < 2

let

j_{i} : V \to M_{i} ≃ Ult (V, E_{i}^{'})

be the natural elementary embeddings.

For each

d ∈^{κ} j (κ)

such that

κ \in d

define the measure

E_{0} (d)

as follows. For each

A \subseteq ⋃ {^{d^{'}} κ ∣ d^{'} \subseteq d, | d^{'} | < κ}

A typical function

ν \in A

is of the form

ν : dom ν \to κ

where

dom ν \subseteq d

, and for each

α, β \in dom ν

such that

α < β

we have

\ddot{ν} (α) < \ddot{ν} (β)

. Moreover,

| dom ν | < ν (κ)

. For each

d ∈^{κ} j_{1} (κ)

such that

κ \in d

define the ultrafilter

E_{1} (d)

as follows. For each

A \subseteq ⋃ {^{d^{'}} V_{κ} ∣ d^{'} \subseteq d, | d^{'} | < κ}

A typical function

ν \in A

is of the form

ν : dom ν \to V_{κ}

where

dom ν \subseteq d

, and for each

α, β \in dom ν

such that

α < β

we have

\ddot{ν} (α) < \ddot{ν} (β)

. Moreover,

| dom ν | < ν (κ)

. Define by recursion the conditions and order on the forcing notion as follows. A basic condition in the extender based Magidor forcing is of the form

⟨ f, A ⟩

, where

f : d →^{< ω} V_{κ}

is a function such that for each

α \in d

we have

f (α)

is a finite

o

-decreasing sequence, and

A \in E_{0} (d) \cap E_{1} (d)

. We can always assume that for each

ν \in A

we have

\max f (α) < \ddot{ν} (α)

for each

α \in dom ν

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. We define the functions

f_{⟨ ν ⟩ ↓}

and

f_{⟨ ν ⟩ ↑}

, employing the same idea used on

f (κ)

to each of the

f (α)

’s, as follows. Assume

o (ν) = 0

. Let

f_{⟨ ν ⟩ ↓} = \emptyset

. Define the function

f_{⟨ ν ⟩ ↑}

by setting for each

α \in d

Assume

o (ν) = 1

. Define the function

f_{⟨ ν ⟩ ↑}

by setting for each

α \in d

Let

f_{⟨ ν ⟩ ↓} : ran \ddot{ν} \to V_{\ddot{ν} (κ)}

be the function defined by setting for each

α \in dom ν

f_{⟨ \ddot{ν} (α) ⟩} = f (α) ∖ l_{α}

. Set

A_{⟨ ν ⟩ ↑} = {τ \in A ∣ \ddot{τ} (κ) > \ddot{ν} (α) for each α \in dom ν}

. If

o (ν) = 0

then set

A_{⟨ ν ⟩ ↓} = ⟨ ⟩

. If

o (ν) = 1

then set

A_{⟨ ν ⟩ ↓} = {τ ↓ ν ∣ τ \in A, o (τ) = 0, dom τ \subseteq dom ν, \ddot{τ} (α) < \ddot{ν} (κ) for each α \in dom τ}

, where

τ ↓ ν : ran \ddot{τ} \to \ddot{ν} (κ)

defined by setting for each

α \in dom τ

τ ↓ ν (\ddot{ν} (α)) = τ (α)

. Then define

{⟨ f, A ⟩}_{⟨ ν ⟩ ↑}

and

{⟨ f, A ⟩}_{⟨ ν ⟩ ↑}

to be

⟨ f_{⟨ ν ⟩ ↑}, A_{⟨ ν ⟩ ↑} ⟩

and

⟨ f_{⟨ ν ⟩ ↓}, A_{⟨ ν ⟩ ↓} ⟩

, respectively. We say the condition

s^{'} ⌢ ⟨ f^{'}, A^{'} ⟩

is stronger than the condition

s ⌢ ⟨ f, A ⟩

(

s^{'} ⌢ ⟨ f^{'}, A^{'} ⟩ \leq s ⌢ ⟨ f, A ⟩

), if

s^{'} \leq s

and

⟨ f^{'}, A^{'} ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ \vec{ν} ⟩}

Assume

G

is generic with

⟨ f^{∗}, A^{∗} ⟩ \in G

, where

f (κ) = ⟨ ⟩

. Letting

f_{G} (α) = ⋃ {f (α) ∣ s ⌢ ⟨ f, A ⟩ \in G}

and

\ddot{f} (α) = ⟨ \ddot{ν} ∣ ν \in f_{G} (α) ⟩

we get that

\ddot{f} (α)

is an

ω^{2}

sequence cofinal in

κ

. Moreover if

s ⌢ ⟨ g, B ⟩ ⌢ t ⌢ ⟨ f, A ⟩ \in G

then setting

g_{G} (τ) = ⋃ {⟨ g^{'}, B^{'} ⟩ \leq ⟨ g, B ⟩ ∣ s^{'} ⌢ ⟨ g^{'}, B^{'} ⟩ ⌢ t^{'} ⌢ ⟨ f, A ⟩ \in G}

and

{\ddot{g}}_{G} (τ) = ⟨ \ddot{ν} ∣ ν \in g_{G} (τ) ⟩

. Then

\ddot{g} (τ)

is an

ω

-sequence cofinal in

τ

. Note there are

| j_{1} (κ) |

new

ω^{2}

-sequences cofinal into

κ

. For each of the reflections down we get the reflected amount of

ω

-sequences. E.g., if

| j_{0} (κ) | = κ^{+ 3}

then there are

τ_{n}^{+ 3}

new

ω

-sequences cofinal in

τ_{n}

Letting

G

be the generic object and defining the function

f_{G} : d →^{ω} κ

by setting for each

α \in d

f_{G} (α) = ⋃ {f (α) ∣ ⟨ f, A ⟩ \in G, α \in dom f}

, we get that for each

α \in d

f_{G} (α)

is an

ω

-sequence cofinal in

κ

. Defining the function

f_{G}

as in the previous paragraph we get

κ

cofinal

ω

-sequences, but still all of them are generated by

f_{G} (κ)

Since the ultrapower

M

is closed only under

κ

-sequences, one cannot enlarge

d

to be of size greater than

κ

while keeping the nice properties of Prikry type forcing notions. However, we can use conditions with different domains, thus adding sequence corresponding to each of the ordinals below

j (κ)

. The domain change, however, causes the forcing to be non-isomorphic to Prikry forcing. Thus if

d ∈^{κ} j (κ)

then define the measure

U_{d}

by letting for each

A \subseteq ⋃ {^{d^{'}} κ ∣ d^{'} \subseteq d}

Define now a condition in the forcing to be of the form

⟨ f, A ⟩

, where

f : dom f →^{< ω} κ

is a function such that for each

α \in dom f

f (α)

is a finite increasing sequence,

dom f ∈^{κ} j (κ)

, and

A \in U_{dom f}

. If

d \subseteq e

and

A \in U_{e}

then set

A↾d = {ν↾d ∣ ν \in A}

. The condition

⟨ g, B ⟩

is said to be a direct extension of the condition

⟨ f, A ⟩

(

⟨ f, B ⟩ ≤^{∗} ⟨ f, A ⟩

) in this forcing if

g \supseteq f

and

B↾ dom f \subseteq A

. Note this definition of the direct order is a major change from all previous definitions. In fact the direct order is a Cohen forcing for adding

j (κ)

subsets to

κ^{+}

. Assume

⟨ f, A ⟩

is a condition and

ν \in A

is a function. The function

f_{⟨ ν ⟩}

is defined by setting for each

α \in dom f

Given a set

A \in U_{d}

set

A_{⟨ ν ⟩} = {μ \in A ∣ μ (κ) > ν (α) for each α \in dom ν}

. Then define the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

to be

⟨ f_{⟨ ν ⟩}, A_{⟨ ν ⟩} ⟩

. We say the condition

{⟨ f, A ⟩}_{⟨ ν ⟩}

is a

1

-point extension of

⟨ f, A ⟩

. By recursion define the

n + 1

-point extension of the condition

⟨ f, A ⟩

to be

{({⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩})}_{⟨ ν_{n} ⟩}

. We say the condition

⟨ g, B ⟩

is stronger than the condition

⟨ f, A ⟩

(

⟨ g, B ⟩ \leq ⟨ f, A ⟩

) if there is

⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} A

such that

⟨ g, B ⟩ ≤^{∗} {⟨ f, A ⟩}_{⟨ ν_{0}, \dots, ν_{n - 1} ⟩}

. This forcing notion is no longer Prikry forcing. Using the same definition of

f_{G}

as before we get

j (κ)

cofinal

ω

-sequence into

κ

. However, while each of the sequences appears in a generic extension by Prikry forcing, the function

f_{G}

itself does not below to a Prikry generic extension.

The point of the previous forcing is that nothing restricts us from using it with elementary embeddings with many generators, thus we get the extender based Prikry forcing. Thus assume

j : V \to M

is an elementary embedding such that

crit (j) = κ

M ⊇^{κ} M

, and

κ < λ < j (κ)

is a cardinal in

V

. Using the previous definition with conditions

⟨ f, A ⟩

such that

dom f ∈^{κ} λ

, we get that

λ

new

ω

-sequences cofinal in

κ

appear in the generic extension, thus

2^{κ} = κ^{ω} \geq λ

. Working out the proof we get that no cardinals are collapsed,

2^{κ} = λ

, and

cf κ = ω

The final generalization achieved so far is to begin with elementary embedding with even more closure properties, i.e.,

j : V \to M

such that

crit (j) = κ

and

M ⊇^{< λ} M

, where

λ > κ

and then work out the definition above to use

d

of arbitrary size below

λ

. This yields a generic extension in which

cf κ = ω

and

2^{κ}

blows up to whatever cardinal the model

M

catches beginning with

λ

up to

j (κ)

. However, the cardinals above

κ

and below

λ

are collapsed in this extension.

Thus throughout this section assume

\vec{E} = ⟨ E_{ξ} ∣ ξ < λ ⟩

is a Mitchell increasing sequence of extenders such that

λ

is measurable, and for each

ξ < λ

crit (j_{ξ}) = κ

M_{ξ} ⊇^{< λ} M_{ξ}

, and

M_{ξ} \supseteq V_{λ + 2}

, where

j_{ξ} : V \to Ult (V, E_{ξ}) ≃ M_{ξ}

is the natural embedding. (We demand

M_{ξ} \supseteq V_{λ + 2}

since we want

λ

to be measurable in all ultrapowers, not only in

V

Let

ℙ_{\vec{E}}

be the supercompact extender based Radin forcing using

\vec{E}

. (see [9]).

Let us recall the cardinal structure in

V^{ℙ_{\vec{E}}}

κ

remains an inaccessible cardinal, hence

{(V_{κ})}^{V^{ℙ_{\vec{E}}}}

is a model of ZFC. while

λ

remains a cardinal, the cardinals between

κ

and

λ

are collapsed. Both

κ

and

λ

are reflected down using the different extenders. Let

τ_{κ}

be reflection of

κ

which a limit cardinal in

V^{ℙ_{\vec{E}}}

. Let

τ_{λ}

be the matching reflection of

λ

. Then

τ_{λ}

is preserved while the

V

-cardinals between

τ_{κ}

and

τ_{λ}

are collapsed.

Proof. Set $d = dom f^{p_{0}} \cup dom f^{p_{1}}$ . Set $f_{0}^{∗} = f^{p_{0}} \cup {⟨ α, ⟨ ⟩ ⟩ ∣ α \in d ∖ dom f^{p_{0}}}$ and $f_{1}^{∗} = f^{p_{1}} \cup {⟨ α, ⟨ ⟩ ⟩ ∣ α \in d ∖ dom f^{p_{1}}}$ . Choose a set $T$ so that $p_{0}^{∗} = ⟨ f_{0}^{∗}, T ⟩$ and $p_{1}^{∗} = ⟨ f_{1}^{∗}, T ⟩$ are conditions, $T↾ dom f^{p^{0}} \subseteq T^{p^{0}}$ and $T↾ dom f^{p^{1}} \subseteq T^{p^{1}}$ . Define the isomorphism $π : ℙ_{\vec{E}} ∕ p_{0}^{∗} \to ℙ_{\vec{E}} ∕ p_{1}^{∗}$ as follows. Thus assume $p^{0} \leq p_{0}^{∗}$ . By the definition of the order there is $⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} T^{p_{0}^{∗}}$ such that $p^{0} ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{n - 1} ⟩}^{∗}$ . I.e., $p^{0} = p_{0}^{0} ⌢ \dots ⌢ p_{n}^{0}$ , where $p_{i}^{0} ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{i - 1} ⟩ ↑ ⟨ ν_{i} ⟩ ↓}^{∗}$ for each $i < n$ , and $p_{n}^{0} ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{n} ⟩ ↑}^{∗}$ . Consider the condition $p_{1 ⟨ ν_{0}, \dots, ν_{n - 1} ⟩}^{∗} = p_{1, 0}^{∗} ⌢ \dots ⌢ p_{1, n}^{∗}$ . Note $dom f^{p_{i}^{0}} \supseteq dom f_{1, i}^{p^{∗}}$ . Let $p_{i}^{1} = ⟨ f_{i}^{1}, T^{p_{i}^{0}} ⟩$ , where $f_{i}^{1} = f^{p_{1, i}^{∗}} \cup f^{p_{i}^{0}} ↾ (dom f^{p_{i}^{0}} ∖ dom f^{p_{1, i}^{∗}})$ . Finally set $π (p^{0}) = p_{0}^{1} ⌢ \dots ⌢ p_{n}^{1}$ . Let us show the function $π$ is order preserving. Fix $q \leq p \leq p_{0}^{∗}$ . We will show $π (q) \leq π (p)$ .

Since $p \leq p_{0}^{∗}$ there is $⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ∈^{< ω} T^{p_{0}^{∗}}$ such that $p = p_{0} ⌢ \dots ⌢ p_{n}$ , where $p_{i} ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{i - 1} ⟩ ↑ ⟨ ν_{i} ⟩ ↓}^{∗}$ for each $i < n$ , and $p_{n} ≤^{∗} p_{0 ⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ↑}^{∗}$ . Since $q \leq p_{0}^{∗}$ there is $⟨ μ_{0}, \dots, μ_{m - 1} ⟩ ∈^{< ω} T^{p_{0}^{∗}}$ such that $q = q_{0} ⌢ \dots ⌢ q_{m}$ , where $q_{i} ≤^{∗} p_{0 ⟨ μ_{0}, \dots, μ_{i - 1} ⟩ ↑ ⟨ μ_{i} ⟩ ↓}^{∗}$ for each $i < m$ , and $q_{m} ≤^{∗} p_{0 ⟨ μ_{0}, \dots, ν_{m - 1} ⟩ ↑}^{∗}$ . Thus $π (p) = p^{'} = p_{0}^{'} ⌢ \dots ⌢ p_{n}^{'}$ and $π (q) = q^{'} = q_{0}^{'} ⌢ \dots ⌢ q_{m}^{'}$ , where

\begin{array}{l} f^{p_{i}^{'}} = f^{p_{0 ⟨ ν_{0}, \dots, ν_{i - 1} ⟩ ↑ ⟨ ν_{i} ⟩ ↓}^{∗}} \cup f^{p_{i}} ↾ (dom f^{p_{i}} ∖ dom f^{p_{0, i}^{∗}}) for each i < n, \\ f^{p_{n}^{'}} = f^{p_{0 ⟨ ν_{0}, \dots, ν_{n - 1} ⟩ ↑}^{∗}} \cup f^{p_{n}} ↾ (dom f^{p_{n}} ∖ dom f^{p_{0}^{∗}}), \\ T^{p_{i}^{'}} = T^{p_{i}} for each i \leq n, \\ f^{q_{i}^{'}} = f^{p_{0 ⟨ μ_{0}, \dots, μ_{i - 1} ⟩ ↑ ⟨ μ_{i} ⟩ ↓}^{∗}} \cup f^{q_{i}} ↾ (dom f^{p_{i}} ∖ dom f^{p_{0, i}^{∗}}) for each i < m, \\ f^{q_{m}^{'}} = f^{p_{0 ⟨ ν_{0}, \dots, ν_{m - 1} ⟩ ↑}^{∗}} \cup f^{q_{m}} ↾ (dom f^{q_{n}} ∖ dom f^{p_{0}^{∗}}), \\ and \\ T^{q_{i}^{'}} = T^{q_{i}} for each i \leq m . \end{array}

Since $q \leq p$ there $k < ω$ such that $q_{0} ⌢ \dots ⌢ q_{k} \leq p_{0}$ . Thus there is $⟨ τ_{0}, \dots, τ_{k - 1} ⟩ ∈^{< ω} T^{p_{0}}$ such that $q_{0} ⌢ \dots ⌢ q_{k} ≤^{∗} p_{0 ⟨ τ_{0}, \dots, τ_{k - 1} ⟩}$ . I.e., $q_{i} ≤^{∗} p_{0 ⟨ τ_{0}, \dots, τ_{i - 1} ⟩ ↑ ⟨ τ_{i} ⟩ ↓}$ for each $i < k$ , and $q_{k} ≤^{∗} p_{0 ⟨ τ_{0}, \dots, τ_{k - 1} ⟩ ↑}$ . Noting that $p_{0 ⟨ μ_{0}, \dots, μ_{i - 1} ⟩ ↑ ⟨ μ_{i} ⟩ ↓}^{∗} = p_{0 ⟨ ν_{0} ⟩ ↓ ⟨ τ_{0}, \dots, τ_{i - 1} ⟩ ↑ ⟨ τ_{i} ⟩ ↓}^{∗}$ for each $i < k$ , and $p_{0 ⟨ μ_{0}, \dots, μ_{k - 1} ⟩ ↑}^{∗} = p_{0 ⟨ ν_{0} ⟩ ↓ ⟨ τ_{0}, \dots, τ_{k - 1} ⟩ ↑}^{∗}$ , we conclude that $q_{0}^{'} ⌢ \dots ⌢ q_{k}^{'} ≤^{∗} p_{0 ⟨ τ_{0}, \dots, τ_{k - 1} ⟩}^{'}$ , hence $q_{0}^{'} ⌢ \dots ⌢ q_{k}^{'} \leq p_{0}^{'}$ .

Proceeding as above for each $p_{i}$ , (e.g., there is $k^{1} \leq ω$ such that $q_{k + 1} ⌢ \dots ⌢ q_{k^{1}} \leq p_{1}$ ) we get that $q^{'} \leq p^{'}$ . □

Recall that for a condition

p = p_{0} ⌢ \dots ⌢ p_{n}

we have

ℙ_{\vec{E}} ∕ p ≃ ℙ_{{\vec{e}}_{0}} ∕ p_{0} \dots ⌢ ℙ_{{\vec{e}}_{n}} ∕ p_{n}

, where

p_{i} \in ℙ_{{\vec{e}}_{i}}^{∗}

and

{\vec{e}}_{n} = \vec{E}

. Thus the following is an immediate corollary of the above lemma by recursion.

For a condition

p \in ℙ_{\vec{E}}^{∗}

define its projection

s (p)

to the normal measure by setting

s (p) = ⟨ f^{p} ↾ {κ}, T^{p} ↾ {κ} ⟩

. Define by recursion the projection of arbitrary condition

p = p_{0} ⌢ \dots ⌢ p_{n} \in ℙ_{\vec{E}}

by setting

s (p) = s (p_{0} ⌢ \dots ⌢ p_{n - 1}) ⌢ s (p_{n})

. It is obvious

s^{″} ℙ_{\vec{E}}

is the Radin forcing using the measures

⟨ E_{ξ} (κ) ∣ ξ < o (\vec{E}) ⟩

. Moreover, if

G

ℙ_{\vec{E}}

-generic then

s^{″} G

s^{″} ℙ_{\vec{E}}

-generic.

Let

G

ℙ_{\vec{E}}

-generic. Work in

V [G]

. Let

⟨ κ_{α} ∣ α < κ ⟩

be the increasing enumeration of

f_{G} (κ)

. Define the sequence

⟨ μ_{α}, U_{α} ∣ α < κ ⟩

by setting for each

α < κ

Note: If

α

is limit, then

μ_{α} = κ_{α}^{+}

is measurable in

V

since it is a reflection of

λ

being measurable in one of the

V

-ultrapowers. On the other hand, if

α

is successor then

μ_{α} = κ_{α}

is measurable in

V

since

E_{0}

concentrates on measurables. Thus for each

α < κ

we can choose

U_{α} \in V

which is a measure in

V

over

μ_{α}

. Define the backward Easton iteration

⟨ P_{α}, {\dot{Q}}_{β} ∣ α \leq κ, β < κ ⟩

by setting for each

α < κ

{\dot{Q}}_{α} = Col (μ_{α}, < κ_{α + 1})

. By theorem 2.2 the iteration

P_{κ}

is cone homogeneous. Let

H \subseteq P_{κ}

be generic.

Working in

V [G * H]

we want to pull into the

HOD

of a generic extension the measures

U_{α}

’s. Define the backward Easton iteration

⟨ R_{α}, Ṡ_{β} ∣ α \leq κ, β < κ ⟩

by setting for each

β < κ

Ṡ_{β} = C_{χ_{β}, 𝔄_{β}}

, where,

𝔄_{β} = {A \in V ∣ A \subseteq {(μ_{β}^{++})}_{V}}

and

\sup_{γ < β} χ_{γ} < χ_{β} < κ

. By theorem 2.2

R_{κ}

is cone homogeneous.

One final definition is in order before the following claim. If

p \in ℙ_{\vec{E}}^{∗}

then set

κ (p) = ran f^{p} (κ)

. If

p = p_{0} ⌢ \dots ⌢ p_{n} \in ℙ_{\vec{E}}

then set by recursion

κ (p) = κ (p_{0} ⌢ \dots ⌢ p_{n - 1}) ⌢ κ (p_{n})

. Note

κ (p)

is the subset of

f_{G} (κ)

decided by the condition

p

Proof. Since $s (p_{0})$ and $s (p_{1})$ are compatible there are stronger conditions $p_{0}^{'} \leq p_{0}$ and $p_{1}^{'} \leq p_{1}$ and Mitchell increasing sequences ${{\vec{e}}_{i} ∣ i \leq k}$ such that $p_{0}^{'}, p_{1}^{'} \in \prod_{i \leq k} ℙ_{\vec{e_{i}}}$ and $κ (p_{0}^{'}) = κ (p_{1}^{'})$ . By the previous corollary there are direct extensions $p_{0}^{∗} ≤^{∗} p_{0}^{'}$ and $p_{1}^{∗} ≤^{∗} p_{1}^{'}$ such that $π : ℙ_{\vec{E}} ∕ p_{0}^{∗} ≃ ℙ_{\vec{E}} ∕ p_{1}^{∗}$ . Most importantly we have $π (Ṗ_{κ} * {\dot{Q}}_{κ}) = Ṗ_{κ} * {\dot{Q}}_{κ}$ is cone homogeneous. Thus by claim 2.3 we are done. □

Proof. We will prove a dense subset of conditions below $⟨ s (p), 1, 1 ⟩$ force $φ (α_{0}, \dots, α_{l})$ . Assume $⟨ p^{0}, {\dot{q}}^{0}, ṙ^{0} ⟩ \leq ⟨ s (p), 1, 1 ⟩$ . Trivially $s (p^{0})$ and $s (p)$ are compatible, hence by the previous corollary there are stronger conditions $⟨ p^{0 *}, {\dot{q}}^{0 *}, ṙ^{0 *} ⟩ \leq ⟨ p^{0}, {\dot{q}}^{0}, ṙ^{0} ⟩$ and $⟨ p^{1 *}, {\dot{q}}^{1 *}, ṙ^{1 *} ⟩ \leq ⟨ p, \dot{q}, ṙ ⟩$ such that $ℙ ∕ ⟨ p^{0 *}, {\dot{q}}^{0 *}, ṙ^{0 *} ⟩ ≃ ℙ ∕ ⟨ p^{1 *}, {\dot{q}}^{1 *}, ṙ^{1 *} ⟩$ . Necessarily $⟨ p^{0 *}, {\dot{q}}^{0 *}, ṙ^{0 *} ⟩ ⊩_{ℙ} φ (α_{0}, \dots, α_{l})$ . □

Letting

I

R_{κ}

-generic over

V [G] [H]

we get the following from the previous corollary together with claim 2.4.

Proof. Since the regulars in the range $[κ_{0}, κ)$ are ${μ_{α} ∣ α < κ}$ , we will be done by showing for each $α < κ$ the measure $U_{α}$ (in $V$ ) lifts to a measure in ${HOD}^{V_{κ}^{V [G] [H] [I]}}$ . In $V$ , $μ_{α}$ is measurable. The set $s^{″} ℙ_{\vec{E}}$ is the plain Radin forcing, hence any measure in $V$ over $μ_{α}$ lifts trivially to a measure on $μ_{α}$ in $V [s^{″} G]$ . In particular the measure $U_{α}$ in $V$ lifts to the measure ${\bar{\bar{U}}}_{α}$ in $V [s^{″} G]$ , which is definable by ${\bar{\bar{U}}}_{α} = {B \in V [s^{″} G] ∣ \exists A \in U_{α} A \subseteq B \subseteq μ_{α}}$ .

Since ${HOD}^{V_{κ}^{V [G] [H] [I]}} \supseteq V_{{(μ_{α}^{++})}_{V}}$ we get $U_{α} \in {HOD}^{V_{κ}^{V [G] [H] [I]}} \subseteq {HOD}^{V [G] [H] [I]} \subseteq V [s^{″} G]$ . Let ${\bar{U}}_{α} = {B \in {HOD}^{V_{κ}^{V [G] [H] [I]}} ∣ \exists A \in U_{α} A \subseteq B \subseteq μ_{α}}$ . Then ${\bar{U}}_{α} \in {HOD}^{V_{κ}^{V [G] [H] [I]}}$ and ${\bar{U}}_{α} \subseteq {\bar{\bar{U}}}_{α}$ . Necessarily ${\bar{U}}_{α}$ is a measure on $μ_{α}$ . □

References

[1] Omer Ben-Neria and Spencer Unger. Homogenerous changes in cofinalities with applications to HOD. Preprint.

[2] James Cummings, Sy David Friedman, and Mohammad Golshani. Collapsing the cardinals of hod. Journal of Mathematical Logic, 15(02):1550007, 2015.

[3] James Cummings, Sy-David Friedman, Menachem Magidor, Dima Sinapova, and Assaf Rinot. Ordinal definable subsets of singular cardinals. Preprint.

[4] Natash Dobrinen and Sy-David Friedman. Homogeneous iteration and measure one covering relative to HOD. Archive for Mathematical logic, 47(7–8):711–718, November 2008. doi:10.1007/s00153-008-0103-5.

[5] Moti Gitik and Menachem Magidor. The Singular Cardinal Hypothesis revisited. In Haim Judah, Winfried Just, and W. Hugh Woodin, editors, Set theory of the continuum, volume 26 of Mathematical Sciences Research Institute publications, pages 243–279. Springer, 1992.

[6] Menachem Magidor. Changing the cofinality of Cardinals. Fundamenta Mathematicae, 99(1):61–71, 1978.

[7] Carmi Merimovich. Extender-based Radin forcing. Transactions of the American Mathematical Society, 355:1729–1772, 2003. doi:10.1090/S0002-9947-03-03202-1.

[8] Carmi Merimovich. Supercompact Extender Based Prikry forcing. Archiv for Mathematical Logic, 50(5-6):592—601, June 2011. doi:10.1007/s00153-011-0234-y.

[9] Carmi Merimovich. Supercompact extender based Magidor-Radin forcing. Annals of Pure and Applied Logic, 168(8):1571–1587, 2017. doi:10.1016/j.apal.2017.02.006.

[10] W. Hugh Woodin. Suitable extender models I. Journal of Mathematical Logic, 10(01n02):101–339, 2010. doi:10.1142/S021906131000095X.

1A cardinal $κ$ is said to be $<λ$ -supercompact if there is an elementary embedding $j : V \to M$ such that $M$ is transitive, $crit j = κ$ , $j (κ) \geq λ$ , and $M ⊇^{< λ} M$ .

2This result was presented at the Arctic Set Theory Worshop 2 in Kilpisjärvi, Finland, February 2015.

3The suggestion was for a short intuitive explanation, really.