Full normalization for transfinite stacks

Abstract

We describe the extension of normal iteration strategies with appropriate condensation properties to strategies for stacks of normal trees, with full normalization. Given a regular uncountable cardinal $Ω$ and an $(m,Ω+1)$-iteration strategy $Σ$ for a premouse $M$, such that $Σ$ and $M$ both have appropriate condensation properties, we extend $Σ$ to a strategy $Σ^*$ for the optimal-$(m,Ω,Ω+1)^*$-iteration game such that for all $λ<Ω$ and all stacks $\vec{\mathcal{T}}=\left<\mathcal{T}_α\right>_{α<λ}$ via $Σ^*$, consisting of normal trees $\mathcal{T}_α$, each of length ${<Ω}$, there is a corresponding normal tree $\mathcal{X}$ via $Σ$ with $M^{\vec{\mathcal{T}}}_\infty=M^{\mathcal{X}}_\infty$. Moreover, if there are no drops in model or degree along the main branches of these trees then the overall iteration maps $i^{\vec{\mathcal{T}}}:M\to M^{\vec{\mathcal{T}}}_\infty$ and $i^{\mathcal{X}}:M\to M^{\mathcal{X}}_\infty$ agree. The construction is the result of a combination of work of John Steel and of the author. We also establish some further useful properties of $Σ^*$, and use the methods to analyze the comparison of multiple iterates via a common such strategy.

Figures (3)

• Figure 1: Extender commutativity. The diagrams commute, where $\vec{D}=\vec{E}\ \widehat{\ }\ \vec{F}$, and a label $\vec{C},k$ denotes a degree $k$ abstract iteration map given by $\vec{C}$.
• Figure 2: The diagram commutes. Arrows labelled with (sequences of) extender(s) indicate the degree $m$ ultrapower map determined by that (sequence of) extender(s), and that the structure at the tip of the arrow is the degree $m$ ultrapower of the structure at its base. The unlabelled arrows correspond to ultrapowers by the appropriate middle segment of $\vec{G}\circledast\vec{F}$. Given a sequence $\vec{E}$, $\vec{E}_{[\alpha,\beta)}$ denotes $\vec{E}\!\upharpoonright\![\alpha,\beta)$.
• Figure 3: Commutativity of minimal inflation. We have $\alpha_2\in C^{02}$, $\alpha_1=f^{12}(\alpha_2)$, $\alpha_0=f^{02}(\alpha_2)=f^{01}(\alpha_1)$, $\gamma^{k\ell}=\gamma^{k\ell}_{\alpha_\ell;\alpha_k}$, $\gamma=\gamma^{12}_{\alpha_2;\gamma^{01}}$, $\tau^{k\ell}=\pi^{k\ell}_{\alpha_\ell;\alpha_k i^{k\ell}\alpha_\ell}$ where $i^{k\ell}=i^{k\ell}_{\alpha_\ell;\alpha_k\alpha_\ell}$, and $\tau=\pi^{01}_{\alpha_1;\alpha_0 i^{02}\alpha_1}$. (So possibly $\mathrm{dom}(\tau)\neq\mathrm{dom}(\tau^{01})$, and possibly $\tau\not\subseteq\tau^{01}$.) Note $\alpha_2=\delta^{02}_{\alpha_2;\alpha_0}=\delta^{12}_{\alpha_2;\alpha_1}$ and $\alpha_1=\delta^{01}_{\alpha_1;\alpha_0}$ and $\gamma^{01}\leq^{\mathcal{X}_1}\alpha_1$ and $\gamma\leq^{\mathcal{X}_2}\gamma^{12}\leq^{\mathcal{X}_2}\alpha_2$. Solid arrows indicate total embeddings, and dotted arrows indicate partial embeddings (with domain and codomain initial segments of the models in the figure). The vertical arrows depict ultrapowers by branch extenders; for example, the left-most depicts the ultrapower map corresponding to $\mathrm{Ult}_n(U^{01}_{\alpha_1;\alpha_0 i^{02}},\vec{E}^{\mathcal{X}_1}_{\gamma^{01}\alpha_1})$ where $n=m^{\mathcal{X}_0}_{\alpha_0 i^{02}}$, and we refer to $i^{02}$ here (not $i^{01}$) as we are considering factoring $\tau^{02}$. The diagram commutes, after restricting to the relevant domains.

Theorems & Definitions (109)

• Theorem 1.1
• Remark 1.2
• Corollary 1.3
• proof
• Corollary 1.4
• proof
• Definition 2.1
• Remark 2.2
• Definition 2.3
• Lemma 2.4