LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

$α + β$ is the order type of $α$ followed by $β$

Statement

Let $(A, <_{A})$ and $(B, <_{B})$ be well-orders (Well-order and well-ordered set) with order types $α = o t (A)$ and $β = o t (B)$ (Every well-order has a unique order type). Their ordered sum $A \oplus B$ is the set $({0} \times A) \cup ({1} \times B)$ with

$(i, x) < (j, y) : ⟺ i \in j, or (i = j = 0 and x <_{A} y), or (i = j = 1 and x <_{B} y),$

that is, a copy of $A$ with a copy of $B$ placed entirely above it. Then:

(a) $A \oplus B$ is a well-order and $o t (A \oplus B) = α + β$ (Ordinal addition $α + β$ ). In particular, taking $A = α$ and $B = β$ with their membership orders, $α + β$ is the order type of a copy of $α$ followed by a copy of $β$ .

(b) If $(W, <)$ is a well-order and $I \subseteq W$ is an initial segment (Initial segment of a well-order), then, with $I$ and $W ∖ I$ carrying the order inherited from $W$ ,

$o t (W) = o t (I) + o t (W ∖ I) .$

No choice principle is used; the whole argument runs on Every well-order has a unique order type, which is itself choice free.

Facts & Assumptions

Given: Well-orders $(A, <_{A})$ , $(B, <_{B})$ and $(W, <)$ . Ordinals carry the membership order, and $o t$ denotes order type. Subsets of a well-order always carry the inherited order, which is again a well-order (Well-order and well-ordered set, Initial segment of a well-order).

[L1]

Every well-order is order isomorphic to exactly one ordinal, its order type, and order isomorphic well-orders have the same order type (Every well-order has a unique order type).

[L2]

A well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set).

[L3]

An order isomorphism is a bijection with $x < y ⟺ f (x) < f (y)$ ; a strictly increasing bijection between total orders is one; identities, inverses and composites of order isomorphisms are order isomorphisms; and an order isomorphism carries the initial segment below a point onto the initial segment below its image (Order embedding and order isomorphism).

[L4]

$W_{< a} = {x \in W : x < a}$ ; an initial segment is a downward closed subset; every initial segment is itself a well-order (Initial segment of a well-order).

[L5]

$α + 0 = α$ , $α + δ^{+} = (α + δ)^{+}$ , and $α + λ = ⋃ {α + β : β \in λ}$ for limit $λ$ (Ordinal addition $α + β$ ).

[L6]

An ordinal is a transitive set strictly well ordered by $\in$ , so for ordinals $μ \in θ$ the initial segment of $θ$ determined by $μ$ is $μ$ itself; $μ^{+}$ is an ordinal and $μ$ is its greatest element (Ordinal (von Neumann), Basic closure properties of ordinals).

[L7]

Transfinite induction over the ordinals: if a property $P$ of ordinals fails at some $β_{0}$ , apply Transfinite induction to the well-order $(β_{0}^{+}, \in)$ and to $S = {ξ \in β_{0}^{+} : P (ξ)}$ ; since every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals) and the initial segment of $β_{0}^{+}$ below $ξ$ is $ξ$ , it follows that if $P$ holds at $ξ$ whenever it holds at every ordinal in $ξ$ , then $P$ holds at every ordinal.

[L8]

Every ordinal is exactly one of $0$ , a successor, or a limit; a nonzero ordinal $λ$ is a limit if and only if $ξ \in λ$ implies $ξ^{+} \in λ$ (Successor and limit ordinals).

Proof

technique · direct

1.1

$A \oplus B$ is a well-order: the relation is total, since two points with different first coordinates are compared by $0 \in 1$ and two points with equal first coordinates are compared inside $A$ or inside $B$ , and it is transitive and irreflexive for the same reason; and a nonempty $S \subseteq A \oplus B$ has a least element, namely $(0, \min {x : (0, x) \in S})$ if $S$ meets ${0} \times A$ , and $(1, \min {y : (1, y) \in S})$ otherwise, the two minima existing by [L2].

L2construct

1.2

If $f : A \to A^{'}$ and $g : B \to B^{'}$ are order isomorphisms of well-orders then $(0, x) \mapsto (0, f (x))$ and $(1, y) \mapsto (1, g (y))$ define an order isomorphism $A \oplus B \to A^{'} \oplus B^{'}$ ; taking $A^{'} = α$ and $B^{'} = β$ with the isomorphisms supplied by [L1], $A \oplus B$ and $α \oplus β$ have the same order type.

L1L3

2.1

Case $β = 0$ : $α \oplus 0 = {0} \times α$ and $(0, x) \mapsto x$ is an order isomorphism onto $α$ , so $o t (α \oplus 0) = α = α + 0$ .

step 1.1L1L3L5

2.2

Case $β = δ^{+}$ , assuming $o t (α \oplus δ) = α + δ$ : the set of points of $α \oplus δ^{+}$ strictly below $(1, δ)$ is exactly $α \oplus δ$ , with the same order, and $(1, δ)$ is the greatest element of $α \oplus δ^{+}$ because every other point is $(0, x)$ or $(1, y)$ with $y \in δ$ ; so extending an order isomorphism $h : α \oplus δ \to α + δ$ by $h (1, δ) : = α + δ$ gives an order isomorphism onto $(α + δ) \cup {α + δ} = (α + δ)^{+}$ , whence $o t (α \oplus δ^{+}) = (α + δ)^{+} = α + δ^{+}$ .

step 1.1L1L3L5L6

2.3

Case $β = λ$ a limit, assuming $o t (α \oplus ξ) = α + ξ$ for every $ξ \in λ$ : let $g$ be the order isomorphism of $α \oplus λ$ onto $θ = o t (α \oplus λ)$ ; for $ξ \in λ$ the points below $(1, ξ)$ form exactly $α \oplus ξ$ , so $g$ carries $α \oplus ξ$ onto the initial segment of $θ$ below $g (1, ξ)$ , which is the ordinal $g (1, ξ)$ , giving $g [α \oplus ξ] = o t (α \oplus ξ) = α + ξ$ ; moreover every point of $α \oplus λ$ lies in some $α \oplus ξ$ with $ξ \in λ$ , since $(0, x)$ lies in $α \oplus 0$ and $(1, y)$ with $y \in λ$ lies in $α \oplus y^{+}$ with $y^{+} \in λ$ by [L8]; hence $θ = g [α \oplus λ] = ⋃ {g [α \oplus ξ] : ξ \in λ} = ⋃ {α + ξ : ξ \in λ} = α + λ$ .

step 1.1L1L3L4L5L6L8

3.1

The three cases of [L8] are exhaustive, and each of steps 2.1, 2.2 and 2.3 derives the claim at $β$ from the claim at every ordinal in $β$ , so by [L7] $o t (α \oplus β) = α + β$ for every ordinal $β$ and every ordinal $α$ .

step 2.1step 2.2step 2.3L7L8

4.1

Claim (a): $A \oplus B$ is a well-order by step 1.1, and $o t (A \oplus B) = o t (α \oplus β) = α + β$ by step 1.2 and step 3.1.

step 3.1step 1.2step 1.1

5.1

Claim (b): let $I$ be an initial segment of $W$ and define $φ : W \to I \oplus (W ∖ I)$ by $φ (x) = (0, x)$ for $x \in I$ and $φ (x) = (1, x)$ otherwise; $φ$ is a bijection, and it is strictly increasing, because $x < y$ with $x \notin I$ forces $y \notin I$ by downward closure of $I$ , so the only mixed case is $x \in I$ , $y \notin I$ , where $φ (x) = (0, x) < (1, y) = φ (y)$ ; hence $φ$ is an order isomorphism by [L3] and $o t (W) = o t (I \oplus (W ∖ I)) = o t (I) + o t (W ∖ I)$ by step 4.1.

step 4.1step 1.1L1L3L4

6.1

Claims (a) and (b) are established.

step 4.1step 5.1∎

Remarks

What this buys. The recursive definition of $+$ is what makes the operation legitimate, but it is a poor tool for computing. The order-type description is the tool: $1 + ω$ is one point followed by a copy of $ω$ , which is again a copy of $ω$ , so $1 + ω = ω$ ; while $ω + 1$ is a copy of $ω$ with a point on top, which has a greatest element and so is not a copy of $ω$ . Both computations are carried out in FALSE: ordinal addition is commutative.

Clause (b) is the one used later. Splitting a well-order at an initial segment is exactly the move behind For $α \leq β$ there is exactly one ordinal $γ$ with $α + γ = β$ : an ordinal $α$ below $β$ is an initial segment of $β$ , so $β = α + o t (β ∖ α)$ outright, with no recursion at all.

The tags $0$ and $1$ are there only to force disjointness. $A$ and $B$ may overlap, or be equal; the ordered sum has to keep the two copies apart, and the pair encoding is the cheapest way to do it. Nothing in the argument depends on the particular tags.

Depends on

Used by

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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

α+βα+β is the order type of αα followed by ββ