Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)
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 pigeonhole principle on N

Statement

Let N be the von Neumann naturals, with 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)), and let < be the order of Order on the natural numbers, so that m<n  ⟺  m∈n and n={ m∈N:m<n } (On N the order is membership: m<n  ⟺  m∈n). Write ≈ for equinumerosity (Equinumerous sets, A≈B and A⪯B). Then:

  1. for every n∈N there is no injection σ(n)→n;
  2. if m<n then there is no injection n→m;
  3. if n≈m with n,m∈N, then n=m;
  4. N≉n for every n∈N;
  5. no natural number is equinumerous with a proper subset of itself: if A⊆n and n≈A, then A=n.

Claim 1 is the pigeonhole principle in its sharpest form, that n+1 pigeons do not fit injectively into n holes; the other four are the consequences the library actually quotes. Claim 3 says a finite set is equinumerous with exactly one natural number, so "the number of elements" is well defined. Claim 4 says N is infinite. Claim 5 says no natural number is Dedekind-infinite.

Why this is proved here. The next item on this page defines finiteness as equinumerosity with a natural number, and the three size classes it introduces are exhaustive by construction but mutually exclusive only because of claim 4. Several later items also need claim 3 or claim 5. The principle is elementary and belongs with the naturals, but it is about counting rather than about order, so it is proved here, immediately before finiteness is defined, from induction and the identification of the order with membership alone. Nothing below uses ordinals, cardinals, or any later material.

Facts & Assumptions

Given: N with 0=∅ and σ(n)=n∪{n}, and N closed under σ, since it is an inductive set (The natural numbers N (von Neumann)); the order m≤n  ⟺  ∃k∈N (m+k=n) and m<n  ⟺  (m≤n and m≠n) (Order on the natural numbers); and A≈B meaning that a bijection A→B exists (Equinumerous sets, A≈B and A⪯B).

[L1]

Induction: if P(0) holds and P(n) implies P(σ(n)) for every n∈N, then P(n) holds for every n∈N (The principle of mathematical induction).

[L2]

On N the order is membership (On N the order is membership: m<n  ⟺  m∈n): N is a transitive set, so every element of a natural number is again a natural number; m<n  ⟺  m∈n; m≤n  ⟺  m⊆n; and consequently n={ m∈N:m<n }.

[L3]

Every natural number is a transitive set and satisfies n∉n (Every natural number is a transitive set and is not a member of itself).

[L4]

Trichotomy: for all m,n∈N exactly one of m<n, m=n, n<m holds (Trichotomy of the order on N).

[L5]

Every natural number n≠0 equals σ(m) for some m∈N (Every nonzero natural number is a successor).

[L6]

Maps (Injection, surjection, bijection): f is injective when f(x)=f(y) forces x=y, and bijective when it is injective and surjective, so every bijection is an injection; a composite of two injections is an injection, a composite of two bijections is a bijection, and a bijection has a two sided inverse which is again a bijection. Two immediate consequences of the definition of injectivity are used below: the restriction of an injection to a subset of its domain is an injection, injectivity being a condition on pairs of points of the domain; and a map whose values all lie in a subset C of its codomain may be read as a map into C, without affecting injectivity.

Proof

technique · direct
1.1

Transpositions. For a set X and a,b∈X define τa,bX:X→X by τa,bX(a)=b, τa,bX(b)=a, and τa,bX(x)=x for x∉{a,b}; the clauses agree where they overlap (if a=b all three read a↦a, so the map is the identity), so this is a well defined function, and τa,bX∘τa,bX=idX, whence τa,bX is a bijection of X onto itself. It carries X∖{a} onto X∖{b}: when a=b this is the identity statement, and when a≠b the elements of X∖{a} are b, sent to a, together with the x∉{a,b}, each fixed, so the image is {a}∪(X∖{a,b})=X∖{b}.

construct
1.2

Base case of claim 1. Here σ(0)=0∪{0}={0} and 0=∅, so a function f:σ(0)→0 would have to supply a value f(0)∈∅, and ∅ has no elements; hence there is no function σ(0)→0 at all, injective or not.

given
1.3

Inductive step, hypotheses. Fix n∈N, assume there is no injection σ(n)→n, and suppose towards a contradiction that some f:σ(σ(n))→σ(n) is injective. Note σ(σ(n))=σ(n)∪{σ(n)}, so σ(n)⊆σ(σ(n)) and σ(n)∈σ(σ(n)); note also n∈σ(n).

assume-hypgiven
2.1

Normalising f at the top point. Put a=f(σ(n)), an element of σ(n) because σ(n) is the codomain of f, and let τ=τa,nσ(n), which is legitimate since a and n both lie in σ(n). Then f′=τ∘f:σ(σ(n))→σ(n) is a composite of an injection with a bijection, hence injective, and f′(σ(n))=τ(a)=n.

step 1.1step 1.3L6
2.2

Every k∈σ(n) satisfies k≠σ(n): were k=σ(n) we would have σ(n)∈σ(n), and no natural number is a member of itself, σ(n) included, since N is closed under σ.

step 1.3L3given
3.1

Let k∈σ(n). Then k∈σ(σ(n)), so f′(k) is defined; and k≠σ(n), so injectivity of f′ gives f′(k)≠f′(σ(n))=n. Since f′(k)∈σ(n)=n∪{n}, this forces f′(k)∈n. Hence the restriction of f′ to σ(n) takes all its values in n and is an injection σ(n)→n.

step 2.1step 2.2L6
4.1

Claim 1. The injection produced in step 3.1 contradicts the assumption made in step 1.3, so no injection σ(σ(n))→σ(n) exists. Since n was arbitrary, this is exactly the induction step for the property P(n) that there is no injection σ(n)→n, and step 1.2 is P(0); so P(n) holds for every n∈N.

step 1.2step 1.3step 3.1L1
5.1

Claim 2. Let m<n. Then m∈n, and m≤n gives m⊆n, so σ(m)=m∪{m}⊆n. If some g:n→m were injective, its restriction to σ(m) would be an injection σ(m)→m, which step 4.1 forbids. Hence there is no injection n→m.

step 4.1L2L6
5.2

Claim 4. Since N is closed under σ we have σ(n)∈N, and N is a transitive set, so σ(n)⊆N. If some F:N→n were a bijection, it would in particular be an injection, and its restriction to σ(n) would be an injection σ(n)→n, which step 4.1 forbids. Hence N≉n.

step 4.1L2L6given
5.3

Claim 5. Let A⊆n with n≈A, and suppose A≠n. Then n≠0, since the only subset of 0=∅ is ∅=0 itself, so n=σ(m) for some m∈N; moreover m∈σ(m)=n and m∉m, so n∖{m}=(m∪{m})∖{m}=m. Choose j∈n∖A, possible because A⊆n and A≠n, and let h:n→A be a bijection; since j∉A we have A⊆n∖{j}, so h read as a map into n∖{j} is an injection n→n∖{j}. The transposition τj,mn is a bijection of n carrying n∖{j} onto n∖{m}=m, so its composite with h is an injection n→m, that is an injection σ(m)→m, which step 4.1 forbids. Hence A=n.

step 1.1step 4.1L3L5L6choose
6.1

Claim 3. Let n,m∈N with n≈m, and suppose n≠m. By trichotomy either m<n or n<m. If m<n, a bijection n→m is in particular an injection n→m, which step 5.1 forbids. If n<m, a bijection n→m has an inverse bijection m→n, which is in particular an injection m→n, and step 5.1 forbids that too, with the roles of m and n interchanged. Hence n=m.

step 5.1L4L6
7.1

Claims 1, 2, 3, 4 and 5 are established in steps 4.1, 5.1, 6.1, 5.2 and 5.3 respectively.

step 4.1step 5.1step 5.2step 5.3step 6.1∎

Remarks

  • Where the work is. Everything rests on claim 1, and claim 1 rests on one device: a map into σ(n) can be modified by a transposition of the codomain so that the top point σ(n) goes to the top value n, after which the rest of the map misses n and lands in n. Without that normalisation the inductive hypothesis does not apply, since an arbitrary injection σ(σ(n))→σ(n) need not send anything to n.

  • No choice is used. Every map built above is defined by an explicit rule: the transposition is given by three cases, and the only element selected anywhere is a single j∈n∖A in step 5.3, a single choice from a nonempty set, which needs no choice principle.

  • Claim 5 and the two notions of infinity. A set is Dedekind-infinite when it is equinumerous with a proper subset of itself. Claim 5 says no natural number is, and transporting along a bijection extends this to every finite set: Dedekind-infinite implies infinite in ZF. The successor map σ:N→N∖{0} shows N itself is Dedekind-infinite, so the restriction to natural numbers in claim 5 is essential. The converse requires later choice and model-theoretic analysis and is not used here.

  • Relation to the ordinals page. Cardinal (initial ordinal) and cardinality ↗ calls an ordinal κ a cardinal when no α∈κ satisfies α≈κ. Claim 3 makes every natural number a cardinal and claim 4 makes ω one, which is what licenses the traditional ℵ0=ω. That page comes much later in the library; the pointer here is orientation only, and nothing above rests on it.

Depends on

Used by

…and 4 more results.

Dependency tree · two levels

26 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