ExampleConstruction: AI-adaptedVerification: 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 at most countable although it is not order isomorphic to $ω$ : order type and cardinality are different invariants

Example

The ordinal $ω + ω$ is at most countable as a set (Finite, countably infinite, countable, uncountable), and it is not order isomorphic to $ω$ (Order embedding and order isomorphism).

There is no tension. Countability is a statement about bijections and ignores order; order type is a statement about order isomorphisms and is finer. Two well-orders on the same countably infinite set can have different order types: $ω$ and $ω + 1$ already show it, as the first example of this page records, and $ω$ and $ω + ω$ show it with the two copies visible.

$ω + ω = o t (\underset{first copy}{\underset{⏟}{0, 1, 2, \dots}} \underset{second copy}{\underset{⏟}{0^{'}, 1^{'}, 2^{'}, \dots}}) .$

Facts & Assumptions

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

[L1]

$ω + ω = o t (ω \oplus ω)$ , where $ω \oplus ω$ is the set $({0} \times ω) \cup ({1} \times ω)$ with the lexicographic order that puts the second copy above the first ( $α + β$ is the order type of $α$ followed by $β$ ).

[L2]

Every well-order is order isomorphic to exactly one ordinal, its order type, and order isomorphic well-orders have the same order type; in particular an order isomorphism is a bijection (Every well-order has a unique order type, Order embedding and order isomorphism).

[L3]

If $A$ and $B$ are at most countable then so is $A \times B$ (A product of two at most countable sets is at most countable); a set equinumerous with an at most countable set is at most countable, and $\approx$ is symmetric and transitive (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[L4]

$ω$ is at most countable, being equinumerous with $N$ by the identity, and every natural number is at most countable (Finite, countably infinite, countable, uncountable, The natural numbers $N$ (von Neumann)).

[L5]

$ν < θ$ implies $α + ν < α + θ$ , and $α + 0 = α$ (claims (a) and (b) 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 β = β$ , Ordinal addition $α + β$ ).

[L6]

$0 \in ω$ ; every ordinal is transitive and $μ \notin μ$ (Ordinal (von Neumann), Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals, Successor and limit ordinals).

Verification

technique · direct

1.1

As a set, $ω \oplus ω = ({0} \times ω) \cup ({1} \times ω) = 2 \times ω$ , since $2 = {0, 1}$ ; and $2 \times ω$ is at most countable by [L3] and [L4], both factors being at most countable.

L1L3L4

1.2

$ω + ω \neq ω$ : since $0 \in ω$ , [L5] gives $ω = ω + 0 < ω + ω$ , and $μ \notin μ$ by [L6].

L5L6

2.1

The order isomorphism of [L1] and [L2] from $ω \oplus ω$ onto the ordinal $ω + ω$ is in particular a bijection, so $ω + ω$ is equinumerous with $2 \times ω$ and hence at most countable by step 1.1 and [L3].

step 1.1L1L2L3

2.2

$ω + ω$ is not order isomorphic to $ω$ : order isomorphic well-orders have the same order type by [L2], and $ω$ and $ω + ω$ are distinct ordinals by step 1.2, each being its own order type.

step 1.2L2

3.1

So $ω + ω$ is an at most countable set carrying a well-order that is not a copy of the well-order $ω$ : cardinality and order type are different invariants.

step 2.1step 2.2∎

Remarks

How far this goes. Every ordinal strictly below $ω_{1}$ is at most countable ( $ω_{1}$ is uncountable, every ordinal below it is at most countable, it is a cardinal and a limit ordinal, and its existence is a theorem of ZF), and there are a great many of them: $ω + ω$ and $ω \cdot ω = ω^{2}$ are at most countable by the argument above, and no two distinct ordinals are isomorphic as orders. So a single countably infinite set carries uncountably many mutually non-isomorphic well-orders, one for each infinite ordinal below $ω_{1}$ . Nothing here says the same of $ω^{ω}$ or of $ε_{0}$ ( $ω^{2}$ , $ω^{ω}$ , and $ε_{0} = \sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots}$ satisfying $ω^{ε_{0}} = ε_{0}$ ): those are ordinals of larger order type, and their cardinality is a question no item on these pages settles, as that item's last remark records.

Why the argument does not need a choice principle. The bijection used at step 2.1 is the collapsing isomorphism of Every well-order has a unique order type, which is unique and therefore never chosen, and A product of two at most countable sets is at most countable is choice free too. Countability of a countable union of countable sets is a different matter and does cost ${A C}_{ω}$ ; that is Countable unions of at most countable sets, assuming ${A C}_{ω}$ and it is not used here.

The confusion this item exists to prevent. " $ω + ω$ is bigger than $ω$ " is true as a statement about ordinals, where bigger means further along the ordinal order, and false as a statement about size. The two readings of "bigger" are exactly order type and cardinality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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)
Countable set (Wikipedia) (standard reference, not scraped)
First uncountable ordinal (Wikipedia) (standard reference, not scraped)

ω+ωω+ω is at most countable although it is not order isomorphic to ωω: order type and cardinality are different invariants