TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

The Feferman–Levy reals are a countable union of countable sets

Statement

In the Feferman–Levy model $N$ ,

$R^{N} = ⋃_{m < ω} R_{m},$

and every $R_{m}$ is countable. Thus the set of all reals is a countable union of countable sets.

Facts & Assumptions

Given: The Feferman–Levy symmetric interpretation $N$ .

[F1]

Hereditarily symmetric names have bounded layer support gives every real in $N$ a Boolean name supported by one $H_{m}$ .

[F2]

The real layers of the Feferman–Levy model puts the sequence $⟨ R_{m} : m < ω ⟩$ in $N$ and identifies $R_{m}$ with the reals having such an $m$ -bounded name.

[F3]

Each Feferman–Levy real layer is countable proves in $N$ that each fixed $R_{m}$ is countable.

[F4]

Hereditarily symmetric interpretations form a transitive ZF model ensures that $N$ is a transitive ZF model, so its sequence, union, and internal countability assertions have their ordinary ZF meanings.

Proof

technique · direct verification of both inclusions and the indexed-family property

1.1

If $x \in R^{N}$ , F1 gives a Boolean real name for $x$ whose coefficients are fixed by some $H_{m}$ ; by F2 this says $x \in R_{m}$ . Hence $R^{N} \subseteq ⋃_{m < ω} R_{m}$ . Conversely F2 defines each $R_{m}$ using names for subsets of $ω$ , so every member of every $R_{m}$ is a real of $N$ . This proves the displayed equality.

F1F2

2.1

F2 supplies the sequence $m \mapsto R_{m}$ itself as a set of $N$ , not merely each layer separately. Its domain is $ω^{N} = ω$ , so its range is a countable indexed family in the exact ZF sense, including possible repeated layers. By F4, Union applied in $N$ gives the set on the right of step 1.1.

F2F4step 1.1

3.1

F3 gives $N ⊨$ “ $R_{m}$ is countable” for every $m < ω$ . Combining this pointwise statement with the sequence from step 2.1 proves that $R^{N}$ is a countable union of countable sets. No function choosing an enumeration of every $R_{m}$ is asserted; forming such a simultaneous family would be the invalid Choice step that the theorem deliberately avoids.

F3step 2.1∎

Depends on

Used by

Countable-union and omega-one regularity principles fail Corollary
The first Feferman–Levy collapse layers Example
The Feferman–Levy reals remain uncountable Theorem

Dependency tree · two levels

14 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

Thomas Jech, The Axiom of Choice, Theorem 10.6, printed pp. 142–144 (standard reference, not scraped)