[proofplan] We prove that forcing iteration is associative by writing down the canonical reassociation map on conditions. A left-associated condition consists of a ground condition $p$, a $P$-forcing name $\dot q$ for a $\dot Q$-condition, and a $P * \dot Q$-name $\dot r$ for a $\dot R$-condition; the translation hypothesis converts $\dot r$ into a $P$-name whose interpretations are $\dot Q$-names for $\dot S$-conditions. This allows us to send $((p,\dot q),\dot r)$ to $(p,(\dot q,\dot r^\flat))$, where $\dot r^\flat$ denotes the translated name. We then check that this assignment is well-defined, preserves and reflects the order, and is onto after the same coding convention is imposed on both sides, which is exactly forcing equivalence for the two forcing posets. [/proofplan]

[step:Fix the translated name convention for third coordinates] Let $\mathsf{Name}_{P * \dot Q}$ denote the class of $P * \dot Q$-forcing names and let $\mathsf{Name}_{P}(\mathsf{Name}_{\dot Q})$ denote the class of $P$-names whose $P$-generic interpretations are $\dot Q_G$-names. Fix the standard recursive ordered-pair coding of forcing names used in two-step forcing iterations. Let \begin{align*} \operatorname{Tr}: \mathsf{Name}_{P * \dot Q} \to \mathsf{Name}_{P}(\mathsf{Name}_{\dot Q}) \end{align*} denote the standard translation map sending each $P * \dot Q$-name $\dot a$ to a $P$-name $\operatorname{Tr}(\dot a)$ such that \begin{align*} (\operatorname{Tr}(\dot a)_G)_H = \dot a_{G * H} \end{align*} for every $P$-generic filter $G$ over $M$ and every $\dot Q_G$-generic filter $H$ over $M[G]$. [claim:Forcing relations are preserved by the two-step name translation] In the fixed recursive coding of names, $\operatorname{Tr}$ is chosen recursively together with an inverse recoding map on its canonical range: ordered pairs in a $P * \dot Q$-name are replaced rank-by-rank by $P$-names for the corresponding $\dot Q$-names, and the inverse map is defined only on names produced by this recursion. For every formula $\varphi(x_1,\dots,x_n)$ in the forcing language of $P * \dot Q$, every condition $(p,\dot q) \in P * \dot Q$, and every tuple $\dot a_1,\dots,\dot a_n$ of $P * \dot Q$-names, \begin{align*} (p,\dot q) \Vdash_{P * \dot Q} \varphi(\dot a_1,\dots,\dot a_n) \end{align*} if and only if \begin{align*} p \Vdash_P ``\dot q \Vdash_{\dot Q} \varphi(\operatorname{Tr}(\dot a_1),\dots,\operatorname{Tr}(\dot a_n))". \end{align*} [/claim] [proof] The construction of $\operatorname{Tr}$ is by recursion on the rank of names: each ordered pair appearing in a $P * \dot Q$-name is recoded as a $P$-name whose $P$-generic interpretation is the corresponding $\dot Q_G$-name. The defining property \begin{align*} (\operatorname{Tr}(\dot a)_G)_H = \dot a_{G * H} \end{align*} therefore follows by induction on the rank of $\dot a$ for every $P$-generic filter $G$ over $M$ and every $\dot Q_G$-generic filter $H$ over $M[G]$. The equivalence of the two forcing assertions follows by induction on the complexity of $\varphi$: atomic membership and equality are exactly the rank-recursion just described, Boolean connectives follow from the recursive definition of forcing, and quantifiers follow because the translation is defined on all $P * \dot Q$-names and has an inverse recoding map on its canonical range. The hypotheses used are precisely that $1_P \Vdash ``\dot Q \text{ is a forcing poset}"$, that $(p,\dot q)$ is a condition in $P * \dot Q$, and that all names being translated are $P * \dot Q$-names. [/proof] For a $P * \dot Q$-name $\dot r$, write \begin{align*} \dot r^\flat := \operatorname{Tr}(\dot r). \end{align*} Thus $\dot r^\flat$ is a $P$-name whose interpretation by a $P$-generic filter is a $\dot Q_G$-name. The hypothesis on $\dot S$ says exactly that this translation sends the $P * \dot Q$-name $\dot R$ to the $P$-name $\dot S$ for a $\dot Q$-name forcing poset, in the sense that \begin{align*} 1_P \Vdash_P ``\dot S \text{ is a } \dot Q\text{-name for a forcing poset}" \end{align*} and, after generic interpretation, \begin{align*} (\dot S_G)_H = \dot R_{G * H}. \end{align*} [/step]

[step:Define the reassociation map on conditions]Define a map between the two forcing iterations \begin{align*} \Phi : (P * \dot Q) * \dot R \to P * (\dot Q * \dot S) \end{align*} as follows. If $a \in (P * \dot Q) * \dot R$, then $a$ has the form \begin{align*} a = ((p,\dot q),\dot r), \end{align*} where $p \in P$, $\dot q$ is a $P$-name, and $\dot r$ is a $P * \dot Q$-name. Define $\Phi(a)$ by \begin{align*} \Phi(((p,\dot q),\dot r)) := (p,\dot t), \end{align*} where $\dot t$ is the $P$-name for the ordered pair \begin{align*} \dot t := (\dot q,\dot r^\flat). \end{align*} We verify that $\Phi(a)$ is a condition in $P * (\dot Q * \dot S)$. Since $a$ is a condition in $(P * \dot Q) * \dot R$, first \begin{align*} p \Vdash_P ``\dot q \in \dot Q", \end{align*} and second \begin{align*} (p,\dot q) \Vdash_{P * \dot Q} ``\dot r \in \dot R". \end{align*} By the forcing-translation lemma just fixed, applied to the formula $x \in \dot R$ and using the hypothesis that $\operatorname{Tr}(\dot R)$ is represented by $\dot S$, the second forcing assertion is equivalent to \begin{align*} p \Vdash_P ``\dot q \Vdash_{\dot Q} \dot r^\flat \in \dot S". \end{align*} Together these two assertions say precisely that \begin{align*} p \Vdash_P ``(\dot q,\dot r^\flat) \in \dot Q * \dot S". \end{align*} Therefore $(p,\dot t)$ is a condition in $P * (\dot Q * \dot S)$.[/step]

[guided]The only point needing care is that the third coordinate lives in different syntactic universes on the two sides. On the left, $\dot r$ is a $P * \dot Q$-name. On the right, the second coordinate of $P * (\dot Q * \dot S)$ must be a $P$-name for a condition in the two-step iteration $\dot Q * \dot S$. Therefore we cannot literally write $(p,(\dot q,\dot r))$ unless $\dot r$ has first been recoded as a $P$-name for a $\dot Q$-name. That is why we define $\dot r^\flat := \operatorname{Tr}(\dot r)$. The translation satisfies \begin{align*} (\dot r^\flat_G)_H = \dot r_{G * H} \end{align*} for every pair of generics $G$ and $H$. Thus $\dot r^\flat$ is the same mathematical object as $\dot r$ after forcing, but it has the correct syntactic type to appear inside a $P$-name for a $\dot Q * \dot S$-condition. Now let \begin{align*} a = ((p,\dot q),\dot r) \end{align*} be a condition in $(P * \dot Q) * \dot R$. By the definition of a two-step iteration, $(p,\dot q)$ must be a condition in $P * \dot Q$, so \begin{align*} p \Vdash_P ``\dot q \in \dot Q". \end{align*} Again by the definition of the outer iteration, the first coordinate $(p,\dot q)$ must force that the third coordinate is a condition in the forced poset: \begin{align*} (p,\dot q) \Vdash_{P * \dot Q} ``\dot r \in \dot R". \end{align*} The forcing-translation lemma fixed in the first step applies because $(p,\dot q) \in P * \dot Q$ and $\dot r$ and $\dot R$ are $P * \dot Q$-names. It turns this last assertion into the corresponding internal assertion over $P$: \begin{align*} p \Vdash_P ``\dot q \Vdash_{\dot Q} \dot r^\flat \in \dot S". \end{align*} Combining the two displayed assertions, $p$ forces that the ordered pair $(\dot q,\dot r^\flat)$ is a condition in the two-step iteration $\dot Q * \dot S$: \begin{align*} p \Vdash_P ``(\dot q,\dot r^\flat) \in \dot Q * \dot S". \end{align*} Therefore \begin{align*} \Phi(((p,\dot q),\dot r)) = (p,(\dot q,\dot r^\flat)) \end{align*} is a condition of $P * (\dot Q * \dot S)$.[/guided]

[step:Check that reassociation preserves the extension relation] Let \begin{align*} a_1 = ((p_1,\dot q_1),\dot r_1) \end{align*} and \begin{align*} a_0 = ((p_0,\dot q_0),\dot r_0) \end{align*} be conditions in $(P * \dot Q) * \dot R$. By the definition of the order on an iteration, \begin{align*} a_1 \leq_{(P * \dot Q) * \dot R} a_0 \end{align*} holds iff \begin{align*} (p_1,\dot q_1) \leq_{P * \dot Q} (p_0,\dot q_0) \end{align*} and \begin{align*} (p_1,\dot q_1) \Vdash_{P * \dot Q} ``\dot r_1 \leq_{\dot R} \dot r_0". \end{align*} Expanding the first condition gives \begin{align*} p_1 \leq_P p_0 \end{align*} and \begin{align*} p_1 \Vdash_P ``\dot q_1 \leq_{\dot Q} \dot q_0". \end{align*} Translating the third-coordinate comparison gives \begin{align*} p_1 \Vdash_P ``\dot q_1 \Vdash_{\dot Q} \dot r_1^\flat \leq_{\dot S} \dot r_0^\flat". \end{align*} These three assertions are precisely the definition of \begin{align*} (p_1,(\dot q_1,\dot r_1^\flat)) \leq_{P * (\dot Q * \dot S)} (p_0,(\dot q_0,\dot r_0^\flat)). \end{align*} Hence \begin{align*} a_1 \leq_{(P * \dot Q) * \dot R} a_0 \end{align*} implies \begin{align*} \Phi(a_1) \leq_{P * (\dot Q * \dot S)} \Phi(a_0). \end{align*} [/step]

[step:Check that reassociation reflects the extension relation] Conversely, suppose \begin{align*} \Phi(a_1) \leq_{P * (\dot Q * \dot S)} \Phi(a_0). \end{align*} Writing out the two images, this means \begin{align*} (p_1,(\dot q_1,\dot r_1^\flat)) \leq_{P * (\dot Q * \dot S)} (p_0,(\dot q_0,\dot r_0^\flat)). \end{align*} By the definition of the order on $P * (\dot Q * \dot S)$, this is equivalent to \begin{align*} p_1 \leq_P p_0, \end{align*} \begin{align*} p_1 \Vdash_P ``\dot q_1 \leq_{\dot Q} \dot q_0", \end{align*} and \begin{align*} p_1 \Vdash_P ``\dot q_1 \Vdash_{\dot Q} \dot r_1^\flat \leq_{\dot S} \dot r_0^\flat". \end{align*} Translating the last assertion back from $P$-names for $\dot Q$-names to $P * \dot Q$-names gives \begin{align*} (p_1,\dot q_1) \Vdash_{P * \dot Q} ``\dot r_1 \leq_{\dot R} \dot r_0". \end{align*} Together with the first two displayed assertions, this is exactly \begin{align*} ((p_1,\dot q_1),\dot r_1) \leq_{(P * \dot Q) * \dot R} ((p_0,\dot q_0),\dot r_0). \end{align*} Therefore $\Phi$ reflects the order. [/step]

[step:Identify the inverse map under the same coding convention] Let $(p,\dot t)$ be a condition in $P * (\dot Q * \dot S)$, presented in the canonical translated-code subposet. By this we mean the dense presentation obtained by replacing each second coordinate by the fixed ordered-pair name supplied by the recursive coding convention, so that \begin{align*} p \Vdash_P ``\dot t = (\dot q,\dot s)" \end{align*} for some $P$-name $\dot q$ and some $P$-name $\dot s$ which is forced to be a $\dot Q$-name lying in the canonical range of $\operatorname{Tr}$. This replacement by canonical representatives is harmless because the fixed coding is interpretation-preserving in every pair of generics and, by the forcing-translation claim, preserves the order relation. Since $(p,\dot t)$ is a condition, \begin{align*} p \Vdash_P ``\dot q \in \dot Q" \end{align*} and \begin{align*} p \Vdash_P ``\dot q \Vdash_{\dot Q} \dot s \in \dot S". \end{align*} Because $\dot s$ lies in the canonical range of $\operatorname{Tr}$, let $\dot s^\sharp$ be the unique inverse translated $P * \dot Q$-name obtained by the inverse recoding map fixed in the first step, so that \begin{align*} \operatorname{Tr}(\dot s^\sharp) = \dot s. \end{align*} Then the preceding forcing assertion translates to \begin{align*} (p,\dot q) \Vdash_{P * \dot Q} ``\dot s^\sharp \in \dot R". \end{align*} Let $\mathbb P_{\mathrm{right}}^{\mathrm{can}}$ denote the canonical translated-code subposet of $P * (\dot Q * \dot S)$ described above, and let $\mathbb P_{\mathrm{left}}^{\mathrm{can}}$ denote the corresponding canonical coded presentation of $(P * \dot Q) * \dot R$. Define the map \begin{align*} \Psi : \mathbb P_{\mathrm{right}}^{\mathrm{can}} \to \mathbb P_{\mathrm{left}}^{\mathrm{can}} \end{align*} by \begin{align*} \Psi((p,\dot t)) := ((p,\dot q),\dot s^\sharp). \end{align*} The preceding paragraph proves that $\Psi((p,\dot t))$ is a condition in $(P * \dot Q) * \dot R$. By construction of $\operatorname{Tr}$ and its inverse coding operation, $\Psi(\Phi(((p,\dot q),\dot r))) = ((p,\dot q),\dot r)$ and $\Phi(\Psi((p,\dot t))) = (p,\dot t)$ after replacing names by their standard equivalent codes. Hence $\Phi$ is a bijection between the two coded presentations of the posets. [/step]

[step:Conclude forcing equivalence from the order isomorphism] The preceding steps show that $\Phi$ is a bijection and that for all conditions $a_1,a_0 \in (P * \dot Q) * \dot R$, \begin{align*} a_1 \leq_{(P * \dot Q) * \dot R} a_0 \iff \Phi(a_1) \leq_{P * (\dot Q * \dot S)} \Phi(a_0). \end{align*} Therefore $\Phi$ is an order isomorphism \begin{align*} (P * \dot Q) * \dot R \cong P * (\dot Q * \dot S). \end{align*} Order-isomorphic forcing posets have exactly corresponding generic filters and hence produce the same forcing extensions. Thus $(P * \dot Q) * \dot R$ and $P * (\dot Q * \dot S)$ are forcing equivalent. [/step]