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

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

Example

The two smallest infinite sums behave differently:

$1 + \omega = \omega, \qquad \omega + 1 = \omega^{+} > \omega.$

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

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

Facts & Assumptions

Given: The ordinals with the addition of Ordinal addition $\alpha + \beta$ , and $\omega$ the least limit ordinal ( $\omega$ is the least limit ordinal, The natural numbers $\mathbb{N}$ (von Neumann)).

[L1]

$\alpha + 0 = \alpha$ , $\alpha + 1 = \alpha^{+}$ , and $\alpha + \lambda = \bigcup\{\alpha + \xi : \xi \in \lambda\}$ for limit $\lambda$ (Ordinal addition $\alpha + \beta$ ).

[L2]

$\beta \le \alpha + \beta$ (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 + \beta = \beta$ and $1 \cdot \beta = \beta$ ).

[L3]

For $m, n \in \omega$ the ordinal $m + n$ lies in $\omega$ (claim (a) of On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ 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]

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

[L5]

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

[L6]

$\alpha + \beta = \mathrm{ot}(\alpha \oplus \beta)$ , where $\alpha \oplus \beta$ is a copy of $\alpha$ with a copy of $\beta$ placed entirely above it ( $\alpha + \beta$ is the order type of $\alpha$ followed by $\beta$ ); 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 \omega$ the ordinal $1 + n$ lies in $\omega$ by [L3], hence $1 + n \subseteq \omega$ by [L5]; and $n \le 1 + n$ by [L2], hence $n \subseteq 1 + n$ .

L2L3L5

1.2

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

L1L5

2.1

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

step 1.1L1L4

2.2

From order types: the map $u : 1 \oplus \omega \to \omega$ 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 + \omega = \mathrm{ot}(1 \oplus \omega) = \mathrm{ot}(\omega) = \omega$ by [L6].

step 1.2L4L5L6

2.3

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

step 1.2L4L5L6

3.1

Both routes give $1 + \omega = \omega$ and $\omega + 1 \ne \omega$ , so $1 + \omega \ne \omega + 1$ ; explicitly $1 + \omega = \omega < \omega + 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 $\alpha + \beta$ together with the fact that $\omega$ is closed under adding a natural number, which is On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ 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 $\alpha + \beta$ is the order type of $\alpha$ followed by $\beta$ . 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.

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 60 results over 28 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)

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