The von Neumann naturals form a Peano system

Depends on

• The natural numbers $\mathbb{N}$ (von Neumann)
• Peano system
• The principle of mathematical induction
• Every natural number is a transitive set and is not a member of itself

Used by

• Addition is a well-defined total operation Corollary
• Multiplication is a well-defined total operation Corollary
• The map n ↦ (n,0) from ℤ to ℤ × ℤ preserves addition and multiplication and does not preserve 1, so the clause f(1) = 1 is not redundant Counterexample
• The factorial n! and the falling factorial n^k̲, defined by recursion in ℕ Definition
• The forward shift on F^ℕ is injective but not surjective Example
• FALSE: every injection of a set into itself is a bijection False statement
• FALSE: for all sets A and B with B having at least two elements, A × B is strictly larger than A False statement
• FALSE: successor-closure alone forces a set to be all of ℕ False statement
• A finite sum is unchanged by a permutation of its index range: ∑_k<n a_π(k) = ∑_k<n aₖ for every bijection π : n → n Lemma
• Addition is cancellative Lemma
• Discreteness: σ(n) is the immediate successor Lemma
• Laws of finite sums and products in ℕ, and ι(∑_k<n aₖ) = ∑_k<n ι(aₖ) Lemma
• No natural number equals its own successor Lemma
• The natural numbers have no zero divisors Lemma
• The right-left macro simulates one stay-put step Lemma
• Trichotomy of the order on ℕ Lemma
• ≤ is a linear order on ℕ Theorem
• Every natural number and ω are cardinals, every infinite cardinal is a limit ordinal, and on the natural numbers the cardinal operations are the published finite counting operations, with | A | in the finite sense equal to | A | in the cardinal sense Theorem
• ℕ × ℕ ≈ ℕ Theorem
• On ω the ordinal + and · are the Peano operations: ω is closed under ordinal +, · and exponentiation, and for naturals m, n the ordinal m + n and m · n are the natural-number sum and product Theorem
• ℚ is countably infinite Theorem
• The well-ordering principle Theorem

Dependency tree · two levels

10 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

• Peano axioms (Wikipedia) (standard reference, not scraped)
• Set-theoretic definition of natural numbers (Wikipedia) (standard reference, not scraped)
• Mathematics 144: Set Theory (UC Riverside lecture notes) (standard reference, not scraped)