We shall construct a smooth category of mice and embeddings in the core model for measures of order 0. The existence of such a category implies that the global principle □ holds in K. We then prove a much stronger, the so-called condensation-coherent version of global □. The key tool of the whole construction is a new criterion on preserving soundness under condensation.

We prove covering theorems for K, where K is the core model below the sharp for a strong cardinal, and give an application to stationary set reflection.

We extend the construction of a global square sequence in extender models from Zeman [8] to a construction of coherent non-threadable sequences and give a characterization of stationary reflection at inaccessibles similar to Jensen’s characterization in L.

We prove new upper bound theorems on the consistency strengths of SPFA (θ), SPFA(θ-linked) and SPFA(θ⁺-cc). Our results are in terms of (θ, Γ)-subcompactness, which is a new large cardinal notion that combines the ideas behind subcompactness and Γ-indescribability. Our upper bound for SPFA(c-linked) has a corresponding lower bound, which is due to Neeman and appears in his follow-up to this paper. As a corollary, SPFA(c-linked) and PFA(c-linked) are each equiconsistent with the existence of a $\Sigma _{1}^{2}$ -indescribable cardinal. Our (...) upper bound for SPFA(c-c.c.) is a $\Sigma _{2}^{2}$ -indescribable cardinal, which is consistent with V = L. Our upper bound for SPFA(c⁺-linked) is a cardinal κ that is $(\kappa ^{+},\Sigma _{1}^{2})$ -subcompact, which is strictly weaker than κ⁺-supercompact. The axiom MM(c) is a consequence of SPFA(c⁺-linked) by a slight refinement of a theorem of Shelah. Our upper bound for SPFA(c⁺⁺-c.c.) is a cardinal κ that is $(\kappa ^{+},\Sigma _{2}^{2})$ -subcompact, which is also strictly weaker than κ⁺-supercompact. (shrink)

We prove that in all Mitchell-Steel core models, □ κ holds for all κ. (See Theorem 2.). From this we obtain new consistency strength lower bounds for the failure of □ κ if κ is either singular and countably closed, weakly compact, or measurable. (Corallaries 5, 8, and 9.) Jensen introduced a large cardinal property that we call subcompactness; it lies between superstrength and supercompactness in the large cardinal hierarchy. We prove that in all Jensen core models, □ κ holds (...) iff κ is not subcompact. (See Theorem 15; the only if direction is essentially due to Jensen.). (shrink)

A $\Sigma _{1}^{2}$ truth for λ is a pair 〈Q, ψ〉 so that Q ⊆ Hλ, ψ is a first order formula with one free variable, and there exists B ⊆ Hλ+ such that (Hλ+; ε, B) $(H_{\lambda +};\in ,B)\vDash \psi [Q]$ . A cardinal λ is $\Sigma _{1}^{2}$ indescribable just in case that for every $\Sigma _{1}^{2}$ truth 〈Q, ψ〉 for λ, there exists $\overline{\lambda}<\lambda $ so that $\overline{\lambda}$ is a cardinal and $\langle Q\cap H_{\overline{\lambda}},\psi \rangle $ is a (...) $\Sigma _{1}^{2}$ truth for $\overline{\lambda}$ . More generally, an interval of cardinals [κ, λ] with κ ≤ λ is $\Sigma _{1}^{2}$ indescribable if for every $\Sigma _{1}^{2}$ truth 〈Q, ψ〉 for λ, there exists $??\leq \overline{\lambda}<\kappa,??\subseteq H_{\overline{\lambda}}$ , and π: $H_{\overline{\lambda}}\rightarrow H_{\lambda}$ so that $??$ is a cardinal, $\langle ??,\psi \rangle $ is a $\Sigma _{1}^{2}$ truth for $??$ , and π is elementary from $(H_{\overline{\lambda}};\in,??,??)$ with $\pi \,|\,??={\rm id}$ . We prove that the restriction of the proper forcing axiom to c-linked posets requires a $\Sigma _{1}^{2}$ indescribable cardinal in L, and that the restriction of the proper forcing axiom to c⁺-linked posets, in a proper forcing extension of a fine structural model, requires a $\Sigma _{1}^{2}$ indescribable 1-gap [κ, κ⁺]. These results show that the respective forward directions obtained in " Hierarchies of Forcing Axioms I" by Neeman and Schimmerling are optimal. (shrink)

We prove that in all Mitchell-Steel core models, □k holds for all k. From this we obtain new consistency strength lower bounds for the failure of □k if k is either singular and countably closed, weakly compact, or measurable. Jensen introduced a large cardinal property that we call subcompactness; it lies between superstrength and supercompactness in the large cardinal hierarchy. We prove that in all Jensen core models, □k holds iff k is not subcompact.

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

We study generalizations of Dodd parameters and establish their fine structural properties in Jensen extender models with λ-indexing. These properties are one of the key tools in various combinatorial constructions, such as constructions of square sequences and morasses.