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.

$P (N)$ is uncountable

Example

The power set $P (N)$ is uncountable (Finite, countably infinite, countable, uncountable): there is no surjection $N \to P (N)$ (Cantor's theorem: $A ≺ P (A)$ ), so $N ≺ P (N)$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ). The proof combines Cantor's theorem with The Schröder-Bernstein theorem: the map $n \mapsto {n}$ is injective (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ , ${a, b} = {c, d}$ if and only if ( $a = c$ and $b = d$ ) or ( $a = d$ and $b = c$ ); in particular ${a} = {c, d}$ if and only if $a = c = d$ ), so $N ⪯ P (N)$ ; and if $P (N)$ were at most countable then $P (N) ⪯ N$ , so Schröder-Bernstein would give a bijection $P (N) \to N$ , hence a surjection $N \to P (N)$ , contradicting Cantor's theorem. No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals $N$ with $0 = \emptyset$ and successor $σ$ (The natural numbers $N$ (von Neumann)), the order $m < n ⟺ m \in n$ with $n = {m \in N : m < n}$ (Order on the natural numbers, On $N$ the order is membership: $m < n ⟺ m \in n$ ), and the power set $P (N) = {z : z \subseteq N}$ (The power set $P (x) = {z : z \subseteq x}$ ).

[F1]

$A$ is finite when $A \approx n$ for some $n \in N$ , countably infinite when $A \approx N$ , at most countable when it is finite or countably infinite, and uncountable when it is not at most countable (Finite, countably infinite, countable, uncountable).

[F2]

$A \approx B$ means a bijection $A \to B$ exists, $A ⪯ B$ means an injection $A \to B$ exists, and $A ≺ B$ means $A ⪯ B$ and not $A \approx B$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[F3]

Every element of a natural number is a natural number, and $m \subseteq N$ for every $m \in N$ (On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[F4]

${a} = {c, d}$ if and only if $a = c$ and $a = d$ ( ${a, b} = {c, d}$ if and only if ( $a = c$ and $b = d$ ) or ( $a = d$ and $b = c$ ); in particular ${a} = {c, d}$ if and only if $a = c = d$ ); and $t \in {a}$ exactly when $t = a$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

[F5]

Cantor's theorem: there is no surjection $A \to P (A)$ for any set $A$ (Cantor's theorem: $A ≺ P (A)$ ).

[F6]

Schröder-Bernstein: if $A ⪯ B$ and $B ⪯ A$ then $A \approx B$ (The Schröder-Bernstein theorem).

[F7]

A bijection is a surjection, a composite of injections is an injection, and the inverse of a bijection is a bijection (Injection, surjection, bijection, $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection).

Verification

technique · direct

1.1F3F4F7

The map $s : N \to P (N)$ , $s (n) = {n}$ , is well defined because ${n} \subseteq N$ by [F3], and it is injective: if ${n} = {m}$ then [F4] gives $n = m$ directly. Hence $N ⪯ P (N)$ .

1.2F1F3F7

If $P (N)$ is at most countable then $P (N) ⪯ N$ . If $P (N) \approx N$ , any bijection $P (N) \to N$ is an injection. If instead $P (N) \approx m$ for some $m \in N$ , fix a bijection $ψ : P (N) \to m$ ; the inclusion map $m \to N$ is available by [F3] and is injective, and the composite of the two injections is an injection $P (N) \to N$ . These are the two alternatives in [F1].

2.1step 1.1step 1.2F5F6F7

Therefore $P (N)$ is not at most countable. Suppose it were. Then $P (N) ⪯ N$ by step 1.2 and $N ⪯ P (N)$ by step 1.1, so [F6] supplies a bijection $P (N) \to N$ ; its inverse is a bijection $N \to P (N)$ by [F7], hence a surjection $N \to P (N)$ , contradicting Cantor's theorem [F5].

3.1step 1.1F1F2F5F7∎

Hence $P (N)$ is uncountable, and $N ≺ P (N)$ : the injection of step 1.1 gives $N ⪯ P (N)$ , while $N \approx P (N)$ would give a bijection $N \to P (N)$ and hence a surjection, contradicting [F5]; so not $N \approx P (N)$ and the strict relation holds by [F2]. No step selects an element from a nonempty family: the only objects named are ${n}$ , a fixed bijection, and its inverse.

Remarks

The argument is the statement of Cantor's theorem: $A ≺ P (A)$ in the "strictly larger" form $N ≺ P (N)$ instantiated at $N$ ; what is added here is the passage from "not at most countable" to the strict domination, which uses Schröder-Bernstein in the contrapositive direction as above.
Finiteness of $P (N)$ is impossible for the same reason: a bijection $P (N) \to m$ would compose with the inclusion $m \subseteq N$ to dominate $P (N)$ by $N$ , which step 2.1 rules out. No separate finite argument is needed.

Depends on

Used by

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

Dependency tree · two levels

41 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)

P(N)P(N) is uncountable