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 natural numbers (von Neumann)
Definition
The set of natural numbers is the smallest inductive set (Inductive set),
which exists and is itself inductive by The natural numbers exist: a smallest inductive set (the Axiom of Infinity, The Axiom of Infinity: there is a set containing a set with no elements and closed under , supplies one inductive set to intersect within, and Separation, The Axiom Schema of Separation: for each formula , , makes the intersection a set). On we take
the distinguished element and the successor function. Thus , , , , and in general is the set of its predecessors.
Definition references
Remarks
"Smallest" means for every inductive set . This minimality is exactly the induction principle (The principle of mathematical induction): a subset of that contains and is closed under is itself inductive, hence contains , hence equals .
With and so defined, satisfies the Peano axioms (Peano system, proved in The von Neumann naturals form a Peano system), so it is a model of the abstract natural numbers. By categoricity (Categoricity: the natural numbers are unique up to unique isomorphism) any other model is uniquely isomorphic to it, so the particular set-theoretic encoding chosen here is immaterial to every arithmetic and order property that follows: those are developed from the Peano axioms, not from the sets themselves.
Depends on
- Inductive set
- The natural numbers exist: a smallest inductive set
- Peano system
- The Axiom of Infinity: there is a set containing a set with no elements and closed under $y \mapsto y \cup \{y\}$
- The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$
Used by
- Anchored iteratively regularized Gauss-Newton with finite discrepancy stopping Algorithm
- Bias-corrected Adam update Algorithm
- Bias-corrected AMSGrad update Algorithm
- Constrained support-search least squares Algorithm
- Exact-arithmetic LSQR with Golub–Kahan bidiagonalization and explicit statuses Algorithm
- Flexible GMRES with variable right preconditioning Algorithm
- Landweber iteration with discrepancy and budget statuses Algorithm
- Penalized support-search least squares Algorithm
- Shor factoring with verified output and bounded outer retries Algorithm
- Unanchored Levenberg–Marquardt step with explicit early stopping Algorithm
- Uncorrected Adam for online convex losses Algorithm
- Uncorrected AMSGrad with a coordinatewise historical maximum Algorithm
- A rational root of xᵏ = m is an integer: if k ≥ 1, m ∈ ℤ, x ∈ ℚ and xᵏ is the image of m, then x is the image of an integer Corollary
- Addition is a well-defined total operation Corollary
- Every linear subspace U of a vector space V has a complement: a linear subspace W with V = U ⊕ W Corollary
- Every nondegenerate interval of ℝ is uncountable Corollary
- Every nonzero integer n is u ∏_i<r pᵢ with u ∈ {1,-1} and every pᵢ prime; u and r are determined by n, and the list is determined up to a permutation Corollary
- For an integer p > 1: p is prime if and only if, for all integers a and b, p ∣ ab implies p ∣ a or p ∣ b Corollary
- If a prime p divides a finite product ∏_i<n aᵢ of integers then p ∣ aᵢ for some i < n; at n = 0 the product is 1 and the hypothesis cannot hold Corollary
- If V = ⨁_i<n Uᵢ with every Uᵢ finite-dimensional, then V is finite-dimensional and dim_F V = ∑_i<n dim_F Uᵢ; in particular dim_F(U ⊕ W) = dim_F U + dim_F W Corollary
- If V has a spanning set with n elements, then every linearly independent subset of V is finite with at most n elements; in particular V has no linearly independent subset equinumerous with ℕ Corollary
- lvertP(A)| = 2^| A| for finite A Corollary
- Multiplication is a well-defined total operation Corollary
- Positive integers 4ᵃ m with m≡ 7 (mod 8) need four nonzero squares Corollary
- ℝ((t⁻¹)) has the nested interval property for lengths tending to 0 Corollary
- Rings of integers are Dedekind domains Corollary
- The extended Euclidean algorithm: the same descent produces integers x, y with ax + by = gcd(a,b), so Bézout coefficients are computed and not merely shown to exist Corollary
- {(1,0), (0,1), (1,1)} spans F² and is linearly dependent, so a spanning set need not be a basis; each of its three two-element subsets is a basis Counterexample
- A commutative monoid in which cancellation holds need not be a group: (ℕ, +) Counterexample
- A conjugate point at which there are many geodesics Counterexample
- A count that overcounts because the blocks are not disjoint, and exactly where the sum rule's hypothesis is spent Counterexample
- A free ultrafilter induces a finitely additive zero-one probability that is not countably additive Counterexample
- A fully converged LSQR solve can amplify a small singular-direction error Counterexample
- A locally finite shrinking-edge ray is not complete Counterexample
- A nonempty surjective image of ℕ need not be equinumerous with ℕ Counterexample
- A poset with a bottom, a top and countably many incomparable middle elements has an infinite interval, so convolution of constant-one functions is not defined Counterexample
- A reflexive coequalizer of sets not preserved by Set(ℕ,-) Counterexample
- A set of ordinals that is not an ordinal: {0,1,ω} Counterexample
- Adam diverges on a periodic bounded-gradient loss sequence Counterexample
- An arbitrary isotopy of arcs need not be a braid isotopy Counterexample
…and 398 more results.
Dependency tree · two levels
12 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
- Set-theoretic definition of natural numbers (Wikipedia) (standard reference, not scraped)
- Axiom of infinity (Wikipedia) (standard reference, not scraped)
- Peano axioms (Wikipedia) (standard reference, not scraped)
- B. Kaya, MATH 320 Set Theory (METU lecture notes) (standard reference, not scraped)