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.

On N the order is membership: m<n  ⟺  m∈n

Statement

Let N=ω be the von Neumann naturals, with 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)), and let ≤ and < be the order defined additively by m≤n  ⟺  ∃k∈N (m+k=n) and m<n  ⟺  (m≤n and m≠n) (Order on the natural numbers). Then N is a transitive set: every element of a natural number is itself a natural number. Moreover, for all m,n∈N:

  1. m<n  ⟺  m∈n;
  2. m≤n  ⟺  m⊆n;
  3. n<σ(n), and m<σ(n)  ⟺  m≤n;
  4. 0≤n, and 0∈n whenever n≠0.

Consequently n={ m∈N:m<n } for every n: a natural number is exactly the set of the naturals below it.

Why this is proved here. Order on the natural numbers defines the order additively and records the identification with membership only as an orienting remark, without proof. The countability arguments on this page use that identification as a working fact, so it is established here, from the additive order and induction alone. Nothing below uses ordinals or any later material.

Facts & Assumptions

Given: N=ω with 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)); m≤n  ⟺  ∃k∈N (m+k=n) and m<n  ⟺  (m≤n and m≠n) (Order on the natural numbers). Note that < is irreflexive by this definition alone, since m<m would require m≠m.

[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]

Addition: m+0=m and m+σ(k)=σ(m+k) (Addition of natural numbers); and 0+n=n for every n (Left identity for addition).

[L3]

≤ is a linear order on N: reflexive, antisymmetric, transitive and total (≤ is a linear order on N); and exactly one of m<n, m=n, n<m holds, so the failure of m≤n is exactly n<m (Trichotomy of the order on N).

[L4]

Discreteness: m<n  ⟺  σ(m)≤n (Discreteness: σ(n) is the immediate successor).

[L5]

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

[L6]

n≠σ(n) for every n∈N (No natural number equals its own successor).

Proof

technique · direct
1.1

N is a transitive set. Let P(n) be "n⊆N". P(0) holds because 0=∅ has no elements. If n⊆N then, since n is itself an element of N, the set σ(n)=n∪{n} is also a subset of N, so P(σ(n)) holds. By induction n⊆N for every n∈N, which is the transitivity of N.

givenL1
1.2

For every n∈N one has n∈σ(n) and n<σ(n). Indeed n∈n∪{n}=σ(n) directly; and taking k=σ(0) gives n+σ(0)=σ(n+0)=σ(n), so n≤σ(n), while n≠σ(n), whence n<σ(n).

givenL2L6
1.3

Mixed transitivity, in both directions. (i) If m≤n and n<p then m<p: transitivity of ≤ gives m≤p; if m=p then p≤n, and n≤p holds because n<p, so antisymmetry gives n=p, contradicting n≠p. Hence m≠p and m<p. (ii) If m<n and n≤p then m<p: transitivity of ≤ again gives m≤p; if m=p then n≤p=m, and m≤n holds because m<n, so antisymmetry gives m=n, contradicting m≠n. Hence m≠p and m<p.

givenL3
1.4

No natural number satisfies m<0. For every m one has 0+m=m, so 0≤m; if also m≤0 then antisymmetry gives m=0, and m<0 additionally demands m≠0.

givenL2L3
2.1

For all m,n∈N: m<σ(n)  ⟺  m≤n. If m≤n then, with n<σ(n) from step 1.2, step 1.3(i) gives m<σ(n). Conversely assume m<σ(n) and suppose m≤n fails; then n<m by trichotomy, so σ(n)≤m by discreteness, and step 1.3(i) applied to σ(n)≤m and m<σ(n) gives σ(n)<σ(n), which irreflexivity forbids. Hence m≤n.

step 1.2step 1.3givenL3L4
2.2

Membership implies order: for every n∈N, every m∈n satisfies m<n. Let P(n) be that statement; P(0) is vacuous since 0=∅. Assume P(n) and let m∈σ(n)=n∪{n}. If m∈n then m<n by P(n), and n<σ(n) by step 1.2, so m<σ(n) by step 1.3(i), whose hypothesis m≤n follows from m<n. If m=n then m<σ(n) by step 1.2. So P(σ(n)) holds, and by induction P(n) holds for every n; the elements m involved are natural numbers by step 1.1, so the statement is about N throughout.

step 1.1step 1.2step 1.3givenL1
3.1

Order implies membership: for every n∈N, every m∈N with m<n satisfies m∈n. Let Q(n) be that statement; Q(0) holds vacuously by step 1.4. Assume Q(n) and let m<σ(n). By step 2.1, m≤n, that is m<n or m=n. In the first case m∈n by Q(n); in the second m∈{n}. Either way m∈n∪{n}=σ(n), so Q(σ(n)) holds, and by induction Q(n) holds for every n.

step 1.4step 2.1givenL1
4.1

Steps 2.2 and 3.1 together give m<n  ⟺  m∈n for all m,n∈N, which is claim 1; and since every element of n is a natural number by step 1.1, this says exactly n={ m∈N:m<n }.

step 1.1step 2.2step 3.1
5.1

If m≤n then m⊆n: let x∈m; then x∈N by step 1.1 and x<m by step 4.1, so x<n by step 1.3(ii) applied to x<m and m≤n, whence x∈n by step 4.1.

step 1.1step 1.3step 4.1
5.2

If m⊆n then m≤n: suppose m≤n fails; then n<m by trichotomy, so n∈m by step 4.1, and m⊆n would give n∈n, which is impossible. Hence m≤n.

step 4.1L3L5
5.3

For every n∈N one has 0≤n by step 1.4; if in addition n≠0 then 0<n, hence 0∈n by step 4.1.

step 1.4step 4.1given
6.1

The transitivity of N is step 1.1, claim 1 is step 4.1, claim 2 is steps 5.1 and 5.2 together, claim 3 is steps 1.2 and 2.1, and claim 4 is step 5.3; the description n={ m∈N:m<n } is part of step 4.1.

step 1.1step 1.2step 2.1step 4.1step 5.1step 5.2step 5.3∎

Remarks

Depends on

Used by

…and 38 more results.

Dependency tree · two levels

23 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