Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck pass
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.

Countable unions of at most countable sets, assuming ACω

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let (An)n∈N be a family of at most countable sets (Finite, countably infinite, countable, uncountable) indexed by N. Then

U=⋃n∈NAn

is at most countable.

The role of ACω. It is spent at exactly one step, step 3.1 below, where a surjection N→An is selected simultaneously for each nonempty An. The individual countability hypotheses assert that these sets of surjections are nonempty; they specify no simultaneous selection.

Facts & Assumptions

Given: A family (An)n∈N of at most countable sets, its union U=⋃n∈NAn, and the Axiom of Countable Choice as an explicit hypothesis.

[L1]

Finite, countably infinite, at most countable; ∅ is finite (Finite, countably infinite, countable, uncountable).

[L2]

A nonempty set X is at most countable if and only if there is a surjection N→X (A nonempty set is at most countable iff it is a surjective image of N).

[L3]

ACω: for every family (Xn)n∈N of nonempty sets there is f with f(n)∈Xn for all n (The Axiom of Countable Choice (ACω)).

[L4]

There is a bijection β:N→N×N (N×N≈N, Equinumerous sets, A≈B and A⪯B).

[L5]

Every nonempty subset of N has a least element (The well-ordering principle).

[L6]

A composition of surjections is a surjection (Injection, surjection, bijection).

Proof

technique · direct
1.1givenL1

If U=∅ then U is finite, hence at most countable.

1.2givenL5

Assume instead U≠∅; then J:={ n∈N:An≠∅ } is nonempty, so it has a least element n0 by [L5].

1.3L4

Fix the bijection β:N→N×N of [L4].

2.1step 1.2givenL2construct

For n∈J let Sn be the set of all surjections N→An, which is nonempty by [L2] since An is nonempty and at most countable; for n∉J put Sn:=Sn0, also nonempty. This makes (Sn)n∈N a family of nonempty sets indexed by N, defined with no choices.

3.1step 2.1L3choose

This is the step that uses choice. Apply ACω [L3] to the family (Sn)n∈N of step 2.1: it delivers a function n↦sn with sn∈Sn for every n, that is, one surjection sn:N→An selected simultaneously for every n∈J. Nothing in the hypotheses names a particular surjection onto An, so this selection cannot be replaced by a definition; it is exactly here, and nowhere else in the proof, that the theorem leaves ZF.

4.1step 3.1given

Define t:N×N→U by t(n,k)=sn(k); the value lies in An⊆U for n∈J and in An0⊆U otherwise, so t is well defined. It is surjective: any x∈U lies in some An, which is then nonempty, so n∈J and x=sn(k) for some k because sn is onto An.

5.1step 1.3step 4.1L2L6

Hence t∘β:N→U is a surjection by [L6], and U≠∅, so U is at most countable by [L2].

6.1step 1.1step 5.1L1∎

In both cases U is at most countable, which is the assertion.

Remarks

Conditionally on Con⁡(ZF), ZF alone does not prove the unrestricted countable-union assertion. The later Relative consistency of the Feferman–Levy choice failures over ZF ↗ supplies a local finite-fragment proof of the relative consistency of ZF with the reals a countable union of countable sets. Combined with the choice-free uncountability theorem R is uncountable (Cantor's nested intervals, 1874), this gives the indicated nonprovability: if ZF proved the union assertion, that consistent extension would prove that the reals are both at most countable and uncountable. These are later metatheoretic orientation references, not hypotheses of the union proof below; the consistency assumption is retained.

  • An at most countable index set is no more general. If I is at most countable and (Ai)i∈I are at most countable, then either I is empty, and the union is ∅, or a surjection r:N→I exists (A nonempty set is at most countable iff it is a surjective image of N) and ⋃i∈IAi=⋃n∈NAr(n), which the theorem covers. That reindexing uses no choice.

  • The two-set union needs no choice at all, and neither does any union of finitely many sets: with A and B both at most countable and nonempty, fix surjections f,g:N→A,B (two choices made one after the other, which is ordinary existential instantiation, not a choice principle) and put u(0,k)=f(k) and u(n,k)=g(k) for n≠0, a surjection N×N→A∪B. This is the form used in The irrationals are uncountable, and keeping it separate from the countable case is the whole point of flagging step 3.1.

  • The proof isolates its exact use of ACω at step 3.1. It does not infer from that proof cost that the hypothesis is necessary; proving such a lower bound belongs to the later symmetric-model development.

Depends on

Dependency tree · 2 levels

Sources