ExampleConstruction: Literature-sourcedVerification: 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.

$1 + ω = ω$ and $ω + 1 > ω$ , computed both from the recursion and as order types

Example

The two smallest infinite sums behave differently:

$1 + ω = ω, ω + 1 = ω^{+} > ω .$

Each is computed twice below: once from the recursive clauses of Ordinal addition $α + β$ , and once from the order-type description of $α + β$ is the order type of $α$ followed by $β$ , where $α + β$ is the order type of a copy of $α$ followed by a copy of $β$ . The two routes are independent, and agreeing is the point of the exercise.

In pictures: putting one extra point before a copy of $ω$ gives a copy of $ω$ again, since the result still looks like $0, 1, 2, \dots$ ; putting one extra point after it gives something with a greatest element, which $ω$ does not have.

Facts & Assumptions

Given: The ordinals with the addition of Ordinal addition $α + β$ , and $ω$ the least limit ordinal ( $ω$ is the least limit ordinal, The natural numbers $N$ (von Neumann)).

[L1]

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

[L2]

$β \leq α + β$ (claim (c) 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 + β = β$ and $1 \cdot β = β$ ).

[L3]

For $m, n \in ω$ the ordinal $m + n$ lies in $ω$ (claim (a) of On $ω$ the ordinal $+$ and $\cdot$ are the Peano operations: $ω$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product).

[L4]

$ω$ is a limit ordinal, so $⋃ ω = ω$ and $ω$ is closed under successor; every nonzero natural number is a successor, and every ordinal in $ω$ is $0$ or a successor (claims (iii) and (iv) of $ω$ is the least limit ordinal, Successor and limit ordinals).

[L5]

Every ordinal is transitive, $μ \subseteq ν$ iff $μ \in ν$ or $μ = ν$ , and $μ \notin μ$ (Ordinal (von Neumann), Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals).

[L6]

$α + β = o t (α \oplus β)$ , where $α \oplus β$ is a copy of $α$ with a copy of $β$ placed entirely above it ( $α + β$ is the order type of $α$ followed by $β$ ); every well-order has exactly one order type and order isomorphic well-orders have the same one (Every well-order has a unique order type); a strictly increasing bijection between total orders is an order isomorphism (Order embedding and order isomorphism).

Verification

technique · direct

1.1

From the recursion: for $n \in ω$ the ordinal $1 + n$ lies in $ω$ by [L3], hence $1 + n \subseteq ω$ by [L5]; and $n \leq 1 + n$ by [L2], hence $n \subseteq 1 + n$ .

L2L3L5

1.2

From the recursion: $ω + 1 = ω^{+} = ω \cup {ω}$ by [L1], so $ω \in ω + 1$ while $ω \notin ω$ by [L5], giving $ω + 1 \neq ω$ and $ω < ω + 1$ .

L1L5

2.1

From the recursion: $1 + ω = ⋃ {1 + n : n \in ω}$ by [L1], and this equals $ω$ , since it is contained in $ω$ by step 1.1 and contains $⋃ {n : n \in ω} = ⋃ ω = ω$ by step 1.1 and [L4].

step 1.1L1L4

2.2

From order types: the map $u : 1 \oplus ω \to ω$ with $u (0, 0) = 0$ and $u (1, n) = n^{+}$ is a bijection, because every nonzero natural number is a successor by [L4] and $n \mapsto n^{+}$ is injective, and it is strictly increasing, because $(0, 0)$ is below every $(1, n)$ and $u (0, 0) = 0 \in n^{+}$ , while $(1, m) < (1, n)$ means $m \in n$ and then $m^{+} \in n^{+}$ by [L5]; so $1 + ω = o t (1 \oplus ω) = o t (ω) = ω$ by [L6].

step 1.2L4L5L6

2.3

From order types: $ω \oplus 1$ has a greatest element, namely the single point of its upper copy, whereas $ω$ has none, since $ξ \in ω$ implies $ξ \in ξ^{+} \in ω$ by [L4]; so the two are not order isomorphic and $ω + 1 = o t (ω \oplus 1) \neq o t (ω) = ω$ by [L6].

step 1.2L4L5L6

3.1

Both routes give $1 + ω = ω$ and $ω + 1 \neq ω$ , so $1 + ω \neq ω + 1$ ; explicitly $1 + ω = ω < ω + 1$ .

step 2.1step 2.2step 2.3step 1.2∎

Remarks

What the two routes cost. The recursive computation needs the limit clause of Ordinal addition $α + β$ together with the fact that $ω$ is closed under adding a natural number, which is On $ω$ the ordinal $+$ and $\cdot$ are the Peano operations: $ω$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product. The order-type computation needs only an explicit bijection and $α + β$ is the order type of $α$ followed by $β$ . Neither is shorter than the other; the second is the one that generalises, since it makes the answer visible before it is computed.

This is the whole of non-commutativity, in miniature. The general statement is FALSE: ordinal addition is commutative, and its proof is exactly the computation above. Everything else about the failure of commutativity is a variation on prepending versus appending.

$ω + 1$ is not $ω$ even though the two sets have the same size. $ω + 1 = ω \cup {ω}$ is countably infinite, being $ω$ with one point added, so the difference between $ω$ and $ω + 1$ is entirely a difference of order type. That distinction is taken up in $ω + ω$ is at most countable although it is not order isomorphic to $ω$ : order type and cardinality are different invariants.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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)
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)

1+ω=ω1+ω=ω and ω+1>ωω+1>ω, computed both from the recursion and as order types