TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Ordinal addition is associative

Statement

For all ordinals $\alpha$ , $\beta$ , $\gamma$ (Ordinal (von Neumann)),

$(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma),$

with $+$ as in Ordinal addition $\alpha + \beta$ . Sums of ordinals may therefore be written without brackets, and this library does so from here on.

No choice principle is used. Associativity is not accompanied by commutativity, which is refuted among this page's false statements.

Facts & Assumptions

Given: Ordinals $\alpha$ , $\beta$ , $\gamma$ , each regarded as a well-order under membership. For well-orders $(X, <_X)$ and $(Y, <_Y)$ , $X \oplus Y$ is the ordered sum on $(\{0\} \times X) \cup (\{1\} \times Y)$ , a copy of $X$ with a copy of $Y$ placed entirely above it ( $\alpha + \beta$ is the order type of $\alpha$ followed by $\beta$ ).

[L1]

For well-orders $X$ and $Y$ , $X \oplus Y$ is a well-order and $\mathrm{ot}(X \oplus Y) = \mathrm{ot}(X) + \mathrm{ot}(Y)$ (claim (a) of $\alpha + \beta$ is the order type of $\alpha$ followed by $\beta$ ).

[L2]

Every well-order is order isomorphic to exactly one ordinal, its order type (Every well-order has a unique order type).

[L3]

A strictly increasing bijection between total orders is an order isomorphism, and order isomorphic well-orders have the same order type (Order embedding and order isomorphism, Every well-order has a unique order type).

[L4]

An ordinal is a transitive set strictly well ordered by membership, so it is a well-order (Ordinal (von Neumann), Well-order and well-ordered set).

Proof

technique · direct

1.1

For an ordinal $\mu$ the identity map is an order isomorphism of $\mu$ onto $\mu$ , so $\mathrm{ot}(\mu) = \mu$ by the uniqueness in [L2].

L2L4

1.2

The elements of $(\alpha \oplus \beta) \oplus \gamma$ are exactly the triples of shapes $(0,(0,a))$ with $a \in \alpha$ , $(0,(1,b))$ with $b \in \beta$ , and $(1,c)$ with $c \in \gamma$ ; those of $\alpha \oplus (\beta \oplus \gamma)$ are exactly $(0,a)$ , $(1,(0,b))$ and $(1,(1,c))$ with the same ranges; and in each of the two ordered sets the three families occur as three consecutive blocks, in the order $\alpha$ -block, then $\beta$ -block, then $\gamma$ -block, with each block carrying its own order.

L1L4

2.1

The map $\psi$ sending $(0,(0,a)) \mapsto (0,a)$ , $(0,(1,b)) \mapsto (1,(0,b))$ and $(1,c) \mapsto (1,(1,c))$ is therefore a bijection preserving the block a point belongs to and its position inside that block, hence strictly increasing, hence an order isomorphism of $(\alpha \oplus \beta) \oplus \gamma$ onto $\alpha \oplus (\beta \oplus \gamma)$ by [L3].

step 1.2L1L3

2.2

Computing both order types with [L1] and step 1.1: $\mathrm{ot}((\alpha \oplus \beta) \oplus \gamma) = \mathrm{ot}(\alpha \oplus \beta) + \mathrm{ot}(\gamma) = (\alpha + \beta) + \gamma$ , and $\mathrm{ot}(\alpha \oplus (\beta \oplus \gamma)) = \mathrm{ot}(\alpha) + \mathrm{ot}(\beta \oplus \gamma) = \alpha + (\beta + \gamma)$ .

step 1.1L1

3.1

The two well-orders are order isomorphic by step 2.1, so their order types agree by [L3], giving $(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$ .

step 2.2step 2.1L3∎

Remarks

Why the order-type route rather than a recursion. Associativity can also be proved by transfinite induction on $\gamma$ , and the limit case then needs the continuity clause of Monotonicity of ordinal $+$ and $\cdot$ : strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities $0 + \beta = \beta$ and $1 \cdot \beta = \beta$ together with the fact that $\{\beta + \xi : \xi \in \lambda\}$ is unbounded in $\beta + \lambda$ . The order-type argument avoids the case analysis entirely: concatenation of well-orders is visibly associative, and $\alpha + \beta$ is the order type of $\alpha$ followed by $\beta$ transports that to the arithmetic.

Associativity does not rescue commutativity. The two are independent: the ordinals under $+$ form a semigroup with identity $0$ and nothing more. $1 + \omega = \omega$ while $\omega + 1 = \omega^{+} \ne \omega$ , which is computed in FALSE: ordinal addition is commutative; and left cancellation holds while right cancellation fails, since $0 + \omega = 1 + \omega$ (FALSE: $\beta < \gamma$ implies $\beta + \alpha < \gamma + \alpha$ ).

Brackets are dropped from here on. Cantor normal forms such as $\omega^{2} + \omega \cdot 3 + 5$ (Cantor normal form: every nonzero ordinal is $\omega^{\beta_0}\cdot c_0 + \cdots + \omega^{\beta_{k-1}}\cdot c_{k-1}$ with $\beta_0 > \cdots > \beta_{k-1}$ and each $c_i$ a nonzero natural number, in exactly one way) are written unbracketed precisely because of this theorem.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Ordinal arithmetic (Wikipedia) (standard reference, not scraped)
T. Jech, Set Theory, 3rd millennium ed., Ch. 2 (Ordinal numbers) (standard reference, not scraped)
R. Moosa, Set Theory course notes (standard reference, not scraped)
Open Logic Project, Open Logic Text (standard reference, not scraped)