Guessing models and the approachability ideal
Rahman Mohammadpour Boban Velickovic


*

 
Institut de Mathématiques de Jussieu - Paris Rive Gauche,
Université Paris Diderot,  8 Place Aurélie Nemours, 75205 Paris Cedex 13, France



rahmanmohammadpour@gmail.com
https://sites.google.com/site/rahmanmohammadpour

Boban Veličković]Boban Veličković

boban@math.univ-paris-diderot.fr
http://www.logique.jussieu.fr/  boban




[2010]03E35, 03E55, 03E05 


 
Starting with two supercompact cardinals we produce a generic extension of the universe in which a principle
that we call GM^+(ω_3,ω_1) holds. 
This principle implies ISP(ω_2) and ISP(ω_3), and hence 
the tree property at ω_2 and ω_3, the Singular Cardinal Hypothesis, and 
the failure of the weak square principle □(ω_2,λ), for all regular λ≥ω_2. 
In addition, it implies that the restriction of the approachability
ideal  I[ω_2] to the set of  ordinals of cofinality ω_1 is the non stationary ideal on this set.
The consistency of this last statement was previously shown by Mitchell. 


Guessing models and the approachability ideal
    [
    December 30, 2023
=============================================





§ INTRODUCTION


In <cit.> C. Weiß  formulated some combinatorial principles that capture the essence of some large cardinal properties, but can hold at small cardinals. 
These principles usually have two parameters, a regular uncountable cardinal κ and a cardinal λ≥κ. 
Among them there are, in increasing strength, the principles TP(κ,λ), ITP(κ, λ), and ISP(κ,λ).

We will write P(κ), if the property P(κ,λ) holds, for all λ≥κ.
The study of these principles was continued by M. Viale and C. Weiß  in <cit.>. 
Using them they obtained  a striking result  saying that any standard forcing construction of a model of the Proper Forcing Axiom ( PFA) 
requires at least a strongly compact cardinal. 
One important concept that emerged from this work is that  of a guessing model. 
These models have generated considerable interest and have a number of interesting applications, see for instance  
<cit.>, <cit.>, <cit.>,  and <cit.>. 

Given the interest of these principles, it is natural to ask if they can hold simultaneously at several successive regular cardinals. 
 In this direction, L. Fontanella <cit.> extended the previous work of U. Abraham <cit.> 
 to obtain, modulo two supercompact cardinals, a model  of  in which ITP(ω_2) and ITP(ω_3) hold simultaneously. 
Now, it was shown in <cit.> that ISP(ω_2) is strictly stronger that ITP(ω_2). In fact, in the model constructed
by B. König in <cit.>, the principle ITP(ω_2) holds, but ISP(ω_2) fails. 
One can then ask if ISP(ω_2) and ISP(ω_3) can hold simultaneously. 
Let us point out that in <cit.> Trang showed the consistency of ISP(ω_3). 
However, in his model CH holds, and therefore the principle ISP(ω_2) fails. 



One concept closely related to the above principles is that of the approachability property on a regular uncountable cardinal λ
and the associated ideal I[λ].
These notions were introduced by Shelah implicitly in <cit.>, and studied by him  extensively over the past 40 years. 
For instance, in <cit.> he showed that if λ is a regular cardinal then S_λ^+^<λ∈ I[λ^+],
and in <cit.> he showed that if κ is regular and κ^+ < λ then I[λ] contains
a stationary subset of S_λ^κ. 
Shelah then asked in <cit.> if  it is consistent to have a regular λ such that I[λ^+] S_λ^+^λ
 is the non stationary ideal on S_λ^+^λ. This major question was finally answered by W. Mitchell <cit.>.
He started with a cardinal κ that is κ^+-Mahlo, and built an involved forcing construction 
yielding a model in which I[ω_2] S_ω_2^ω_1 is the non stationary ideal on S_ω_2^ω_1.
One feature of this construction is that it uses □_κ in the ground model, and so  ω_3∈ I[ω_3] in the extension.  
It is therefore unclear if Mitchell's method can be adapted to obtain a model in which both I[ω_2] S_ω_2^ω_1
and I[ω_3] S_ω_3^ω_2  contain only non stationary sets. 
The connection with the principles introduced by Weiß  is the following. 
If κ is a regular uncountable cardinal then ISP(κ^+) implies that there is a stationary subset of S_κ^+^κ
that is not in I[κ^+], but it does not imply Mitchell's result. 



The main purpose of this paper is to formulate and show the relative consistency of a principle that we call GM^+(ω_3,ω_1).
This statement implies  ISP(ω_2) and ISP(ω_3) and hence the tree property 
at ω_2 and ω_3. It also implies Mitchell's result, namely that 
I[ω_2] S_ω_2^ω_1=  NS_ω_2 S_ω_2^ω_1. 
Starting with a model with two supercompact cardinals κ < λ we produce a generic
extension in which κ=ω_2, λ = ω_3, and GM^+(ω_3,ω_1) holds. 
In fact for Mitchell's result we do not need the full strength of the principle GM^+(ω_3,ω_1), 
a weaker principle FS(ω_2,ω_1) suffices. In order to obtain FS(ω_2,ω_1) it is enough
to assume that λ is just inaccessible. 


The origin of this paper is as follows. Inspired by Mitchell's breakthrough, I. Neeman <cit.> 
introduced a method for iterating proper forcing notions using finite chains of elementary submodels as side conditions. 
This allowed him to give a new proof of the consistency of PFA using this type of iteration. 
More importantly, this opened a possibility of iterating forcing while preserving two successive cardinals
and potentially getting strong forcing axioms at ω_2 and higher cardinals. 
The second author then extended Neeman style iteration to more general classes of forcing.
This lead to the notion of a virtual model. Using this type of models as side conditions allows us
not only to  generalize Neeman's iteration theory to semiproper forcing, but also to formulate and prove iteration
theorems for  large classes of forcing notions preserving two uncountable cardinals, such as ω_1 and ω_2. 
This theory is presented in <cit.> and <cit.>. 
In fact, our main poset is an adaptation of the pure side condition forcing from <cit.> to two types
of models, but replacing models of size ω_1 by  models having a strong closure property
that we call Magidor models. 
  
The paper is organized as follows. In 1 we present the preliminaries and fix some notations. 
In 2 we review the theory of virtual models from <cit.> and <cit.>
and adapt it to the context of Magidor models. 
In 3, we introduce our main forcing notion ℙ^κ_λ and establish some of its properties. 
Finally, in 4  we study guessing models in the generic extension by ℙ^κ_λ,
and show that if κ is supercompact and λ> κ is inaccessible then 
ISP(ω_2) and FS(ω_2,ω_1) hold in the generic extension. 
If λ is also supercompact we show that GM^+(ω_3,ω_1) holds as well. 
     
     
     
     
     


§ PRELIMINARIES

  
Throughout this paper by a model M we mean a set or a class such that 
(M,∈) satisfies a sufficient fragment of ZFC. 
For a model M, we let M denote its transitive collapse and we let π_M be the collapsing map. 
For a set X  and an uncountable regular cardinal κ, we let 𝒫_κ(X) denote the set of all subsets of X of size less than κ.
We say that a subset 𝒮 of 𝒫_κ(X) is stationary if, for every function F:[X]^<ω→ X, 
there exists A∈𝒮 such that A∩κ∈κ and A is closed under F. 
For regular cardinals κ < λ, we let S_λ^κ denote the set {α < λ : (α)=κ}. 
For a cardinal θ we let H_θ denote  the collection of all sets whose transitive closure has size less than θ.

We now recall some relevant definitions from <cit.>.  For a set or class M we say that a set x⊆ M is
bounded in M if there is y∈ M such that x⊆ y. 

 Let γ be a regular cardinal. 
A set or a class M is said to be γ-guessing if for any x⊆ M which is bounded in M,
if x is γ-approximated by M, i.e. x∩ a ∈ M, for all a∈ M∩𝒫_γ (M),
then x is M-guessed, i.e. there is g∈ M such that x= g∩ M.
 

We say that a transitive model R is a powerful if it is closed under taking subsets, i.e.
if x∈ R and y⊆ x then y∈ R. 

We are mainly interested in the case R= V_α, for some ordinal α, or R= H_θ, for some uncountable regular cardinal θ.  
For a powerful model R, a regular cardinal γ and a cardinal κ, we let 


    𝔊_κ,γ(R) = { M∈𝒫_κ(R): M≺ R   M }.




For a powerful model R, GM(κ,γ,R) is the statement that  
𝔊_κ,γ(R) is stationary in 𝒫_κ(R).
GM(κ,γ) is the statement that GM(κ,γ, H_θ) holds,
 for all sufficiently large regular θ. 


 Notice that if M is γ-guessing and γ≤γ' then M is γ'-guessing.

Therefore  GM(κ, γ) implies GM(κ, γ').


The statement GM(κ,ω_1) is a reformulation of the principle ISP(κ) introduced
by  C. Weiß  in <cit.> and further studied in <cit.>,  <cit.> and <cit.>.
It was shown in <cit.> and  <cit.> that ISP(κ) implies 
the two cardinal tree property TP(κ, λ) and the failure of the weak square principle 
□ (κ,λ), for all regular λ≥κ. 
The equivalence between GM(κ,ω_1) and  ISP(κ) was established
in <cit.>, where it was also proved  that ISP(ω_2) follows from the Proper Forcing Axiom. 
ISP(κ) has strong influence on cardinal arithmetic. 
By using the results of Viale <cit.>,  Krueger <cit.> showed that, for a regular cardinal κ,
 the principle ISP(κ), and hence GM(κ,ω_1), implies the Singular Cardinal Hypothesis holds above κ. 
Let us also mention that in <cit.> Trang showed the consistency of GM(ω_3,ω_2)
assuming the existence of a supercompact cardinal.  In his model the Continuum Hypothesis holds.


We also recall the related notion of the  γ-approximation property, introduced by Hamkins in <cit.>.
     

Let γ be an uncountable regular cardinal. Suppose M and N are transitive models (sets or classes), M⊆ N and γ∈ M. 
We say the pair (M,N) satisfies the γ-approximation property, if whenever x∈ N is a bounded subset of M
such that x∩ a∈ M, for all a∈ M with |a|^M <γ, then x∈ M. 


 Suppose  R is a powerful model and let γ be a regular cardinal with γ∈ R.  
Note that M≺ R is a γ-guessing model if and only if the pair (M, V) satisfies the γ-approximation property. 


Our plan is to strengthen the principle GM(ω_2,ω_1) in order to control the approachability ideal on ω_2. 
Let us first recall the relevant definitions from <cit.>. 

 Let λ be a regular cardinal. A λ-approaching sequence is
a sequence of bounded subsets of λ. If a̅ = (a_ξ: ξ < λ) is a λ-approaching sequence, 
we let B(a̅) denote the set of all δ < λ such that 
there is a cofinal subset c⊆δ such that:


  * otp(c) < δ, in particular δ is singular, 

  * for all γ < δ, there exists η < δ such that c ∩γ = a_η.




Suppose λ is a regular cardinal. Let I[λ] be the ideal generated by the sets B(a̅), 
for all λ-approaching sequences a̅,
and the non stationary ideal NS_λ.  


 It is straightforward to check that I[λ] is a normal ideal on λ, but it may be non proper.
I[λ] is called the approachability ideal on λ. 


Shelah asked if it is consistent that I[κ^+] S_κ^+^κ=  NS_κ^+ S_κ^+^κ,
for a regular cardinal κ.   Mitchell in <cit.> answered this question affirmatively by showing the following. 


Assume that κ is a κ^+-Mahlo cardinal. Then there is a generic extension in which 
I[ω_2] S_ω_2^ω_1=  NS_ω_2 S_ω_2^ω_1.




In his paper <cit.>, Mitchell mentions that the large cardinal assumption used in his result is necessary
 by an unpublished theorem of Shelah; a proof can be found in <cit.>, Theorem 13. 
 It is also mentioned at the end of  <cit.> that one can prove the same result for λ^++ 
 where λ is a regular cardinal, more precisely let λ regular be given, 
 then under the same assumption (with κ>λ) of his theorem there is a generic extension of the universe 
 satisfying I[λ^++] S_λ^++^λ^+ =  NS_λ^++ S_λ^++^λ^+.


We now formulate a principle that implies Mitchell's result. 

 Suppose γ≤κ are regular uncountable cardinals. 
The principle FS(κ^+,γ) asserts that, 
for every X∈ H_κ^+, there is a collection 𝒢 of γ-guessing models of cardinality κ all containing X
such that { M∩κ^+: M∈𝒢} is κ-closed and unbounded in κ^+. 



Suppose κ is a regular uncountable cardinal and FS(κ^+,κ) holds. 
Then we have that I[κ^+] S_κ^+^κ=  NS_κ^+ S_κ^+^κ. 



Suppose that FS(κ^+),κ holds. Let a̅=(a_ξ : ξ <κ^+) be a κ^+-approaching sequence. 
Let 𝒢 be the family of κ-guessing models  all containing a̅ whose existence is guaranteed by FS(κ^+). 

We show that  M∩κ^+ ∉ B(a̅), for any M∈𝒢 such that (M∩κ^+)=κ. 
Fix one such M∈𝒢. Let δ = M∩κ^+ and suppose c⊆δ satisfies 
(1) and (2) of <ref>. Let μ =  otp(c). Note that μ< δ, hence μ∈ M. 
Since a̅∈ M, we have that c∩γ∈ M, for all γ <δ, and hence c∩ Z∈ M, for all Z∈ M with |Z|<κ.
Since M is a κ-guessing model,  there must be d∈ M such that c∩δ = d∩δ. We may assume d⊆κ^+.
Then c is an initial segment of d, so if ρ is the μ-th element of d then d∩ρ = c.
Since μ, d ∈ M, we have ρ∈ M as well, and hence c=d ∩ρ∈ M. 
But then δ= sup (c) belongs to M, a contradiction. 


FS(ω_2,ω_1)  is a local principle, i.e. it refers only to H_ω_3, therefore it cannot imply GM(ω_2,ω_1). 
We now formulate a principle that implies both FS(ω_2,ω_1) and GM(ω_2,ω_1).
We state it  for any pair of  uncountable regular cardinals γ≤κ. 



 Let   γ≤κ  be regular cardinal cardinals. A model  M of cardinality κ^+
is strongly γ-guessing if it is the union of an increasing chain (M_ξ : ξ <κ^+)
of γ-guessing models of cardinality κ and M_ξ= ⋃{ M_η : η < ξ}, for every ξ of cofinality κ. 


 We only define the notion of strongly γ-guessing for sets M whose
cardinality is a successor of a regular cardinal κ. We have not explored other variations of this concept. 
Note that if M is strongly γ-guessing then M is γ-guessing. 


For a powerful model R and regular cardinals γ and κ, we let 


    𝔊^+_κ^++,γ(R) = { M∈𝒫_κ^++(R): M≺ R   M }.



For a powerful model R, GM^+(κ^++,γ,R) states that  
𝔊^+_κ^++,γ(R) is stationary in 𝒫_κ^++(R).
GM^+(κ^++,γ) is the statement that GM^+(κ^++,γ, H_θ) holds,
 for all sufficiently large regular θ. 


Clearly GM^+(κ^++,γ) implies both 
FS(κ^+,γ) and GM(κ^+,γ).
The main result of this paper is the following.


Suppose that κ is supercompact and λ > κ is inaccessible. Then there is a forcing notion such that 
in the generic extension  GM(ω_2,ω_1) and FS(ω_2,ω_1) hold. 
If, in addition, λ is supercompact, then GM^+(ω_3,ω_1) holds as well. 


 By what we have said above the principle GM^+(ω_3,ω_1) implies the following: 
I[ω_2] S_ω_2^ω_1=  NS_ω_2 S_ω_2^ω_1,
the principles ISP(ω_2) and ISP(ω_3), and hence
the tree tree property at ω_2 and ω_3, the Singular Cardinal Hypothesis, and the failure of the weak square
principle □ (ω_2,λ), for all regular λ≥ω_2. 
It is also not hard to see that it implies the negation of the weak Kurepa Hypothesis at ω_1
and that the continuum is at least ω_3. 


The notion of strong properness, introduced by Mitchell in <cit.>, plays the key role in our construction. 
Let us recall the following definition. 

 Let ℙ be a forcing notion and A a set. We say that p∈ℙ
is (A,ℙ)-strongly generic if for all q≤ p there is a condition q A∈ A such that any 
r≤  q A with r∈ A is compatible with q. 




Let ℙ be a forcing notion, and 𝒮 a collection of sets. 
We say that ℙ is 𝒮-strongly proper if, for every A∈𝒮 and p∈ A∩ℙ,
there is q≤ p that is (A,ℙ)-strongly generic. 


 
The following  proposition connects the approximation property with strong properness. 



Let ℙ be a forcing notion and κ an uncountable regular cardinal. 
Suppose ℙ is 𝒮-strongly proper, for some stationary subset 𝒮
of 𝒫_κ(ℙ). If G is V-generic over ℙ, then (V,V[G])
has the κ-approximation property. 


Work in V. Let α be an ordinal, Ẋ a ℙ-name, and suppose some condition p∈ℙ
forces that Ẋ⊆α and  Ẋ∩Ž∈ V, for all  Z∈ V with |Z|^V< κ.
Fix a sufficiently large regular cardinal θ. By the stationarity of 𝒮, we can find M≺ H_θ
containing p,ℙ, Ȧ, and such that M∩ℙ∈𝒮. 
Let q≤ p be (M∩ℙ)-strongly generic. Since M∩ℙ is of size <κ, 
by strengthening q if necessary, we may assume that q decides Ẋ∩ M. 
Since q (M∩ℙ) and p are compatible, and M is elementary, they are compatible in M. 
Therefore, by replacing q (M∩ℙ) by a stronger condition in M,  we may assume that it extends p. 
We now argue that q (M∩ℙ) decides Ẋ. Otherwise, by elementary of M, we
can find ξ∈α∩ M and r_0,r_1∈ M with r_0, r_1≤ q (M∩ℙ) such that r_0 forces ξ∈Ẋ
and r_1 forces ξ∉Ẋ. Now, by strong genericity of q, we have that r_0 and r_1 are both compatible
with q. Let s_0 be a common extension of q and r_0, and s_1 a common extension of q and r_1. 
Then s_0, s_1≤ q  and force contradictory information about ξ∈Ẋ. 
This contradicts the fact that q decides Ẋ∩ M.
 

We will also need the following well-known theorem due to Magidor.


The following are equivalent for a regular cardinal κ.


  * κ is supercompact.

  * For every γ>κ and x∈ V_γ there exist κ̅< γ̅<κ, 
and an elementary embedding j:V_γ̅→ V_γ with critical point κ̅ such 
that j(κ̅)=κ and x∈ j[V_γ̅]. 



 
 
 
 
 
 
 


§ VIRTUAL MODELS


In this section we review the notion of virtual models introduced in  <cit.> and <cit.>. 
In <cit.> we  used virtual models of two types: countable and internally club (I.C.) models of size ℵ_1.
In the current situation we replace the I.C. models by models that have a much stronger closure property that we
call Magidor models. 

We shall consider the language ℒ obtained by adding a single constant symbol c to the standard language ℒ_ϵ of set theory.
Let us say that a structure 𝒜 of the form (A,∈, κ) is suitable
if A is a transitive set satisfying  in the expanded language, 
when κ, the interpretation of the constant symbol c, is inaccessible in A. 
We shall often abuse notation and refer to the structure (A,∈,κ) simply by A.
Suppose 𝒜 is a suitable structure. If α is an ordinal in A,
we let A_α denote A∩ V_α. Finally, we let

    E_𝒜={α∈ A : A_α≺ A }.

Note that E_A is a closed, possibly empty, subset of ^A. It is not definable in A, but E_A∩α
is uniformly definable in A with parameter α, for each α∈ E_A. 
If α∈ E_A  we let next_A(α) be the least ordinal in E_A above α,
if such an ordinal exists. Otherwise, we leave next_A(α) undefined.
We start with a simple technical lemma.

  
Suppose M is an elementary submodel of a suitable structure A. Then


  * If α∈ E_A and (M∩^A)∖α≠∅, then min(M∩^A∖α)∈ E_A.

  * sup ( E_A∩ M) =  sup (E_A∩sup (M∩^A)).




 The second item follows from the first one, so we only give the proof of (1). 
Let β be the least ordinal in M∖α.
We need to show that A_β is an elementary submodel of A. 
Suppose otherwise, then by the Tarski-Vaught criterion,
 there is a tuple x̅∈ A_β
and a formula φ (y,x̅) such that A ∃ y φ(y,x̅),
but there is no y∈ A_β such that A ∃ y φ(y,x̅).
Since β∈ M and M is an elementary submodel of A,
there is such a tuple x̅∈ A_β∩ M.
Now, β is the least ordinal in M above α,
therefore x̅∈ M∩ A_α.
Since A_α is an elementary submodel of A,
there is y'∈ A_α witnessing that A_αφ(y',x̅)
and so A φ(y',x̅).
Since α≤β, it follows that y'∈ A_β, a contradiction.



 Suppose M is a submodel of a suitable
structure A and X is a subset of A. Let

    Hull(M,X) ={ f(x̅) : f∈ M, x̅∈ X^<ω, f x̅∈ (f)}.



The main reason we have defined the Hull operation in this way is that it allows us to define
the Skolem hull of M and X without referring explicitly to the ambient model A.

 Suppose A is a suitable structure,
M is an elementary submodel of A and X is a subset of A.
Let δ be sup (M∩^A), and suppose X∩ A_δ is nonempty.
Then Hull(M,X) is the least elementary submodel of A containing M and X∩ A_δ.


 For each γ∈ A, let id_γ be the identity function
on A_γ. Clearly, if γ∈ M then id_γ∈ M. Therefore,
X∩ A_δ is a subset of Hull(M,X). Let γ∈ M be such that X∩ A_γ is nonempty.
For each z∈ M, the constant function c_z defined on A_γ is in M,
therefore M is a subset of Hull(M,X). The minimality of Hull(M,X) is clear from the definition.
It remains to show that Hull(M,X) is an elementary submodel of A.
We check the Tarski-Vaught criterion for Hull(M,X) and A. Let φ be a formula and
a_1,…,a_n ∈ Hull(M,X) such that A∃ u φ(u,a_1,…,a_n).
Then we can find functions f_1,…, f_n∈ M and tuples x̅_1,…,x̅_n ∈ X^<ω
such that a_i=f_i(x̅_i), for all i. If D_i is the domain of f_i, this implies that x̅_i∈ D_i.
By regularity and the axiom of choice in A we can find a function g defined on D_1 ×…× D_n
such that for every y̅_1∈ D_1,…,y̅_n ∈ D_n, if there is u such that
Aφ (u, f_1(y̅_1),…,f_n(y̅_n)) then
g(y̅_1,…,y̅_n) is such a u. Moreover, by elementarity of M,
we may assume that g∈ M. Let a =g(x̅_1,…,x̅_n).
It follows that a∈ Hull(M,X) and A φ (a,a_1,…,a_n).
Therefore, Hull(M,X) is an elementary submodel of A.


Now, let us fix an inaccessible cardinal  κ, a cardinal λ >κ such that 
V_λ satisfies .   We shall write
 E instead of E_V_λ and next(α) instead of next_V_λ(α).
For each α∈ E, we shall define certain families ℱ_α∈ V_λ, 
as well as relations R_α and operations O_α on V_λ. 
Being a member of ℱ_α will be expressed by a Σ_1-formula with parameter V_α
and similarly for R_α and O_α.
If A is another suitable structure we can interpret these formulas in A and obtain
families ℱ_α^A, relations R_α^A and operations O_α^A. In this section we shall only consider
suitable A such that the interpretation of the constant symbol c is κ and A⊆ V_λ. 
Note that if we have such an A and α∈ E_A ∩ E with A_α = V_α then ℱ_α^A ⊆ℱ_α.
Similarly, if x,y∈ A are such that xR_α^A y then xR_α y, and if x∈ A then O_α^A(x)=O_α(x). 
If M is an elementary submodel of a suitable A and α∈ E_A ∩ M we shall write 
ℱ_α^M for ℱ_α^A∩ M, and R_α^M and O_α^M  for restrictions of  R_α^A and O_α^A to M.


 Suppose α∈ E. We let 𝒜_α denote the set of all
transitive A that are elementary extensions of V_α and have the same cardinality as V_α.


Note that if A ∈𝒜_α and α∈ A then E_A∩α=E∩α.
If A∈𝒜_α we will refer to V_α as the standard part of A.
Note that if A has nonstandard elements then α∈ E_A. 





Suppose α∈ E. We let 𝒱_α denote the collection of all substructures M of V_λ of
size less than κ such that,
 if we let A= Hull(M,V_α), then A∈𝒜_α and M is an elementary 
submodel of A.


 We refer to the members of 𝒱_α as the α-models. 
 We write 𝒱_< α for ⋃{𝒱_γ : γ∈ E ∩α}.
 Collections 𝒱_≤α and 𝒱_≥α are defined in the obvious way. 
 We will write 𝒱 for 𝒱_< λ . 
 If M∈𝒱, we then write  η(M) for the unique ordinal α such that M∈𝒱_α.


 Note that if M ∈𝒱_α then sup(M ∩)≥α.
In general, M is not elementary in V_λ, in fact, this only happens if M ⊆ V_α.
In this case we will say that M is a standard α-model.





 We refer to members of 𝒱 as
 virtual models. We also refer to members of 𝒱^A, for some
suitable A with A⊆ V_λ, as general virtual models.


 Suppose M,N∈𝒱 and α∈ E.
We say that an isomorphism σ:M→ N is an α-isomorphism
if it has an extension to an isomorphism σ̅: Hull(M,V_α)→ Hull(N,V_α).
We say that M and N are α-isomorphic and write M≅_αN if
there is an α-isomorphism between them. Note that if  σ and σ̅ exist, they are unique.


 
Clearly, ≅_α is an equivalence relation, for every α∈ E. Note that if M ∈𝒱_γ,
for some γ < α, then the only model α-isomorphic to M is M itself.
Suppose  α,β∈ E and α≤β.
It is easy to see that, if M,N∈𝒱 are β-isomorphic,
then they are α-isomorphic.  We will now see that, if α <β, then
for every β-model M there is a canonical representative of the ≅_α-equivalence
class of M which is an α-model.


 Suppose α and β are members of  E
and M is a β-model. Let Hull(M,V_α) be the transitive collapse of
Hull(M,V_α), and let π be the collapsing map. We define  M α to be π[M],
i.e. the image of M under the collapsing map of Hull(M,V_α).


 Note that if β < α then Mα = M.
If β≥α, then Hull(M,V_α) belongs to 𝒜_α, so Mα is
an α-model which is α-isomorphic to M. Note also that if β=α, then
Mα =M since Hull(M,V_α) is already transitive.

Note also that if A∈𝒜_α then 𝒱_α^A ⊆𝒱_α. 
Therefore, if A,B∈𝒜_α, M ∈𝒱^A, and N ∈𝒱^B, we can 
still write M ≅_α N if M α = N α. This is 
of course equivalent to the existence of an α-isomorphism between M and N.


The following is straightforward.

 Suppose α,β∈ E and
α≤β. Let M∈𝒱. Then
(M β)α = Mα.

 
 

We also need to define a version of the membership relation, for every α in E.

 Suppose M,N∈𝒱  and α∈ E. 
We write M∈_α N if there is M'∈ N with M' ∈𝒱^N such that M'≅_α M. 
If this happens, we say that M is α-in N.


Note that if M⊆ V_α, this simply means that M∈ N. However, in general,
we may have M ∈_α N even if the rank of M is higher than the rank of N.
We shall often use the following simple facts without mentioning them. 

 
Suppose M, N ∈𝒱 with M∈ N. Let α∈ E, and suppose 
N'∈𝒱^A, for some A∈𝒜_α,  and σ : N → N' is an α-isomorphism. 
Then M and σ(M) are α-isomorphic. 


 Since | M|  < κ < | V_α|, we conclude that M⊆ Hull(N,V_α), 
and hence Hull(M,V_α) ⊆ Hull(N,V_α). Let σ̅ be the extension 
of σ to Hull(N,V_α). 
 It follows that σ̅ Hull(M,V_α) is
an isomorphism between Hull(M,V_α) and Hull(σ(M),V_α).
Hence σ̅ M is an α-isomorphism between M and σ(M).


 Let α,β∈ E with α≤β.
Suppose M,N ∈𝒱_≥β and M∈_β N. 
Then Mα∈_α Nα.


Fix some M'∈ N such that M≅_β M'. Since α≤β, we have that M≅_α M'. 
If π  is the Mostowski collapse map of Hull(N,V_α), then π(M')∈ Nα. 
On the other hand, since | M | < κ <| V_α|, we have that Hull(M',V_α) ⊆ Hull(N,V_α) and
π [M']= π (M'). It follows that π Hull(M',V_α) is an isomorphism between Hull(M',V_α)
and Hull(π(M'),V_α). 
Therefore, M≅_απ(M')∈ Nα.
 


We refer to the following proposition as the continuity of the α-isomorphism.

Let α be a limit point of E. Suppose N,M∈𝒱 and M≅_γ N for unboundedly many γ below α.
Then M≅_α N.


For each γ∈ E ∩α, let σ_γ be the unique isomorphism between Hull(M,V_γ) and Hull(N,V_γ)
such that σ_γ[M]=N. If γ < γ', we have that σ_γ' Hull(M,V_γ)= σ_γ.
Let σ = ⋃{σ_γ : γ∈ E∩α}. Then σ witnesses that M and N are α-isomorphic. 





Let α be a limit point of E of uncountable cofinality. Assume that M,N∈𝒱 and N is countable. 
Suppose that M∈_γ N for unboundedly many γ<α. Then M∈_α N.


Since N is countable and α is of uncountable cofinality, there is M'∈ N with M'∈𝒱^N such that M≅_γ M', for unboundedly many γ∈ E∩α. 
By  <ref> we have that M ≅_α M', and hence M∈_α N. 


In our forcing we will use two types of virtual models, the countable ones and  some nice models of size less than κ defined below.


For α∈ E, we let 𝒞_α denote the collection of countable models in  𝒱_α. 
We define similarly 𝒞_<α, 𝒞_≤α and 𝒞_≥α. We write 𝒞 for 𝒞_<λ, and
 𝒞_ st for the collection of standard models in 𝒞.








Suppose λ is of uncountable cofinality. Then 𝒞_ st contains a club in 𝒫_ω_1(V_λ).


 First note that since λ is of uncountable cofinality E is unbounded  and thus club in λ.
Suppose M is a countable elementary submodel of (V_λ, ∈, E). Let α = sup (M ∩ E). 
Note that M∩ ORD is unbounded in α. Hence M is a standard α-model.


The following definition is motivated by Magidor's reformulation of supercompactness, see <ref>.



We say that  a model M  is a κ-Magidor model if, letting M be the transitive collapse of M and π the collapsing map, 
M=V_γ̅, for some γ̅<κ with cof(γ̅) ≥π (κ), and V_π(κ)⊆ M. 
If κ is clear from the context we omit it. 


 Suppose κ is supercompact and μ >κ with cof(μ) ≥κ. 
Then the set of κ-Magidor models is stationary in 𝒫_κ(V_μ).


 
Fix a function F: [V_μ]^< ω→ V_μ. We have to find a κ-Magidor model closed under F. 
Let γ>μ be such that V_γ satisfies a sufficient fragment of ZFC. 
Since κ is supercompact, by <ref> we can find κ̅< γ̅<κ and
an elementary embedding j: V_γ̅→ V_γ with critical point κ̅ such that j(κ̅)=κ
and such that F [V_μ]^<ω∈ j [V_γ̅]. Note that this implies that V_μ∈  j [V_γ̅].
Let μ̅ be such that j(μ̅)= μ.
Since cof(μ) ≥κ, by elementarity we must have that cof(μ̅)≥κ̅. 
Let N = j [V_μ̅]. Then N is a κ-Magidor elementary submodel of V_μ that is closed under F, as required. 
 

 Let 𝒰^κ_α be the collection of all M∈𝒱_α that are κ-Magidor models. 
We define 𝒰^κ_<α, 𝒰^κ_≤α, and 𝒰^κ_≥α in the obvious way. 
We write 𝒰^κ for 𝒰^κ_< λ. When κ is clear from the context, we omit it.
We also write 𝒰_ st for the standard models in 𝒰.


 Suppose M is a κ-Magidor α-model. Let V_γ̅ be its transitive collapse, and let j be the inverse of the collapsing map π.  
Let κ̅= π (κ), and let A=  Hull(M,V_α). Note that j:V_γ̅→ A is an elementary embedding with critical point κ̅
and j(κ̅)= κ. 


By <ref> we have the following immediate corollary. 


Suppose κ is supercompact and λ is inaccessible. Then 𝒰_ st is stationary in 𝒫_κ(V_λ).


 
 
 
















 

Note that  both classes 𝒞 and 𝒰 of virtual models are closed under projections. 
We shall study some particular finite collections of these two types of models. 
We start by establishing the following easy fact. 



Let α∈ E. Suppose M,N,P∈𝒱 and M∈_α N∈_α P. 
If either N is countable or P is a Magidor model then M∈_α P. 


Pick N'∈ P with N'∈𝒱^P which is α-isomorphic to N. We first establish that N'⊆ P. 
If N is countable this is immediate. Suppose both N and P are Magidor models.
Let N' be the transitive collapse of N', and let π be the collapsing map. 
 Then N'∈ V_κ∩ P since | N '| < κ. Since P is a Magidor model,
we know that V_κ∩ P is transitive, and hence N'⊆ P, but then also N'⊆ P. 
Let σ be an α-isomorphism between N and N', and let M'∈  N with M'∈𝒱^N
be a model that is α-isomorphic to M. By <ref> we know that σ(M')
is α-isomorphic to M', and also to M by the transitivity of ≅_α.
On the other hand σ(M')∈ N' ⊆ P and thus M∈_α P, as desired. 


Our next goal is to define when a virtual model M is active at some α∈ E. 


Let M∈𝒱. We say that M is active at α∈ E if 
η (M)≥α and Hull (M,V_κ_M)∩ E ∩α is unbounded in E∩α,
where κ_M = sup (M∩κ). We say that M is strongly active at α if η(M)≥α
and M∩ E∩α is unbounded in E∩α. 



 We are primarily interested in the case M ∈𝒞∪𝒰.
First note that if M is a Magidor model, then V_κ_M⊆ M, hence M is active at some α∈ E
if and only if it is strongly active at α. 
The situation is quite different for countable models. 
If M is countable, then the set of α∈ E at which M is strongly active is at most countable,
while the set of α∈ E at which M is active can be of size |V_κ_M|. 
One feature of our definition is that if N∈_α M, then for all γ∈ E∩α,
if N is active at γ then so is M.


Let us also remark what happens at levels α that are successor points of E.
Suppose  α =  next(β), for some β∈ E, and M is active at α.
 We must have β∈ M as β = max (E∩α). 
we must also have sup (M∩ ORD)≥α since η(M)≥α,. If sup (M∩ ORD)= α
then M is a countable standard model. If sup (M∩ ORD)>  α, let 
γ = min (M ∩ ORD∖α), and let A= Hull(M,V_γ). 
Then by <ref> γ∈ E_A. 
Since γ∈ M, we have that E_A∩ (γ +1)∈ M and therefore
we can compute α in M as the the next element of E_A∩ (γ +1) above β. 
Thus, in this case we have α∈ M. 


It will be convenient to also have the following definition. 

 Suppose M∈𝒱. Let a(M)= {α∈ E : M α} and α (M)=max a(M).


Note that a(M) is a closed subset of E of size at most |  Hull(M,V_κ_M)|.

 Let M∈𝒱 and N∈𝒰. Suppose α∈ E, M and N are active at α,
and M∈_α N. Then α∈ N.


 We may assume that M and N are α-models. Let A=  Hull(N,V_α). Then A∈𝒜_α. 
Fix M^*∈ N with M^*∈𝒱^A which is α-isomorphic to M.
Since M^* is α-equivalent to M, we have that α∈ a^A(M^*). 
On the other hand, a^A(M^*)∈ N and has size <κ_N, hence a^A(M^*)⊆ N.
It follows that α∈ N. 



 Let M∈𝒱 and N∈𝒰. 
Suppose α∈ a(M) is a limit point of E and M ∈_γ N, for all γ∈ E ∩α. 
Then α∈ N and M ∈_α N. 



Let a = a(M)∩ N ∩α. Note that A is unbounded in α and has size < κ_N. Since N is closed under <κ_N-sequences,
it follows that a∈ N, and hence α = sup (a) ∈ N. For γ < α, let M_γ = Mγ.
For γ∈ a, we have that  M ∈_γN, and hence M_γ∈ N. 
Let A_γ =  Hull(M_γ,V_γ). For γ, δ∈ a with γ < δ, we have
that M_δγ = M_γ. In other words, A_γ is the transitive collapse of Hull(M_δ,V_γ)
, and if σ_γ,δ is the inverse of the collapsing map, we have σ_γ,δ[M_γ]=M_δ. 
Each of the maps σ_γ,δ is definable from M_δ and γ, and hence it belongs to N.
Now, N is closed under <κ_N-sequences and therefore the whole system (A_γ, σ_γ,δ : γ≤δ∈ a) belongs to N.
Let A be the direct limit of this system, and let σ_γ be the canonical embedding of A_γ to A.
If we let π_γ be the collapsing map of Hull(M,V_γ) to A_γ, we then have that, for every γ < δ, 
the following diagram commutes:




    Hull(M,V_γ) r id[swap]dπ_γ    Hull(M,V_δ) dπ_δ
    
    A_γrσ_γ,δ    A_δ


Since Hull(M,V_α) = ⋃{ Hull(M,V_γ): γ∈ a }, we have 
that A is isomorphic to Hull(M,V_α). 
Therefore, its transitive collapse is A_α= Hull(Mα,V_α), and if we let π be the collapsing map, 
π [M]= Mα. We can therefore identify A with A_α, and we get that σ_γ [M_γ]=Mα, 
for any γ∈ a. Thus Mα∈ N, as required. 


We now  define an operation that will play the role of intersection for virtual models. 
We call it the meet. We only define the meet of two models of different types. 
Suppose N∈𝒰 and M∈𝒞. Let N be the transitive collapse of N,
and let π be the collapsing map. Note that if N∈ M, then N∩ M is a countable elementary submodel 
of N. Then N∩ M ∈N since N is closed under countable sequence.
Note that π^-1(N∩ M)= π^-1[N∩ M], and this model is elementary in N.


 Suppose N∈𝒰 and M ∈𝒞. Let α = max (a(N)∩ a(M)). 
We will define N  M if N∈_α M. Let N be the transitive collapse of N, and let π
be the collapsing map. 
Set

    η = sup (sup (π^-1[N∩ M]∩ ORD)∩ E∩ (α +1)).

We define the meet of N and M to be N M=π^-1[N∩ M]η.


To make sense of the above definition, we need to prove the following.


Under the assumptions of the above definition, N M∈𝒞_η.


Since η(N)≥α we can form the model A= Hull(N,V_α) and,  we therefore have N ≺ A
and V_α≺ A. 
 Since N∈ M, we have that N∩ M ≺N.
Therefore, we have π^-1[N∩ M] ≺ N. 
Now, η∈ E ∩ (α +1) and so V_η≺ V_α≺ A. 
Moreover, sup (π^-1[N∩ M]∩ ORD) ≥η. 
By <ref> we have that Hull(π^-1[N∩ M],V_η)≺ A and 
V_η⊆ Hull(π^-1[N∩ M],V_η).
It follows that the transitive collapse of Hull(π^-1[N∩ M],V_η) belongs to 𝒜_η
and thus the image of π^-1[N∩ M] under the collapsing map belongs to 𝒞_η. 


 Let N∈𝒰 and M∈𝒞. Suppose α∈ E and the meet N M is defined and active at α.
Then (N  M)∩ V_α = N∩ M ∩ V_α. 

 Let β = max (a(N)∩ a(M)). Since the meet of N and M is defined we must have N ∈_β M. 
Since N M is active at α, we must have α≤β. 
Let  N'∈𝒱^M be such that N'≅_β N. Let σ be the β-isomorphism between 
N and N'. Notice that σ is the identity on N∩ V_β and thus also on N∩ V_α.
 Let N denote the common transitive collapse of N and N', and let π and π' be the collapsing maps. 
Then the following diagram commutes.


    [row sep=2.5em]
    N drπrrσ      N' [swap]dlπ'
       N


Note that (N M)∩ V_α = π^-1[N∩ M]∩ V_α = σ^-1[N∩ M∩ V_α].
Since σ is the identity on N ∩ V_α, it follows that (N  M)∩ V_α = N∩ M ∩ V_α. 



 Let α∈ E. Suppose N∈𝒰 and ∈𝒞, the meet N M is defined, 
 and N and M strongly active at α. Then N M is strongly active at α. 

 Let β= max (a(N)∩ a(M)). Since both N and M are active at α, we must have α≤β. 
Let N'∈ M  with N'∈𝒱^M be such that N'≅_β N. 
Let σ be the β-isomorphism between N' and N.  Then σ N'∩ V_β is the identity. 
Note that N'∩ M∩ E ∩α is unbounded in E∩α.
Since N'∩ V_α = N∩ V_α,  we must have that N∩ M∩ E ∩α is also unbounded in E∩α. 
By <ref>, N M is strongly active at α. 



The next proposition states the meet operation commutes with projections. 


Let N∈𝒰 and M∈𝒞. Suppose α∈ E and the meet N M is defined and active at α.
Then (N  M)α = N α M α. 


First note that if N M is active at α, then α∈ a(N) ∩ a(M). It follows that α is the maximum of 
a(Nα) ∩ a(Mα).
Then note that N M depends only on max (a(N)∩ a(M)), N, and M∩N, where N is the transitive collapse of N. 
Now, N is also the transitive collapse of Nα. In fact, if σ is the α-isomorphism between N and Nα,
and π and π' are the collapsing maps of N and N' respectively, then π = π ' ∘σ. Therefore, 
σπ^-1[N∩ M] is an an α-isomorphism between π^-1[N∩ M]
 and π'^-1[N∩ Mα]. It follows that (N  M)α = N α M α. 




Let α∈ E. Suppose N∈𝒰, M∈𝒞, both are active at α and N∈_α M.
Let P be another virtual model also active at α. Then P ∈_α N  M if only if P∈_α N and P∈_α M.



By <ref> we may assume that N,M and P are all α-models. 
Assume first that P ∈_α N M. In particular this means that N  M is active at α. 
In particular we have that N M ⊆ N, and hence P ∈_α N. 
Fix N' ∈𝒱^M which is α-isomorphic to N. Let N be the transitive collapse 
of both N and N' and let π and π' be the respective collapsing maps. 
Note that σ=π ' ∘π^-1 is the α-isomorphism between N and N'. 
Then σ [N  M] = N'∩ M.  Pick also P'∈ N  M which is α-isomorphic to P. 
By <ref> P' and σ (P') are also α-isomorphic. 
Since σ (P')∈ M, by the transitivity of ≅_α we get that P is α-isomorphic to  σ(P').
This implies that P∈_α M.

Now assume P∈_α N and P∈_α M. By <ref> we know that α∈ N.
Since P is an α-model, we conclude that P∈ N.
If also α∈ M, we have that N, P ∈ M and N M = N∩ M. Therefore, P∈ N  M. 
Assume now that α∉ M and let α^*= min (M ∩λ∖α).
Let A=  Hull(M,V_α). Since we assumed that M is an α-model, we have that A∈𝒜_α
and α∈ E_A.
By <ref>   we also have that α^*∈ E_A. Fix P^*, N^* ∈ M that are α-isomorphic to P and N respectively.
By projecting them to α^* if necessary, we may assume P^*, N^*∈𝒱_α^*^A.
Moreover, N^* is a Magidor model from the point of view of A. 
Since P^*∈_α N^* and α^* is the least ordinal in M above α we have 

    M∀δ∈ E_A∩α^* P^*∈_δ N^*.

Moreover, M "P^*  is active at α^*". Since α^* is a limit point of E_A,
we can apply <ref> in A and conclude that  α^*∈ N^* and P^* ∈ N^*.
Hence P^*∈ N^* ∩ M. Let σ be the α-isomorphism between N^* and N.
Then σ [N^* ∩ M]= N M. Hence σ (P^*)∈ N  M and is α-isomorphic to P.
It follows that P∈_α N  M.


One feature of the meet  is the following absorption property.


Suppose N∈𝒰, M∈𝒞, and the meet N M is defined. 
Let α∈ E, and suppose P is a Magidor α-model active at α such that P∈_α N  M. 
Then P M = P  (N  M). 


Since P∈_α N  M and P is active at α, so is N M, and hence both N and M are active at α as well. 
Let P be the transitive collapse of P.
Then P∈ N∩ V_κ, and since N∩ V_κ is transitive, we have P⊆ N. 
Hence P∩ (N  M)= P∩ M. It follows that P M = P  (N  M).


 Let α∈ E. Suppose N∈𝒰, M∈𝒞 and the meet N M is defined
and active at α. Suppose P∈𝒱 and N,M∈_α P. Then N M∈_α P.

 We may assume M,N and P are all α-models. If α∈ P then N,M∈ P, and hence also N M∈ P.
Suppose now α∉ P.  Let A= Hull(P,V_α) and let  α^*=min (P∩ ORD∖α). 
Note that α^* has uncountable cofinality in A. By <ref>  we have α^*∈ E_A. We can find N^*,M^*∈ P 
such that N^*≅_α N and M^*≅_α M. We may assume that N^*∈𝒰_α^*^A and M^*∈𝒞_α^*^A. 
Work for a moment in A. Since N^*∈_α M^*, α^* is the least ordinal of P above α, and N^*,M^*∈ P, we have

    A∀γ∈ E_A∩α^* N^* ∈_γ M^*.

By applying <ref> inside A we have that N^*∈_α^*  M^*, and hence A can compute the meet, say Q, of N^* and M^*.
Then Q∈ P, and by applying <ref> inside A, we get  Qα = N^*α M^*α. 
Hence Q≅_α N M.




Let α∈ E and let  ℳ be a set of virtual models.
We let ℳα={Mα:M∈ℳ} and 
ℳ^α={Mα: M∈ℳ is active at α}.



We can now define what we mean by an  α-chain.


Let α∈ E and let ℳ be a subset of 𝒰∪𝒞. 
We say ℳ is an α-chain if for all distinct  M,N∈ℳ, either M∈_α N or N∈_α M,
or there is a P∈ℳ such that either M∈_α P∈_α N  or N∈_α P∈_α  M.



Suppose α∈ E and ℳ is a finite subset of  𝒰∪𝒞.
Then ℳ is an α-chain if and only if there is an enumeration 
{ M_i : i <n } of ℳ such that M_0∈_α M_1∈_α⋯∈_α M_n-1. 


 Suppose first ℳ is an α-chain. Define the relation < on ℳ by letting M < N iff κ_M < κ_N. 
It is straightforward to see that < is a total ordering on ℳ. We can then let { M_i: i <n } be the <-increasing enumeration of ℳ. 
Conversely, suppose ℳ = { M_i : i < n } is the enumeration such that M_0∈_α M_1∈_α⋯∈_α M_n-1. 
Let i<j <n. If j= i+1 then M_i∈_α M_j. Suppose j > i+1. If M_j is a Magidor model or if there are no Magidor models between M_i and M_j
by <ref> we conclude that M_i∈_α M_j. Otherwise let k < j be the largest such that M_k is a Magidor model. 
Then again by <ref>, we conclude that M_i∈_α M_k∈_α M_j. 


Let α∈ E and let ℳ be an α-chain. Let ∈_α^* be the transitive closure of ∈_α. 
Then ∈_α^* is a total ordering on ℳ.
For M,N∈ℳ, we say M is α-below N in ℳ, or equivalently N is α-above  M in ℳ, if 
M∈_α^* N in ℳ. Now using the transitivity of ∈_α^* we can form intervals in ℳ. 
Let 

    (M,N)^α_ℳ={ P∈ℳ : M∈_α^* P∈_α^* N}.

Similarly we can define [M,N]^α_ℳ, [M,N)^α_ℳ, etc. 
For convenience we also allow that the endpoints of the intervals to be ∅ or V_λ; let (∅, N)^α_ℳ 
be {P∈ℳ^α :P∈_α^*N}  in the first case, and let (N,V_λ)_ℳ^α be {P∈ℳ : N∈^*_α P} in the second.




§ MAIN FORCING


We  fix an inaccessible cardinal κ and a cardinal λ > κ with 
(λ)≥κ such that (V_λ,∈,κ) is suitable. 
We start by defining the forcing notions 𝕄^κ_α, for all α∈ E∪{λ}. 


Suppose α∈ E. We say that p=_p belongs to 𝕄^κ_α if:


  * _p is a finite subset of 𝒞_≤α∪𝒰^κ_≤α that is closed under meets, 

  * _p^δ is a δ-chain, for all δ∈  E∩ (α +1).

We let _q≤_p if for all M∈_p there is N∈_q such that  N η(M)=M.
Finally, let 𝕄^κ_λ=⋃{𝕄^κ_α: α∈ E} with the same ordering.


 Conditions (1) and (2) can be merged to a single condition. Let us say that a δ-chain  consisting of models active at δ
is closed under meets if for every M,N∈, if the meet M N is defined and active at δ then M N∈. 
Thus we can simply say that _p^δ is a δ-chain closed under meets, for all δ∈ E∩ (α +1). 
The order is natural since if Nη(M)= M, then N carries all the information that M does. 


If κ < λ are supercompact cardinals then 𝕄^κ_λ forces the principles GM^+(ω_3,ω_1).
Let us explain what happens. Suppose G is generic over 𝕄^κ_λ. 
Then ω_1 is preserved, but κ becomes ω_2 and λ becomes ω_3 in V[G].

Let  ℳ_G= ⋃ G, and let G_α = G∩𝕄^κ_α, for α∈ E. 
One can show that for every  α∈ E and β > α, V_β[G_α] is a strong ω_1-guessing model in V[G]. 
To see this  fix some δ∈ E ∖β with cof(δ)<κ. 
One shows that if M is a Magidor model in _G^δ then M[G_α] is an ω_1-guessing model in V[G]. 
Moreover, if M is a Magidor model which is a limit of Magidor models in the δ-chain _G^δ then 
M∩ V_δ is covered by the union of the previous models in _G^δ.
Therefore, if we let 𝒢 = { (M∩ V_β)[G_α]: M ∈_G^δ∩𝒰^κ_δ},
then 𝒢 is an increasing sequence of ω_1-guessing models which is continuous at uncountable limits 
and the union of this sequence is V_β[G_α]. 
We will actually present a proof not for the forcing 𝕄^κ_λ, but for a slight variation 
ℙ^κ_λ. We would like to arrange that in addition the set 
{sup (M∩κ) : M∈_G^δ} be a club in κ, for all δ∈ E with cof(δ)<κ. 


In order to achieve this we will add decorations to the conditions of 𝕄^κ_λ. 
This device,  introduced by Neeman  <cit.>, consists of attaching to each model M of an ∈-chain a finite set d_p(M)
which belongs to all models N of the chain such that M∈ N. In a stronger condition this finite set is allowed to increase.
The main point is that d_p(M) controls what models can be added ∈-above M in stronger conditions.
In our situation there are some  complications. First, we have not one chain, but a δ-chain, for each δ∈ E. 
It is therefore reasonable to have decorations for each level δ∈ E. Now, models from a higher level project to lower levels
at which they are active, but also in order to arrange strong properness for countable models, some models from lower levels
will be lifted to higher levels and put on the chain. This imposes a subtle interplay between the decorations on different levels. 
In order to describe this precisely, we need to make some preliminary definitions. 

 Suppose _p∈𝕄^κ_λ. 
Let ℒ(_p)= { Mα: M∈_p  and α∈ a(M)}. 


 Suppose _p∈𝕄^κ_λ. We say that M∈ℒ(_p) is _p-free
if  every N∈_p with M∈_η(M)N  is strongly active at η(M). 
Let ℱ(_p) denote the set of all M∈ℒ(_p) that are _p-free. 

 
Note that if _q≤_p then ℒ(_p)⊆ℒ(_q) and ℱ (_q)∩ℒ(_p)⊆ℱ(_p). 
In other words, a node M∈ℒ(_p) that is not  _p-free is not _q-free, for any  ℳ_q≤ℳ_p.
We are now ready to define our main forcing notion. 
 
 Suppose α∈ E∪{λ}. We say that a pair p=(_p,d_p) belongs to ℙ^κ_α if 
 _p∈𝕄^κ_α, d_p is a finite partial function from ℱ(_p) to 𝒫_ω(V_κ), and 


  (*)   if M ∈ (d_p), N∈_p, and M∈_η(M) N, then d_p(M)∈ N. 

We say that q≤ p if _q ≤_p, and for every M∈(d_p) there is γ∈ E∩ (η(M)+1)
such that Mγ∈(d_q) and d_p(M)⊆ d_q(Mγ). 



 We refer to d_p as the decoration of p. The point is that if M∈ (d_p) is a δ-model then 
d_p(M) constraints what models N with M∈_δ N can be put on  _q^δ, for any q≤ p.
In general, M may not be _q-free, in which case M∉(d_q), but then we have some γ≤δ 
 such that Mγ is _q-free and d_p(M)⊆ d_q(Mγ). 
 Note that then we must have d_p(M)∈ N, for any N∈_q such that M∈_δ N. 

 
The ordering on ℙ^κ_λ is clearly transitive. We will say that q is stronger than p
if q forces that p belongs to the generic filter, in order words, any r≤ q is compatible with p.
We write p∼ q if each of p and q is stronger than the other. We identify equivalent conditions, often without saying it. 
Our forcing does not have meets, but if p and q do have a weakest lower bound we will denote it by p q. 
To be precise we should refer to p q as the ∼-equivalence class of a weakest lower bound, 
but we ignore this point since it should not cause any confusion. 
Note that if p∈ℙ^κ_α and M∈_p is a δ-model that is not active at δ,
we may replace M by Mα(M) and we get an equivalent condition. 
Thus, if α∈ E and (α)≥κ, then ℙ^κ_α is forcing equivalent to 
⋃{ℙ^κ_γ : γ∈ E∩α}. 


 Suppose p∈ℙ^κ_λ and δ∈ E. If M,N∈_p^δ with M∈_δ^* N,
we will write (M,N)_p^δ for the interval (M,N)__p^δ, and similarly, for [M,N)_p^δ, (M,N]_p^δ, etc. 



Suppose α, β∈ E and  α≤β. For  every p∈ℙ^κ_β, 
we let _pα = _pα and d_pα =d_pℱ(_pα). 
It is easily seen that p= (_pα,d_p α)∈ℙ^κ_α. 
The following  is straightforward.


Suppose α,β∈ E with α≤β. Let p∈ℙ^κ_β 
and let q∈ℙ^κ_α be such that q ≤ pα.
Then there exists r∈ℙ^κ_β such that r≤ p,q.



 We let _r = _p ∪_q. Note that _r is closed under meets. 
 We define d_r  by letting  d_r(M)=d_q(M) if M∈(d_q), and d_r(M)= d_p(M) if M∈(d_p) with η(M) > α. 
It is straightforward that r is as required. 


 The condition r from the previous lemma is the greatest lower bound of p and q, so we will write r = p  q. 


 
Suppose α∈ E. Then ℙ^κ_α is a complete suborder of ℙ^κ_λ. 


 
 


Our goal is to prove that our poset ℙ^κ_λ is strongly proper for an appropriate class of models. 
We start by showing that if a condition p belongs to a model M we can always add M to _p and form a new condition. 

 Let p∈ℙ^κ_λ and M∈𝒞∪𝒰 be such that p∈ M.
Then there is a weakest condition p^M≤ p with M∈_p^M.


Suppose first that M is a Magidor model. Then we let ℳ_p^M= _p
and d_p^M=d_p. It is straightforward that p^M=(_p^M,d_p^M) is as required. 

 Now assume that M is countable. We let _p^M be the closure of _p∪{ M} under meets. 
  Fix δ∈ E. We  show that ℳ_p^δ is an ∈_δ-chain. 
 We may assume that  M is active at δ since otherwise ℳ_p^M^δ=∅.
 By <ref> we know that the only models added to ℳ_p^δ in order to form ℳ_p^M^δ are Mδ 
 and N M for N∈ℳ_p^δ such that N M is active at δ.  
 Suppose N∈_p^δ is such a model, and let P be the ∈_δ-predecessor of N in _p^δ, if it exists. 
First note that N∩ M∈ N since N is closed under countable sequence. 
Therefore, N M∈ N. Moreover, if P exists by <ref> we have that P∈_δ N M. 
This establishes that _p^M^δ is a δ-chain. 
 
 Let us now define the decoration d_p^M. Suppose N∈(d_p) is a δ-model. Then δ∈ M. 
 If M is strongly active at δ, then by <ref>, for every Magidor model P∈_p
 if  P M is  active at δ then it is strongly active at δ. Hence N is _p^M-free.
 We  then keep N in (p^M) and let d_p^M(N)=d_p(N). 
 Now, suppose M is not strongly active at δ. This means that δ has uncountable cofinality in M.
 Let δ̅= sup (M∩δ) and note that δ̅ is a limit point of E. 
 We claim that Nδ̅ is _p^M-free. Indeed, if there is P∈_p^M such that 
 N∈_δ̅ P and P is  not strongly active at δ̅, then P∈ M, and hence η(P)≥δ. 
 Moreover, P is active but not strongly active at δ as well. 
 Since N∈_δ̅P and N,P∈ M it follows that N∈_γ P, for unboundedly many γ∈ E∩δ∩ M. 
 But then by <ref> applied in M we conclude that N∈_δ P, and hence N is not _p-free, a contradiction. 
 Notice also that if P∈_p and N∈_δ̅ P then by  <ref> again we must have
 that N∈_δ P and thus d_p(N)∈ P. Therefore, we can replace N by Nδ̅ and 
 let d_p^M(Nδ̅)=d_p(N). 
 It is straightforward to check that p^M is a weakest extension of p such that M∈_p^M.


If N,M are virtual models it will be convenient to set α (N,M)= max (a(N)∩ a(M)). 

 Suppose p∈ℙ^κ_λ and M∈ℒ(_p) is a Magidor model. 
For N∈_p we let N M = N α (N,M) if κ_N < κ_M, 
otherwise N M is undefined. 
Let  

    _p  M = { N  M : N ∈_p}.

Let d_p  M= d_p  ((d_p)∩ M), and let p  M = (_p  M, d_p  M).


 Suppose p∈ℙ^κ_λ and M∈ℒ(_p) is a Magidor model. 
Then p M ∈ℙ^κ_λ∩ M and p≤ p M. 



Since p is a condition, we have that if N∈_p and κ_N < κ_M, then N∈_γ^* M, for 
all γ∈ a(N)∩ a(M). By <ref> we then conclude that N∈_γ M, for all such  γ.
By <ref> we have that α(N,M)∈ M, and hence N α(N,M)∈ M. 
We also have that d_p  M∈ M, thus p  M ∈ M. 
Let us check that _p M∈𝕄^κ_λ. Suppose δ∈ E.
If M is not active at δ then  _p M^δ is empty, otherwise it is equal to 
(∅,Mδ)_p^δ, which is obviously  a δ-chain.
To check that _p M is closed under meets, suppose N M,P M∈_p M 
and their meet is defined. 
Note that then N  P is also defined and, by <ref> (N P)  M = N M  P M. 
It is straightforward to check that every N∈(d_p M) is _p M-free, 
and (*) from <ref> holds. 
Finally, the fact that p≤ p M follows from the definition. 






Suppose p∈ℙ^κ_λ and M∈ℒ(ℳ_p) is a Magidor model. 
Suppose q∈ M∩ℙ^κ_λ extends p M.
Then q is compatible with p and the meet p q  exists. 


We define r∈ℙ^κ_λ and check that it is a weakest condition extending p and q. 
Let ℳ_r=ℳ_p∪ℳ_q. 
We check that if δ∈ E, then _r^δ is a δ-chain closed under meets, meaning
if P,Q∈_r^δ and the meet P Q is defined and active at δ then P Q ∈_r^δ. 
Fix such δ∈ E. If M is not active at δ, then _r^δ = _p^δ and thus has
the required property since p is a condition. Now, suppose M is active at δ. 
If R ∈_r^δ and R∈_δ^*M, then by <ref> we know that R ∈_δ M, 
and by <ref> we get that δ∈ M. Hence R∈ M and therefore R∈_q^δ. 
Therefore, _r^δ is the union of _q^δ and [Mδ, V_λ)_p^δ,
and hence is a δ-chain. Now suppose P,Q∈_r^δ and their meet is defined
and active at δ. We need to check that Q P ∈_r^δ. 
If both P and Q belong either to _q^δ or _p^δ, this follows from the fact
that p and q are conditions.  Since Q∈_δ P and _q^δ is an ∈_δ^*-initial segment of _r^δ,
we may assume Q∈_q^δ and P∈_p^δ∖_q^δ. 
The proof goes by induction on the number of Magidor models on the δ-chain 
[Mδ, P)_p^δ. 
If M∈_δ P then M P ∈_p^δ and is δ-below Mδ, hence
belongs to _q^δ. On the other hand, by  <ref> we have 
Q P= Q  (M  P), and since _q^δ is closed under meets we get 
that Q P∈_q^δ. 
In general, if N is the ∈_δ^*-largest Magidor model in [Mδ, P)_p^δ,
by <ref>, we have that Q∈_δ N ∈_δ P. In particular, N P is defined
and by <ref> we have that Q  P = Q  (N P). 
Now, we are done if N P ∈_q^δ as q is a condition.
Otherwise, it belongs to the interval [Mδ, P)_p^δ.
Then there are fewer Magidor models in [Mδ, N P)^δ_p and thus we can use
the induction hypothesis. 

Let d_r = d_q ∪ d_p  ((d_p)∖ M). 
Let us check that every N∈(d_r) is _r-free. For simplicity, let η=η (N). 
If N∈(d_p)∖ M, then 
there is no P∈_q such that N∈_η P, and hence the conclusion follows from the fact that p is a condition.
Suppose now N∈(d_q) and P∈_r is such that N∈_η P. We have to check 
that P is strongly active at η. We may assume that P is a countable model. 
If Pη is η-below M, then P M  is defined and P M≅_η P, 
therefore, the conclusion follows from the fact that q is a condition. 
If Pη is η-above M, then M P is defined and belongs to _p.
Moreover,  by <ref>, N∈_η M P. 
Now (M P) M is defined, and belongs to _q^α(M P,M),  and is strongly active at η since N is _q-free. 
Therefore, P is also strongly active at η. 
The fact that d_r satisfies condition (*) from <ref> is straightforward. 
Finally, the fact that r is the weakest common extension of p and q follows readily from the definition. 
 

By <ref> and  <ref> we immediately get the following. 

 
   The forcing ℙ^κ_λ is 𝒰-strongly proper.
   
 
 
  
We now proceed to define an analogue of p M for  countable models M∈ℒ(_p).
The situation here is more subtle since p M may not belong to the original forcing, only its version as defined in M.
We first analyze the part  involving _p. It will be useful to make the following definition. 

 Let  be a subset of 𝒞∪𝒰 and M∈𝒞. 
For δ∈ E, we let ( M)^δ = { N ∈^δ : N ∈_δ M}. 



Let  _p∈𝕄^κ_λ and δ∈ E. Suppose M∈ℳ_p^δ is  countable. 
Then (_p M)^δ is a δ-chain closed under meets and

    (_p M)^δ = (∅,Mδ)_p^δ∖⋃{ [N M,N)^δ_p:N∈ (ℳ_p M)^δ and is a Magidor model}.

Here, if N M is defined and not active at δ, by [N M,N)_p^δ we mean (∅, N)_p^δ. 



It is clear that  (ℳ_p M)^δ⊆ (∅,M)_p^δ.
Suppose P∈_p^δ and P∈_δ M. 
Then, for any Magidor model N∈ (P,M)_p^δ, we have P∈_δ N by <ref>.
Then by   <ref> we have that P∈_δ N M. 
Conversely, suppose P is in  (∅,M)^δ_p, but not in (ℳ_p M)^δ.
Then, by <ref> again, there must be a Magidor model N∈_p^δ such that P∈_δ N ∈_δ M. 
Let N be the ∈_δ^*-least such model. If N M is not active at δ, then P∈ (∅,N)_p^δ.
Suppose N M is active at δ. We have to show that either P=N M or N M ∈_δ^*P. 
Indeed, otherwise we have P∈_δ^* N M. Note that there cannot be a Magidor model Q∈_p^δ 
with P∈_δ Q ∈_δ N M since then we would have Q∈_δ M as well, and this contradicts the minimality of N.
Since _p^δ is a δ-chain, by <ref> we conclude that P∈_δ N M, but then also P∈_δ M, 
a contradiction. The fact that (_p M)^δ is a δ-chain follows from the above analysis. 
By <ref> it is also closed under meets. 



 Let p∈ℙ^κ_λ and M,N∈_p.
If there is γ∈ a(M)∩ a(N) such that N∈_γ M, then N∈_δ M, for all δ∈ a(M)∩ a(N). 


 Let α = α(M,N). If N∈_α M then N∈_γ M, for all γ∈ a(M)∩ a(N), by 
<ref>. Now suppose N∉_α M. If M is a Magidor model we have κ_M≤κ_N,
and hence there is no γ such that N∈_γ M. 
Assume now that M is countable. Then by <ref> there is a Magidor model P∈_p^δ with P∈_δ M
such that Nδ is in the interval [P M, P)_p^δ. 
Now, P M is active at all γ∈ a(N)∩α and Nγ is in the interval 
[(P M)γ, Pγ)_p^γ,
for all such γ. But then, by <ref> again, N ∉_γ M, for all γ∈ a(M)∩ a(N).



It would be useful to introduce some notation. 

 Suppose M∈𝒱 and  is a finite subset of 𝒱. Let α∈ E. 
We write ∈_α M if N∈_α M, for all N∈. 


 Suppose _p∈𝕄^κ_λ and δ∈ E. 
Suppose M∈_p^δ is a countable model,  ∈_δ M is a finite δ-chain closed under meets,
and  (_p M)^δ⊆. Then the closure of _p^δ∪ under meets that are active at δ
is a δ-chain. 



 
 Let us first show that _p^δ∪ is a δ-chain. Indeed, by <ref> 
 it is obtained by adding  to  the intervals [N M, N)_p^δ, where N∈ (_p M)^δ is a Magidor 
 model, and the interval [M,V_λ)_p^δ. Consider one such interval, say [N M,N)_p^δ. 
 If P is the last model of  before N then P∈_δ M by the assumption that ∈_δ M,  
 and P∈_δ N by <ref>. Hence by <ref> we have that P∈_δ N M. 
 It follows that _p^δ∪ is a δ-chain. 
 
 Let us now consider what happens when we close _p^δ∪ under meets that are active at δ. 
Suppose Q, P∈_p^δ∪, Q is a Magidor model, P is countable, and Q∈_δ P.
If P∈ then Q∈_δ P∈_δ M, and hence by <ref> Q∈ M, and so Q∈ as well. 
Since  is closed under meets, we have that Q P∈. 
Now suppose P∈_p^δ∖. By <ref> we have that P∈ [M,V_λ)_p^δ
or P∈ [N M,N)_p^δ, for some Magidor model N∈ (_p M)^δ.
The two cases are only notationally different, so let us assume that there is  a Magidor model  N∈ (_p M)^δ 
such that P∈ [N M,N)_p^δ. 
We may assume that Q∈.
Note that  Q∈_δ N and Q∈_δ M, hence by <ref> Q∈_δ N M.
If there is a Magidor model R∈_p such that Q∈_δ^* R∈_δ^* P, 
let R be the ∈_δ^*-largest such model. By <ref> we have that R∈_δ P and
hence R P is defined and is below P on the δ-chain _p^δ. 
Moreover, since _p∪ is a δ-chain, also by <ref>, we have Q∈_δ R. 
Now, by <ref> we have that Q∈_δ R  P, and by <ref> we have  Q P = Q (R P). 
Therefore, we may assume that there are no Magidor models R∈_p^δ with Q∈_δ R ∈_δ P. 
Now, let { P_i : i < k} list all countable models on the chain [N M,N)_p^δ below the first Magidor model, if it exists. 
Then P_0= N M and P= P_j, for some j. Note that Q∈_δ P_i, for all i<k, again by <ref>.
Now let S be the ∈_δ^*-predecessor of N  on the δ-chain _p^δ∪, if it exists, otherwise let S be ∅. 
Note that S∈_δ N M. Indeed, if S∈_p this follows from <ref>, and the fact that 
there are no Magidor models in (S,N M)_p^δ.  If S∈ then S∈_δ M and thus S∈_δ N M. 
Now, by <ref> we have that S∈_δ P_i, for all i< k. 
Hence, by <ref> we have S∈_δ Q P_i, for all i. 
By <ref> we have Q P_i∈_δ P_i+1, for all i < k-1. 
Since Q is a Magidor model, we also have that Q P_i ∈_δ Q, for all i<k.
By <ref> again, we have that Q P_i ∈_δ Q P_i+1, for all i< k-1. 
Therefore, S∈_δ Q P_0∈_δ…∈_δ Q P_k-1∈_δ Q,
and Q P appears on this chain. If S=∅ then an initial segment of this chain may be nonactive
at δ, but the remainder is still a δ-chain. 
 




Now, suppose p∈ℙ^κ_λ and M∈_p is a countable β-model, for some β∈ E. 
Let A= Hull(M,V_β). Then A∈𝒜_β. 
Note that E_A∩β= E∩β, and if β∈ A then β∈ E_A. 
Also, note that the definitions of ℙ^κ_α and the order  relation is Σ_1 with parameter V_α. 
For α∈ E_A, let (ℙ^κ_α)^A be the version of ℙ^κ_α as defined in A.  
Then  (ℙ^κ_α)^A= ℙ^κ_α if α < β, and 
(ℙ^κ_β)^A⊆ℙ^κ_β. 
We will let 𝒱^M_α= 𝒱^A_α∩ M, and
(ℙ^κ_α)^M= (ℙ^ κ_α)^A∩ M, if α∈ E_A∩ M. 
Suppose N∈_p and  N∈_δ M, for some δ∈ a(M)∩ a(N),
Then by <ref>, N∈_α M, where α = α (M,N). 
Note that if M is a standard β-model then α < β. 
It may be that α∉ M, but then, if we let α^*= min (M∩ ORD∖α), we have
that α^*∈ E_A∩ M, and α^* is of uncountable cofinality in A. 
By the previous remarks, if M is a standard β-model or β∈ M then α^*∈ E∩ (β +1),
otherwise α^* may be in the nonstandard part of M.
Since N∈_α M, there is a model N^*∈ M with N^*∈𝒱^A
which is α-isomorphic to N. Now, M can compute N^*α^*, hence we may assume
N^*∈𝒱^A_α^*. Moreover, such N^* is unique. Indeed, if there is another model N^**∈ M with the same
property, since α^* is the least ordinal in M above α and N^*≅_α N^**
we would have that N^*≅_δ N^**, for all δ∈ E_A ∩α^*∩ M.
Hence, by <ref> applied in M,  we would have that N^*=N^**.
This justifies the following definition. 


 
Suppose p∈ℙ^κ_λ and let M∈ℒ(_p) be a countable β-model, for some β∈ E. 
Let N∈_p and let α = α (M,N). If N∈_α M we let α^*= min (M∩ ORD∖α).
We define N M to be the unique  N^*∈𝒱^M_α^* such that N^* ≅_α N.  
Otherwise we leave N M undefined. Let
 
    _ p M = { N M : N∈_p},  and


    (d_p  M)= { N M: N∈(d_p)  and  N∈_η (N)M }.

If N∈(d_p) and N∈_η(N) M, let d_p M(N M)= d_p(N).
Let p M = (_p M,d_p  M). 


 Suppose N∈ (d_p) and let η= η(N). If N∈_η M then M is strongly active at η since N is _p-free. 
If η∈ M then we put N in (d_p M) and keep the same decoration at N. 
If η∉ M we lift N to the least level η^* of M above η, we put the resulting model N^* in (d_p M)
and copy the decoration of N to N^*.  If P∈_p is such that Pη =N then (P M)η^* = N^*.
Moreover, from N^* we can recover N as N^*sup (η^*∩ M). Thus, the function d_p M is well defined. 
Note also that p M ∈ M. 



Suppose p∈ℙ^κ_λ and M∈ℒ(_p) is a countable β-model, for some β∈ E.
Let 

    α= max{α(N,M): N∈_α(N,M)M  and  N∈_p}.

Let α^*=min (M∩ ORD∖α). Then p M∈ (ℙ^κ_α^*)^M.


 Let A= Hull(M,V_β) and work in A.  It is clear that _p M is a finite subset of 
𝒞_≤α^*^A ∪𝒰_≤α^*^A. 
We first show that  _p M^γ is a γ-chain closed under meets, for all γ∈ E_A∩ (α^*+1). 
Fix such γ and let δ=min (M∩ ORD∖γ) and δ̅= sup (M∩δ). 
If δ̅= δ then γ = δ, and hence γ∈ M and the conclusion follows from the fact that p is a condition
and <ref>.
Let us assume now that δ̅< δ. Note that then δ̅,δ∈ E, δ is of uncountable cofinality in M,
and is a limit point of E. 
Note that if P∈_p M is a δ-model that is active at γ then a(P) is cofinal in δ.
Moreover, a(P)∈ M and since δ̅= sup (M∩δ) we have that δ̅∈ a(P).
This implies that _p M^γδ̅= _p^δ̅ M. 
Therefore, by <ref> it is a δ̅-chain closed under active meets. 
Now, suppose N,P∈_p M^δ and N∈_δ̅ P.
Since δ̅= sup (M∩δ) we have that N∈_ξ P, for unboundedly many ξ∈ E∩δ. 
We conclude that N∈_δ P. Indeed, if P is countable this follows from <ref> applied in A, and
if P is a Magidor model this follows from <ref>, again applied in A.
Moreover, assuming N is a Magidor model and P is countable, and Nγ Pγ is defined and active at γ
then, by <ref>, N P is defined and active at unboundedly many ξ∈ E∩δ, and hence it is also active at δ and δ̅. 
It follows that _p M^δ is a δ-chain closed under meets, and hence _p M^γ
is  a γ-chain closed under meets as well. 

Let us check that every P^*∈(d_p M) is _p M-free. 
If P^*  ∈(d_p) this is immediate. 
Otherwise, P^* is of the form P M, for some P∈(d_p)
such that η(P)∉ M. Let η=η(P) and η^*=η(P^*). Note that M is strongly active at η
and η^* is the least ordinal of M above η. Suppose N∈_p M is such that P^*∈_η^* N. 
Then Nη∈ℒ(_p) and P∈_η N. Since P is _p-free, N must be strongly active at η. 
Since η= sup (M∩η^*) and N∈ M we must have that N is strongly active at η^* as well. 
This also establishes (*) from <ref>. Indeed, if P^*∈_η^* N then P∈_η Nη, and
hence d_p(P)⊆ N, since Nη∈ℒ(_p), and p is a condition. 
This completes the proof that p M= (ℙ^κ_α^*)^A.


 Note that if p,q∈ℙ^κ_λ are such that q≤ p and M∈_p then 
q M ≤ p M. 


We are planning to show that if p is a condition and M∈_p is a countable β-model
then, for  any q≤ p M with q∈ M, p and qβ  are compatible, and in fact
the meet p qβ exists. 
Before that we show the following special case of this statement. 


 Suppose p∈ℙ^κ_λ and δ∈ E. 
Suppose M∈_p^δ is a countable model,  ∈_δ M, ∈𝕄^κ_δ, 
and  (_p M)^γ⊆^γ, for all γ∈ E∩ (δ +1). 
Suppose further that P∉_η(P)M, for all P∈(d_p). 
Let _q be the closure of _p ∪ under meets and let d_q=d_p. Finally, let q=(_q,d_q).
Then q∈ℙ^κ_λ. 


 Let us first check that _q^γ is a γ-chain closed under active meets, for all γ∈ E.
Fix γ∈ E.  If M is not active at γ then _q^γ =_p^γ, so this follows from the fact that p is a condition. 
 If M is active at γ then  this follows from <ref>. 

Thus, it remains to check that every P∈ (d_p) is _q-free
and d_p(P)∈ Q, for all Q∈_q such that P∈_η(P)Q. 
Now, fix one such P∈(d_p) and let η = η(P).
If M is not active at η, then no model of  is active at η, and hence Q∈_p, for all Q∈_q such that P∈_η Q. 
The conclusion then follows from the fact that p is a condition and d_p is its decoration. 
Suppose now that M is active at η, but P is either equal to Mη or is above Mη on the η-chain _p^η.
Then, again any Q∈_q such that P∈_η Q is in _p, and the conclusion follows as above. 
Suppose now that M is active at η and P∈_η^*M. Note that _q^η is obtained by
closing _p^η∪^η under meets that are active at η. 
Suppose P is below Mη on _p^η. By the assumption, P∉_η M, hence by <ref>, 
there must be a Magidor model N∈ (_p M)^η such that P is in the interval [N Mη ,N)_p^η.
By <ref>, we have that P∈_η N and thus d_q(P)∈ N. 
Note that P also belongs to the interval [N Mη,N)_q^η.
Suppose Q∈_q and P∈_η Q. By replacing Q with Qη, we may assume that Q∈^η.
Note that Q cannot be a countable model since then we would have P∈_ηM. 
If Q is a Magidor model in ^η then Q cannot be below N since then it would be below N Mη on _q^η.
Therefore, Q must be either equal to N or above N on the η-chain  ^η. 
Then we would have N∩ V_κ⊆ Q ∩ V_κ, and hence d_p(P)∈ Q.
If Q∈_p then Q is strongly active at η and d_p(P)∈ Q, since p is a condition. 
It remains to consider the case when Q is of the form R S, for some Magidor model R∈^η
and countable S∈_p^η∖^ η.
Now, we must have R=N or N∈_η R since otherwise R, and hence also  R S, would be below N Mη.
Since d_p(P)∈ N, we must have d_p(P)∈ R. 
Moreover, since S ∈_p^η, and d_p is the decoration of p, 
S must be strongly active at η and d_p(P)∈ S. 
By <ref>, R S is strongly active at η. 
By <ref>, we have R S ∩ V_η = R∩ S∩ V_η, and hence d_p(P)∈ R S=Q. 




 
 
Suppose p∈ℙ^κ_λ and M∈ℒ(_p) is a countable β-model, for some β∈ E.
Let α^*∈ M be such that p M∈ (ℙ^κ_α^*)^M.
Then for any q∈ (ℙ^κ_α^*)^M with q≤ p M, p and qβ are compatible,
and the meet p qβ exists. 


 Let _r be the closure of _p ∪_qβ under meets. By <ref> we already know
that _r^δ is a δ-chain, for all δ∈ E. Hence _r∈𝕄^κ_λ. 
It remains to define the decoration d_r, and check that it satisfies (*) from <ref>.
Let 

    D_p= { P∈(d_p) : P∉_η(P) M}.

 Now, suppose P∈(d_q). 
 
 Let δ (P) be the largest ordinal γ∈ E∩ (η(P)+1) such that M is strongly active at γ. 
 Let 
 
    D_q= { Pδ(P) : P∈ (d_q)}.

Note that, for every P∈(d_q), we have (P δ(P)) M = P, and P is active at δ(P). 
Observe that D_p and D_q are disjoint. 
Let (d_r)= D_p ∪ D_q and define d_r by: 

    d_r(P) =  
                 d_p(P)     P∈ D_p 
    
                 d_q(P M)     P∈ D_q  and η(P)≤β

We have to check that every P∈(d_r) is _r-free and condition (*)  holds. 
By <ref> we have that (_r,d_p D_p) is already a condition,
so we may assume P∈ D_q. 
Fix one such P∈ D_q, and  let η = η(P).  

Note that it suffices to show that the least model, say R,  on the η-chain _r^η above P
is strongly active at η, and d_r(P)∈ R. 
By  <ref> either R∈_η M or R=N Mη, for some Magidor model N∈ (_p M)^η. 
Now, if R is of the form N M, then, since N and  M are strongly active at η, by <ref>, so is R. 

Moreover, N M∈ℒ(_q) and d_q(P M)∈ M∩ N. It follows that d_r(P)∈ R.
Suppose now that  R∈_η M. Let ρ= min (E∩ M∖η). 
Then P M and R M are ρ-models, R M∈ℒ(_q), and P M ∈_ρ R M. 
Therefore, R M is strongly active at ρ, and d_q(P M)∈ R M. 
Since (R M) ∩ V_κ = R∩ V_κ, we get that d_q(P M)∈ R, and hence d_r(P)∈ R. 
Moreover, since R M is strongly active at ρ, it follows that R is strongly active at η. 
This shows that all the models in (d_r) are _r-free and condition (*) holds for r. 
The fact that r≤ p,qβ and is in fact the weakest such condition follows from the definition.  


 Suppose p∈ℙ^κ_λ and M∈_p is a countable β-model,
for some β∈ E. If either M is standard or β∈ M we have that p  M∈ℙ^κ_λ. 
 In particular, <ref> shows that if p∈ℙ^κ_λ then p and p M 
are compatible. Now, we have already observed that, if  q∈ℙ^κ_λ and q≤ p,
then q M ≤ p M. Therefore, even though  it may not be the case that p≤ p M,
 every p forces p M to belong to the generic filter, and hence p is stronger than p M. 


Now, by <ref> and <ref> we immediately get the following. 



ℙ^κ_λ is 𝒞_ st-strongly proper.
 

Suppose M∈𝒞 and p∈ M∩ℙ^κ_λ. Let p^M be the condition defined
in <ref>. If q≤ p^M then M∈ℒ(_q) and q M∈ M, and by <ref>, q M ∈ℙ^κ_λ. 
Then, by <ref> any extension r of q M with r∈ M 
is compatible with q, and moreover q r exists. 
Thus, p^M is a (M,ℙ^κ_λ)-strongly generic condition extending p.




A  similar proof shows that the forcing ℙ^κ_α is strongly proper for the collection of
all  M∈𝒞 such that α∈ M. 




Let F be a filter in ℙ^κ_λ. Then we let ℳ_F denotes ⋃{ℳ_p: p∈ F}.


Let G be a ℙ^κ_λ-generic filter over V. 
We let G_α=G∩ℙ^κ_α, for all α∈ E. 
The following is straightforward. 



 Let δ∈ E with cof(δ)<κ. Then ℳ_G^δ is a δ-chain.

 
 

 Let δ∈ E  with cof(δ)<κ. 
Suppose M∈_G^δ is a Magidor model and is not the least model in _G^δ.
Then  M∩ V_δ = ⋃{ Q∩ V_δ : Q∈_δ M  Q∈_G^δ}. 


 It suffices to show that if p∈ℙ^κ_λ and M∈_p^δ is a Magidor model
that is not the least model of _p^δ, and x∈ M∩ V_δ, then there is q≤ p
and Q∈_q which is active at δ such that  Q∈_δ M and x∈ Q. 
Let N∈_p be active at δ such that N∈_δ M. 
Fix some Q^*∈𝒞 such that N,M,x∈ Q^*. By Lemma <ref> there
is a condition q≤ p such that Q^*∈_q. Since N∈_δ M and N∈_δ Q^*,
if we let Q= M∧ Q^*, by <ref> N∈_δ Q, and hence Q is active at δ. 
Moreover, Q∈_δ M and by <ref> Q∩ V_δ = N∩ Q^* ∩ V_δ and hence
x∈ Q. It follows that the condition q and the model Q are as required. 







 Assume κ is supercompact. 
Then ℙ^κ_λ preserves ω_1 and κ, and collapses all cardinals 
between ω_1 and κ to ω_1. 


By  <ref>, 𝒞_ st is stationary  in 𝒫_ω_1(V_λ), and 
by <ref>, ℙ^κ_λ is 𝒞_ st-strongly proper. Hence ω_1 is preserved. 
By <ref>, 𝒰 is stationary in 𝒫_κ(V_λ), and by <ref>,
ℙ^κ_λ is 𝒰-strongly proper. Hence κ is preserved. 
Now,  fix  a  cardinal μ<κ. Let G be a ℙ^κ_λ-generic filter over V. 
Fix  α∈ E of cofinality less than κ. 
A standard density argument shows that there exists a Magidor  model N∈_G^α  such that μ∈ N. 
By <ref>  ℳ_G^α is an ∈_α-chain. 
Let N^* be the least Magidor model above N in ℳ_G^α, and let  I=(N,N^*)^α__G.
Note that every model in I is countable and ∈_α is transitive on I. 
Hence if P,Q∈ I and P∈_α Q then P∩ V_α⊆ Q∩ V_α. 
Another standard density argument shows that, for every x∈ N∩ V_α, there is P∈ I such that 
x∈ P. Thus, { P∩ V_α: P∈ I} is an increasing chain of countable sets whose union covers N∩ V_α. 
It follows that N∩ V_α is of cardinality at most ω_1. Since μ belongs to the transitive part of N,
we also get that | μ | ≤ω_1. 




ℙ^κ_λ collapses cardinals of the interval between κ and λ to κ.


Let α∈ E be of cofinality less than κ, and let G be a V-generic filter over ℙ^κ_λ.. 
Let U_α be the set of Magidor models in _G^α. By <ref>, we have that 
∈_α is transitive on U_α. Note that if P,Q ∈ U_α then P∩ V_α⊆ Q∩ V_α. 
Now, a standard density argument using the stationarity of 𝒰 shows that, for every x∈ V_α, there is P∈ U_α such that x∈ P. 
It follows that { P∩ V_α : P∈ U_α} is an increasing family of sets of size <κ whose union is V_α.
Therefore, V_α has cardinality ≤κ in V[G].   




Suppose λ is an inaccessible cardinal. Then ℙ^κ_λ is λ-c.c.


For each p∈ℙ^κ_λ, let a(p)=⋃{ a(M): M∈_p}. 
Note that a(p) is a closed subset of E of size <κ, for all p. 
Suppose A is a subset of P^κ_λ of cardinality λ. 
Since λ is inaccessible, by a standard Δ-system argument, we can find a subset B of A of size λ 
and a subset a of E such that a(p)∩ a(q)= a, for all distinct p,q∈ B. 
Note that a is closed, and if we let γ = max(a) then γ∈ E.
Since B has size λ, by a simple counting argument, we may assume there is ∈𝕄^κ_γ
such that _pγ =, for all p∈ B. 
Now, pick distinct p,q∈ B, and define _r= _p ∪_q and d_r= d_p ∪ d_q. 
Let r=(_r,d_r). It is straightforward to check that r∈ℙ^κ_λ and r≤ p,q. 
  



 Suppose G is V-generic over ℙ^κ_λ and α∈ E is of cofinality less than κ. 
Let C_α(G)= {κ_M : M∈_G^α}. 




Let G be a V-generic filter over ℙ^κ_λ. Then C_α(G) is a club in κ, for all α∈ E
of cofinality <κ.  Moreover, if α < β then C_β(G)∖ C_α(G) is bounded in κ. 

 
Let us check the second statement first. Fix α, β∈ E such that (α), (β) <κ, and α <β.
By a standard density argument using the stationarity of 𝒰 there is p∈ G and a Magidor model M∈_G which is active at both α and β. 
Therefore, any model N above Mβ on the β-chain _G^β is also active at α. 
It follows that C_β(G)  ∖ C_α(G)  ⊆κ_M. 

We work in V and prove the first statement by induction on α. 
Let ^α and Ċ_α be canonical ℙ^κ_λ-names for _G^α and C_α(G), for  α∈ E.
Now, fix  α∈ E of cofinality less than κ and suppose
the statement has been proved for all α̅∈ E∩α of cofinality <κ. 
Suppose γ <κ and p∈ℙ^κ_λ forces that γ is a limit point but not a member of Ċ_α 
We may assume that there is a model M∈_p^α such that p forces that M is the least model on the α-chain ^α
such that γ≤κ_M. Then we must have γ < κ_M. Let P be the previous model on _p^α before M. 
We may assume that such a model exists since p forces that γ is a limit point of Ċ_α.  
Note that κ_P <γ since p forces that γ∉Ċ_α.

Case 1. Suppose M is strongly active at α.
Since  P is _p-free and we may assume that P∈(d_p), by defining d_p(P)=∅ if necessary. 
Since γ < κ_M, we can find δ∈ M such that γ≤δ < κ_M. 
Define a condition q as follows. Let _q=_p, and let (d_q)=(d_p). 
Let d_q(P)= d_p(P)∪{δ}, and d_q(Q)=d_p(Q), for any other Q∈ (d_p). 
Let q= (_q,d_q). Then q is a condition and forces that the next model of ^α above P contains δ.
Hence, it  forces that there is no element of Ċ_α between κ_P and γ, 
and so it forces that γ is not a limit point of Ċ_α, a contradiction. 

Case 2. Suppose now that M is not strongly active at α. Then M is countable.
Let A= Hull(M,V_α), let α^*
be the least ordinal of M above α, and let α̅= sup (M∩α). 
Note that α^*∈ E_A, α̅ is a limit point of E of cofinality ω, and that P is also active at α̅.
Now, by the proof of the second part of the lemma,  p  forces that Ċ_α∖Ċ_α̅⊆κ_P,
and so it also forces that γ is a limit point of Ċ_α̅.
By the inductive assumption Ċ_α̅ is forced to be a club, so there is q≤ p and some N∈_q^α̅ such that κ_N= γ. 
Now,  for each Q∈ (_q M)^α̅, we can find a unique model Q^*∈ M with Q^*∈𝒱_α^*^A
such that Q^*α̅= Q. Let ^*= { Q^*: Q ∈ (_p M)^α̅}. 
Working in A, ^* is an α^*-chain closed under meets that are active at α^*.
Let = { Q^*α : Q^*∈^*}. Then ∈_α M, is an α-chain closed under meets
that are active at α, and (_q M)^α⊆. 
We now define a condition r. Let _r be the closure of _p and  under meets. 
By applying <ref>, for all levels δ∈ E∩ (α̅,α], we have that _r∈𝕄^κ_λ. 
Let d_r=d_q and r=(_r,d_r). Observe that _r^η = _q^η, 
for all  η∈ E ∖ (α̅,α].
Also, if R∈ (d_q) and η(R)∈ (α̅, α] then R∉_η(R)M, since M is not strongly active at η (R).
By <ref>, we conclude that r is a condition. Also, we have that r≤ q. 
Recall that N∈_q^α̅ and κ_N=γ.
Let Q be the model on the α̅-chain _r^α̅ immediately before Mα̅.  
Then Q^* ∈^*, and hence Q^*α∈_r. Let R=Q^*α. 
In other words, we lifted the model Q to level α and called this model R. 
Note that κ_R= κ_Q. 
Then r forces that R∈_α and γ≤κ_R < κ_M, which contradicts the fact
that p forces that γ∉Ċ_α and M is the least model on _α with γ≤κ_M. 
This completes the proof of the lemma. 







§ GUESSING MODELS IN V[G]


We assume κ is supercompact and λ is inaccessible and analyze ω_1-guessing models 
in the the generic extension by ℙ^κ_λ. 
Suppose α∈ E. We have already established in <ref>  that ℙ^κ_α
is a complete suborder of ℙ^κ_λ. 
Let us fix  a V-generic filter G_α over ℙ^κ_α, and let ℚ_α  denote the quotient forcing. 
Recall that  ℚ_α consists of all p∈ℙ^κ_λ such that  pα∈ G_α,
with the induced ordering. Forcing with this poset over V[G_α] produces a V-generic filter G for ℙ^κ_λ
such that G∩ℙ^κ_α= G_α. 
We first show that the pair (V[G_α],V[G]) has the ω_1-approximation property. 
We will need the following definition. 

Let 𝒞^α_ st denote the set of all M∈𝒞_ st such  that η(M)> α, α∈ M,
and  Mα∈_G_α. 


 𝒞^α_ st is stationary subset of 𝒫_ω_1(V_λ)
in the model V[G_α]. 


We work in V. Let 𝒞̇^α_ st and _α be the canonical ℙ^κ_α-names
for 𝒞^α_ st and _G_α.
Suppose p∈ℙ^κ_α forces that  Ḟ: [V_λ]^<ω→ V_λ is a function.

Let θ be a sufficiently large regular cardinal. By <ref>, 𝒞_ st is club in 𝒫_ω_1(V_λ),
hence we can find a countable M^*≺ H(θ)  containing all the relevant objects such that
letting M=M^*∩ V_λ we have that M ∈𝒞_ st. 

Let M'= Mα.  Note that p∈ M', so we can form the condition p^M'.
Then  p^M'  is (M',ℙ^κ_α)-strongly generic and p^M'≤ p. 
 Let σ be the α-isomorphism between M and M'. 
Note that σ(q)=q, for all q∈ M∩ℙ^κ_α. 
Hence, M ∩ℙ^κ_α=  M' ∩ℙ^κ_α.
Therefore, p^M' is also (M,ℙ^κ_α)-strongly generic, and thus it is (M^*,ℙ^κ_α)-generic.
Since Ḟ∈ M^*, it follows that p^M' forces that M is closed under Ḟ.
It also forces that M' belongs to _α, hence it forces that M belongs to 𝒞̇^α_ st. 


 Suppose α∈ E and let G_α be V-generic over ℙ^κ_α. 
Then ℚ_α is 𝒞^α_ st-strongly proper.


 
Work in V[G_α]. Let p∈ℚ_α, and M∈𝒞^α_ st be such that p∈ M. 
Let p^M be the condition defined in <ref>. Since α∈ M we have pα∈ M, and also pα∈ Mα.
Note that p^Mα = (pα)^Mα. 
Since pα∈ G_α and Mα∈_G_α, we have that p^Mα∈ G_α,
thus p^M∈ℚ_α. 
Let us show that p^M is (M,ℚ_α)-strongly generic. 
Suppose q≤ p^M and qα∈ G_α. 
Since α∈ Mα we have  (q M)α= (qα) (Mα), 
and hence q M ∈ M ∩ℚ_α.
Let r≤ q M be such that r∈ M ∩ℚ_α.
By <ref>, r and q are compatible in ℙ^κ_λ and the meet r q exists. 
Now, observe that the meet of rα and qα exists, and 
rα qα =(r q)α. Since rα, qα∈ G_α,
we conclude that rα qα∈ℚ_α. 
It follows that q and r are compatible  in ℚ_α.



Now, by <ref>, <ref>, and <ref>, we get the following. 

 The pair (V[G_α],V[G]) has the ω_1-approximation property. 


 
 


Suppose now N∈𝒰.
Let 1^N=({ N}, ∅). By <ref>, 1^N is
(N,ℙ^κ_λ)-strongly generic. Moreover, for every q≤1^N and r≤ q N,
q and r are compatible, and the meet q r exists. Let ℙ_N= ℙ^κ_λ∩ N
and let 

    ℙ^κ_λ N = { q∈ℙ^κ_λ : N∈_q}.
 
Then the map p↦ p^N is a complete embedding from ℙ_N to ℙ^κ_λ N. 
Now, fix a V-generic filter G_N over ℙ_N. 

 Let G_N be a V-generic filter over ℙ_N. 
Let 𝒞^N_ st denote the set of all M∈𝒞_ st such  that N∈ M and N M∈_G_N.



The collection 𝒞^N_ st is stationary in 𝒫_ω_1(V_λ) in the model V[G_N].



This is very similar to the proof of <ref>. 
We work in V. Let 𝒞̇^N_ st be the canonical ℙ_N-name for 𝒞^N_ st.
Suppose p∈ℙ_N forces that  Ḟ: [V_λ]^<ω→ V_λ is a function.
Let θ be a sufficiently large regular cardinal. By <ref>, 𝒞_ st is stationary in 𝒫_ω_1(V_λ),
hence we can find a countable M^*≺ H(θ)  containing all the relevant objects.
Let M=M^*∩ V_λ, and note that M ∈𝒞_ st. Since N∈_η(N)M, the meet N M is defined.
Let η = η (N M) and let σ be the η-isomorphism between N∩ M and N M.
Note that σ (q)=q, for all q∈ℙ_N. 
Now, p^N M is (N M, ℙ_N)-strongly generic, hence also (N∩ M, ℙ_N)-strongly generic, 
and therefore it is (M^*,ℙ_N)-generic. It follows that p^N M forces that M∈𝒞̇^N_ st and
is closed under Ḟ. 


Let ℚ_N denotes the quotient forcing (ℙ^κ_λ N)/G_N. 



ℚ_N is 𝒞^N_ st-strongly proper.



Work in V[G_N]. Let p∈ℚ_N and  M∈𝒞^N_ st be such that p∈ M. 
Let p^M be the condition defined in <ref>. Since p,N∈ M, we have p N ∈ M. 
Thus, p N ∈ N∩ M. 
Observe that p^M N= (p N)^N M.  
Since p N ∈ G_N and N M ∈_G_N, we have that p^M N ∈ G_N,
thus p^M∈ℚ_N. 
Let us show that p^M is (M,ℚ_N)-strongly generic. 
Suppose q≤ p^M and q∈ℚ_N.  
Observe that (q M) N = (q N) (N M), and hence q M ∈ℚ_N.
Let r≤ q M be such that r∈ M∩ℚ_N.  
By <ref>, r and q are compatible in ℙ^κ_λ and the meet r q exists. 
Note that  r N∈ N∩ M ⊆ N M,  and r N extends (q N) (N M). 
Hence, again by <ref>, the meet of r N and q N exists,
and  r N  q N = (r q) N. 
Since r N, q N ∈ G_N,  we have that r N  q N ∈ G_N. 
It follows that r and q are compatible in ℚ_N. 



Suppose G is a V-generic filter over  ℙ^κ_λ. 
As before, for α∈ E,  let G_α= G∩ℙ^κ_α.




Let α∈ E. Suppose N∈_G is a Magidor model with α∈ N.
 Then N[G_α]  is an ω_1-guessing model in V[G]. 


 
 Let N be the transitive collapse of N, and let π be the collapsing map. 
 For convenience, let us write κ̅ for κ_N. 
Then N=V_γ̅, for some  γ̅ with (γ̅)≥κ̅ 
and π(κ)= κ̅. Let α̅= π(α). 
Note that π (ℙ_N)= ℙ^κ̅_α̅. 
Let G_N= G_α∩ N and  G^κ̅_α̅= π [G_N]. 
Then the transitive collapse N[G_N] of N[G_N] is equal to V_γ̅[G^κ̅_α̅]= V_γ̅^V[G_N].
Hence N[G_N] is an ω_1-guessing model in V[G_N]. 
On the other hand, by <ref>,  the quotient forcing ℚ_N is 𝒞^N_ st-strongly proper,
 and 𝒞^N_ st is stationary in 𝒫_ω_1(V_λ).
It follows by <ref> that the pair (V[G_N], V[G]) has the ω_1-approximation property.
Thus,  N[G_N] remains an ω_1-guessing model in V[G]. 


 
 
A similar argument shows the following. 

 Suppose μ > λ and N≺ V_μ is a κ-Magidor model
containing all the relevant parameters. Then N[G] is an ω_1-guessing model in V[G]. 


 
 
  
Now, by <ref> we have the following. 

  The principle GM(ω_2,ω_1) holds in V[G].
 
 
 
 
 

 The principle FS(ω_2,ω_1) holds in V[G]. 



Fix  X∈ H(ω_3)^V[G]. We have to find a collection 𝒢 of ω_1-guessing models 
containing X such that { M∩ω_2: M ∈𝒢} is an ω_1-closed unbounded subset of ω_2. 
Back in V we can find α∈ E, and a canonical ℙ^κ_λ-name Ẋ, such that Ẋ[G_α]=X.
Fix some  β∈ E∖ (α +1) with (β) <κ. 
By a standard density argument, we can find a Magidor model M∈_G_β such that α, Ẋ∈ M. 
Suppose P∈_G_β is also a Magidor model and M∈_β P. Notice that M∩ V_β⊆ P∩ V_β, 
so Ẋ∈ P, and hence X∈ P[G_α]. By <ref>, P[G_α] is an ω_1-guessing model, for all such P.
Now, by <ref>, the set C_β(G) is club in ω_2,
and hence the family 𝒢= { P∈_G_β∩𝒰: M ∈_β P} is as required. 



Finally, we observe that if λ is also supercompact, then  GM^+(ω_3,ω_1) holds in V[G] as well. 
In fact, we show that for all μ >λ the set of strong ω_1-guessing models is stationary in 𝒫_ω_3(V_μ[G]). 
 
  Suppose μ > λ and N≺ V_μ is a λ-Magidor model
 containing all the relevant parameters. Then N[G] is a strong ω_1-guessing  model. 


 Since N is a λ-Magidor model, its transitive collapse N  equals V_γ̅, for some γ̅< λ.
Let λ̅= N∩λ.  Note that (λ̅)≥κ, and hence 
the transitive collapse N[G]  of N[G] equals V_γ̅[G_λ̅].
On the other hand, by <ref>, the pair (V[G_λ̅],V) has the ω_1-approximation property. 
Moreover, by <ref>,  𝒫_ω_1 ^V_γ̅[G_λ̅](V_γ̅[G_λ̅])
is cofinal in  𝒫_ω_1^V[G](V_γ̅[G_λ̅]). 
Therefore, V_γ̅[G_λ̅] and hence also N[G] remains an ω_1-guessing model in V[G]. 
To see that V_γ̅[G_λ̅]   is a strong ω_1-guessing model, 
fix some δ∈ E with δ > γ̅ and cof(δ)<κ. 
Note that if M∈_G^δ is a Magidor model with λ̅∈ M then by <ref> M[G_λ̅] is
an ω_1-guessing model. Moreover, if M∈_G^δ is a limit of such Magidor models
then by <ref>,

    M∩ V_γ̅ = ⋃{ Q∩ V_δ : Q∈_δ M  Q∈_G^δ}.

Hence if we let 𝒢 be the collection of the models (M∩ V_γ̅)[G_λ̅],
for Magidor models M∈_G^δ with λ̅∈ M, then 𝒢 is an increasing ⊆-chain of length ω_2 which is continuous
at ω_1-limits and whose union is V_γ̅[G_λ̅].
Therefore, V_γ̅[G_λ̅] and hence also N[G] s a strong ω_1-guessing model in V[G], as required. 


Now, by <ref> and <ref> we conclude the following.

 Suppose κ < λ are supercompact cardinals. Let G be V-generic over ℙ^κ_λ. 
Then in V[G] the principle GM^+(ω_3,ω_1) holds. 

 
 
 









 plain










