[proofplan] We prove $(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$ by transfinite induction on $\gamma$, with $\alpha, \beta$ fixed arbitrary ordinals. The base case $\gamma = 0$ is immediate from $\delta + 0 = \delta$ in the definition of ordinal addition. The successor case uses the successor clause $\delta + \varepsilon^+ = (\delta + \varepsilon)^+$ twice and the inductive hypothesis. The limit case is more delicate: we must first verify that $\beta + \lambda$ is itself a limit ordinal (so the limit clause of addition applies on the right-hand side), then use continuity of addition in its second argument to slide the sup across. [/proofplan]

[step:Set up the transfinite induction on $\gamma$]Fix ordinals $\alpha$ and $\beta$. We prove by [transfinite induction](/theorems/1463) on $\gamma$ that \begin{align*} P(\gamma) : \quad (\alpha + \beta) + \gamma = \alpha + (\beta + \gamma). \end{align*} Recall the definition of ordinal addition: for any ordinals $\delta, \varepsilon$, \begin{align*} \delta + 0 &= \delta, \\ \delta + \varepsilon^+ &= (\delta + \varepsilon)^+, \\ \delta + \lambda &= \sup\{\delta + \xi : \xi < \lambda\} \quad \text{($\lambda$ a non-zero limit)}. \end{align*} Transfinite induction requires verifying $P$ at $0$, at successors, and at non-zero limits.[/step]

[guided]Since ordinal addition is defined by [transfinite recursion](/theorems/1464) on the second argument, the natural variable on which to induct is the last argument $\gamma$. We fix $\alpha, \beta$ as arbitrary parameters and induct on $\gamma$. Transfinite induction has three cases — one for each clause of the recursive definition: - **Base case** ($\gamma = 0$): verify $P(0)$ directly. - **Successor case** ($\gamma = \delta^+$): assume $P(\delta)$, prove $P(\delta^+)$. - **Limit case** ($\gamma = \lambda$ a non-zero limit): assume $P(\xi)$ for all $\xi < \lambda$, prove $P(\lambda)$. The definition of addition we use is the standard transfinite recursion: - $\delta + 0 = \delta$ (base), - $\delta + \varepsilon^+ = (\delta + \varepsilon)^+$ (successor), - $\delta + \lambda = \sup_{\xi < \lambda}(\delta + \xi)$ (limit, for $\lambda \neq 0$ a limit). Each of our three induction steps uses the corresponding clause on both sides of $P(\gamma)$.[/guided]

[step:Verify the base case $\gamma = 0$]Compute both sides using $\delta + 0 = \delta$: \begin{align*} (\alpha + \beta) + 0 &= \alpha + \beta, \\ \alpha + (\beta + 0) &= \alpha + \beta. \end{align*} Hence $(\alpha + \beta) + 0 = \alpha + (\beta + 0)$, establishing $P(0)$.[/step]

[guided]The base case is a direct two-line computation. Using the base clause $\delta + 0 = \delta$ applied twice: - Left: $(\alpha + \beta) + 0 = \alpha + \beta$ (apply the clause with $\delta = \alpha + \beta$). - Right: first $\beta + 0 = \beta$ (apply with $\delta = \beta$), then $\alpha + \beta$ (unchanged). Both sides equal $\alpha + \beta$, so $P(0)$ holds.[/guided]

[step:Verify the successor case assuming $P(\delta)$]Fix an ordinal $\delta$ and assume the inductive hypothesis \begin{align*} P(\delta): \quad (\alpha + \beta) + \delta = \alpha + (\beta + \delta). \end{align*} We prove $P(\delta^+)$. Using the successor clause twice and the inductive hypothesis: \begin{align*} (\alpha + \beta) + \delta^+ &= \bigl((\alpha + \beta) + \delta\bigr)^+ && \text{(successor clause, with $\varepsilon = \delta$, $\delta' = \alpha + \beta$)} \\ &= \bigl(\alpha + (\beta + \delta)\bigr)^+ && \text{(inductive hypothesis $P(\delta)$)} \\ &= \alpha + (\beta + \delta)^+ && \text{(successor clause, with $\varepsilon = \beta + \delta$, $\delta' = \alpha$)} \\ &= \alpha + (\beta + \delta^+) && \text{(successor clause, with $\varepsilon = \delta$, $\delta' = \beta$)}. \end{align*} Hence $(\alpha + \beta) + \delta^+ = \alpha + (\beta + \delta^+)$, establishing $P(\delta^+)$.[/step]

[guided]We want to prove $P(\delta^+)$ assuming $P(\delta)$. The key tool is the successor clause $\varepsilon + \zeta^+ = (\varepsilon + \zeta)^+$ — it lets us "peel off" the outermost successor. *Left-hand side of $P(\delta^+)$:* \begin{align*} (\alpha + \beta) + \delta^+. \end{align*} Apply the successor clause with outer base $\alpha + \beta$ and inner ordinal $\delta$: \begin{align*} (\alpha + \beta) + \delta^+ = \bigl((\alpha + \beta) + \delta\bigr)^+. \end{align*} Now the quantity inside the successor is the LHS of $P(\delta)$, which by the inductive hypothesis equals $\alpha + (\beta + \delta)$: \begin{align*} \bigl((\alpha + \beta) + \delta\bigr)^+ = \bigl(\alpha + (\beta + \delta)\bigr)^+. \end{align*} *Right-hand side of $P(\delta^+)$:* \begin{align*} \alpha + (\beta + \delta^+). \end{align*} Apply the successor clause inside, with base $\beta$ and inner $\delta$: $\beta + \delta^+ = (\beta + \delta)^+$. Then apply it outside, with base $\alpha$ and inner $\beta + \delta$: $\alpha + (\beta + \delta)^+ = (\alpha + (\beta + \delta))^+$. So \begin{align*} \alpha + (\beta + \delta^+) = \alpha + (\beta + \delta)^+ = \bigl(\alpha + (\beta + \delta)\bigr)^+. \end{align*} Both sides equal $(\alpha + (\beta + \delta))^+$, confirming $P(\delta^+)$. The successor case is essentially mechanical: unfold both sides one step, apply the inductive hypothesis, and observe the results coincide.[/guided]

[step:Establish that $\beta + \lambda$ is a non-zero limit ordinal when $\lambda$ is]Let $\lambda$ be a non-zero limit ordinal. Before handling the limit case of $P$, we check that $\beta + \lambda$ is itself a non-zero limit ordinal. This is needed because the limit clause of addition $\delta + \mu = \sup_{\xi < \mu}(\delta + \xi)$ applies only when $\mu$ is a non-zero limit — on the right-hand side we will apply this clause with $\mu = \beta + \lambda$. [claim:$\beta + \lambda$ is a non-zero limit ordinal] *Non-zero.* By the limit clause, $\beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\}$. Since $\lambda > 0$, pick any $\xi_0 < \lambda$ (for instance $\xi_0 = 0$). Then $\beta + \xi_0 \leq \beta + \lambda$, and since $\beta + 0 = \beta$, the set contains $\beta$. Also $\beta + \lambda \geq \beta + 0^+ = \beta^+ > \beta \geq 0$, so $\beta + \lambda \neq 0$. *Limit.* We show $\beta + \lambda$ has no immediate predecessor, i.e., is not a successor. Suppose $\beta + \lambda = \mu^+$ for some ordinal $\mu$. Then $\mu < \beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\}$, so by definition of supremum there exists $\xi^* < \lambda$ with $\mu < \beta + \xi^*$. Because $\lambda$ is a limit, $(\xi^*)^+ < \lambda$ as well, and by the successor clause \begin{align*} \beta + (\xi^*)^+ = (\beta + \xi^*)^+ > \mu^+ = \beta + \lambda. \end{align*} (The strict inequality $(\beta + \xi^*)^+ > \mu^+$ follows from $\beta + \xi^* > \mu$ and monotonicity of the successor.) But $(\xi^*)^+ < \lambda$ gives $\beta + (\xi^*)^+ \leq \sup\{\beta + \xi : \xi < \lambda\} = \beta + \lambda$, a contradiction. Hence $\beta + \lambda$ is a non-zero ordinal with no immediate predecessor, i.e., a non-zero limit ordinal. [proof] *Non-zero.* $\beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\} \geq \beta + 0 = \beta \geq 0$, and since $\lambda > 0$ contains at least $0$ and $1$, the set contains $\beta^+ > 0$, so the sup is positive. *Limit.* If $\beta + \lambda = \mu^+$, then $\mu < \beta + \lambda$, so by definition of sup there exists $\xi^* < \lambda$ with $\mu < \beta + \xi^*$. Since $\lambda$ is a limit, $(\xi^*)^+ < \lambda$, hence \begin{align*} \beta + \lambda \geq \beta + (\xi^*)^+ = (\beta + \xi^*)^+ > \mu^+ = \beta + \lambda, \end{align*} a contradiction. [/proof] [/claim][/step]

[guided]Why is this check needed? The definition of $\delta + \mu$ has three clauses keyed to $\mu \in \{0, \text{successor}, \text{non-zero limit}\}$. On the RHS of our target identity $\alpha + (\beta + \lambda)$, we want to apply the limit clause with outer base $\alpha$ and inner $\mu = \beta + \lambda$. That application is only legal if $\beta + \lambda$ is a **non-zero limit ordinal**. If $\beta + \lambda$ were a successor, we would be forced to use the successor clause instead, and the structure of the limit step would collapse. So we pause the main induction and prove the lemma: *if $\lambda$ is a non-zero limit, then so is $\beta + \lambda$*. Two things to verify: *Non-zero.* We have $\beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\}$. Since $\lambda > 0$ and $\lambda$ is a limit, $\lambda \geq \omega$, so in particular $0, 1 \in \lambda$. Taking $\xi = 0$ gives $\beta + 0 = \beta$ in the set; taking $\xi = 1$ gives $\beta + 1 = \beta^+$. So the sup is at least $\beta^+ \geq 1 > 0$. *Limit.* We show $\beta + \lambda$ is not a successor. Suppose for contradiction $\beta + \lambda = \mu^+$. Since $\mu < \mu^+ = \beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\}$, by definition of the supremum (which is the *least* upper bound of the set), $\mu$ is not an upper bound — so some member of the set strictly exceeds $\mu$. That is, there exists $\xi^* < \lambda$ with $\beta + \xi^* > \mu$. Now we use the fact that $\lambda$ is a limit: $(\xi^*)^+ < \lambda$ (limits have no greatest element, and they are closed under successors of elements). So the ordinal $\beta + (\xi^*)^+$ belongs to $\{\beta + \xi : \xi < \lambda\}$, hence lies below or at the sup: \begin{align*} \beta + (\xi^*)^+ \leq \sup\{\beta + \xi : \xi < \lambda\} = \beta + \lambda = \mu^+. \end{align*} But by the successor clause of addition, $\beta + (\xi^*)^+ = (\beta + \xi^*)^+$, and $\beta + \xi^* > \mu$ gives $(\beta + \xi^*)^+ > \mu^+$ (the successor operation is strictly monotone). So \begin{align*} \mu^+ < (\beta + \xi^*)^+ \leq \mu^+, \end{align*} a contradiction. Conclusion: $\beta + \lambda$ has no predecessor, hence is a limit ordinal.[/guided]

[step:Verify the limit case $P(\lambda)$ using the inductive hypothesis on all $\xi < \lambda$]Let $\lambda$ be a non-zero limit ordinal, and assume the inductive hypothesis \begin{align*} \forall\, \xi < \lambda: \quad (\alpha + \beta) + \xi = \alpha + (\beta + \xi). \end{align*} We compute both sides of $P(\lambda)$. By the limit clause (applicable since $\lambda$ is a non-zero limit): \begin{align*} (\alpha + \beta) + \lambda = \sup\{(\alpha + \beta) + \xi : \xi < \lambda\}. \end{align*} By the inductive hypothesis, $(\alpha + \beta) + \xi = \alpha + (\beta + \xi)$ for each $\xi < \lambda$. Substituting into the sup, \begin{align*} (\alpha + \beta) + \lambda = \sup\{\alpha + (\beta + \xi) : \xi < \lambda\}. \end{align*} For the right-hand side, $\beta + \lambda$ is a non-zero limit ordinal by the previous step, so the limit clause applies: \begin{align*} \alpha + (\beta + \lambda) = \sup\{\alpha + \eta : \eta < \beta + \lambda\}. \end{align*} It remains to show \begin{align*} \sup\{\alpha + (\beta + \xi) : \xi < \lambda\} = \sup\{\alpha + \eta : \eta < \beta + \lambda\}. \tag{$*$} \end{align*} [claim:Identity ($*$)] *LHS $\leq$ RHS.* Each $\xi < \lambda$ yields $\beta + \xi \leq \beta + \lambda$, and strict inequality holds: indeed $\xi^+ < \lambda$ (since $\lambda$ is a limit), so $\beta + \xi < \beta + \xi^+ \leq \beta + \lambda$. Hence $\beta + \xi < \beta + \lambda$, i.e., $\beta + \xi$ is a valid value of $\eta$ in the RHS sup. Therefore $\alpha + (\beta + \xi) \leq \sup\{\alpha + \eta : \eta < \beta + \lambda\}$ for every $\xi < \lambda$, and taking sup over $\xi$ gives LHS $\leq$ RHS. *RHS $\leq$ LHS.* Let $\eta < \beta + \lambda$. By definition of $\beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\}$ as a supremum, $\eta$ is not an upper bound of $\{\beta + \xi : \xi < \lambda\}$, so there exists $\xi^* < \lambda$ with $\eta \leq \beta + \xi^*$ (more precisely $\eta < \beta + \xi'$ for some $\xi' < \lambda$, but $\eta \leq \beta + \xi^*$ for some $\xi^* < \lambda$ suffices). Hence \begin{align*} \alpha + \eta \leq \alpha + (\beta + \xi^*) \leq \sup\{\alpha + (\beta + \xi) : \xi < \lambda\}, \end{align*} where the first inequality uses monotonicity of addition in the second argument. Taking sup over $\eta < \beta + \lambda$ gives RHS $\leq$ LHS. Hence the two sups are equal. [proof] *LHS $\leq$ RHS.* For each $\xi < \lambda$, $\beta + \xi < \beta + \lambda$ (by the argument above using $\xi^+ < \lambda$), so $\alpha + (\beta + \xi)$ is one of the values whose sup defines the RHS, hence bounded by the RHS sup. Taking sup over $\xi < \lambda$ gives LHS $\leq$ RHS. *RHS $\leq$ LHS.* For any $\eta < \beta + \lambda = \sup\{\beta + \xi : \xi < \lambda\}$, there exists $\xi^* < \lambda$ with $\eta \leq \beta + \xi^*$. By monotonicity of addition in the second argument, $\alpha + \eta \leq \alpha + (\beta + \xi^*)$, which is bounded by the LHS sup. Taking sup over $\eta < \beta + \lambda$ gives RHS $\leq$ LHS. [/proof] [/claim] Combining, \begin{align*} (\alpha + \beta) + \lambda = \sup\{\alpha + (\beta + \xi) : \xi < \lambda\} = \sup\{\alpha + \eta : \eta < \beta + \lambda\} = \alpha + (\beta + \lambda), \end{align*} establishing $P(\lambda)$. This completes the transfinite induction and proves $(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$ for all ordinals $\alpha, \beta, \gamma$. $\blacksquare$[/step]

[guided]The limit case is where the real work happens. We have the inductive hypothesis for every $\xi < \lambda$, and we want to lift it to $P(\lambda)$. *Compute the LHS using the limit clause.* Since $\lambda$ is a non-zero limit, the limit clause gives \begin{align*} (\alpha + \beta) + \lambda = \sup_{\xi < \lambda}\bigl((\alpha + \beta) + \xi\bigr). \end{align*} Applying the inductive hypothesis term-by-term inside the sup: \begin{align*} (\alpha + \beta) + \lambda = \sup_{\xi < \lambda}\bigl(\alpha + (\beta + \xi)\bigr). \tag{A} \end{align*} *Compute the RHS using the limit clause.* On the right-hand side of $P(\lambda)$, we have $\alpha + (\beta + \lambda)$. To apply the limit clause (with outer base $\alpha$ and inner ordinal $\beta + \lambda$), we need $\beta + \lambda$ to be a non-zero limit ordinal — this is exactly what we checked in the previous step. Hence \begin{align*} \alpha + (\beta + \lambda) = \sup_{\eta < \beta + \lambda}(\alpha + \eta). \tag{B} \end{align*} *Match (A) and (B).* The two sups are taken over different indexing sets, so we must show they compute the same ordinal. This is the identity $(*)$ in the claim above. The idea is a **cofinality** argument: the map $\xi \mapsto \beta + \xi$ sends $\{\xi : \xi < \lambda\}$ into $\{\eta : \eta < \beta + \lambda\}$ with image **cofinal** in the target, i.e., every $\eta < \beta + \lambda$ is bounded by some $\beta + \xi^*$. Then the composed map $\xi \mapsto \alpha + (\beta + \xi)$ is cofinal in $\{\alpha + \eta : \eta < \beta + \lambda\}$, so the sups agree. Both inequalities in the claim: *LHS $\leq$ RHS.* For $\xi < \lambda$: since $\lambda$ is a limit, $\xi^+ < \lambda$, so $\beta + \xi < \beta + \xi^+ \leq \sup_{\zeta < \lambda}(\beta + \zeta) = \beta + \lambda$. Thus $\beta + \xi$ is a legal value of $\eta$ in (B)'s indexing. So $\alpha + (\beta + \xi) \leq \sup_{\eta < \beta + \lambda}(\alpha + \eta)$ for each $\xi < \lambda$, and taking sup over $\xi$ gives LHS $\leq$ RHS. *RHS $\leq$ LHS.* Pick $\eta < \beta + \lambda$. By definition of $\beta + \lambda$ as a sup, $\eta$ is strictly below the sup, so there exists $\xi^* < \lambda$ with $\eta \leq \beta + \xi^*$ (the definition of sup ensures we can find an element of the set exceeding $\eta$, but we just need $\eta$ bounded above by some $\beta + \xi^*$). By [monotonicity of ordinal addition in the second argument](/theorems/1473) — addition is non-decreasing when the right argument increases — $\alpha + \eta \leq \alpha + (\beta + \xi^*)$, which is a value in the LHS sup. Taking sup over $\eta < \beta + \lambda$ gives RHS $\leq$ LHS. Both inequalities give $(*)$. Chaining (A), $(*)$, and (B): \begin{align*} (\alpha + \beta) + \lambda \overset{\text{(A)}}{=} \sup_{\xi < \lambda}(\alpha + (\beta + \xi)) \overset{(*)}{=} \sup_{\eta < \beta + \lambda}(\alpha + \eta) \overset{\text{(B)}}{=} \alpha + (\beta + \lambda). \end{align*} This closes the limit case. Base case, successor case, and limit case together complete the transfinite induction, establishing associativity of ordinal addition. *Why $(*)$ works structurally.* The proof of $(*)$ is a standard **cofinal reindexing** of a supremum: if $\varphi: \Lambda \to M$ is an order-preserving map with cofinal image in $M$, then for any monotone $F$ we have $\sup_{\xi \in \Lambda} F(\varphi(\xi)) = \sup_{\eta \in M} F(\eta)$. In our setting $\varphi(\xi) = \beta + \xi$, $\Lambda = \lambda$, $M = \beta + \lambda$, $F(\eta) = \alpha + \eta$. Cofinality of the image is precisely the fact that $\sup\{\beta + \xi : \xi < \lambda\} = \beta + \lambda$.[/guided]