Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)
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.

Refuted: every limit ordinal has an at most countable cofinal subset — ω1 has none, assuming countable choice

Statement refuted

False claim: every limit ordinal has an at most countable cofinal subset (Cofinal subset of an ordinal, Finite, countably infinite, countable, uncountable).

The claim is plausible because every limit ordinal a reader meets first does have one. ω is cofinal in itself and at most countable; and every at most countable limit ordinal λ is cofinal in itself and at most countable, so the claim holds for all of them, and ω+ω and ω2 are among them, both being shown at most countable earlier on this page. Whether ωω and ε0 are at most countable is a question no item on these pages settles, so neither is offered here as an instance.

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). The first uncountable ordinal ω1 (The first uncountable ordinal ω1:=ℵ(ω)) refutes the claim: it is a limit ordinal, and no at most countable subset of it is cofinal in it.

The hypothesis is not removable, and the item states it in the title: without a choice principle the refutation itself fails, since consistently with ZF the ordinal ω1 is the supremum of an ω-sequence of at most countable ordinals. That is recorded in Choice ledger for this page: ω1 exists in ZF, and the boundedness theorem does not.

Facts & Assumptions

Given: The Axiom of Countable Choice (The Axiom of Countable Choice (ACω)) and ω1, the first uncountable ordinal (The first uncountable ordinal ω1:=ℵ(ω)).

[L1]

C⊆α is cofinal in α when every ξ∈α satisfies ξ≤η for some η∈C (Cofinal subset of an ordinal).

[L2]

Counterexample

technique · direct
1.1

The claim does hold for every at most countable limit ordinal λ: the set λ itself is a subset of λ, it is at most countable by hypothesis, and it is cofinal in λ by [L1], since every ξ∈λ satisfies ξ≤ξ∈λ. In particular it holds at λ=ω by [L4].

L1L4
1.2

ω1 is a limit ordinal by [L2], so it is an instance of the claim.

L2
2.1

No at most countable C⊆ω1 is cofinal in ω1, by [L3]; so the claim fails at ω1.

step 1.2L1L3
3.1

Therefore ω1 is a limit ordinal with no at most countable cofinal subset, and the claim that every limit ordinal has one is false.

step 2.1step 1.2step 1.1∎

Remarks

What separates ω1 from the countable limit ordinals. A limit ordinal is always cofinal in itself, so the claim can only fail when the ordinal is itself uncountable. ω1 is the least uncountable ordinal (ω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), so it is the first place where the claim can fail at all, and under ACω it does fail there.

The refutation carries the hypothesis it uses. Assuming countable choice: every at most countable subset of ω1 is bounded below ω1, so no at most countable subset of ω1 is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable is stated under ACω and spends it at exactly one step, so this counterexample inherits the same cost. A page that quotes this item must carry ACω forward into its own statement; Choice ledger for this page: ω1 exists in ZF, and the boundedness theorem does not is the ledger, and it names the model in which the conclusion fails outright.

What is deliberately not said at this point in the reading order. In the later vocabulary this item says cf⁡(ω1)>ω, or that ω1 is regular. The cofinality and regular/singular vocabulary is introduced later in Cofinality cf⁡(α), and regular and singular cardinals ↗, so this earlier example stays in the subset language of Cofinal subset of an ordinal. Nothing is lost: the applications, such as the non-normality of the deleted Tychonoff plank, use exactly the subset form.

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