Guessing and non-guessing of canonical functions

It is possible to control to a large extent, via semiproper forcing, the parameters ( β 0 , β 1 ) measuring the guessing density of the members of any given antichain of stationary subsets of ω 1 (assuming the existence of an inaccessible limit of measurable cardinals). Here, given a pair ( β 0 , β 1 ) of ordinals, we will say that a stationary set S ⊆ ω 1 has guessing density ( β 0 , β 1 ) if β 0 = γ ( S ) and β 1 = sup { γ ( S ∗ ) : S ∗ ⊆ S , S ∗ stationary } , where γ ( S ∗ ) is, for every stationary S ∗ ⊆ ω 1 , the infimum of the set of ordinals τ ≤ ω 1 + 1 for which there is a function F : S ∗ ⟶ P ( ω 1 ) with o t ( F ( ν ) ) < τ for all ν ∈ S ∗ and with { ν ∈ S ∗ : g ( ν ) ∈ F ( ν ) } stationary for every α < ω 2 and every canonical function g for α . This work involves an analysis of iterations of models of set theory relative to sequences of measures on possibly distinct measurable cardinals. application of these techniques I show how to force, from the existence of a supercompact cardinal, a model of PFA + + in which there is a well-order of H ( ω 2 ) definable, over 〈 H ( ω 2 ) , ∈ 〉 , by a formula without parameters.