ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6.1-sol)

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 set of binary sequences is equinumerous with $P (N)$ , hence uncountable

Example

Let ${0, 1}^{N}$ be the set of all functions $N \to {0, 1}$ , where $0 = \emptyset$ and $1 = σ (0)$ (The set $B^{A}$ of all functions $A \to B$ , The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ). The map $S \mapsto χ_{S}$ sending $S \subseteq N$ to its characteristic function, $χ_{S} (n) = 1$ for $n \in S$ and $χ_{S} (n) = 0$ for $n \notin S$ , is a bijection $P (N) \to {0, 1}^{N}$ (The power set $P (x) = {z : z \subseteq x}$ , Injection, surjection, bijection). Hence ${0, 1}^{N} \approx P (N)$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ) and the set of binary sequences is uncountable (Finite, countably infinite, countable, uncountable, $P (N)$ is uncountable). This is the function-space form of Cantor's diagonal argument, and it is the form in which the library records that infinite products of at-most-countable sets need not be at most countable. No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals $N$ with $0 = \emptyset$ and $1 = σ (0)$ (The natural numbers $N$ (von Neumann)), the unordered pair ${0, 1}$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ), and the set ${0, 1}^{N}$ of functions $N \to {0, 1}$ (The set $B^{A}$ of all functions $A \to B$ , For sets $A$ and $B$ the collection of all functions $A \to B$ is a set, being a subset of $P (A \times B)$ ). Membership in ${0, 1}$ is membership in $N$ : $t \in {0, 1}$ exactly when $t = 0$ or $t = 1$ .

[F1]

$1 \neq 0$ , since $1 = σ (0)$ and $σ (n) \neq 0$ for every $n \in N$ (The von Neumann naturals form a Peano system).

[F2]

Separation and set notation: for a set $X$ and a property, ${z \in X : φ (z)}$ is the set of elements of $X$ with that property (The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ ); $S \subseteq N$ means every element of $S$ is an element of $N$ , and $P (N) = {z : z \subseteq N}$ (Subset $x \subseteq y$ , proper subset $x ⊊ y$ , and the separation notation ${z \in x : φ (z)}$ , The power set $P (x) = {z : z \subseteq x}$ ).

[F3]

A function is a relation with a unique value at each point of its domain; $f : A \to B$ means $dom f = A$ and $ran f \subseteq B$ ; and two functions with the same domain and the same values are equal (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ). Ordered pairs are those of the Cartesian product $A \times B$ (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

[F4]

Injection, surjection, bijection; images and preimages (Injection, surjection, bijection, The image $R [A]$ and the preimage $R^{- 1} [B]$ of a set under a relation).

[F5]

$A \approx B$ means a bijection $A \to B$ exists; $\approx$ is symmetric and transitive (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ); $A$ is finite when $A \approx n$ for some $n \in N$ , countably infinite when $A \approx N$ , at most countable when it is one of the two, and uncountable when it is not at most countable (Finite, countably infinite, countable, uncountable).

[F6]

$P (N)$ is uncountable ( $P (N)$ is uncountable).

Verification

technique · direct

1.1F2F3givenconstruct

For $S \subseteq N$ the set $χ_{S} : = {(n, v) \in N \times {0, 1} : (n \in S \land v = 1) \lor (n \notin S \land v = 0)}$ exists by Separation, and it is a function $N \to {0, 1}$ with $χ_{S} (n) = 1$ for $n \in S$ and $χ_{S} (n) = 0$ for $n \notin S$ . Indeed, for each $n \in N$ exactly one of $n \in S$ , $n \notin S$ holds, so exactly one value $v \in {0, 1}$ is related to $n$ , namely $1$ in the first case and $0$ in the second; and $0, 1 \in {0, 1}$ by the definition of the unordered pair.

2.1step 1.1F1F3

The assignment $S \mapsto χ_{S}$ is injective. If $χ_{S} = χ_{T}$ as sets of ordered pairs, then for every $n \in N$ one has $n \in S$ iff $χ_{S} (n) = 1$ iff $χ_{T} (n) = 1$ iff $n \in T$ : the outer equivalences are step 1.1, and in the middle, a function value that is not $1$ is $0$ , which differs from $1$ by [F1], so $χ_{T} (n) = 1$ holds exactly when $χ_{T} (n) \neq 0$ , that is exactly when $n \in T$ . Hence $S = T$ by Extensionality of sets.

2.2step 1.1F2F3

The assignment $S \mapsto χ_{S}$ is surjective. Let $f : N \to {0, 1}$ and put $S_{f} : = {n \in N : f (n) = 1}$ , a subset of $N$ by Separation. For each $n$ , either $f (n) = 1$ or $f (n) = 0$ because $f (n) \in {0, 1}$ ; in the first case $n \in S_{f}$ and step 1.1 gives $χ_{S_{f}} (n) = 1 = f (n)$ , and in the second case $n \notin S_{f}$ and $χ_{S_{f}} (n) = 0 = f (n)$ . Thus $χ_{S_{f}}$ and $f$ have the same domain $N$ and the same values, so they are equal by [F3], and $f$ is in the image of the assignment.

3.1step 2.1step 2.2F4F5

By steps 2.1 and 2.2 the characteristic-function map is a bijection $P (N) \to {0, 1}^{N}$ , so ${0, 1}^{N} \approx P (N)$ by [F5].

4.1step 3.1F5F6

The set ${0, 1}^{N}$ is uncountable. If it were at most countable, then ${0, 1}^{N} \approx m$ for some $m \in N$ or ${0, 1}^{N} \approx N$ by [F5]; symmetry and transitivity of $\approx$ with step 3.1 would give $P (N) \approx m$ or $P (N) \approx N$ , so $P (N)$ would be at most countable, contradicting [F6].

5.1step 3.1step 4.1∎

Therefore the binary sequences form a set equinumerous with $P (N)$ and are uncountable, as claimed. The only objects constructed are the characteristic functions, defined by an explicit formula from $S$ , and the set $S_{f}$ , separated from $N$ by the condition $f (n) = 1$ ; at no point is an element selected from a nonempty family of sets, so no choice principle is used.

Remarks

The construction is the function-space form of Cantor's diagonal argument: reading $S$ as a subset of $N$ and $s (n) = χ_{S} (n)$ as a binary sequence, the passage $S \mapsto χ_{S}$ identifies $P (N)$ with ${0, 1}^{N}$ , and the diagonal set of Cantor's theorem: $A ≺ P (A)$ reappears here as the sequence that flips every diagonal bit.
This example is the case $A = N$ of the fact that infinite products of at-most-countable sets need not be at most countable, in agreement with $P (N)$ is uncountable: the product is the power set in characteristic-function guise.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

John K. Hunter, An Introduction to Real Analysis (complete author-hosted lecture notes, 307 pp.) (standard reference, not scraped)
Jiri Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I (author-hosted complete book PDF) (standard reference, not scraped)

The set of binary sequences is equinumerous with P(N)P(N), hence uncountable