[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.
[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]
[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)$.
[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]
[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^+)$.
[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]
[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]
[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]
[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$
[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]
[/step]